Paolo Torrini
email: p.torrini@univ-lille.fr

David Nowak
email: d.nowak@univ-lille.fr

Narjes Jomaa
email: n.jomaa@univ-lille.fr

Mohamed Sami
email: mohamedsami.cherif@yahoo.com

Cherif Cristal

Formalising Executable Specifications of Low-Level Systems

Formal models of low-level applications rely often on the distinction between executable layer and underlying hardware abstraction. This is also the case for the model of Pip, a separation kernel formalised and verified in Coq using a shallow embedding. DEC is a deeply embedded imperative typed language with primitive recursion and specified in terms of small-step semantics, which we developed in Coq as a reified counterpart of the shallow embedding used for Pip. In this paper, we introduce DEC and its semantics, we present its interpreter based on the type soundness proof and extracted to Haskell, we introduce a Hoare logic to reason about DEC code, and we use this logic to verify properties of Pip as a case study, comparing the new proofs with those based on the shallow embedding. Notably DEC can import shallow specifications as external functions, thus allowing for reuse of the abstract hardware model. 1 2

Introduction

Formal modelling and verification of OS kernels involve different aspects of theorem proving: realistic modelling of low-level systems, scalable verification of program behaviour with respect to abstract specifications, executable models, generation of efficient, certified low-level code. Models have often complex structures in terms of components and levels of abstraction [START_REF] Gu | CertiKOS: an extensible architecture for building certified concurrent OS kernels[END_REF][START_REF] Klein | seL4: formal verification of an OS kernel[END_REF][START_REF] Jomaa | Proof-oriented design of a separation kernel with minimal trusted computing base[END_REF]. A natural distinction arises between the mathematical modelling of low-level requirements, typically associated with an abstract model of the platform, and the executable model of the platform-independent application which we also call the service layer. Primarily, the abstract model needs to be extensible with respect to concrete models of specific architectures, whereas the executable model needs to be translated to an efficient implementation language. Working with a theorem prover such as Coq [START_REF] Bertot | Interactive Theorem Proving and Program Development[END_REF] or Isabelle [START_REF] Nipkow | Isabelle/HOL: A Proof Assistant for Higherorder Logic[END_REF], this is a difference that matters for the choice of the representation in the base language.

A deep embedding of an object language captures its abstract syntax in terms of abstract datatypes, therefore providing a reified representation that supports manipulation, notably translations, as well as operational specifications of behaviour, thus allowing for a naturally executable characterisation of control flow. However, reasoning about abstract datatypes involves a significant overhead in relation to the pervasive use of constructors and destructors. Moreover, conventional datatypes are not extensible. A shallow embedding consists of defining semantically the constructs of the object language in the base language, hence providing their characterisation in terms of denotational semantics, thus not only keeping the maths as simple as possible, but also allowing for extensibility in a non-problematic way. On the other hand, a shallow embedding does not provide any direct way to manipulate language constructs, and it makes it hard to separate object execution from evaluation in the base language.

Going back to our problem, we would generally like to associate the executable model with a deep embedding and the abstract platform model with a shallow one. Our approach consists in deeply embedding an object language that allows importing specifications written in the metalanguage as external function calls. We call the object language thus formalised a deeply embedded language extension (DLE). A DLE can be thought of as a domain specific extension of the base language, taking it closer to the target domain in the sense of syntax (i.e. with language constructs close to the instructions to be modelled) and of behavioural specification (i.e. with an operational semantics close to its model of execution).

Motivation

In this paper, we focus on the development of a specific DLE in connection with the formal development of the Pip protokernel [START_REF] Jomaa | Proof-oriented design of a separation kernel with minimal trusted computing base[END_REF][START_REF] Bergougnoux | Porting the Pip proto-kernel's model to multi-core environments[END_REF][START_REF] Yaker | Ensuring IoT security with an architecture based on a separation kernel[END_REF][START_REF] Bergougnoux | The repository of Pip[END_REF]. Separation kernels [START_REF] Zhao | High-assurance separation kernels: a survey on formal methods[END_REF] are systems designed to provably ensure noninterference properties with respect to distinct applications running on the same machine [START_REF] Klein | seL4: formal verification of an OS kernel[END_REF][START_REF] Gu | CertiKOS: an extensible architecture for building certified concurrent OS kernels[END_REF][START_REF] Dam | Formal verification of information flow security for a simple ARM-based separation kernel[END_REF]. Usually a separation kernel is based on a formal model that is verified with respect to its security policy and translated to a low-level language for efficiency.

Pip is a separation kernel in which the kernel functionalities are reduced to a minimum needed to allow for efficient memory management and context switching (hence its characterisation as protokernel) [START_REF] Jomaa | Proof-oriented design of a separation kernel with minimal trusted computing base[END_REF]. It provides a service API allowing for partitions to be created, allocated memory and removed at runtime according to a hierarchical model. Partitions form a tree and each partition manages its own subpartitions. The security policy of Pip is based on three memory access properties: the parent partition can access the memory of its children (vertical sharing), sibling partitions cannot share memory with each other (horizontal isolation), and no partition can access kernel memory (kernel isolation). The Pip system is implemented in C and assembly, relying on a model written in Coq, the structure of which is shown in Fig. 1. The executable model, corresponding to the service API, is built on top of an abstract platform model that covers hardware abstraction layer (HAL) and hardware, the former in terms of the high-level specification of low-level, platform-specific C and assembly functions, the latter in terms of an abstract model of the physical memory and the MMU. The service layer of Pip relies on a fragment of C that can be represented as a comparatively simple imperative language, one that is not difficult to capture in functional terms. This fragment, which we call IL here, corresponds to a typed first-order sequential language with call-by-value, primitive recursion and mutable references. Crucially, we do not need to return pointers, to use call by reference, structures or arrays. Non-termination can always be ruled out relying on hardware parameters.

The executable model has been formalised in Coq on top of hardware abstraction using a shallow embedding of IL based on its monadic semantics, and the verification of the security properties, presented in [START_REF] Jomaa | Proof-oriented design of a separation kernel with minimal trusted computing base[END_REF], has been carried out directly on the MC code using an associated Hoare logic, without going through a higher-level model of the service layer. The service layer is about 1300 lines of what we specifically call monadic code (MC), semantically corresponding to IL, while the HAL is about 300 lines of monadic specification. The verification involves rather long proofs [START_REF] Bergougnoux | The repository of Pip[END_REF] (several tens of thousands of lines), of which over ten thousands for the abstract platform model.

Modelling Pip at the shallow level has made it possible to focus on system development from the start, independent of any work on language development. However, translation to a low-level language is mandatory for efficiency. The closeness of IL to a fragment of C made it possible to carry out automatically the translation of MC to C source code. Such translation, defined on Gallina abstract syntax, has been implemented in Haskell [START_REF] Hym | The repository of Digger[END_REF] and it returns efficient, yet unverified code. Unfortunately, verifying code obtained in this way seems rather hard, as it would involve comparing semantically two large languages such as C and Gallina.

We would like to obtain a certified translation at a comparatively lower cost, by focusing on a smaller source language, building a reified representation of our object language, and by targeting an existing formalisation of C such as CompCert C [START_REF] Blazy | Mechanized semantics for the Clight subset of the C language[END_REF], defining a verified translator in Coq. For this reason, we have developed in Coq a DLE that we call DEC [START_REF] Torrini | DEC 1.0 specification[END_REF][START_REF] Torrini | The repository of DEC[END_REF], as an object-level counterpart of IL. As a deep embedding, DEC can be the source of a translation function defined in Coq by pattern matching on the abstract syntax. Unlike MC, DEC has an interpreter based on its small-step operational semantics. This makes it possible to analyse the control flow in Coq, and it could help significantly in comparing formally the behaviour of a program with that of its translation to another language. Although in practice it is difficult to run the interpreter in Coq, it is possible to rely on the extraction mechanism to obtain an efficient program based specifically on the operational semantics of DEC rather than on generic Gallina evaluation.

Given DEC, there are indeed two distinct possibilities for the verification of Pip, as shown in Fig. 2. Both plans involve translating the MC model to DEC. Plan A consists additionally in proving the semantic equivalence between the two models, relying for the rest on the verification of the security properties in the shallow embedding as presented in [START_REF] Jomaa | Proof-oriented design of a separation kernel with minimal trusted computing base[END_REF]. Plan B, on the other hand, consists in verifying properties directly on the DEC model. In this case, given the large size of the existing verification based on MC, one of the main priorities is to maximise its reuse in verifying DEC code. This can be achieved particularly for the abstract platform model, relying on the DLE character of DEC. In this Our contribution (beyond the semiformal characterisation of IL) consists in two aspects that are essential to our verification approach: the development of DEC as DLE (ca. 10,000 lines code), and the development of an appropriate Hoare logic for DEC (ca. 2,000 lines code), allowing for syntax-driven, compositional proofs and reuse of the abstract platform model. We applied our approach to a case study (ca. 2,000 lines code on top of a significant amount of reuse), proving auxiliary invariants of Pip functions in their translation to DEC.

In section 3 we give a preliminary overview of IL, characterising it mathematically in terms of its operational semantics. In section 4 we present the development of DEC, with its interpreter (section 5) and the associated Hoare logic (section 6). Section 7 presents the verification of Pip invariants based on DEC code, and compares it with their verification based on MC. In section 8 we discuss related work, in section 9 conclusions and further work.

Preliminaries

We start with a semiformal, mathematical specification of IL, the language we use to illustrate succinctly the operational semantics DEC is based on, and to connect it with MC through a mathematical specification of its denotational semantics. IL is parametric in the primitive types Typ (ranged over by t), in the state type W, and in the actions Act, ranged over by a, associated with side effects and used to represent external functions. Values of primitive types are informally regarded as a set Val ranged over by v. Function types, ranged over by ft, are each defined by a tuple of primitive types for the parameters, and a primitive type for the return value. The syntax of IL is constituted of intrinsically well-typed expressions Exp and functions Fun (ranged over by e and f respectively). We rely on higher-order abstract syntax (HOAS), treating identifiers as formal variables and programs as closed terms, thus avoiding the need for environments. For brevity, we represent tuples as heterogeneous lists, which we treat as typed by type lists (denoted Typs), extending to them a standard list notation (including map). We use the Haskell convention for naming lists.

Exp
) := ts → W → (W * t)
We specify the small-step transition relation using configurations defined as pairs (s, X) where s : W is a state and X may be either an expression or a list of them. We make the presentation more concise by giving only the reduction rules and relying on evaluation contexts to specify call-by-value. Evaluation contexts allow us to compute the redex at each step. As usual [START_REF] Felleisen | The revised report on the syntactic theories of sequential control and state[END_REF], we write [ ] to denote the hole in which to plug the redex in, and C[e] to denote the splitting of an expression into context and redex. Notice that val simply lifts values to expressions, and the final value can be obtained by unlifting from an expression of form val v. The denotational semantics of IL can be defined along the lines of the monadic translation in [START_REF] Moggi | Notions of computation and monads[END_REF], using a state monad with state W (see Appendix A). The result corresponds to the shallow embedding used in the formalisation of Pip [START_REF] Jomaa | Proof-oriented design of a separation kernel with minimal trusted computing base[END_REF].

The Deep Embedding

DEC [START_REF] Torrini | The repository of DEC[END_REF] is a strongly normalising, functional imperative language with primitive recursion, implemented in Coq as an DLE based on IL, parametric in the type of the mutable state. The constructs of DEC are internally specified as functional ones. Nonetheless, Coq functions can be imported as external functions, and these can be stateful, although the totality requirement of the metalanguage ensures that they are terminating. In this sense, DEC is a functional language that can be extended with generic effects, as well as a deeply embedded functional interface which can be used to extend a stateful model. Unlike the HOAS-style presentation of IL, DEC relies on environments, on explicit typing relations, and on a semantic representation which uses propagation rules rather than evaluation contexts, following an approach closer to [START_REF] Churchill | Reusable components of semantic specifications[END_REF] and to the original presentation of structural operational semantics (SOS) [START_REF] Plotkin | A structural approach to operational semantics[END_REF], a choice made to allow for explicit manipulation of identifiers without the need to implement α-renaming. As a distinctive computational feature, DEC has typing relations with inductive principles which are strong enough to carry the weight of the type soundness proof, while minimising type annotation.

Relying on Coq modules, the definition of DEC is parametric in the type of the mutable state W and in the type of the identifiers Id, the latter required to have decidable equality. We model environments as homogeneous lists, and to this purpose, unlike in HOAS, we need to introduce a deep embedding of object types and values. Our object types (i.e. deep types) are lifted Gallina types (i.e. shallow ones). Their type could be treated as trivial hiding, i.e. Σ(λX:Type,X), but we prefer to rely on a type class ValTyp:Type→Prop to ensure lifting is explicitly allowed, hence defining our type VTyp of value types as From the deep typing point of view, DEC is intended as a first-order language, therefore it would not be strictly necessary to allow for the body of program expressions to contain occurrences of function definitions, as opposed to function variables. However, allowing function definitions to be syntactical subexpressions leads to a stronger built-in induction principle. Partly for this reason, DEC is essentially designed as first-order fragment of a higher-order language. The deep type of function types Inductive FTyp : Type := FT (prms_type: valTC) (ret_type: VTyp).

ensures the first-order restriction, requiring that parameters are deep datavalues. Function environments (funEnv) and function typing contexts (funTC) are defined as lists, in analogy to valEnv and valTC. The namespace distinction between value identifiers and function identifiers is enforced at the level of head normal forms, here called q-values and q-functions.

Inductive QValue : Type := Var (x: Id) | QV (v: Value).

The inductive type of expressions is mutually defined with functions, qfunctions, and lifted expression lists that represent parameters. The function constructor FC represents an iterate-style construct, where tenv gives the list of the formal parameters with their types, n is a natural number that represents fuel, e0 is the function body for n=0, e1 is the function body for n>0, x is the function identifier used in recursive calls, and fenv is the local function environment. Constructors Var and FVar lift identifiers to the corresponding head-normal forms. Similarly QV and QF lift normal forms. PS lifts expression lists to parameters. Concerning expressions, Val and Return are lifting constructors, IfThenElse represents conditional branching, BindN sequencing and BindS local binding of identifiers to expressions (i.e. let-style binding). BindMS allows for multiple binding of identifiers to normal forms, i.e. for local environments, and it is needed for internal processing in our environment-based representation. Apply represents application of recursive functions. Modify represents application of external one-argument functions, where the function type is T1→T2. Modify works as a constructor of generic effects, handled by the stateful functions associated with the corresponding record of type Read and write instructions can then be defined, given UnitVT:ValTyp unit (here @ is used to make implicit arguments explicit). Notice that function definitions are meant to represent closed terms, as they may occur as subterms in expressions. For this reason, a function definition is defined as a closure with respect to its function identifiers, by including fenv as local function environment. This measure prevents variable capture and suffices to ensure we can type check recursive functions without annotating them with their return type.

The typing relations on expressions, functions, q-functions and parameters are defined by mutual induction, where MatchEnvs maps a binary relation over two lists. 3Inductive ExpTyping : funTC→valTC→funEnv→Exp→VTyp→Type := ... | Apply_Typing : ∀ (ftenv: funTC) (tenv fps: valTC) (fenv: funEnv) (q: QFun) (ps: Prms) (pt: PTyp) (t: VTyp), pt = PT (map snd fps) → MatchEnvs FunTyping fenv ftenv → QFunTyping ftenv fenv q (FT fps t) → PrmsTyping ftenv tenv fenv ps pt → ExpTyping ftenv tenv fenv (Apply q ps) t | Modify_Typing : ∀ (ftenv: funTC) (tenv: valTC) (fenv: funEnv) (T1 T2: Type) (VT1: ValTyp T1) (VT2: ValTyp T2) (XF: XFun T1 T2) (q: QValue), QValueTyping tenv q (vtyp T1) → ExpTyping ftenv tenv fenv (@Modify T1 T2 VT1 VT2 XF q) (vtyp T2) with QFunTyping : funTC→funEnv→QFun→FTyp→Type := ... In the typing of function application, the type of the actual parameters is compared with that of the formal ones obtained from the q-function typing, which means either consulting the function typing context (ftenv) in case of an identifier, or else checking the function type. In the typing of external function calls the relevant types and the function definition are passed as a record.

Our function typing relation has a comparatively non-standard, algorithmic character.

with FunTyping : Fun→FTyp→Type := | Fun0_Typing: ∀ (ftenv: funTC) (tenv: valTC) (fenv: funEnv) (e0 e1: Exp) (x: Id) (t: VTyp), MatchEnvs FunTyping fenv ftenv → ExpTyping ftenv tenv fenv e0 t → FunTyping (FC fenv tenv e0 e1 x 0) (FT tenv t) | FunS_Typing: ∀ (ftenv: funTC) (tenv: valTC) (fenv: funEnv) (e0 e1: Exp) (x: Id) (n: nat) (t: VTyp), let ftenv := (x, FT tenv t) :: ftenv in let fenv := (x, FC fenv tenv e0 e1 x n) :: fenv in MatchEnvs FunTyping fenv ftenv → ExpTyping ftenv tenv fenv e1 t → FunTyping (FC fenv tenv e0 e1 x n) (FT tenv t) → FunTyping (FC fenv tenv e0 e1 x (S n)) (FT tenv t)

Given a function f := FC fenv tenv e0 e1 x n to type, while the types of the parameters are supplied by tenv, the return type needs to be inferred, either from e0 when n = 0, or else from e1. This involves also inferring the types of the local functions in fenv, not supplied by f. Hence the typing relation requires a function environment as argument, rather than just a function typing context, and given the function environment update in case of n > 0, type inference requires induction on the fuel.

We have developed our typing definitions in parallel with the proof of a type soundness theorem which in fact we carry out by mutual induction on the typing relations. However, the induction principle supplied automatically by Coq turned out to be weak, particularly given our use of lists to represent parameters and our typing of parameters where Forall2T maps a relation on lists. We solved this problem by supplying customised and stronger mutual induction principles (called ExpTyping_str_rect for expressions and similarly for the other categories), obtained by instantiating a more general one, proved by means of the mutually recursive version of the fix tactic [START_REF] Bertot | Interactive Theorem Proving and Program Development[END_REF]. Reasoning by induction on the typing relations, we can prove that each well-typed object is uniquely typed. This is also the case for functions.

Lemma UniqueFunType (f: Fun) (ft1 ft2: FTyp) (k1: FunTyping f ft1) (k2: FunTyping f ft2) : ft1 = ft2.

Although the typing of functions depends on their fuel, we can prove The dynamic semantics of DEC, defined in terms of small-step rules, is comparatively standard and close to the IL presentation, though far less concise, as propagation rules are needed for each constructs. It relies on a notion of configuration parametrised by syntactic categories (i.e. expressions, parameters, q-values and q-functions).

Inductive AConf (T: Type) : Type := Conf (state: W) (qq: T).

The step rules for q-values and q-functions are just environment lookups.

Inductive QVStep : valEnv → AConf QValue → AConf QValue → Type Inductive QFStep : funEnv → AConf QFun → AConf QFun → Type
The step rules for expressions and parameters (evaluated from left to right) are defined by mutual induction, using the principle supplied by Coq. The reduction rule of Modify enacts the monadic behaviour of the stateful action associated with xf, returning the value computed by x_eval and changing the state according to x_exec.

The SOS Interpreter

The small-step semantics can be used to compute well-typed programs in well-typed environments. First of all, we extend the definitions of transition steps to reflexive-transitive closures (represented by inductive types, e.g. EClosure : funEnv → valEnv → AConf Exp → AConf Exp → Type). Then, after using double induction on the step relation and its reflexive-transitive ex-tension to prove a weakening lemma (for expressions as shown, and similarly for parameters) our strong mutual induction principle on typing suffices to prove a type soundness theorem, with the following formulation for expressions (and similarly for the other mutually defined categories). 4Lemma whereas type soundness, in the case of a terminating language, involves a weak normalisation result typically provable by induction on the step relations. Our typing relations incorporate the inductive aspect on fuel, and therefore suffice to prove normalisation. We prove determinism of evaluation, again by induction on typing. Determinism together with weak normalisation give us strong normalisation, and indeed this makes it possible to ensure that our type soundness proof can be used as an SOS interpreter to evaluate DEC programs. We can run the interpreter on simple expressions, but Coq's evaluation mechanism (notoriously fragile [START_REF] Leroy | Using Coq's evaluation mechanisms in anger[END_REF]) currently does not carry us far enough, particularly in connection with our extensive use of dependent types. Nonetheless, we can rely on the Coq extraction mechanism to obtain a certified and efficient implementation of the SOS interpreter. We used extraction to Haskell to generate code which we compiled and run with GHC. The pres-ence of dependent types in our Coq code required some adjustments. In fact, when Coq types have no direct translation into Haskell, the extraction mechanism will use the Haskell type Any (which can be understood as the union of all possible types). This means that in order to print the result of running the interpreter, we need to supply explicitly the translated type using the Haskell function unsafeCoerce. As expected, the Haskell interpreter is recursively defined on a term that in Coq has the dependent type of the typing relation. In fact, the computational content of our carefully designed algorithm rests entirely on that relation, rather than on its arguments. Although such arguments have no computational role, they are still present in the extracted code, as they have computational types. But the lazy evaluation strategy of Haskell ensures that they are not evaluated, and thus they can be safely given the value undefined.

In the future we would like to tackle the aspect of evaluation in Coq too, in order to show the semantic adequacy of DEC with respect to MC. We have defined a translation of DEC to Gallina, relying on the strong induction principle on typing as we did for type soundness. Ideally we would like to show that for each DEC program, the proof term of this translation is equal to the term obtained from the SOS interpreter.

Hoare Logic

We defined a Hoare logic to verify well-typed DEC programs with respect to state properties expressed in Gallina. Our definitions of Hoare triples allow for the postcondition to depend on the value returned by the computation, following [START_REF] Cock | Secure microkernels, state monads and scalable refinement[END_REF][START_REF] Swierstra | A Hoare logic for the state monad[END_REF], and for the computation to depend on function and value environments. We provide the syntax {{ P }} fenv >> env >> e {{ Q }} to write triples for expressions, where the unary predicate P gives the precondition and the binary predicate Q the postcondition of running the SOS interpreter on a welltyped expression e in well-typed environments fenv for functions and env for values, corresponding to the following definition where the transitive closure hypothesis states that the expression e, evaluated in state s, leads to value v in an updated state s . The syntax {{ P }} fenv >> env >> ps {{ Q }} and an analogous definition are used for Hoare triples for parameters. Notice that in contrast with the triples for MC [START_REF] Jomaa | Proof-oriented design of a separation kernel with minimal trusted computing base[END_REF] where well-typedness is shallow and implicit, here the typing information is deep and thus needs to be explicit. In principle, this explicitness could bring additional discriminating power, making it easier to distinguish between types that are meant to be different, with different actions associated to them, though modelled by the same shallow type. However, this comes to the cost of an overhead in the proofs. On the other hand, an untyped version of the triples could not rely on termination, and therefore would be rather weak in comparison with the shallow counterpart. We supply a Hoare logic library based on our triples, notably including Hoare logic structural rules for each DEC construct, in order to allow for a verification style that is essentially syntax-driven. Most of these rules support bidirectional use, i.e. both by weakest precondition and strongest postcondition, and correspond to big-step rules. For example, the following is the main rule for BindS

{{P0}} fenv >> env >> e1 {{P1}} → (∀ v: Value, {{P1 v}} fenv >> (x,v)::env >> e2 {{P2}}) → {{P0}} fenv >> env >> BindS x e1 e2 {{P2}}
This rule allows a triple for the expression BindS x e1 e2 to be broken down into sequential triples for e1 and e2 (the latter in an updated value environment). The main rule for the Apply constructor can be conveniently split into two distinct ones, in order to deal with the recursive update of the function environment, which does not take place with zero fuel As another example, given an external function record xf: XFun t1 t2, the rule for Modify has more naturally the form of a weakest precondition (we show the case when the argument q is already a lifted value): The validity of these rules is proved by inverting the corresponding operational semantic rules, making use of the determinism of DEC.

Case Study: Verifying Properties of Pip

The model of Pip in the shallow embedding [START_REF] Jomaa | Proof-oriented design of a separation kernel with minimal trusted computing base[END_REF] is based on Gallina code which can be regarded as a monadic representation of IL. The LLI monad used in that representation is defined as an abstract datatype and it wraps together hardware state and undefined behaviours, analogously to applying a state transformer to an error monad [START_REF] Moggi | Notions of computation and monads[END_REF][START_REF] Wadler | Comprehending monads[END_REF]. The primitive types are Booleans and subsets of naturals. The HAL functions correspond to the actions in IL. The monadic operations ret and bind, which can be easily proved to satisfy the monadic laws provide the semantics for sequencing, let binding and function application.

Primitive recursion and conditional expressions are encoded in terms of the corresponding Gallina notions (see Appendix A for a semiformal definition of the corresponding denotational semantics).

The executable specification of Pip rests on a platform model which includes the representation of physical memory as association lists of physical addresses and values, and the specification of HAL primitives corresponding to architecture-dependent functions [START_REF] Jomaa | Proof-oriented design of a separation kernel with minimal trusted computing base[END_REF][START_REF] Bergougnoux | The repository of Pip[END_REF]. Stateful functions such as get and put are only used in the definition of the HAL primitives, thus ensuring that Pip services can access the state only through specific actions. A physical address is modelled as a page identifier (corresponding to a fixed-size chunk of memory) and an offset value called index.

Record page := {p :> nat; Hp: p < memorySize}. Record index := {i :> nat; Hi: i < pageSize}. Definition paddr := page * index.

The value datatype sums up the types of values that can be found in the configuration pages. Here Pentry stands for physical entry, Ventry for virtual entry, and vaddr for virtual address. Physical entries (PTEs) associate a page with its accessibility information.

Record Pentry : Type:= {pa: page; present: bool; accessible: bool}.

The management of memory is based on a tree-like partition structure. The partition tree is a hierarchical graph in which each node contains a handle called partition descriptor (PD) together with the configuration of the partition, defined as a set of entities, the main one being the MMU configuration. This has the structure of a tree of fixed levelNum depth where physical addresses (including those pointing to possible children in the partition tree) are essentially leaves, whereas valid virtual addresses represent maximal branches. In fact, virtual addresses are modelled as lists of indices of length levelNum+1. Each of them is translated by the MMU either to the null address or to a physical one, by interpreting each index in the list as offset in the page table at the corresponding level in the MMU. Partitioning management also uses two auxiliary entities, which can be described as shadows of the MMU. The first shadow is used to find out which pages are assigned children, and it uses the type Ventry.

The second shadow is used to associate each PD to the virtual address it has in the parent partition. The comparatively low-level representation of these structures in the Coq model is based on lists and relies on consistency invariants to ensure e.g. that a list represents a tree. The physical state in Pip is defined by the PD identifier of the currently active partition and the relevant part of the memory state (i.e. essentially, the configuration pages).

Record state: Type := {currentPartition: page; memory: list (paddr * value)}.

In the monadic model of Pip, this defines the state for the LLI monad [START_REF] Jomaa | Proof-oriented design of a separation kernel with minimal trusted computing base[END_REF][START_REF] Bergougnoux | The repository of Pip[END_REF]. In the deep embedding formalisation [START_REF] Torrini | The repository of DEC[END_REF][START_REF] Cherif | Project report -modelling and verifying the Pip protokernel in a deep embedding of C[END_REF], we rely on a concrete module where Id is instantiated with strings, and W with state. The HAL primitives correspond to the actions which are executed as external function calls by means of Modify. Since the current definition of DEC does not include rules for error handling, we delegate undefined behaviour to each action, using option types. This involves some adjustments. For example, the original HAL primitive in [START_REF] Bergougnoux | The repository of Pip[END_REF] to read a physical address in a given page The fact that the composition of state and error is essentially inverted by the translation is not problematic in our model: all the proofs on the hardware primitives turned out to be easy to adjust.

We translated to DEC three auxiliary functions which are defined in the MC model [START_REF] Bergougnoux | The repository of Pip[END_REF], called getFstShadow, writeVirtual and initVAddrTable. For each function, we proved the main invariant associated with it for its DEC translation, along the lines of the proofs in the shallow embedding, reusing the HAL model in the sense we have described above. The top-level proofs in the shallow embedding are comparatively small (about 50, 100 and 250 lines, respectively), but they are quite representative as they involve using several HAL primitives, sequencing and let-binding, reading from the state (getFstShadow), updating the state (writeVirtual), as well as a conditional and a recursive function (initVAddrTable). Following in the footsteps of the shallow proofs, the deep embedding results in comparable top-level proofs (about 100, 100 and 350 lines respectively), with an overhead due mainly to DEC type-checking, and to the lifting-unlifting of values on which properties may depend. In the case of getFstShadow, we have experimented with alternative definitions of HAL primitives, showing that the top-level proof does not change and therefore, in principle, that DEC could support refinement of abstract specifications. In the case of initVAddrTable, we also proved the invariant following a more thoroughly syntax-driven approach, in the spirit of our Hoare logic. This resulted in a significantly shorter top-level proof (about 170 lines, mainly instantiations of metavariables), though it involved proving additional HAL-level lemmas (about 300 lines) not supplied by the original model, yet general enough to be potentially reusable.

The function getFstShadow is used to return the physical page of the first shadow for a given partition, and it is implemented monadically using readPhysical as well as getSh1idx and Index.succ as HAL primitives.

Definition getFstShadow (p : page) : LLI page := bind getSh1idx (λ x, bind (Index.succ x) (λ y, readPhysical p y)).

This function can be translated to DEC as follows Definition GetFstShadow (p : page) : Exp := BindS "x" GetSh1idx (BindS "y" (IndexSucc "x") (ReadPhysical p "y")).

where all the subexpressions are based on lifted primitives. The invariant that has been proved for the DEC code [START_REF] Torrini | The repository of DEC[END_REF][START_REF] Cherif | Project report -modelling and verifying the Pip protokernel in a deep embedding of C[END_REF] is the following closely matching the shallow version in [START_REF] Bergougnoux | The repository of Pip[END_REF]. Here again GetPartitions and NextEntryIsPP are lifted HAL primitives. GetPartitions returns the list of all sub-partitions of a given partition, NextEntryIsPP returns a Boolean depending on whether the successor of the given index in the given configuration page points to the given physical page, whereas PartitionDescriptorEntry defines a specific property of the partition descriptor. The typing information that is explicit in the shallow embedding needs to be extracted from the deep type, and this makes for most of the overhead in the deep proof.

The function writeVirtual writes a virtual address to the physical memory and it is used to update configuration pages in the second shadow. It is a HAL primitive, and therefore can be adjusted and lifted to DEC as an external function. The associated invariant ensures that the given value is actually written to the given location, while the properties which do not depend on the updated part of the state are preserved. This example illustrates reuse quite well. Although the invariant requires a comparatively long proof in the shallow embedding, this proof can be replicated almost exactly in the deep embedding, using the same (of many) HAL lemmas.

The recursive function initVAddrTable is used to initialise the virtual addresses in the second shadow. Its translation has a comparatively complex DEC structure, involving a conditional and the use of tableSize as fuel. The DEC structure of InitVAddrTableAux makes it convenient to adopt a syntaxdriven approach based on the application of Hoare logic rules (as opposed to unfolding the definition of Hoare triple), in order to facilitate automation and maximise reuse. Indeed, it has been easy to write a tactic in Ltac (the scripting language of Coq) to semi-automate the application of such rules. In comparison, pattern-matching on terms in MC might be trickier. On the other hand, the impact of this basic form of automation is restricted by the need to instantiate metavariables with comparatively complex terms for properties. Moreover, the proof uses induction on tableSize (in analogy to the shallow one).

Related Work

Differences and complementarity between shallow and deep embedding have been widely discussed in functional programming, in relationship with the development of embedded domain specific languages (EDSLs) [START_REF] Gibbons | Folding domain-specific languages: Deep and shallow embeddings (functional pearl)[END_REF][START_REF] Svenningsson | Combining deep and shallow embedding of domainspecific languages[END_REF][START_REF] Jovanovic | Yin-yang: Concealing the deep embedding of dsls[END_REF][START_REF] Carette | Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages[END_REF]. Combinations of shallow and deep embedding have been proposed e.g. in [START_REF] Svenningsson | Combining deep and shallow embedding of domainspecific languages[END_REF] to deal at once with the expression problem (related to extending a deeply embedded language) and the interpretation problem (related to extending the semantic interpretation of a shallow embedding). Their approach consists in extending a deeply embedded core language with a shallowly embedded frontend, thus the opposite of what we do with a DLE. In fact, they share our intent of separating the interpretation of the EDSL from that of the metalanguage. However, they want the high-level qualities of a shallow embedding (e.g. usability and extensibility of the syntax) for the top level part of the EDSL, whereas we need those qualities in the abstract model underneath (where in facts proofs tend to be, mathematically speaking, higher-level ones).

In applications of theorem proving, the difference between shallow and deep embedding has often been associated with a tradeoff between ease in dealing with mathematically higher-level proofs and language manipulation [START_REF] Wildmoser | Certifying machine code safety: Shallow versus deep embedding[END_REF]. For example, Cogent [START_REF] O'connor | Refinement through restraint: bringing down the cost of verification[END_REF] is a domain-specific language that has been used to verify file systems in the context of the seL4 project [START_REF] Klein | seL4: formal verification of an OS kernel[END_REF]. Targeting Isabelle, Cogent compiles both to a shallow embedding, used in higher-level verification, and to a deep one, used in verifying C source code (an approach that bears some analogy with our plan A mentioned in section 2).

In the Coq community, refinement from abstract models based on shallow embedding to deeply embedded lower-level ones has been discussed in the context of higher-level formal development [START_REF] Delaware | Fiat: Deductive synthesis of abstract data types in a proof assistant[END_REF] as well as in hardware design [START_REF] Chlipala | The Bedrock structured programming system: Combining generative metaprogramming and Hoare logic in an extensible program verifier[END_REF][START_REF] Vijayaraghavan | Modular deductive verification of multiprocessor hardware designs[END_REF]. CertikOS [START_REF] Gu | Deep specifications and certified abstraction layers[END_REF][START_REF] Gu | CertiKOS: an extensible architecture for building certified concurrent OS kernels[END_REF] provides a method to formally develop low-level applications in Coq, targeting an extension of CompCert Clight and assembly code [START_REF] Blazy | Mechanized semantics for the Clight subset of the C language[END_REF], allowing for composition and refinement of modular specifications which can be imported as external functions into the deeply embedded CompCert frontend. In comparison, our notion of DLE has a radically lighter-weight, domain specific character, relying on a separation of concerns between verification of the executable model (discussed in this paper) and translation to the implementation language. Moreover, unlike our basic Hoare logic, CertikOS provides advanced support for modular reasoning through contextual refinement [START_REF] Gu | Deep specifications and certified abstraction layers[END_REF].

Conclusions and Further Work

We have presented the core development of DEC as a DLE, with an interpreter based on its small-step operational semantics. The translation of DEC to C is ongoing work, and so is the proof that its denotational translation to the monadic code agrees with its operational semantics. As a preliminary experiment in using DEC as modelling language, we formalised functions of Pip in DEC and we proved model invariants associated with them. The DLE approach has proved fruitful in two main respects: it has enabled us to match neatly the modelling distinction between platform abstraction and service layer with a linguistic one between external and internal functions, hence defining a formal interface between the two; it has supported modular reuse of abstract platform components and associated proofs along that interface, within a framework that allows for direct manipulation of the executable code.

The notion of DLE is essentially oriented toward the design of intermediate, executable models. In the case of DEC, the DLE has been designed to ensure well-typedness and termination. This choice has been made to match the original model in the shallow embedding, rather than the ultimate C target. More generally, the idea we presented is to build domain specific modelling languages that support program development by refining stateful specifications into imperative code, while preserving in Coq the separation of concerns between layered modelling in a language with a comparatively simple model of execution, and translation to a richer implementation language.

A Appendix: Denotational Semantics

We can define a denotational semantics of IL relying on a monadic translation similar to the one in [START_REF] Moggi | Notions of computation and monads[END_REF] based on a state monad M with fixed state type W . The semantics is defined by a translation of IL to the monadic metalanguage (4-7), for types (Θ t ), expressions (Θ e ), expression lists (Θ es ) and functions (Θ f ), using the auxiliary definitions here also included [START_REF] Torrini | The repository of DEC[END_REF][START_REF] Gu | CertiKOS: an extensible architecture for building certified concurrent OS kernels[END_REF][START_REF] Klein | seL4: formal verification of an OS kernel[END_REF].

condM : M Bool → M t 1 → M t 1 →

Fig. 1 :

 1 Fig.1: The design of Pip: the system and its model

Fig. 2 :

 2 Fig. 2: Two verification plans: A and B

  Ctx := [ ] | binds Ctx (Exp ) | binds Val Ctx | cond Ctx (Exp ) (Exp ) | call (Fun ) Ctxs | xcall (Act ) Ctxs Ctxs := Ctx :: (Exps ) | Val :: Ctxs s e -→ s e s C[e] -→ s C[e ] s binds (val v) e -→ s e v s cond (val true) e 1 e 2 -→ s e 1 s cond (val false) e 1 e 2 -→ s e 2 s call (fun e 0 e 1 0) (map val vs) -→ s e 0 vs s call (fun e 0 e 1 (S n)) (map val vs) -→ s e 1 (fun e 0 e 1 n) vs s xcall ts a (map val vs) -→ s val v where a vs s = (s , v)

  ΣValTyp, with associated lifting function vtyp: Type → VTyp. Deep values are defined by lifting shallow values, hiding their type, and their type Value is defined as ΣValueI, where Inductive ValueI (T: Type) : Type := Cst (v: T). and lifting is cst: ∀ T:Type, T → Value. Value environments and value typing contexts are then given types list(Id*Value) and list(Id*VTyp), respectively abbreviated as valEnv and valTC. The value typing relation ValueTyping:Value→VTyp→Type reduces to extracting and equating the shallow types of the two arguments, whereas the identifier typing relation IdTyping:valTC→Value→VTyp→Type relies on the application of the lookup function findE.

  Inductive Fun : Type := FC (fenv: funEnv) (tenv: valTC) (e0 e1: Exp) (x: Id) (n: nat) with QFun : Type := FVar (x: Id) | QF (f: Fun) with Exp : Type := Val (v: Value) | Return (q: QValue) | IfThenElse (e1 e2 e3: Exp) | BindN (e1 e2: Exp) | BindS (x: Id) (e1 e2: Exp) | BindMS (fenv: funEnv) (venv: valEnv) (e: Exp) | Apply (qf: QFun) (args: Prms) | Modify {T1 T2: Type} {VT1: ValTyp T1} {VT2: ValTyp T2} (XF: XFun T1 T2) (arg: QValue) with Prms : Type := PS (es: list Exp).

  Record XFun (T1 T2: Type) : Type := { x_mod : W→T1→W*T2 ; x_exec : W→T1→W := λw x, fst (x_mod w x) ; x_eval : W→T1→T2 := λw x, snd (x_mod w x) }. For example, generic read and write actions can be defined as follows Definition xf_read {T: Type} (f: W → T) : XFun unit T := {| x_mod := fun x _ ⇒ (x, f x) |}. Definition xf_write {T: Type} (f: T → W) : XFun T unit := {| x_mod := fun _ x ⇒ (f x, tt) |}.

  Definition Read {T: Type} (VT: ValTyp T) (f: W → T) : Exp := @Modify unit T UnitVT VT (xf_read f) (QV (cst unit tt)). Definition Write {T: Type} (VT: ValTyp T) (f: T → W) (x: T) : Exp := @Modify T unit VT UnitVT (xf_write f) (QV (cst T x)).

  with PrmsTyping : funTC→valTC→funEnv→Prms→PTyp→Type := | PS_Typing: ∀ (ftenv: funTC) (tenv: valTC) (fenv: funEnv) (es: list Exp) (ts: list VTyp), Forall2T (ExpTyping ftenv tenv fenv) es ts → PrmsTyping ftenv tenv fenv (PS es) (PT ts).

Inductive

  Forall2T {A B : Type} (R: A→B→Type): list A→list B→Type := | Forall2_nilT : Forall2T R nil nil | Forall2_consT : ∀ x y l l , R x y → Forall2T R l l → Forall2T R (x::l) (y::l ).

FunTyping (FC fenv

  tenv e0 e1 x (S n)) ft → FunTyping (FC fenv tenv e0 e1 x n) ft and conversely sigT (fun ft0 ⇒ FunTyping (FC fenv tenv0 e0 e1 x (S n)) ft0) → FunTyping (FC fenv tenv0 e0 e1 x n) ft → FunTyping (FC fenv tenv0 e0 e1 x (S n)) ft.

  Inductive EStep: funEnv→valEnv→AConf Exp→AConf Exp→Type := ... with PrmsStep: funEnv→valEnv→AConf Prms→AConf Prms→Type := ...The reduction rules forApply and particularly the decreasing character of the recursive one (shown below), supplemented by the call-by-value propagation rules, ensures the termination of recursive functions in a way that corresponds to the iterate-style construct of IL. Here isValueList2T is used to check whether a list of expressions equals a list of lifted values, and mkVE:valTC→list Value→valEnv constructs a value environment from a typing context and a list of values of the same length.

|

  Apply_RS1 : ∀(fenv fenv : funEnv) (env: valEnv) (n: W) (e0 e1: Exp) (es:list Exp) (vs:list Value) (x: Id) (i: nat) (pt:valTC), isValueList2T es vs → length pt = length vs → EStep fenv env (Conf Exp n (Apply (QF (FC fenv pt e0 e1 x (S i))) (PS es))) (Conf Exp n (BindMS ((x,(FC fenv pt e0 e1 x i))::fenv ) (mkVE pt vs) e1))Notice the use of BindMS to introduce a local environment, with the following step rules.

|

  BindMS_RS : ∀(fenv fenv : funEnv) (env env : valEnv) (n: W) (v: Value), EStep fenv env (Conf Exp n (BindMS fenv env (Val v))) (Conf Exp n (Val v)) | BindMS_PS : ∀(fenv fenvL:funEnv) (env envL:valEnv) (n n : W) (e e : Exp), EStep (fenvL++fenv) (envL++env) (Conf Exp n e) (Conf Exp n e ) → EStep fenv env (Conf Exp n (BindMS fenvL envL e)) (Conf Exp n (BindMS fenvL envL e ))

  Definition THoareTriple_Eval (P : W → Prop) (Q : Value → W → Prop) (fenv: funEnv) (env: valEnv) (e: Exp) : Prop := ∀ (ftenv: funTC) (tenv: valTC) (t: VTyp) (k1: MatchEnvs FunTyping fenv ftenv) (k2: MatchEnvs ValueTyping env tenv) (k3: ExpTyping ftenv tenv fenv e t) (s s : W) (v: Value), EClosure fenv env (Conf Exp s e) (Conf Exp s (Val v)) → P s → Q v s .

  let f := FC fenv tenv e0 e1 x 0 in {{P0}} fenv >> env >> PS es {{P1}} → (∀ vs: list Value, {{P1 vs}} fenv >> (mkVE tenv vs) >> e0 {{P2}}) → {{{P0}} fenv >> env >> Apply (QF f) (PS es) {{P2}} whereas it does otherwise (i.e. fenv is updated with the assignment of function f0 to the identifier x) let f0 := FC fenv tenv e0 e1 x n in let f1 := FC fenv tenv e0 e1 x (S n) in {{P0}} fenv >> env >> PS es {{P1}} → (∀ vs, {{P1 vs}} (x, f0)::fenv >> (mkVE tenv vs) >> e1 {{P2}}) → {{P0}} fenv >> env >> Apply (QF f1) (PS es) {{P2}}

  let q := QV (cst t1 v) in let g := λs, xf.x_eval s v in let h := λs, xf.x_exec s v in {{λ s. Q (g s) (h s)}} fenv >> env >> Modify xf q {{Q}}

  Definition LLI (A: Type) : Type := state → result (A * state). Inductive result (A: Type) : Type := val: A → result A | undef: nat → state → result A.

  Definition ret : A → LLI A := fun a s ⇒ val (a, s). Definition bind : LLI A → (A → LLI B) → LLI B := fun m f s ⇒ match m s with | val (a, s ) ⇒ f a s | undef a s ⇒ undef a s end.

  Inductive value : Type:= | PE: Pentry → value | VE: Ventry → value | PP: page → value | VA: vaddr → value | I: index → value.

  Definition readPhysical (p: page) (i: index) : LLI page := bind get (λs, match (lookup p i (memory s) page_beq index_beq) with | Some (PP a) ⇒ ret a | Some _ ⇒ undefined 5 | None ⇒ undefined 4 end). gets translated to the following Definition readPhysical (p: page) (i: index) (s: state) : option page := match (lookup p i (memory s) page_beq index_beq) with | Some (PP a) ⇒ Some a | _ ⇒ None end.

  which can be lifted to DEC as external function. Definition xf_read (p: page) : XFun (option index) (option page) := {| x_mod := fun (s: W) (x: option index) ⇒ (s, match x with | Some i ⇒ readPhysical p i s | None ⇒ None end) |}. Definition ReadPhysical (p:page) (x:Id) : Exp := Modify (xf_read p) (Var x).

  (t : Typ) := val t | cond (Exp Bool) (Exp t) (Exp t)

| binds (t : Typ) (Exp t ) (t → Exp t) | call (ts : Typs) (Fun t ts) (Exps ts) | xcall (ts : Typs) (Act t ts) (Exps ts) Exps (ts : Typs) := map Exp ts Fun (t : Typ) (ts : Typs) := fun (ts → Exp t) ((ts → Exp t) → ts → Exp t) Nat Act (t : Typ) (ts : Typs

  The associated invariant ensures that after execution each entry of the given configuration table contains the default value defaultVAddr, regardless of the current index (cidx).

	(Val (cst unit tt))).
	Definition InitVAddrTable (p:page) (i:index) : Exp :=
	Apply (QF (FC emptyE [("x",vtyp index)] (Val (cst unit tt))
	(InitVAddrTableAux "initVAddrTable" "x" p)
	"initVAddrTable" tableSize)) (PS[Val (cst index i)]).
	Lemma InitVaddrTableInv (p: page) (cidx: index)
	(fenv: funEnv) (env: valEnv) : {{λ s, (λ idx : index , idx < cidx →
	(ReadVirtual table idx (memory s) = Some defaultVAddr)) }}
	fenv >> env >> InitVAddrTable p cidx
	{{λ _ s idx, ReadVirtual p idx (memory s) = Some defaultVAddr}}.
	Definition InitVAddrTableAux (f i: Id) (p:page) : Exp :=
	BindN (WriteVirtual p i defaultVAddr)
	(IfThenElse (LtLtb i maxIndex) (BindS "y" (BindS "idx" (IndexSucc i)
	(ExtractIndex "idx")) (Apply (FVar f) (PS [VLift (Var "y")])))

  M t 1 := λx 0 x 1 x 2 . bind x 0 (λv 0 . bind x 1 (λv 1 . bind x 2 (λv 2 . if then else v 0 v 1 v 2 ))) = ret x Θ e (bindse 1 (λx : t. e 2 )) = bind (Θ e e 1 ) (λx : t. Θ e e 2 ) Θ e (cond e 1 e 2 e 3 ) = condM (Θ e e 1 ) (Θ e e 2 ) (Θ e e 3 ) Θ e (call fc es) = bind (Θ es es) (Θ f fc) Θ e (xcall a es) = bind (Θ es es) a Θ es : Exps ts → M ts Θ es es = mapM Θ e es(6)Θ f : Fun t ts → ts → M t Θ f (fun (λ x : ts. e 0 ) (λ (r : ts → Exp t) (x : ts). e 1 ) n) = iterateM ts t (λ x : ts. Θ e e 0 ) (λ (r : ts → M t) (x : ts). Θ e e 1 )) n

	(1)
	(5)
	(7)

mapM : (∀t. Exp t → M t) → Exps ts → M ts := λf es. match es with [] ⇒ [] | e :: es ⇒ bind (f e) (λx. (bind (mapM f es ) (λxs. ret (x :: xs)))) (2) iterateM (ts : Typs) (t : Typ) (e 0 : ts → M t) (e 1 : (ts → M t) → (ts → M t)) (n : Nat) (xs : ts) : M t := match n with 0 ⇒ e 0 xs | S n ⇒ e 1 (iterateM ts t e 0 e 1 n ) xs (3) Θ t (Exp t) := M t Θ t (Exps ts) := M ts Θ t (Fun t ts) := ts → M t Θ t (Act t ts) := ts → M t (4) Θ e : ∀t. Exp t → M t Θ e (val x)

This work was funded by the EU Celtic-Plus Project ODSI C2014/2-12.

DEC can be found at https://github.com/2xs/dec.git[START_REF] Torrini | The repository of DEC[END_REF].

Details in 2xs/dec/src/langspec/LangSpec.v[START_REF] Torrini | DEC 1.0 specification[END_REF]

Specification and proofs in 2xs/dec/src/DEC1[START_REF] Torrini | The repository of DEC[END_REF]

Acknowledgments. We wish to thank all the other members of the Pip Development Team, especially Gilles Grimaud and Samuel Hym, Vlad Rusu and the anonymous reviewers for feedback and discussion. This work has been funded by the European Celtic-Plus Project ODSI C2014/2-12.


domain: math shs

text:
Catherine Houdement
email: catherine.houdement@univ-rouen.fr

Traveling in spatiality, in spatial sense

Keywords: Spatial sense, spatial knowledge, geometrical thinking

published or not. The documents may come

Traveling in spatiality, in spatial sense

Introduction

A travel abroad enriches our way of thinking and furthers our understanding of the values and behaviours of his/her own culture. For us just the same an intellectual trip outside the country (or the language) helps deepen our knowledge and analysis of our way of thinking. The study initially aims to compare the perspectives of educational researchers regarding the notion of spatial sense.

Along the way, it documents the conceptual frameworks which support research.

In ZDM issue 47, Geometry in the Primary School, the theme of spatial sense is common to all papers [START_REF] Mulligan | Looking within and beyond the geometry curriculum: Connecting spatial reasoning to mathematics learning[END_REF]. Could it be that the study involves primary school or that the imagery in thought is a topical subject in recent neuroscience research? In the 36 papers of the ICMI Study Perspectives on Teaching Geometry for the 21st Century (1998) the word spatial was mentioned 353 times but never in a title. Our ongoing study is based on (not yet completely extensive) reading of ZDM 47 and CERME texts on Geometry since the first time (2003) that a specific group about Geometry exists. Such a group has persisted for all the CERME under the name Geometrical Thinking (except 2011 Geometrical teaching and learning).

In short, this paper provides an overview on spatial sense the difference theoretical frameworks regarding it, based on literature published in ZDM issue 47 and CERME papers of the last decade (2003)(2004)(2005)(2006)(2007)(2008)(2009)(2010)(2011)(2012)(2013)(2014)(2015).

First definitions and motivations for studies about spatial sense

Many expressions (spatial reasoning, spatial sense…..) are related to spatial when considering English papers from cross-and interdisciplinary fields of mathematics education, psychology, child development and neuroscience: In a first approach we consider these expressions as equivalent and agree the large definition quoted by [START_REF] Mulligan | Looking within and beyond the geometry curriculum: Connecting spatial reasoning to mathematics learning[END_REF], from Spatial Reasoning Group (2015) "Spatial reasoning (or spatial ability, spatial intelligence, or spatiality) refers to the ability to recognize and (mentally) manipulate the spatial properties of objects and the spatial relations among objects. Examples of spatial reasoning include: locating, orienting, decomposing / recomposing, balancing, diagramming, symmetry, navigating, comparing, scaling, and visualizing." (Mulligan, 2015, p. 513).

It should be noted that this definition considers spatial in a broader sense than 3D-situations or 3Dgeometrical thinking. In this paper we are interested in spatial skills, which are not associated with objects 3D.

Many researchers stress the utility of spatial reasoning for mathematical learning and problem solving [START_REF] Owens | The complexity of learning geometry and measurement[END_REF][START_REF] Sinclair | New opportunities in geometry education in primary school[END_REF], and to Science, Technology, Engineering and Mathematics Education [START_REF] Mulligan | Looking within and beyond the geometry curriculum: Connecting spatial reasoning to mathematics learning[END_REF]. [START_REF] Tahta | About geometry[END_REF] and others note the ability to mobilize wisely spatial skills in mathematical and scientific thought, which [START_REF] Battista | Spatial structuring in geometric reasoning[END_REF], quoted by Mulligan, 2015, p. 514) named spatial structuring and defined as: "the mental operation of constructing an organization or form for an object or set of objects. It determines the object's nature, shape, or composition by identifying its spatial components, relating and combining these components, and establishing interrelationships between components and the new objects" [START_REF] Battista | Spatial structuring in geometric reasoning[END_REF].

Spatial structuring is also an important component of the early learning of numbers, of measurement units, and well of geometrical thought (Van den [START_REF] Van Den Heuvel-Panhuizen | Kindergartner's performance in two types of imaginery perspective-taking[END_REF][START_REF] Mulligan | Looking within and beyond the geometry curriculum: Connecting spatial reasoning to mathematics learning[END_REF]. Van den Heuvel-Panhuizen et al. (2015, p. 347) outline the strong relationship between spatial and mathematical abilities. Mathematical performance and spatial abilities are positively correlated, not only in mathematical domains that are ostensibly spatial.

French scholars as Berthelot & Salinwith a long story of research on geometrical educationagree on the place of spatial abilities in geometry learning, also for geometrical proof. But they have always emphasised (since the 1990s) their interest for everyday life: "the treatment of spatial abilities is the main source not only of many of the further learning difficulties met by secondary school pupils, but also of some of the main deficiencies in spatial representation needs in everyday life" (Berthelot & Salin, 1998, p. 71). This point of view has encouraged them to define and elaborate, unconstrained by geometry (or dissociated by classical geometry), what they called spatial knowledge.

In conclusion it appears that spatial abilities are critical for learning mathematics and beyond. As these abilities are naturally associated with geometry, geometry seems the ideal niche for their teaching. It could even be read between the lines that it would be, nowadays, the main reason for teaching geometry in compulsory school education. Indeed, the present trend in some countries is to marginalize geometry in curricula in favor of probability and statistics [START_REF] Maschietto | Introduction to the papers and posters of WG4: Geometrical Thinking[END_REF]. Obviously spatial reasoning nourishes geometric reasoning (Mithalal-Le Doze, 2015), but geometric reasoning needs other abilities, like defining and classifying (in the sense of [START_REF] Brunheira | Prospective teachers' development of geometric reasoning through an exploratory approach[END_REF], axiomatic reasoning, and doesn't take in account non-mathematical forms of deduction... Furthermore spatial problems, like finding one's way in an unknown town, cannot be assimilated to geometrical tasks. Studying spatial reasoning for itself seems to be interesting.

Spatial sense in CERME papers (2003 to 2015)

Let us first examine how the successive CERME (2003 to 2015) working groups named Geometrical Thinking deal with spatial sense.

The Group Geometrical Thinking worked within the continuity in the CERME3, 4 and 5 (2003,2005,2007). In CERME5 the topic Spatial abilities and Geometrical tasks was considered; it is noted: if it seems possible to agree about Geometrical tasks, it is necessary to precise what spatial abilities mean. We try to do it in the next section.

In CERME6 (2009) spatial abilities is not a specific topic of the Group even though it could be present in the sub-theme Teaching, thinking and learning 3D Geometry.

In CERME7 (2011) spatial abilities is connected to diagrammatic reasoning. Deliyanni et al. (2011) explore spatial abilities in relation with 2D-geometrical figure understanding and consider the influence on reasoning of the different diagram's apprehensions [START_REF] Duval | Geometrical pictures: Kinds of representation and specific processes[END_REF]: perceptual, sequential and operative. [START_REF] Braconne-Michoux | Relations between geometrical paradigms and Van Hiele levels[END_REF] proposes to intertwine the Geometrical Paradigms [START_REF] Houdement | Elementary geometry split into different geometrical paradigms[END_REF][START_REF] Houdement | Geometrical working space, a tool for comparison[END_REF] and the Van Hiele levels which integrates visualization, a spatial ability.

In CERME8 (2013) the Group introduction proposed four competencies (see Figure 1) to support geometrical thinking: reasoning, figural, operational and visual [START_REF] Maschietto | Introduction to the papers and posters of WG4: Geometrical Thinking[END_REF] and assume that the links between these competencies are more important for geometrical work. Spatial abiliies, spatial sense are not explicitly mentioned but it seems (see above in [START_REF] Mulligan | Looking within and beyond the geometry curriculum: Connecting spatial reasoning to mathematics learning[END_REF] CERME9 (2015) in the continuity of CERME8 is supported by the same model (Figure 1). The topic quoted in relation with spatial abilities is visualization. The authors [START_REF] Ceretkova | Introduction to WG4: Geometrical thinking[END_REF] stress the influence of geometric knowledge on visualization, beyond perceptive and psychological aspects.

How do educational researches deal with the issue of spatial abilities? More precisely what kind of theoretical frames do they use or construct for their research?

Theoretical frameworks for spatial abilities

Specifying the frame the authors use in order to analyse spatial abilities is quite rare: only once in ZDM, only a few times in CERME papers before CERME9. Let us give some examples of such frames.

Example 1

In [START_REF] Panaoura | Spatial abilities in relation to performance in geometry tasks[END_REF] spatial abilities are commonly addressed by three major dimensions spatial visualization, spatial orientation and spatial relations. These researchers use an analysis model for spatial abilities [START_REF] Demetriou | The functional and developmental organization of cognitive developmental sequences[END_REF] with three components, namely image manipulation, mental rotation and coordination of perspectives to investigate whether or not and to what extent primary and secondary school students' spatial abilities are related to their performance on geometry tasks involving 2D figures, 3D figures, or nets of

Example 2

In Berthelot & Salin's research (quoted in [START_REF] Douaire | Teaching geometry to students (from five to eight years old)[END_REF] spatial knowledge is knowledge which enables to control one's relations to the surrounding space, the sensible world. This control may consist in recognizing, describing, manufacturing or transforming objects; moving, finding, communicating objects' position; recognizing, describing, constructing or transforming a route (Berthelot & Salin, 1999, p. 38). Children begin to integrate spatial knowledge before going to school while experimenting, and sharing with adults about their actions. Spatial knowledge cannot be reduced to geometrical knowledge but can be necessary to solve a geometrical problem.

It should be noted that this definition relies on problems (what Berthelot & Salin name spatial problems). In Brousseau's theory (the theoretical frame of Berthelot & Salin's research) knowledge is what enables to solve problems, and problems solving is a condition for learning. For instance how to define knowledge to be taught to use efficiently a map when lost in an unknown town? First identifying situations in which using plans and maps are necessary; second analysing the spatial interactions to solve them and thus indentifying the necessary knowledge.

Daily life interactions take place in space of different sizes which exert different constraints on the actions. Microspace is very close to the subject, like a sheet of paper, a computer screen, a touch screen; in this space objects can be moved, touched, turned; it corresponds to the usual grip relations. Mesospace is the surrounding space, inside a room, a building; the subject can move inside it, mesospace is the space of usual domestic spatial interactions. Macrospace is the broader space, unknown city, rural or maritime spaces; the subject has only local views, he had to conceptualize (Berthelot & Salin, 1998, p. 72;Douaire & Emprin, 2015, p. 532). Thus spatial knowledge is structured into three main conceptions, microspatial conception, mesospatial conception, macrospatial conception. For instance, following this frame, a straight line can be conceived as a print trace produced with a ruler, the edge of a door, or a set of trees properly aligned in a orchard. This framework has different functions: in Berthelot & Salin, as in [START_REF] Douaire | Teaching geometry to students (from five to eight years old)[END_REF] the framework allows them to construct situations as means to teach students spatial knowledge (as to alignment and straightness, through the good use of a map to navigate). In other described cases, the frame allows to evaluate and compare performances of students, or to map spatial abilities.

Example 3

Following [START_REF] Newcombe | Spatial development[END_REF], Van den Heuvel-Panhuizen et al. (2015, p. 346) distinguish between two kinds of spatial skills: between-objects representation and transformation skills (for example in Perspective-Taking tasks -PT--, like the Three Mountains of [START_REF] Piaget | The child's conception of space[END_REF] and within-objects representation and transformation skills (for example a mental rotation).

The aim of their research is to assess children's PT-skills focusing on the difference between two components of what they named IPT (Imaginary Perspective-Taking): visibility and appearance. These two competencies are highlighted by the items they proposed to the children.

Visibility

A boy walks along the street. What does he see?

Appearance

How do you see Mouse if you look at it from above like a bird? It could be noted that the 3D situation (meso-or macro-spatial) is communicated to the 2D representation (micro-spatial).

The analysis of their tests with more than 300 children of Netherlands and Cyprus (age 4-5) shows that kindergartners of the two countries can answer correctly: on average respectively 70% and 55% of the visibility items, and 40% and 30% of the appearance items; that the development of the IPT competence visibility precedes the development of the IPT competence; that specific item characteristics of the evoked context could also influence the difficulty level of the item.

Example 4

In the 1990s [START_REF] Duval | Geometrical pictures: Kinds of representation and specific processes[END_REF][START_REF] Duval | Les conditions cognitives de l'apprentissage de la géométrie: Développement de la visualisation, différenciation des raisonnements et coordination de leur fonctionnement[END_REF] has brought an important contribution to necessary visualization of the drawing (implicitly in a microspace) for geometric reasoning. Some authors rely particularly on Duval's research, e.g., Mithalal-LeDoze (2009, 2015), [START_REF] Papadaki | Working with visually impaired students: Strategies developed in the transition from 2D geometrical objects to 3D geometrical objects[END_REF] and [START_REF] Swoboda | Mathematization of rotation as a didactic task[END_REF].

With iconic visualization "the drawing is a true physical object, and its shape is a graphic icon that cannot be modified. All its properties are related to this shape (…)" (Mithalal-LeDoze, 2009, p. 797). With non iconic visualization "the figure is analysed as a theoretical object represented by the drawing, using three main processes: Instrumental deconstruction: in order to find how to build the representation with given instruments), Heuristic breaking down of the shapes: the shape is split up into subparts, as if it was a puzzle), Dimensional deconstruction: the figure is broken down into figural unitslower dimension units that figures are composed of -, and the links between these units are the geometrical properties (…)" (Mithalal-LeDoze, 2009, p. 797;[START_REF] Papadaki | Working with visually impaired students: Strategies developed in the transition from 2D geometrical objects to 3D geometrical objects[END_REF]. Duval quoted two other processes Change of Scale and Change of Orientation.

Studying visually impaired students moving 2D objects to imagine 3D objects, [START_REF] Papadaki | Working with visually impaired students: Strategies developed in the transition from 2D geometrical objects to 3D geometrical objects[END_REF] introduces a new source for mental images, the kinesthetic one. For these students visualization integrated many repetitions of the same gesture, cross-checking it with one's everyday life tactile experience and geometrical knowledge as objects' definitions. Visualization is clearly more than vision, what Duval wrote for a long time describing different ways (iconic and non iconic) of visualizing a figure. But [START_REF] Papadaki | Working with visually impaired students: Strategies developed in the transition from 2D geometrical objects to 3D geometrical objects[END_REF] introduces a new dimension in visualization, a dynamic one; conceiving a figure 3D as the result of a reproducible movement of a figure 2D. [START_REF] Swoboda | Mathematization of rotation as a didactic task[END_REF] stresses the rotation as a natural transformation for young students; mental rotation is a fundamental component of the frame of [START_REF] Demetriou | The functional and developmental organization of cognitive developmental sequences[END_REF], and of non iconic apprehension of Duval too. Maybe the rotary motion and the rotation as transformation could be studied sooner (than the line symmetry) in compulsory school to enrich visualization skills.

Conclusion

Spatial sense and the different frames regarding it is now better mapped. We will not go back on what was discussed above, but just stress some difference between the frames regarding it.

1) The framework of Berthelot & Salin in relation with the size of space enables to realize that almost all the mentioned situations or items of the ZDM and CERME papers (except [START_REF] Douaire | Teaching geometry to students (from five to eight years old)[END_REF] are located in the microspace; a priori they only request microspatial knowledge 1 . The existence and importance of mesospatial and macrospatial knowledge seem underestimated. For example in the paper of [START_REF] Van Den Heuvel-Panhuizen | Kindergartner's performance in two types of imaginery perspective-taking[END_REF] spatial apprehension of a picture (or a drawing, microspace) is considered as an apprehension of the evoked real world (mesoor macro-space).

2) Some papers try to isolate "basic" skills or "basic" items which could be predictive of spatial sense and serve for students assessment, analysing spatial situations (for example [START_REF] Van Den Heuvel-Panhuizen | Kindergartner's performance in two types of imaginery perspective-taking[END_REF] or geometrical problems (Duval 1999[START_REF] Duval | Les conditions cognitives de l'apprentissage de la géométrie: Développement de la visualisation, différenciation des raisonnements et coordination de leur fonctionnement[END_REF]. On the other hand Berthelot & Salin, in coherence with their support framework, don't attempt to describe finely "the" spatial skills but ask students to solve real spatial problems in which spatial skills are at work.

3) [START_REF] Papadaki | Working with visually impaired students: Strategies developed in the transition from 2D geometrical objects to 3D geometrical objects[END_REF] and [START_REF] Swoboda | Mathematization of rotation as a didactic task[END_REF] allow us to realize that gestures can be a powerful help to mentally construct geometrical images and facilitate visualization. Among the gesture the rotary motion (rotation) could play an important role. 4) Visualization is enriched with new entries as gestures and motion; it has gained increasing importance on the spatial skills. But what is meant by this term? Another inquiry to lead…

  to "have a place" in each competency. Two papers assume a spatial entry (other than 3D activities): in Sevil & Aslan-Tutak (2013) and particularly de Freitas & Mc Carthy (2013) emerges a new face of spatial abilities, the gestural / haptic ones.

Figure 1 :

 1 Figure 1: The geometrical competencies (Maschietto et al., 2013)

Figure 2 :

 2 Figure 2: Examples of drawings and questions in the test (Van den Heuvel-Panhuizen et al., 2015)

Proceedings of CERME10


text:
Jacques Douaire
email: jacques.douaire@wanadoo.fr

Fabien Emprin
email: fabien.emprin@univ-reims.fr

Teaching geometry to students (from five to eight years old) "All that is curved and smooth is not a circle"

Keywords: Geometry, teaching, learning, primary education, spatial ability

The ERMEL team (IFé, ENS-Lyon) in France, builds complete engineering to teach math in elementary school. For several years, we have been experimenting with teaching situations on space and geometric learning for 5-8 years old students. In this paper, we focus on the results about the relationship between actions on objects, graphs and first geometric properties about curved line. Our methodology involves an analysis of the student's way of solving problems and thus their abilities, but it also allows us to make a hypothesis on what it is that teachers need in order to carry these learning situations out.

Issue of this paper

Our research takes place in the French context of geometry teaching in primary school. Our goal is to build a proven, complete and reliable teaching engineering and thus to improve geometry teaching.

In CERME 9, we reported our results about the knowledge of straight line for the same kind of students, not as an element of geometrical figure but as a usual or new component of the pupil's practice. Several point of view in the WG4 showed the similar approach and questions were shared:

 The relation between everyday and geometrical concept, perception, language and manipulation  How to start with low level, and long planning time  What kind of tools for the research and tools for teaching geometry are there? (How to help teacher to know what student are able to do)

In this paper, we aim to make our contribution to the three first topics of the WG4 group: what is doing, learning and teaching geometry at school?

Why working on geometry teaching?

A starting point of our research is a finding of deficiencies in the geometry teaching practices in the early grades of elementary school. A short analysis of easily available French resources for teaching geometry to young pupils shows that two mains goals are pursued: learning geometric words and drawing abilities. Spatial activities also exist but without much problem solving, and also unrelated to the pupil's initial knowledge or mathematical activity. This research is also based on the idea that students' abilities are insufficiently taken into account in geometry teaching in primary school. Thus we have to identify the knowledge at stake in this learning and take the students' already acquired knowledge into account.

About our team

ERMEL is the research team on mathematics education in primary school (in French "Équipe de Recherche en Mathématiques à l'École Élémentaire") belonging to the French institute of education (IFé). ERMEL team is made up of primary school teachers, teachers' trainers and researchers working in different regions of France. Results of these researches lead to comprehensive books publications including complete teaching engineering. Studies on teaching and learning conducted since 1999 are about geometry teaching more precisely on the analysis of spatial and geometric skills that students from primary school to GS (5-6 years old) CE1 (7-8 years old) can build. Key issues of these researches are knowledge creation and resources production for teachers and teachers' trainers as well as the study of the appropriation of these resources. In CERME 9 we have clarified our theoretical framework and the steps of our methodology: a didactic engineering, based on an experiment conducted in many classrooms for several years [START_REF] Douaire | Teaching geometry to students (from five to eight years old)[END_REF]. In this paper, we try to explain the transition between space and graphic knowledge which is often underestimate.

Purpose of the study

Our previous studies [START_REF] Douaire | Teaching geometry to students (from five to eight years old)[END_REF] showed that the knowledge developed by pupils in meso-space by solving problems does not necessarily build a geometric knowledge usable on paper. This lead us to ask many questions: in particular, what are the opportunities for pupils to understand the underlying patterns of drawings on a sheet of paper?

We have to clarify the relationship between two types of knowledge, spatial and geometric, and especially the discovery of the meanings of lines on a sheet of paper, and how these plots can provide information about objects in space. If several works address the distinction between drawing or figure at the beginning of the "college" (Parzsyz, 1988) or the apprehension of the components of a figure at the end of primary school [START_REF] Duval | Les conditions cognitives de l'apprentissage de la géométrie: Développement de la visualization, différenciation des raisonnement et coordination de leurs fonctionnements[END_REF][START_REF] Perrin-Glorian | Comment peut-on penser la continuité de l'enseignement de la géométrie de 6 à 15 ans. Le jeu sur les supports et les instruments[END_REF], our research concerns the emergence of graphic representations a few years earlier.

In this working group we will identify the contributions of space experiments in the construction of geometrical knowledge. Our goal is that pupils overcome the overall perception of a figure and develop the analysis of its components.

We analyze learning involved by a problem solving of closed curves figures construction, the characteristics of different implementations, as well as the needs of teachers. We present insights of learning situations for space experiments and we question the relevance of a resource based on the needs of teachers for its implementation identified in the context of ongoing Ermel research.

Presentation of the experimentation

Experimentation concern procedures (graphics, practices, discourse ...) that can be developed by 7year-olds pupils to distinguish circles from ellipses and other rounded shapes. We are not trying to develop early knowledge of the circle, but to promote the passage from a global perception of drawings and shapes to a geometric analysis of geometric shape underlying.

Some questions concern the comparison procedures: what are the abilities of students of CP (6 years old) or CE1 (7 years old) to distinguish a circle from another closed curve (an "almost circle")? What use of superposability as a validation procedure for that?

We present an experiment in progress: students have to produce closed rounded shapes, and must prove if they are different from others.

Proposed situation

The problem is to build closed shapes using four circular or elliptic arcs (quarter of a big circle, little circle or an ellipse figure 1). Identifying that shapes built are different lead students to develop and formulate analytical geometric criteria.

Two major phases of this situation are analyzed successively, the first concerns the problem solving phase to produce shapes: we briefly analyze the productions. The second concern comparison of production. We also present some exchanges during the validation of the solutions.

Finally, a brief summary will address the explicit needs of teachers.

Presentation of the activity

Each pair of students has a deck of 16 cards: 4 quarts of a small circle, 4 quarters of a large circle and 8 quarters of an ellipse (shapes figure 1 are cut following dotted lines like in figure 2). The major axis of the ellipse is the diameter of the large circle. The minor axis of the ellipse is the diameter of the small circle. Thus, shapes can be linked.

Figure 2

Several successive phases in this situation:

1-To ensure the pupils' appropriation of the constraints of the problems they are experimented one by one. Each pupil must first assemble pieces to form a closed shape. Then they verify that these solutions are really closed. These discussions lead to clear assembly instructions: "Are only accepted shapes that are joined edge to edge (assembly like in figure 3 are rejected)". In this first phase, the students do not need to draw, but to assemble pieces of heavy paper. Then pupils have to make closed shapes using exactly four arcs. The findings, confirmed by teachers and observers in classes are that all students are aware of the goal, namely produce closed curves ("tracks") consisting of four arcs at the end of devolution phase. Students have understood the problem's rules.

Figure 1

Figure 3 2-Then each student looks for new solutions. In order to save their shapes and be able to make new assembly pupils are asked to draw on tracing paper (or lite paper) the outline of each new shape found. When students believe they cannot find new shapes the search stops, and solutions are pooled: are they different? If a student thinks he has found another solution, it is displayed and compared with previous. Students explain why they think it is different or it's the same as another already displayed. The goals of the pooling are to identify products that meet or not the constraints and identify the identical solutions.

Possible shapes

The solutions are:

 reconstruction of three basic shapes (large circle, small circle, ellipse) solutions 1-3  combining two half ellipses contiguous or half a small circle (ovoid: solution 4) a large circle (such as "roly poly" or "roller" or solution ... 5). Radius or half axes being concurrent.  combining alternative quarters of small circle and large circle (solution 6)  combining two quarters of alternating ellipses with a quarter of a small circle and a quarter wide circle (solution 7)  combining two quarter ellipses and a small circle (8, 9) or large circle (14,15)  juxtaposing four quarter ellipses (10, 11)  juxtaposing two quarters ellipse with on one side a quarter of large circle, and on the other side a quarter of small (12,13).

Of course, the goal of this situation is not to find all solutions but finding shapes form 1 to 5 with also one or two shapes they cannot name globally is enough for pupils to learn.

Description of pupils' strategy to produce shapes

 choose pieces of random way;  if unsuccessful start from scratch;  put two pieces, then try the other two;  replace one or two pieces in an assembly already achieved;  place the fourth piece by estimating its size.

Description of the comparison procedure

Solutions are shown on the blackboard (some of them may be identical but differently oriented).

We describe comparison strategy used by pupils: 1. Use of the overall look of the drawing (perceptual validation): a. recognition of known shape (circle, round, egg ...); b. rely on variables: overall size, width; c. rely on differences of regularity in curves. 2. Identification of the elements that compose the shape (analytical aspect). 3. Recognition of identical shapes by rotation or reversal. 4. Use of construction processes, with the possibly of remaking to the class. 5. Use of symmetry properties of the shape, mention of the folding ... 6. Use of a practical validation by overlapping.

Strategies based on perception are meanly used.

Those results confirm that spatial abilities are often neglected and that it is a great challenge of our current research. This pooling highlight some questions linked with the drawing:

• the impact of the thickness of the lines on strategy using perception,

• the acceptable tolerance to judge the compliance with constraint, for example the fact that the curve is closed.

The fact is that those questions emerge are important because it lead pupils to progressively give up perception in favor of the analysis of the shape. This dialogue during the validation of solutions illustrated this aspect.

Exchanges during the validation

The solutions are exposed to the blackboard and students check if the set is suitable. T Yes, there is the problem of drawing, we will not be going back to that. Is this circuit possible to do? " (Many S.) Yes

We can see in this transcript that pupils manage to move away from the drawing to analyze the shape. plutôt un"." que ";"

After a pupil has the drawing of his shape on one hand and follows the lines of the set of pieces to check is the shapes are the same (we will show a video of this moment).

Analysis of learning at stake

Firstly, the effects of the situation on pupils learning we can observe are:

1-A change in perception of the role of vocabulary: a.

The familiar vocabulary for describing the known forms, is not effective for others. Many different shapes can look like an egg ... b.

Since drawing on paper is not always successful students have to describe the shapes by analyzing the way they have been built: the arcs used and their sequence of use.

2-

The progressive understanding of the role of sheet layouts to work on the lines (here curves, but straight in other situations) 3-A better knowledge of the circle, based on the development of procedures compared with other forms [START_REF] Artigue | Conceptions du cercle chez les enfants de l'école élémentaire[END_REF]

4-

The practice of displacement to produce new solutions and to recognize identical figures arranged differently 5-Transition from a practical validation based on the superposition to a validation based on the analysis of the properties 6-

The perseverance in research: the students have to rely on perseverance and go to the end of the task, and of course explain, justify, criticize, debate.

We think that, at the end of this situation, students are able to explain, with their words, several of their learnings.

Secondly, we have analyzed what are the difficulties, and what is possible to propose to pupils. We think, after several experiences, that the main obstacles are not epistemological; they do not come from the inability of students to analyze forms or working on their uncluttered representation. But it is rather didactic obstacles created by neglecting their knowledge and solving capacity. There is a necessary transition from a perceptive approach of the shapes to the analysis of their geometrical characteristics (size, composition, curvature…). In our progression of learning we also offer other situations which contribute to this passage from "global" (for instance, students perceive the regularity of form) to "analytic".

Thirdly we try to find condition of a real use in classrooms. For those of teachers who are not satisfied with their way of teaching geometry we think it is important to propose activities that are real problems (where pupils have to produce new strategies) and to clarify learnings at stake. But we think that it would be unrealistic for a teacher whose main objective would be to set a vocabulary to embrace the process. Potential learning is related to the possibility for the teacher to understand the issues: allow students to implement the different comparison procedures.

This workshop proposes to enlighten those issues.

In this presentation we have not detailed the many changes in the description of the situation, related to successive and necessary experiments for students to produce the specified procedures. On this aspect of the construction of a teaching situation, we simply discuss the question of the context: is it necessary for such young students to evoke a familiar context? The way quarter-circles or ellipses are drawn have also been choose different during the experiment: either simple lines (parts of the cited figures), double lines to evoke real-world objects: railway circuits. But does the latter choice provide a better understanding of the constraints (in particular the continuity of lines)? We currently believe that, on the contrary, this approach makes the problem harder to understand.

Figure 4 :

 4 Figure 4: 15 different shapes were found

  Student (S2) I believe we cannot do it ... Teacher (T) The others, are you sure? S2 appears to confirm T This drawing there you think that doing it is impossible? S2 show the drawing of the shape and try to express something. team who have made this track, you come back to the dashboard. are bumps S …but in all there are bumps ... because we do not succeed in drawing….

Proceedings of CERME10

Conclusions and prospects

Let us return briefly to the issues addressed:

On learning targeted: what learnings can be developed based on the perception (regularity of a shape) to contribute to the analysis of geometrical properties? We mentioned a shift from a parts assembly problem to a drawing problem (a graphical problem); to that extent, the sensitive space has changed. First it is the space of action on the shapes to assemble, which has been among the first personal procedures of the students in the resolution phase. During the pooling, pupils focus on curves continuity and sensitive space become the place where graphical plots are questioned: they are new geometrical objects.

On taking initial knowledge of students into account: how knowledge, language, gesture, participate in the apprehension of the common elements to the diverse types of spaces? How are first procedures and knowledge of the "graphical-space" combined with previous experience on objects? In particular, these prior knowledge is not primarily "declarative" but rely on gestures (eg the difference between rotate and reverse or the use of drawing with instruments without necessarily aiming to represent a geometric objects ...) They are also expressed in the language forms, as part of a language used by the student to control his actions or to communicate about a production (formulation of a procedure, checking of constraints validation of a solution ...). The importance of this learning is often underestimated in education in favor of the use stereotyped and offline vocabulary.

Our research aims to analyze and develop, not only in this specific example, general student abilities via experience and actions on objects with graphical plots. Thus they evolve from a spatial perception to geometric characteristics of the shapes. Our concerns are also those of [START_REF] Swoboda | Mathematization of rotation as a didactic task[END_REF] about problem solving mainly with older students: "Therefore, the problem of bringing students to the ability of making mental transformations I treat as an educational task. In the literature, there is no explicit opinion on what educational level there is possible to create such skills. » Thematic Working Group 04 Proceedings of CERME10