Xavier Denis

Deductive program verification for a language with a Rust-like typing discipline

Deductive program verification seeks to eliminate bugs in software by translating programs annotated with specifications into logical formulas which are then solved using semiautomated tools. When verifying programs using a mutable heap, it is often required to show that pointers do not alias each other, ensuring there is only one way to modify structures in memory. This leads to cumbersome proof obligations and makes verification much more challenging. Newer languages like Rust feature pointers as well but prevent aliasing through the type system. This opens the door to simpler approaches to verification, free of tedious proof obligations.

We propose a technique for the verification of Rust programs by translation to a functional language. The challenge of this translation is the handling of mutable borrows, pointers with control of aliasing in a region of memory. To overcome this, we used a technique inspired by prophecy variables to predict the final values of borrows. The main contribution of this work is to prove this translation correct. We developed a proof-of-concept tool to show the viability of this approach.

Introduction

Over the past 50 years programming languages have made major strides, allowing programmers to reason about and abstract ever larger software projects. Yet, when performance and efficiency become concerns, they resort to low-level programming languages like C/C++ or even assembly. These languages offer control over memory and in particular allow unrestricted usage of pointers to build complex data structures and efficient algorithms. This power comes at a cost. Reasoning about the correctness of pointer programs is very tricky. The challenge is aliasing, when a value can be accessed through more than one name. When two variables are aliased, changing either also changes the other. This makes it difficult to reason about code because programmers must keep in mind all potential aliases to understand the state of their programs.

Languages like C which have pervasive aliasing make this incredibly challenging and it often is a source of bugs in software. For example, Figure 1, performs a swap using XOR to avoid allocating a temporary variable [START_REF]Aliasing (computing[END_REF]. But there's a bug! If the user provides the same pointer to both arguments, this function will write 0 to it instead. Aliasing and related issues like buffer overflows occur constantly, and cause many safety and correctness issues in C software.

In most programs, programmers make the implicit assumption that values are not aliased, but in C the compiler offers no help to verify this. When attempting to formally verify a C program, such aliasing assumptions must become explicit, and it can easily turn into a nightmare [START_REF] Bornat | Proving Pointer Programs in Hoare Logic[END_REF]. Many approaches exist in the literature to overcome aliasing issues in the formal verification of programs in C-like languages. This work takes another path: instead considering a language like Rust, which offers a strong type system to control aliasing.

The Rust Programming Language

The Rust programming language is a recent entry in the field of systems programming languages. Its 1.0 release, published in 2015 [START_REF][END_REF] aims to "empower everyone to build reliable and efficient software" [START_REF]Rust Programming Language[END_REF]. Rust provides memory-safety without requiring a garbage collector through its type system [START_REF] Matsakis | The rust language[END_REF]. The type system uses a system of ownership to ensure that mutable references cannot alias. When the xorSwap program of Figure 1 is translated to Rust, as shown in Figure 2, the bug is no longer possible: a call to that function using the same argument twice will trigger a type checking error.

Ownership in Rust

In Rust every memory cell has a unique owner, which has exclusive read and write permissions. This is sufficient to program in Rust using a functional programming style. The program of Figure 3 illustrates this: it constructs a pair, and then increments the second component, not by mutation but by producing a new pair. But this style is limiting and more imperative programming style is desirable.

Borrows and Lifetimes To perform memory mutation, Rust uses safe pointers called references that can borrow these permissions from their owner. But then aliasing arises and it is where the Rust-specific type system comes into play: such a borrow restricts the permission of the original owner for a limited period of time so that aliasing is controlled. When a reference is created it can come in one of two forms: either unique and mutable or shareable but immutable. The Rust compiler infers the lifetime of references after which the permissions are restored to the owner. The program of Figure 4 illustrates this, exploiting the ownership and borrowing mechanisms of Rust. When x is mutably borrowed into y, it transfers its read and write permissions to y and so loses access to its own contents. The function inc, takes ownership of its argument, consuming it, so Rust implicitly reborrows y before calling inc. Reborrowing consists in borrowing the permissions of a borrow for a shorter lifetime than the original borrow. This mechanism makes borrows flexible and intuitive to use, because after each call to inc, morally we should be allowed to use y again. During compilation Rust statically verifies that borrows are used correctly, inferring the lifetime of each borrow.

Verification

What does it mean for a program to be correct? A common answer is that the program should satisfy a logical specification. This specification encodes the properties expected of a program. For example, a specification of xor_swap could be that the values of x and y are exchanged. To verify that programs satisfy specifications many techniques can be used, from model checking [START_REF] Godefroid | Software model checking: The VeriSoft approach[END_REF], to dependent types [START_REF] Leroy | CompCert-a formally verified optimizing compiler[END_REF] or deductive verification [START_REF] Kirchner | Frama-C: A software analysis perspective[END_REF].

Deductive verification of programs works by translating a program and its specification into a collection of verification conditions such that their truth implies the program follows its specification. These verification conditions can be discharged using a variety of tools, though commonly, automated SMT solvers are used. This highly automated approach to program verification is appealing because it allows engineers to focus their attention on developing a specification rather than proving logical formulas.

Verification conditions can be generated by several techniques, including the weakest precondition calculus. This approach starts with the postcondition of a specification and asks what the weakest precondition that upholds the postcondition is. A rule is determined for each syntactic element of the language, and then recursively applied to translate a whole program to this logical form.

Deductive verification tools for languages with aliasing like C generate non-aliasing conditions [START_REF] Kirchner | Frama-C: A software analysis perspective[END_REF] as part of the verification. By leveraging the ownership property of Rust programs, we can eliminate these conditions and simplify the verification conditions required to prove specifications true.

Contributions

We present a schema for the deductive verification of Rust programs by translation to a functional language. This translation handles both mutable and immutable borrows as well as owned pointers. This paper is structured in several sections, Section 2 presents µMIR, a fragment of Rust allowing only owned data. Using µMIR, we detail the type system which enforces ownership and its semantics. We then present a schema for the verification of µMIR and prove it correct.

The Section 3 section extends µMIR with mutable and immutable references into MiniMir. We explain how the introduction of references impacts the type system and semantics. Then we present a translation of MiniMir to a functional language with non-determinism and extend the proof of µMIR to handle references. In Section 4 the translation, we developed a proof-of-concept implementation and showed it is capable of verifying real Rust programs.

Instruction ::= x ':=' 'box' x | x ':=' 'unbox' x | x ':=' 'copy' x | x ':=' 'copy' '*' x | 'drop' x | 'swap' '(' x ',' x ')' | x ':=' x op x | x ':=' const | '(' x ',' x ')' ':=' x | x ':=' '(' x ',' x ')' | x ':=' 'inj' i x | 'call' f ( x , .., x ) | 'assert' x Statement ::= Instruction ';' 'goto' | 'match' x '{' inj 0 x → 'goto' , inj 1 x → 'goto' '}' | 'return

A basic language with ownership

Rust is a complex programming language, targeted at industrial use with a large syntax and underspecified operational semantics. During compilation, the Rust compiler translates programs to MIR, an intermediate language with a greatly simplified syntax and a graph structure. Since 2018, with the introduction of non-lexical lifetimes, the rules for borrow checking are formulated on the MIR graph rather than source Rust. This makes MIR an attractive starting point for verification of Rust since, with its smaller syntax and simpler static analysis, translations and proofs stay smaller. We begin by formalizing a fragment of MIR containing only owned values called µMIR. This restriction makes it impossible to express many programs but gives room to focus on the other defining characteristic of µMIR, its graph structure.

The µMIR language

A program P is a collection of function declarations, and must contain a function main which acts as the entry point. Function declarations are in turn composed of a triple (∆, , σ) consisting of a set of labeled statements ∆, an entry label , and a function signature σ. Function signatures are made of the function name, a collection of input parameter names and types and the return type. The syntax of µMIR is described in Figure 5.

Statements come in three forms: an instruction followed by a goto, a match on a variable or a return. We write P f, to refer to the statement associated with the label of the function f in program P. Instructions perform the basic operations of the language. In each instruction the variables are annotated with their types. There are instructions to allocate, dereference and deallocate an owned pointer on the heap. In µMIR a box type is an owned pointer to a value, granting the owner exclusive access to the pointed region of memory. Values of certain types can be copied, and the contents of a box can be as well. Appendix A includes the rules for determining if a value can be copied. Dropping is the mechanism through which variables are freed. In µMIR, writing to memory is done by swapping values. Finally, primitive operations like assigning literals, arithmetic and comparisons are supported. µMIR also includes instructions to interact with products and sums. 3 is expressed in µMIR. To save space we put several statements on a single line. The code size blows up but decomposes the individual operations that happened in Figure 3 in a manner very similar to actual MIR.

A type system for ownership

The type system of µMIR is responsible for enforcing the unique ownership of every value in a program. Operations which manipulate boxes consume their inputs, removing them from the typing context and introducing new bindings for the results. Because of the imperative, graph structure of µMIR, the typing judgements take a different form from most languages. The presence of cycles within a graph make traditional natural deduction trees impossible to use. Instead, each program point is assigned a typing context, and typing relates the contexts before and after the evaluation of a statement.

Each label of a function is associated with a partial variable context Γ. The partial variable context is a collection of items of the form x : T , where x is a variable name and T is a type. In a µMIR program P, each function f is given a whole context Ξ which is the collection of the partial contexts for all labels in f . Additionally, we use Σ to refer to the collection of signatures found in a program.

Typing judgements for instructions have the form Γ f I Γ , which relate the partial contexts before and after executing the instruction I in the function f . In this representation, the mechanism of ownership becomes clearer, for example looking at (box) shows how when a box is created, the original variable y is destroyed to ensure the new pointer x remains the unique owner.

(box) Σ; y : T, Γ f x box T := box y T Γ, x : box T Typing judgements for statements have the form Σ; Ξ; P f,a S and verify that the statement with label a in function f , types with the expected partial context. Σ; Ξ a f I Σ; Ξ (sequence) Σ; Ξ; P f,a I; goto The rule for (box) checks that the instruction I can be typed using Ξ a , producing Ξ . In this approach, each statement checks an edge of the µMIR graph. The rules for (function) and (program) check that each function forms a graph. The full typing rules can be found in Appendix A.

Operational Semantics of µMIR

The operational semantics of µMIR is given by a reduction relation over an abstract heap machine. The configurations of the µMIR machine are of the form f ; | S | F | H , where f is the name of the function being executed and is a label in f , S is the call stack, F is the frame, and H is the heap. The stack is composed of triples [f ; , x, F] of a return label, a variable name for the result and a frame. A frame F is a partial function from variable names to addresses. We support pointer arithmetic: adding an address and an integer to obtain an address. The heap maps those addresses to a value which is either: an address, an integer, a boolean value, or unit. Complex values such as pairs or sums are stored in contiguous regions of the heap. Operations which must move or copy these values calculate the size of the values from their types:

|T 1 × T 2 | = |T 1 | + |T 2 | |T 1 + T 2 | = 1 + max(|T 1 |, |T 2 |) |box T | = |bool| = |int| = |unit| = 1 Definition 2.1 (Notations).
If F is a partial function, and A is a subset of its domain, then A -F denotes the domain restriction removing A from the domain of F , and is defined as

A -F = {(x, v) | (x, v) ∈ F, x ∈ A}
Below, we include the rule for drop, which deallocates a variable. When a variable is dropped, we lookup it's address in the current frame and remove it from the heap. The remaining reductions are given in Appendix B.

P f ; = drop x T ; goto ' (drop) f ; | S | F ⊕{(x, a)} | H → P f ; | S | F | {a} -H

Type preservation by reduction

We would like to ensure that the only way for a well-typed µMIR program to get stuck is by failing an assertion. This property allows us to reduce the safety of a program to the validity of its assertions. But if we look at the semantics from Section 2.3, it is clear that the machine can easily get stuck when the frame and heap contain invalid addresses or missing data. To correct this, we define a notion of well-typed configurations which restrict us to only the configurations that could appear when evaluating a well-typed program. We can then prove the standard preservation of typing for these configurations, showing that for well-typed programs only assertions can block evaluation.

Definition 2.2 (Heap Fragment Type).

When we write H a : T , we mean to say that the heap fragment H starting at location a, corresponds to a value of type T .

H 1 a : T 1 H 2 a + |T 1 | : T 2 H = H 1 ⊕ H 2 H a : T 1 × T 2 H a + 1 : T i H ⊕{(a, i)} a : T 0 + T 1 H p : T H ⊕{(a, p)} a : box T c is a literal of T T ∈ {int, bool, unit} {(a, c)} a : T
A well-typed configuration is just a configuration where the heap H contains exactly the variables accessible in the frame F. Definition 2.3. A frame F is well-typed at f ; for a portion of a heap H if f is typed with Ξ in P, and:

H = x∈F H x dom(F) = dom(Ξ ) ∀x ∈ F, H x x : Ξ (x) A configuration f ; | S | F | H is
well-typed for a well-typed program P when it satisfies the following conditions:

∀i ∈ [1, |S|], S[i] = [f i ; i , x i , F i ] ⇒ well-typed F i f i ; i H i well-typed F f ; H 0 H = H 0 ⊕ i∈[1,|S|] H i
We can now define what it means for reduction to preserve types, it simply ensures that the heap is composed exactly of the values expected at a given program point.

Theorem 2.4 (Type Preservation). Given a well-typed configuration C, if C → P C , then C is well-typed.
We don't prove this lemma and instead we will prove an extended version in Section 3.4.

Verification of safety for µMIR programs

To verify µMIR code, we translate it to a functional language. Then we prove that when the translation does not get stuck, neither does the µMIR program. This might seem redundant since Section 2.4 already proved preservation of typing, but by translating to a functional language it becomes possible to leverage existing deductive verification tools. To verify µMIR code, we will translate it to a functional language and use existing tools to verify the translated program. This approach is also easily extensible to arbitrary specifications which can be represented as pure logical functions. Simplification In the following sections, we only consider programs without function calls, and therefore we ignore the stacks of the µMIR machine. The problems raised by function calls are orthogonal to the primary challenge of this proof and the one in Section 3.5.3. As a result, programs only consists in the body of the main function.

The µML language

For µMIR, we will target a simple ML family language which we call µML. It is an untyped ML dialect equipped with assertions, and call-by-value semantics described by an abstract machine with environment. The rules of the µML abstract machine can be found in Appendix E. The translation takes a well-typed µMIR CFG and produces a set of mutually recursive µML functions with the same entrypoint as µMIR. A labeled statement becomes a function where the arguments are the entire domain of the partial variable context associated with the label. Each goto is compiled to a function call, and the arguments are the variables in the domain of Ξ . Most instructions from µMIR are translated to their direct counterparts in µML. For example, here is the traduction of the construction of a pair:

: x := (y, z); goto ' fun a = let x = (y, z) in a
where a = dom(Ξ ) and a = dom(Ξ ) Interestingly, the operations related to the box type are entirely erased since we are not interested in the memory layout in µML:

: x box T := box y T ; goto ' fun a = let x = y in a : x T := unbox y box T ; goto ' fun a = let x = y in a
where a = dom(Ξ ).

The full translation rules are presented in Appendix C.

Translating Figure 6 When we run the translation we produce the following set of functions.

Correctness of the translation

We have a translation, but what does it actually produce? To ensure the translation is correct, we will show that whenever the µML translation of a program is safe, that is, it does not get stuck, then so is the original program.

Theorem 2.5 (Safety). Given a well-typed program Γ P, if P is safe, then P is safe.

In order to prove Theorem 2.5, we establish a simulation ∼ P between the input program P and its translation P . We will give the exact definition of ∼ P later, but what's important is that it restricts the µMIR heap and µML environment to ensure that the values in the environment correspond to regions of heap memory. Using this simulation we prove auxiliary lemmas, from which the proof to Theorem 2.5 will be formed.

The proof of safety is achieved using the following three lemmas.

Lemma 2.6 (Preservation of Simulation). Given a µMIR configuration C and a µML configuration K such that

C ∼ P K, if C → P C then K → K and C ∼ P K .
Lemma 2.7 (Progress). Given a µMIR configuration C and a µML configuration K such that

C ∼ P K, if K is not stuck then C is not stuck.
Lemma 2.8 (Terminal Configurations). Given a terminal µML configuration K, for any µMIR configurations C such that C ∼ P K, then C is terminal.

Proof of Theorem 2.5. Suppose that C is not safe, therefore there exists a trace C → * P C which gets stuck. By iterating Lemma 2.6, there exists K , such that C ∼ P K . Because K is safe, it cannot be stuck and must either be terminal or continue reducing. If K is a terminal configuration then by Lemma 2.8 there is a contradiction since C is not terminal. If K is not terminal then there exists K such that K → K K and by Lemma 2.7 there exists C such that C → P C , therefore C is not stuck.

Simulation Invariant

In order to describe the simulation relation ∼ P which relates µMIR and µML programs, we show how to translate a region of a heap into a µML value. This relation is called the readback of the heap. The region of memory associated with each µMIR variable will be translated to a µML value. Because µMIR features only owned values and no borrowing, heap regions are intrinsically separated, which makes the readback a fairly direct and natural operation.

The readback of a heap region is guided by the type of the variable, it extends the heap typing relation covered in Section 2.4, associating a µMIR value to the concerned region of memory. Definition 2.9 (Readback). R(H, a, T, v) is a 4-place relation between a heap, address, type and a µML value.

R(H 1 , a, T 1 , v 1 ) R(H 2 , a + |T 1 |, T 2 , v 2 ) H = H 1 ⊕ H 2 R(H, a, T 1 × T 2 , (v 1 , v 2 )) R(H, a + 1, T i , v) R(H ⊕{(a, i)}, a, T 0 + T 1 , inj i v) R(H, p, T, v) R(H ⊕{(a, p)}, a, box T, v) c is a literal of T T ∈ {int, bool, unit} R({(a, c)}, a, T, c)
The correspondence between a heap, frame and environment is given by HeapEnv which selects the correct elements from the readback to populate the environment. Definition 2.10 (HeapEnv). HeapEnv(F, H, Γ, E) is a 4-place relation between a µMIR frame and heap, a partial variable environment and a µMIR environment where:

dom(F) = dom(E) H = x∈dom(F) H x ∀x ∈ dom(F), R(H x , F(x), Γ(x), E(x))
The final simulation relation ∼ P uses HeapEnv to relate a µMIR heap to a µML environment and restricts µML programs to the translation of the corresponding µMIR label. The full relation is given in Appendix D along with the proof of Theorem 2.4. The proof proceeds by case analysis on the reductions of µMIR, shuffling memory around to show that the resulting readback is exactly what was expected. We exclude it for space considerations.

Recap

In Section 2 we presented a small unstructured language with an ownership discipline enforced by typing. This language simulates the behavior of owned values in MIR. We then showed how to translate µMIR programs to µML, a standard ML dialect and proved Theorem 2.5 showing that this translation is correct and permits the verification of µMIR programs. During function calls in µMIR every argument is consumed, making it impossible to call a function with the same argument twice. To solve this, Rust uses borrows which allow a variable to lend its read and write permissions temporarily. While a value is borrowed, the original owner is frozen until the end of the borrow's lifetime. We can pass a function a borrowed reference as an argument, giving it temporary ownership of the contents, while recovering control when the borrow expires. We extend µMIR with the operations required to create and manipulate borrows as well as ghost operations used to ensure their safety. We call this resulting language MiniMir, because it's a mini language that does the maximum!1

Instruction ::= v ':=' '&mut' α v | 'immut' v | v ':=' 'unnest' v | '(' 'ref' v ',' 'ref' v ')' ':=' * v | 'thaw' α | α ≤ α Statement ::= 'match' *x '{' inj 0 'ref 'y 0 → 'goto' 0 , inj 1 'ref' y 1 → 'goto' 1 , '}' | . . .

The MiniMir language

Just like in µMIR, programs are collections of function declarations. The syntax of signatures is more complex, functions can be parameterized over lifetime variables α and lifetime constraints α ≤ β. Let us consider an example:

fn fst_proj < α| > (p : &mutαint x int) → &mutαint
The signature for fst_proj takes as input a mutable borrow alive for α of a pair of ints (represented at runtime as a pointer to a pair of ints), and returns a borrow lasting for the same lifetime α of a single int. Here, function is parameterized over α, allowing us to instantiate it with different lifetimes at different points in a program. The instructions and statements are extended with operations to create a mutable borrow (x &mutα T := &mutαy T ), to turn a mutable borrow into an immutable borrow (immut y &mutα T ) and to unnest borrows (x &mutα T := unnest y &mutαP T ). Unnesting is an essential operation when working with borrows. It collapses a layer of indirection between borrows, transforming a &mutα&mut β T into a &mutα T . To interact with product types, a borrow of a pair can be destructed into a pair of borrows (let (ref x P T 0 , ref y P T 1 ) := *z P (T 0 ×T 1 ) ).

The statements of MiniMir includes a new kind of match (match *x { .. }) which allows programs to turn a borrow on a sum into a borrow on the value contained in the sum. When this occurs, programs are free to modify the value held in the sum but cannot change the constructor of the sum.

To verify the safety of borrows, we also add several ghost instructions, to thaw (end) a lifetime and to impose an ordering over lifetimes.

We can see this translation applied to Figure 4 in Figure 8. In this translation we inlined the inc function to make presentation simpler.

Extending types with borrowing

By creating pointers to values, borrows introduce aliasing. To prevent that, when a value is borrowed for a lifetime α, the original name will be made inaccessible or frozen until the end of α. To verify this safety property, the type system tracks a partial order on lifetimes, ensuring that borrows cannot outlive their prescribed lifetime. When the type system encounters a thaw α instruction, it checks that all relevant borrows have been released and restores access to frozen variables.

We extend the type system of µMIR with partial lifetime contexts, which consist of a collection of elements α ≤ β. The partial variable context for MiniMir consists of elements of the form x : †α T or x : • T , the first denoting a variable is frozen for lifetime α while the second denotes it is not frozen.

The whole context of a function (Ξ, Λ) also collects the partial lifetime contexts for every label in the function. The forms of judgements extend naturally, using the lifetime contexts where appropriate. The judgements for instructions and statements are extended with partial lifetime contexts, while the judgement for functions is extended with a whole lifetime context.

The typing judgement for x &mutα T := &mutαy T expresses how the original value y is frozen until α expires while granting x access for that lifetime. No modifications are made to the partial lifetime context L as creating a borrow does not immediately place it in an ordered relation.

(borrow-mut) Σ; y : • T, Γ; L f x &mutα T := &mutαy T Γ, x : • &mutα T, y : †α T ; L When a lifetime is ended using a thaw α, the type system ensures that everything borrowed for α has been dropped and that all lifetimes β ≤ α have already been thawed. After a lifetime is thawed, all variables in the context which were frozen for α are unfrozen, restoring access. The complete type system for MiniMir is included in Appendix F.

Operational Semantics of MiniMir

The operational semantics of MiniMir changed little compared to µMIR. Because instructions like thaw are ghost, they become no-ops in the semantics. The primary addition of MiniMir, the mutable borrow, creates a new pointer to a value. The extended semantics for MiniMir is included in Appendix G.

Type preservation by reduction

Simplification In the following sections, as in the end of Section 2, we only consider programs without function calls. Again, the problems raised by function calls are orthogonal to the primary challenge of this proof and the one in Section 3.5.3.

The banality of the semantics for mutable references is exactly what we desired. They create pointers that the type system ensures can only be used safely. To prove this we extend Theorem 2.4 to the full language of MiniMir.

We extend the heap fragment typing of Section 2.4 to include reference types. Since mutable references are non-aliasing, the heap fragment types must ensure that there are never two active pointers to the same region of memory. To ensure mutable borrows are only used once in a heap, we use a borrow store The borrow store holds tokens for the lender and the borrower. By consuming the borrow store, the heap typing can ensure each borrow is used only once. Definition 3.1 (Borrow Store). A borrow store is a finite set of elements of the form take r α (a, T ) or give r α (a, T ), where a is an address, T is a type and r is either i for immutable or m for mutable. A borrow store B is safe if for every address a appearing in B it contains exactly the tokens take m α (a, T ) and give m α (a, T ) or contains give i α (a, T ) and zero or more take i α (a, T ).

We extend heap fragment typing and well-typing of Section 2.4. The judgments have the form, B; H |= a : n T , where B a borrow store and n ∈ { †α; •}. The definition of a well-typed configuration is then extended to ensure borrow stores are safe. Definition 3.2 (Heap Fragment Type for MiniMir). Below are the heap typing rules for mutable and immutable references. The borrow store checks that both the lender and borrower agree on the addresses and types borrowed. The full rules are found in Appendix I.

dom(Ξ ) = dom(F) H = x∈F H x B = x∈F B x saf e(B) B x ; H x |= x : n Ξ (x, n)
Using these expanded definitions, the proof of preservation extends easily to handle mutable and immutable references. Whenever a borrow is created or dropped, the corresponding tokens are inserted or removed from the borrow store.

Theorem 3.4 (Type Preservation). Given a well-typed MiniMir configuration

C, if C → P C , then C is well-typed.
The interesting cases of this proof are discussed in Appendix I

Verification by translation

We extend our translation from µMIR with support for mutable and immutable references. Our encoding of mutable borrows into a functional language relies on their non-aliasing. When a borrow is created through x &mutα T := &mutαy T , the type safety of MiniMir tells us that y cannot At the end of α, y will have been updated with all the changes performed on x. In some sense, when we translate x &mutα T := &mutαy T , we would like to replace y with the final value pointed to by x. Since we can't see into the future, we non-deterministically guess a value for y. Our translation represents mutable borrows as a pair of the current and final value being borrowed, like in RustHorn [START_REF] Matsushita | RustHorn: CHC-based Verification for Rust Programs (full version)[END_REF]. When the borrow is created we assign to y the final value of the borrow. As the translated program executes, the current value of x is updated. When the borrow is frozen, we rule out any executions that guessed the wrong final value by checking that the current and final values are equal.

The MiniML language

MiniML is an extension of µML with non-determinism. The any expression picks an arbitrary value, and a assume { e } evaluates an assumption e, if it doesn't reduce to true, then it diverges. The operational semantics of µML are extended to include these constructs in Appendix J.

Expression, e ::= 'any' | 'assume' '{' e '}' | ...

Translating from MiniMir to MiniML

The translation of µMIR to µML is adapted to MiniMir. When a borrow is created, the borrow is assigned the current value being borrowed and its final value. In the translation we use two operators to access borrows defined as: *x fst x and ^x snd x.

: x &mutα T := &mutαy T ; goto ' fun a = let x = (y , any ) in let y = ^x in a

When a mutable borrow is made immutable, we use the assume expression to equate its current value and final value. The full translation is presented in Appendix H. In Figure 9, the program of Figure 8 is translated to MiniML. Instructions with produce no output in the translation are elided entirely.

Correctness of translation

We now examine the correctness of the translation presented in the previous section. Our safety theorem has the same structure as in µMIR but because of the non-determinism of MiniML the notion of safety changes to be programs in which all traces are non blocking.

Theorem 3.5 (Safety). Given a well-typed MiniMir program P, if P is safe, then P is safe.

The proof of this theorem is structured in the same manner as for µMIR. To establish a simulation between MiniMir and MiniML we must extend the translation of memory to handle borrows.

When we define the simulation between MiniMir and MiniML, we find that mutable borrows cause us a problem. Each time a borrow is created, the translated program must guess the final value of the borrow, a value which appears nowhere in the memory of the MiniMir program. The readback must make the correct guess to constrain the traces in the simulation. We simplify this problem by supposing the existence of a prophecy map, which contains the correct final value for every pair of borrowed address and type. Using this prophecy map, we can define the readback of MiniMir as an extension of the heap typing just like with µMIR. Definition 3.6 (Readback). The readback of Definition 2.9 is extended with support for mutable and immutable borrows. For each value being readback, it will produce a mapping containing every sub-value within.

A(a, T Formally, HeapEnv (B, A, F, H, Γ, E) is a 6-place relation between an activeness, a borrow store, a prophecy map, a MiniMir frame and heap, a partial typing environment and a MiniML environment where:

) = v R †α ({give m α (a, T )}, A, ∅, a, T, (a, T, v)) R †α (B, A, H, a, T, E) R †α ({give i α (a, T )} ∪ B, A, H, a, T, E) A(a, T ) = v R n ({take i α (a, T )}, A, {(p,
dom(F) = dom(E) H = x∈dom(F) H x E = {(x, V x (F (x), T )) | x : n T ∈ Γ} ∀x ∈ dom(F), R n (B x , A, H x , F(x), Γ(x, n), V x )
It turns out, rather essentially, that the prophecy map we need can be calculated from a MiniMir trace. To do this, we take a trace and walk it backwards, each time a thaw α is encountered, the end of a lifetime has been reached. At that moment the values of all variables that were frozen are readback.

P f ;l = thaw α HeapEnv (A, B, F , H , Ξ f ; , E) A = A ⊕ give r α (a,T )∈B {E | R †α (B a , A, H a , a, Ξ f ; (a, •), E)} McFly * (A , [f ; ] | -| F | H → P f ; | -| F | H | B , A)
In order to use McFly * we use a simulation between MiniMir traces and MiniML configurations. The simulation relation, ∼ P calculates the required prophecy map using McFly * , and uses it to ensure that the heap translates to the MiniML environment. At the same time the code is constrained to be the translation of the initial configuration of the trace.

We structure the proof of Theorem 3.5 using the same three lemmas as before: progress, terminal configurations and preservation. Using these lemmas, the proof proceeds in the same manner as Theorem 2.5. The statements of the first two lemmas change to account for the non-determinism of MiniML but, the structure of their proofs remains the same, thus we leave them in Appendix I, and focus on the proof of Lemma 3.8.

Lemma 3.8 (Preservation of Simulation). Given a MiniMir trace

Θ = C → * P C and a MiniML configuration K such that Θ ∼ P K, if C → P C , there exists a K such that K → K and C → * P C ∼ P K .
The general structure of the proof remains unchanged from µMIR, it proceeds by case analysis on the reductions of MiniMir. The reductions relating to owned values proceed exactly as before, shuffling information around. Instead, the essential difficulty of this proof comes down to showing that McFly * finds the correct final value for every borrow. The intuition is that once a value is frozen, it cannot change, and therefore at the moment that we find the prophecy it must have the same value as when it was frozen.

Consider the case of immut y &mutα T , here we freeze a mutable reference x, the translation of this gives assume { *y = ^y }; a . To preserve the simulation, the MiniMir configuration must reduce to a, with memory compatible with the heap. In sum, this means showing that the final value of x is the same as it's current value.

By the preservation of heap typing, we observe that when the borrow is frozen, the memory H x of x must be transferred back to the variable which was borrowed. To show that McFly * found the correct final value, we note that by inversion on McFly * , the prophecy for x must come from some future configuration C of C. We then use Lemma I.6 to show that the memory of C can be readout. Finally, since by typing frozen cells of memory cannot change by reduction, the readout of H x must be the same at C as it was at C. Since this value forms the prophecy for x, it must be the case the the current and final values of the borrow are equal and that the MiniML program can progress.

The proof is detailed more formally in Appendix I.

Experimentation

As further validation of the translation presented in Section 3, we implemented a proof-ofconcept tool as an extension to the Rust compiler. This tool takes Rust programs in their MIR representation and translates them to WhyML, the specification and programming language of the Why3 verification suite. The translated programs can then be checked using the Why3 prover interface. Using this tool we were able to verify simple programs working on structures such as linked lists.

One of the primary implementation challenges is determining where the thaw should be in MIR code. The borrow checker of Rust infers a position where it should be inserted but that information is hidden from other passes. Extracting that information is essential as the safety of this tool relies on correct placement of thaws to mark the end of lifetimes.

We also took advantage of this tool to test several simple extensions, such as support for preconditions, post-conditions and invariants in code being verified. Each of these is lowered, nearly directly to the equivalent Why3 constructs. This enabled us to verify the functional correctness of several programs. A few of these programs are included in Appendix K

Conclusion

During this internship, we developed a schema to verify Rust-like programs by translation to a functional language. Our source language MiniMir, is translated to MiniML, an ML-like language with non-determinism. In our translation we represent mutable borrows as pairs of their current and future values. To prove that our translation is correct, we developed an original simulation technique between an execution trace and a functional configuration. The proof requires us to show that we can predict the future values of each borrow, and we show that we can statically identify points in the program which can be used to predict those values. Finally, we validated this technique experimentally by implementing this translation as a proof-of-concept tool. Our tool was able to verify safety properties for simple programs using list operations.

Related Work. The Frama-C [START_REF] Kirchner | Frama-C: A software analysis perspective[END_REF] tool for C allows the verification of C in the presence of aliasing through non-aliasing hypotheses which assert pair-wise non-aliasing of variables. Asserting that all variables are non-aliasing requires quadratic amounts of hypotheses, which overwhelms automation like SMT solvers. Other languages like Spark/Ada rule out all aliasing through their type system. Recent work has been done on how to add aliasing references like in Rust [START_REF] Dross | Recursive Data Structures in SPARK[END_REF].

To verify Rust programs, the team behind Prusti [START_REF] Astrauskas | Leveraging Rust types for modular specification and verification[END_REF] translates programs to a separation logic with fractional permissions. Currently, their approach is limited in the properties it is able to prove and their implementation supports a more limited subset of Rust programs than the approach offered by MiniMir. Another approach is that of RustHorn [START_REF] Matsushita | RustHorn: CHC-based Verification for Rust Programs (full version)[END_REF], which translates programs to Constrained Horn Clauses using the same encoding of mutable references we use. RustHorn however cannot represent user specifications and can only show that programs don't fail assertions. Additionally, their approach of translating to CHCs means that they rely entirely on automated solvers with no method to allow human guidance.

Future Work. The approach presented in section 3 allows us to verify Rust-style programs using both mutable and immutable references. However, the proof of correctness is complex using an original form of simulation. Formalizing this development in Coq would give a much firmer base for further extensions to the language. The work on RustBelt [START_REF] Jung | RustBelt: Securing the foundations of the Rust programming language[END_REF], could serve a starting point for a Coq formalization, since key lemmas like type safety are already proven on the core language λRust. Currently, we have not considered the questions of specification languages for Rust, the encoding for datatype invariants and ghost code more generally remains an open question. To put this translation into application and incorporate extensions, the tool developed for this internship needs to be extended to more gracefully handle real-world Rust programs.

A Complete Type System of µMIR

Copy(int)

Copy(bool) Copy(unit)

Copy(T 0 ) Copy(T 1 )

Copy(T 0 × T 1 )
Copy(T 0 ) Copy(T 1 )

Copy(T 0 + T 1 ) Case (intro-pair) Recall that the reduction for introducing a pair is the following:

y : T ∈ Γ Copy(T ) (copy-val) Σ; Γ f x T := copy y T Γ, x : T y : box T ∈ Γ Copy(T ) (copy-ref) Σ; Γ f x T := copy *y P T Γ, x : T (unbox) Σ; y : box T, Γ f x T := unbox y box T Γ, x : T (box) Σ; y : T, Γ f x box T := box y T Γ, x : box T x : box T, y : box T ∈ Γ (swap) Σ; Γ f swap(x P T , y P T ) Γ T ∈ {int, unit} (drop)
Σ; x : T, Γ f drop x T Γ (intro-sum) Σ; y : T i , Γ f x T 0 +T 1 := inji y T Γ, x : T 0 + T 1 (intro-pair) Σ; y : T 0 , z : T 1 , Γ f x T 0 ×T 1 := (y T 0 , z T 1 ) Γ, x : T 0 × T 1 (const-intro) Σ; Γ f let x = C Γ, x : T C x : bool ∈ Γ (assert) Σ; Γ f assert x Γ (op) Σ; y : int, z : int, Γ f x T := y int op z int Γ, x : T op (elim-pair) Σ; z : T 0 × T 1 , Γ f let (x T 0 , y T 1 ) := z T 0 ×T 1 Γ, x : T 0 , y : T 1 fn g (x 0 : T 0 , ...x n-1 : T n-1 ) → T n ∈ Σ (call) Σ; x 0 : T 0 , .., x n-1 : T n-1 , Γ f let x = g(x0, .., xn -1) Γ, x : T n Σ; Ξ a f I Σ; Ξ (sequence) Σ; Ξ f,a I; goto Ξ a = {x : Σ retf } (return) Σ; Ξ a f,a return x where Σ ret f = {T n | fn g (x 0 : T 0 , ...x n-1 : T n-1 ) → T n = Σ(f )} Ξ a = x : T 0 + T 1 , Γ a Ξ i = y i : T i , Γ a i ∈ {0, 1} (match-val) Σ; Ξ f,a match x T 0 +T 1 { inj0 y0 T 0 → goto 0 , inj1 y1 T 1 → goto 1 } P f ; = assert x; goto ' H(F(x)) = true f ; | S | F | H → P | S | F | H P f ; = swap(x P T , y P T ); goto ' F(x) = a F(y) = b f ; | S | F | H → P f ; | S | F | ([H(a), H(a) + |T |) ∪ [H(b), H(b) + |T |)) -H +M H (H(a), H(b), |T |) + M H (H(b), H(a), |T |) P f ; = x := C; goto ' {a} ⊥ dom(H) f ; | S | F | H → P | S | F + {(x, a)} | H + {(a, C)} i = H(a) [b, b + |T i |) ⊥ dom(H) P f ; = match x T 0 +T 1 { inj0 y0 T 0 → goto 0 , inj1 y1 T 1 → goto 1 } f ; | S | F + {(x, a)} | H → P i | S | F + {(y i , b)} | [a, a + |T 0 + T 1 |) -H +M H (b, a + 1, |T i |) P f ; = x T 0 ×T 1 := (y T 0 , z T 1 ); goto ' [c, c + |T 0 | + |T 1 |) ⊥ dom(H) A = [a 0 , a 0 + |T 0 |) + [a 1 , a 1 + |T 1 |) f ; | S | F + {(y, a 0 ), (z, a 1 )} | H → P | S | F + {(x, c)} | A -H + M H (c, a 0 , |T 0 |) + M H (c + |T 0 |, a 1 , |T 1 |) P f ; = let (x T 0 , y T 1 ) := z T 0 ×T 1 ; goto ' A = [c, c + |T 0 | + |T 1 |) [a 0 , a 0 + |T 0 |) ⊥ [a 1 , a 1 + |T 1 |) ⊥ dom(H) f ; | S | F + {(z, c)} | H → P | S | F + {(x, a 0 ), (y, a 1 )} | A -H + M H (a 0 , c, |T 0 |) + M H (a 1 , c + |T 0 |, |T 1 |) P f ; = x T 0 +T 1 := inji y T ; goto ' s = max(|T 0 |, |T 1 |) A = [a, a + |T i |) [b, b + s + 1) ⊥ dom(H) f ; | S | F + {(y, a)} | H → P | S | F + {(x, b)} | A -H + (b, i) + M H (b + 1, a, s) P f ; = let x = g(x0, .., xn -1) f ; | S | F + {(y i , a i ) | i ∈ [n]} | H → P g | [ , x, F]; S | {(x i , a i ) | i ∈ [n]} | H P f ; = return x f ; | [ , t, F ]; S | F | H → P | S | F + {(y, F (
f ; | S | F ⊕{(y, a 0 ), (z, a 1 )} | H → P | S | F ⊕{(x, c)} | H where A = [a 0 , a 0 + n 0 ) ⊕ [a 1 , a 1 + n 1 ) H = A -H ⊕ M H (c, a 0 , n 0 ) ⊕ M H (c ⊕ n 0 , a 1 , n 1 )
By inversion on

∼ P , K = let x = (y,z) in a | E | K which reduces to K = a | E ⊕{x, (y, z)} | K .
We know that y and z both have a readback judgement. When we translate their memories to the cells of x, that readback will remain the same. Then it's simple produce a readback for R

(A -(H 1 ⊕ H 2 ) ⊕ M H (c, a 0 , n 0 ) ⊕ M H (c + n 0 , a 1 , n 1 ), c, T 1 × T 2 , (v 1 , v 2 )
). With this we can translate the memory of C to the environment of K , preserving the simulation.

Case (assert) When when we evaluate an assertion, assert x bool , we know that H(F(x)) = true. By hypothesis, we know that x can be translated to a µMIR value, which tells us that E(x) = true. From this we can easily see that the assertion must then also evaluate to true in µMIR. From this we preserve the simulation.

Case (swap) When we evaluate a swap, we produce from

C = [f ; ] | -| F | H a configuration who's heap is: A = [H(a), H(a) + |T |) ∪ [H(b), H(b) + |T |) H = A -H + M H (H(a), H(b), |T |) + M H (H(b), H(a), |T |)
All this amounts to is that the memories of x and y are each translated to the other's position. The readbacks will therefore swap as well. This corresponds to the translation of the swap which also swaps the two variables in µML, preserving the simulation.

The other cases work in the same manner, memory is translated between cells following the motion of data in and out of sum and product types. (drop) Σ; x : T, Γ; L f drop x T Γ; L (immut) Σ; x : &mutα T, Γ; L f immut x Γ, x : &α T ; L (intro-sum) Σ; y : T i , Γ; L f x T 0 +T 1 := inji y T Γ, x : T 1 + T 2 ; L (intro-pair) Σ; y : T 1 , z : T 2 , Γ; L f x T 0 ×T 1 := (y T 0 , z T 1 ) Γ, x : T 1 × T 2 ; L (const-intro) Σ; Γ; L f let x = C Γ, x : T C ; L x : bool ∈ Γ (assert) Σ; Γ; L f assert x Γ; L y : int, z : int ∈ Γ (op) Σ; Γ; L f x T := y int op z int Γ, x : T op ; L (elim-pair) Σ; z : T 1 × T 2 , Γ; L f let (x T 0 , y T 1 ) := z T 0 ×T 1 Γ, x : T 1 , y : T 2 ; L P ∈ {&mutα, &α} (elim-pair-ref) Σ; z : P (T 1 × T 2 ), Γ; L f let (ref x, ref y) = z Γ, x : P T 1 , y : P T 2 ; L ∀j, 0 ≤ j < l, β aj ≤ β bj ∈ L ∀i, 0 ≤ i < n + 1, T i = T i [α 0 /β 0 , .., α m-1 /β m-1 ] fn g α 0 , ..., α m-1 | α a0 ≤ α b0 , ..., α a l-1 ≤ α b l-1 (x 0 : T 0 , ...x n-1 : T n-1 ) → T n ∈ Σ (call) Σ; x 0 : T 0 , .., x n-1 : T n-1 , Γ; L f let x = g β0,..

E Complete Operational Semantics of µML

f e | E | K -→ f | E | arg e • K v | E | arg e • K -→ e | E | f un v • K v | E | f
..] • E | ret E • K v | E | ret E • K -→ (v, E) | E | K E(x) = (rec f x = e and ... and g y = e', E ) v | E | K -→ f st E(x) | [x → f st E(x)] • snd E(x) | K x | E | K -→ E(x) | E | K let x = e in e' | E | K -→ e | E | let x e • K v | E | let x e • K -→ e' | [x → (v, E)] • E | K let (x, y) = e in e' | E | K -→ e | E | unpair x y e • K (v0 , v1 ) | E | unpair x y e • K -→ e' | [x → (v 0 , E)] • [y → (v 1 , E)] • E | K match e with | inj0 x0 → e0 | inj1 x1 → e1 end | E | K -→ e | E | match x 0 e 0 x 1 e 1 • K inji v | E | match x 0 e 0 x 1 e 1 • K -→ ei | [x i → (v, E)] • E | K (e0 , e1 ) | E | K -→ e0 | E | f st e 1 • K v0 | E | f st e 1 • K -→ e1 | E | snd v 0 • K x, y ∈ dom(E) v1 | E | snd v 0 • K -→ (x, y) | [x → (v 1 , E)] • [y → (v 2 , E )] • E | K inji e | E | K -→ e | E | inj i • K v | E | inj i • K -→ inji v | E | K e0 op e1 | E | K -→ e 0 | E | lef top op e 1 • K v0 | E | lef top op e 1 • K -→ e 1 | E | rightop op v 0 • K op((v 0 , E), (v 1 , E )) = r v1 | E | rightop op v 0 • K -→ r | E | K assert { e } | E | K -→ e | E | assert • K true | E | assert • K -→ () | E | K e ; e' | E | K -→ e | E | seq e • K v | E | seq e • K -→ e' | E | K
Ξ i = y i : T i , Ξ a Λ i = Λ a i ∈ {0, 1} (match-val)
Σ; x : T 0 + T 1 , Ξ a ; Λ a f,a match x T 0 +T 1 { inj0 y T 0 0 → 0 inj1 y T

G Complete Operational Semantics of MiniMir

The semantics of µMIR are extended with the following rules:

voidFigure 1 :Figure 2 :

 12 Figure 1: Swap implemented with XOR which assumes arguments are non-aliased

Figure 3 :Figure 4 :

 34 Figure 3: Updating a box functionally

Figure 5 :

 5 Figure 5: Grammar of µMIR

0

  : t1 := 1; t2 := 2; t3 := ( t1 , t2 ); x := box t3 ; goto 4 4: t4 := unbox x ; ( t5 , t6 ) := t4 ; t7 := t6 + 1; goto 5; 5: t8 := ( t5 , t7 ); x := box t8 ; goto 9; 9: t9 := unbox x ; ( x1 , x2 ) := t9 ; goto 12 12: t10 := 3; t11 := x2 = t10 ; assert t11 ; goto 14 14: drop x2 ; drop t10 ; drop t11 ; goto 17 17: ret := (); return ret

Figure 6 :

 6 Figure 6: Figure 3 translated to µMIR

  Expression, e ::= 'let' x '=' e' 'in' e | e e' | x | v | e op e' | 'match' e 'with' '|' inj 0 x 0 '->' e '|' inj 1 x 1 '->' e 'end' | 'let' '(' x, y ')' = e | 'assert' '{' e '}' | '(' e ',' e ')' | inj i e | 'rec' FunDef 'and' ... 'and' FunDef FunDef ::= 'fun' f x ... x = Expr Values, v ::= '(' v ',' v ')' | inj i v | n | 'rec' FunDef 'and' ... 'and' FunDef 2.5.2 Translating from µMIR to µML

  let rec l0 () = let t1 = 1 in let t2 = 2 in let t3 = ( t1 , t2 ) in let x = box t3 in l4 x and l4 x = let t4 = x in let ( t5 , t6 ) = t4 in let t7 = t6 + 1 in l7 t5 t7 and l7 t5 t7 = let t8 = ( t5 , t7 ) in let x = t8 in l9 x and l9 x = let t9 = x in let ( x1 , x2 ) = t9 in l11 x1 x2 and l11 x1 x2 = let t10 = 3 in let t11 = ( x2 = t10 ) in assert { t11 }; l14 x1 t10 t11 and l14 x1 t10 t11 = let ret = () in ret

Figure 7 :

 7 Figure 7: The syntax of MiniMir as an extension of µMIR

1 :

 1 t1 := 0; t2 := & mutα t1 ; goto 3 3: t3 := * t2 ; t4 := t3 + 1; t5 := & mutα t4 ; swap ( t2 , t5 ); goto 7 7: immut t5 ; drop t5 ; goto 9 9: t6 := * t2 ; t7 := t6 + 1; t8 := & mutα t7 ; swap ( t2 , t8 ); goto 13 13: immut t8 ; drop t8 ; goto 15 15: immut t2 ; drop t2 ; thaw α; goto 17 17: t4 := t1 ; assert { t4 = 2 }; drop t4 ; t0 := (); drop t1 ; return t0

Figure 8 :

 8 Figure 8: Translation of Figure 4, with the function inc inlined.

  give m α (a, T ); ∅ |= a : †α T B; H |= a : †α T give i α (a, T ), B; H |= a : †α T B; H |= a : n T take m α (a, T ), B; {(p, a)} ⊕ H |= p : n &mutα T take i α (a, T ); {(p, a)} |= p : n &α T Definition 3.3. A well-typed configuration f ; | -| F | H of a well-typed program P if it satisfies the following conditions:

Figure 9 :

 9 Figure 9: Translation of Figure 8 to MiniML

:

  immut y &mutα T ; goto ' fun a = assume { *y = ^y }; a

  a)}, p, &α T, (p, T, v)) R n (B, A, {a} -H, H(a), T, E) A(H(a), T ) = v R n (take m α (a, T ) ∪ B, A, {(p, a)} ⊕ H, p, &mutα T, E + (a, T × T, (E(H(a)), v))) Definition 3.7 (HeapEnv). The relation HeapEnv shows how to construct an ML environment from a MiniMir configuration. It uses the heap types of a configuration to readback memory cells as ML values.

  x))} | H C Translation from µMIR to µML : x box T := box y T ; goto ' let x = y in a : x T := unbox y box T ; goto ' let x = y in a

  un rec f x = e and ... and g y = e' • K -→ e | [f → rec f x = e and ... and g y = e', .., g → .

F

  Complete Type System of MiniMir y : T ∈ Γ Copy(T ) (copy-val) Σ; Γ; L f x T := copy y T Γ, x : T ; L y : P T ∈ Γ P ∈ {&mutα, &α, box} Copy(T ) (copy-ref) Σ; Γ; L f x T := copy *y P T Γ, x : T ; L (unbox) Σ; y : box T, Γ; L f x T := unbox y box T Γ, x : T ; L (box) Σ; y : T, Γ; L f x box T := box y T Γ, x : box T ; L (borrow-mut) Σ; y : T, Γ; L f x &mutα T := &mutαy T Γ, x : &mutα T, y : †α T ; L P ∈ {box, &mut β } α ≤ β ∈ L (unnest) Σ; y : &mutα P T, Γ; L f x &mutα T := unnest y &mutαP T Γ, x : &mutα T ; L P ∈ {&mutα, box} x : P T, y : P T ∈ Γ (swap) Σ; Γ; L f swap(x P T , y P T ) Γ; L T ∈ {int, unit, &α}

  ,βm -1 (x0,.., xn -1) Γ, x :T n ; L (sub-lifetime) Σ; Γ; L f α ≤ β Γ; L, α ≤ β, L α ∈ Σ expf L = L \ {α ≤ β | ∀β, α ≤ β ∈ L} Γ = {thaw α (v) | v ∈ Γ} ∃β, β ≤ α ∈ L ∀ x : n T ∈ Γ , α ∈ lifetimes(T ) (thaw) Σ; Γ; L f thaw α Γ ; Lwhere Σ exp f is the set of lifetimes that survive the function f .

  thaw α (v) = x : T v = x : †α T v otherwise Σ; Ξ a ; Λ a f I Σ; Ξ ; Λ (sequence) Σ; Ξ; Λ f,a I; goto Ξ a = {x : Σ retf } (return) Σ; Ξ; Λ f,a return x where Σ ret f = {T n | fn g ... | ... (x 0 : T 0 , ...x n-1 : T n-1 ) → T n = Σ(f )}

1 1 → 1 } 1 → 1 }Ξ

 111 Ξ i = y i : P T i , Ξ a Λ i = Λ a i ∈ {0, 1} P ∈ {&mutα, &α} (match-ref) Σ; x : P (T 0 + T 1 ), Ξ a ; Λ a f,a match *x P T 0 +T 1 { inj0 ref y P T 0 0 → 0 inj1 ref y P T 1 = x i : T i Λ = {β aj ≤ β bj | ∀j, 0 ≤ j < l} ∀S ∈ ∆, Σ; Ξ f,a S fn f α 0 , .., α m-1 | α a0 ≤ α b0 , .., α a l-1 ≤ α b l-1 (x 0 : T 0 , .., x n-1 : T n-1 ) → T n (function) Σ, Ξ (∆, , σ) Σ = {σ | ∀(∆, , σ) ∈ P} ∀f ∈ P, Σ f (program) P

P

  f ; = immut y &mutα T ; goto ' (immut) | S | F | H → P | S | F | H P f ; = x &mutα T := &mutαy T ; goto ' F(y) = a b ∈ dom(H) (borrow-mut) | S | F | H → P | S | F + {(x, b)} | H + {(b, a)} P f ; = x &mutα T := unnest y &mutαP T ; goto ' b ∈ dom(H) (unnest) | S | F + {(y, a)} | H + {(a, p)} → P | S | F + {(x, b)} | H + {(b, H(p))} P f ; = match *x { .. } i = H(a) (match-ref) | S | F + {(x, a)} | H → P i | S | F + {(y i , H(a) + 1)} | HH Translation from MiniMir to µML : x T := copy *y P T ; goto ' let x = *y in a P ∈ {&α, &mutα} : x &mutα T := &mutαy T ; goto ' let x = (y , any ) in let y = ^x in a : x &mutα T := unnest y &mutαP T ; goto ' let x = (* *y , *^y) in assume { ^*y = ^^y }; a P = &mut β : x &mutα T := unnest y &mutαP T ; goto ' let x = (*y , ^y ) in a P = box : immut y &mutα T ; goto ' assume { *y = ^y }; a : swap(x P T , y P T ); goto ' let t = *x in let x = (*y , ^x) in let y = (t, ^y) in a P = &mutαT let (y,x) = (x,y) in a otherwise : thaw α; goto ' () : α ≤ β; goto ' () : let (ref x P T 0 , ref y P T 1 ) := *z P (T 0 ×T 1 ) ; goto ' let (xn , yn ) = *z in let (xe , ye ) = ^z in let x = (xn , xe ) in let y = (yn , ye ) in a P = &mutα : let (ref x P T 0 , ref y P T 1 ) := *z P (T 0 ×T 1 ) ; goto ' let (x, y) = z match * x T { inj0 ref y0 P T 0 → 0 inj1 ref y1 P T 1 → 1 } begin match * x with | inj0 y0 → let y0 = (y0 , any ) in assume { ^x = inj0 ^y0 }; let x = ( inj0 ^y0 , ^x) in L0 | inj1 y1 → let y1 = (y1 , any ); assume { ^x = inj1 ^y1 }; let x = ( inj1 ^y1 , ^x) in L1 end })) , }; rev (& mut l1 ); let l2 = List { head : Some ( Box :: new ( Node { val : 10 , next : Some ( Box :: new ( Node { val : 1 , next : None })) , })) , }; assert_eq! ( l1 , l2 ); }

Reference to the famous slogan for a French cleaning product "Mini Mir, Mini Prix, mais il fait le maximum" reference needed

Ξ = x i : T i ∀S ∈ ∆, Σ; Ξ; ∆ f,a S (function) Σ, Ξ (∆, , fn g (x 0 : T 0 , ...x n-1 : T n-1 ) → T n ) Σ = {σ | ∀(∆, , σ) ∈ P} ∀f ∈ P, Σ f (program) P B Complete Operational Semantics of µMIR Definition B.1 (Notations). If F is a partial function, and A is a subset of its domain, then A -F denotes the domain restriction removing A from the domain of F , and is defined as

The operation A ⊕ B denotes the disjoint union of partial functions, it is only defined when dom(A) ∩ dom(B) = ∅. The notation a ⊥ b ( disjoint sets) signifies that a ∩ b = ∅. The notation a 0 ⊥ a 1 ⊥ .. ⊥ a n is used to denote the pairwise disjointness of the sets a 0 , .., a n . The notation M H (t, s, n) ( memory copy) is a shorthand for copying n cells of H starting at s to addresses starting at t. It is defined as The stack has the following form:

As the name implies, it represents the function calls currently being evaluated. Each element of the stack is a triple composed of a return label, a variable name for the result and a frame obtained from the caller at the moment the call is performed.

Proof of Lemma 2.6. The proof proceeds by case-analysis on the transition relation → P . Each case must shuffle memory around to show that the resulting configuration will readback in a manner which preserves the simulation.

I Proof of simulation preservation for MiniMir

Definition I.1 (Heap Fragment Type for MiniMir). The heap types of MiniMir extend the judgements of µMIR with a borrow store, checking that every borrow has a source and that they agree on typing.

Proof. The proof proceeds by case-analysis on the reductions of MiniMir. We will show several cases which illustrate preservation for owned data, mutable borrows and immutable borrows.

Case (intro-pair) Given a configuration C with code x T 0 ×T 1 := (y T 0 , z T 1 ), we know that that we must have B y ; H y |= a 0 : • T 1 , and B z ; H z |= a 1 : • T 2 . We from this we construct

It's immediately apparent that when we move the memories of y and z into the cells of H x , we obtain the desired heap typing.

Case (borrow-mut)

The reduction of C with code x &mutα T := &mutαy T , adds a new pointer x holding the address of y to H. By hypothesis we have B y ; H y |= a : • T . We need to produce two new judgements after evaluating this instruction, one for x : &mutα T and one for y : †α T . To preserve typing we add a pair of tokens give r α (a, T ), take r α (a, T ) to B. Using these tokens we can construct {give r α (a, T )}; ∅ |= a : †α T for y and {take r α (a,

Case (immut) By hypothesis we have {take r α (a, T )} ∪ B x ; {(p, a)} ⊕ H x |= p : • &mutα T . By the safety of B we know there must be {give r α (a, T )} ∪ B y ; H y |= a : †α T . By inversion, this judgement must contain the a subtree for {give r α (a, T )}; ∅ |= a : †α T . We must transform the judgement for x into one for an immutable reference. We do this by removing give r α (a, T ), take r α (a, T ) and inserting give i α (a, T ), take i α (a, T ) into the borrow store. As a result the ownership of H x Here we give the complete definition of the readback for MiniMir.

Definition I.3 (Readback).

The readback of a MiniMir heap constructs a map of address and type to MiniML value.

Lemma I.4 (Progress). Given a MiniMir trace C → * P C and a MiniML configuration K such that C → * P C ∼ P K, if K is not stuck then C is not stuck.

Lemma I.4. The proof proceeds by case analysis on the reductions of MiniML. In each step we exploit our hypothesis HeapEnv(F, H, Γ, E) to show that the MiniMir heap must be well-formed and allow reduction. In the case of assertions we note that for the MiniML assertion to evaluate to true, the readback requires the MiniMir heap to also hold true.

Lemma I.5 (Terminal Configurations). Given a terminal MiniML configuration K, for any

MiniMir trace Θ such that Θ ∼ P K, then Θ = C → P and C terminal.

Proof. The only terminal configurations for MiniML possible with the simulation are those in relation with return instructions inside the main function of the MiniMir program.

Proof. By induction over the type T we observe that when we perform a readback with a frozen activeness †α we will leave out subtrees of the active readback.

At the end of a trace we may still have active borrows (if the trace is stuck), to handle this situation, we perform a readback of each borrowed variable. During this readback we do not require the heap to be separated, which avoids the need for any prophecies by allowing cells to be reused in several readbacks. Proof. We find ourselves required to prove that for all variables in the frame of the initial configuration Θ 0 we have a readback. We prove this by induction on the type of the variable. Whenever we encounter a borrow, we must show that there is a prophecy in A for this borrow. By inversion on McFly, either there is a thaw for the lifetime of the borrow and we have a prophecy, or it is active until the end of the trace and we must also have a prophecy. Using this we can construct the readback for every variable and thus translate the heap to an environment.

Definition I.9 (Simulation Relation). The relation ∼ P between a well-typed MiniMir trace Θ and a Krivine configuration is defined by the following conditions:

The proof proceeds by case-analysis on the reduction C → P C . The cases related to owned data ((intro-pair), (constant)) proceed like in µMIR. The most interesting cases of this proof are those for creating and freezing a borrow.

Case (borrow-mut)

To preserve our simulation, we must ensure that the translated code reduces properly to the next label and that the resulting memories stay linked by HeapEnv.

Because we create a new borrow, to have a readback, we need a prophecy map which includes this new borrow. We get this by Lemma I.8, we know that there must be a prophecy for the borrowed variable.

Case (immut) As a reminder, the operational semantics tell us that the operation is a no-op. The translation of immut gives us

To preserve the simulation, the machine must reduce the assume, which means proving that *x = ^x.

Let F(x) = a, by inversion on the HeapEnv, we know that there is

. By the safety of B, there must be a variable y which consumes give m α (a, T ), by assigning y the memory H x in C , we can preserve the existence of the readback.

Let R †α (B y , H x , F(y), T, V y ,) be the readback of y in C . We know that (H(a), T x ) ∈ dom(V y ).

Let C be either the first configuration in Θ such that P f ; = thaw α or the last configuration of Θ. By applying Lemma I.8, we know that C must have a readback. Since (H(a), T x ) ∈ dom(V y ), by Lemma I.6, (H(a), T x ) must be included in the readback of y at C . This means that by inversion on the readback of C , there must be a R †α (B x , A , H x , H(a), T x , V x ).

Because we froze all the memory associated with H(a) at C, we know that B x ⊆ B x and H x ⊆ H x . By typing we know that B x can only have immutable give and take tokens. Since that means we control all the memory, H x = H x . Finally since A ⊆ A, it must be that V x = V x .

All of this allows us to conclude that

J Operational Semantics of MiniML

MiniML extends µML with the following continuations K ::= assume | ... and the following reductions.

assume


Philippe Guionneau
email: philippe.guionneau@icmcb.cnrs.fr

Mathieu Marchivie

Pr Guillaume Chastanet

Dr Philippe Hdr

Dr Mathieu Guionneau

Dr Marchivie

Guillaume Hdr

Chastanet

Multiscale approach of

come

Spin crossover (SCO) materials are often mentally associated with phenomena and potential applications that deal with magnetic bi-stability. This is mainly due to historical reasons that give a key role to the molecular magnetism scientific community, literally as the precursor community in highlighting, investigating and promoting this phenomenon [1]. Today, however, interest in this phenomenon goes far beyond this initial scientific community. Indeed, as much as the changes in magnetic and optical properties associated with this phenomenon are astounding and of exceptional richness, so many other aspects are now coming to the forefront, both fundamentally and in terms of practical applications [2]. For example, changes in the shape and size of materials, possibly in the form of crystals or composites, when undergoing SCO are of major interest because of their amplitude, diversity, controllability and the multiplicity of stimuli that can be used. The latter include thermo-, piezo-and photo-stimuli as well as any combination. Indeed, the change of mechanical properties in response to external stimuli in SCO crystals, including possible up to 10% volume reversible jumps [3,4], can lead to consider them as a family by their own into the attractive world of stimuli-responsive materials aside for instance well known diarylethene based molecular crystals [5] or thermo-salient crystals [6,7]. To date, actuators represent, indeed, one of the greatest opportunities for SCO solids [7,8].

The SCO is a phenomenon that corresponds to a modification of the electronic configuration in some metal ions due to at least one external stimulus. It is therefore, intrinsically, an atomic-scale phenomenon. However, as developed below, all the physical scales of the SCO solid account to truly master the diversity of the corresponding physical properties. This leads us to state the concept of a multiscale approach. To some extent, this mutiscale concept is reminiscent from the concept of reaction cavity in condensed matter that deals with the effects of the environment of a chemical specie on the solid properties [9]. For example, for iron(II) ions that are the most studied ones and on which the discussion below will therefore focus, SCO implies an interchange between the high-spin (HS) and the low-spin (LS) configurations. In this case, the HS to LS modification involves a paramagnetic/diamagnetic transition, inducing most of the time a change of color, and a drastic decrease of the iron to surrounding-atoms distances [4,10]. Depending on the compound, however, the SCO can be reversible, or not, and, interestingly, at the scale of the sample can lead to an incredible diversity of physical behaviors providing a rich panel of properties, sometimes even antagonists from one sample to another. The reason is that, spreading from the metal ion, the SCO propagates to all other physical scales, each of them reacting differently and each of them may or may not, depending on the solid in question, act on the others. Indeed, all scales of the material from the coordination polyhedron to the macroscopic object reflect in different ways, each with its own characteristics, the initial perturbation of the electronic configuration corresponding to the SCO. All the physical properties of the sample, or even of the device, are thus influenced by what happens at all levels of the material. To date, though the SCO phenomenon is thoroughly investigated, all the links between the atomic scale modifications and its macroscopic consequences are far to be understood since, very often, new data provide unexpected or non-anticipated behaviors [2,11]. The causal chains are still to be understood in a global picture. One key point to achieve the latter is to envisage a multiscale view.

The most spectacular and obvious multi-scale causal chain to observe and describe is probably that of structural changes. Firstly, because crystallography's characterization tools are very advanced and allow the investigation of a chosen physical scale. For example, in radiation diffraction, information on coherent domains, physical scale of the nm, can be obtained CONCEPT simultaneously on the same image (the same diffractogram) as that relating to the atomic environment of the metal ion (Å) or the parameters of the unit-cell (a few Å). This is obtained via different characteristics that are very weakly correlated such as, respectively, the width, the intensities and the positions of the Bragg peaks. Secondly, structural changes in SCO materials, especially those based on Fe(II) compounds, appear sometimes so huge in molecular crystals that they might challenge the very concept of solid when their reversible nature is taken into account leading to the notion of fatigability. Thus, over the last three decades of studies, the accumulation of structural data has made it possible to evidence the pathway at the different scales of modifications related to SCO, in all its diversity (Figure 1). Among them, the volume change can be taken as the narrative thread explaining the complexity of what happens in a crystalline solid subject to SCO. In this regard, it is necessary to be sharp on the vocabulary, which was not always the case in the initial studies reported in the literature that could have been a source of confusion. In particular, the term "volume", which is widely used in publications discussing SCO materials, deserves to be clarified. The volume modification of the coordination polyhedron due to the SCO (Vpoly) is the same whatever the compound and the material, it depends only on the type of metal ion and the atoms bonded to form the polyhedron [4]. For instance, for one iron(II) metal ion surrounded by six nitrogen atoms, the polyhedron volume modification at the SCO is always Vpoly = 3.0(3) Å 3 (from 13.0(3) Å 3 in HS to 10.0(2) Å 3 in LS). This corresponds to a decrease of 23 % when going from HS to LS by cooling, applying pressure or reverse light irradiation and an increase of 30 % when going from LS to HS by warming, negative pressure or light irradiation [10]. Note that for the sake of clarity we illustrate below values in the SCO sense from HS to LS. This spectacular volume change is then modulated at the scale of the molecule, which can reacts in very different ways including modifications of conformation and bond breaking for instance [10,11,12]. The volume variation on this scale appears extremely variable from one molecular complex to another but is very often between 0.5 and 5%, approximately [13]. The volume variation of the molecule is therefore very small compared to the variation of the polyhedron. This systematically implies a rearrangement of the ligands around the metal to compensate for the expansion of the coordination sphere that, again, offers a large panel of behaviors. Such a diversity is fascinating, involving, for example, changes in conformation [10, 12a], ligand rotations [14] and even bond breaks [8b, 9b]. Although the increase in volume at the molecule scale is relatively moderate, the rearrangement of the ligands has a significant impact at the higher scale, which leads, in most cases, to a significant expansion of the crystal lattice. The upper scale, the crystal lattice, is then also affected, to a greater or lesser extent depending on the flexibility of the molecular rearrangement. Sometimes it generates first order phase transition, ultimately symmetry breaking, and/or large modifications such as molecular shifts or chains rotations and/or twinning [3,[7][8][9][10][11][12][13][14][15][16]. The result is that the volume variation of the unit-cell is never as high as the initial -23 % of the polyhedron from HS to LS. Instead, the variation of the unit-cell size, Vunit-cell, appears quite commonly in the range between -2 and -5% [4,10] but can also, in rare cases, exceed -10% [3]. Note that it may be also almost null and even, as very recently highlighted, be in the opposite sense as shown by the Vunit-cell of +1.6% from HS to LS 2 reported in an iron(II) molecular crystal in relation with a rotation of ligand at the SCO [14]. The consequences of this change of volume at the upper scales, notably the coherent-domain one and the sample itself, are less documented in the literature. The investigation of the coherent domain, i.e. the space that contains strictly a unique periodic atomic packing, appears quite recent in the SCO field. The reported results indicate already very interesting features and indubitably add a degree to the complexity of the multiscale response to SCO [17]. Some results tend to show that the amplitude could be very similar to the unitcell one [3,17]. This is however probably very dependent on the sample, notably on its nature (single-crystal, powder, nanoparticules). The macroscopic volume change of the sample itself is also a data poorly documented, though some attempts by optical microscopy have been reported [18]. Many compounds studied evidenced a structural fatigability upon cycling them, as a result of all these mechanical strains spreading on all the physical scale of the material. Crystals can sometimes explode but, in some cases a strong mechanical resilience [19] or a thermal healing process have been observed [17b], illustrating that a generality is not a totality. Incidentally, recalling that the change in volume can be reversible by applying a stimulus that may or may not be of the same nature, one can appreciate how SCO crystals are very good candidates for shape memory materials.

The above example of the volume change therefore illustrates the multiscale aspect of SCO but one can imagine how much more complicated it is in reality given the number of parameters to be taken into account and the number of events that can take place. Note that this global concept goes far beyond the notion of cooperativity used in the literature as a key aspect to describe the SCO features but that is commonly only related to intermolecular interactions. The real description of the cooperativity of the SCO shall undoubtedly use this concept of multiscale approach to establish the future theoretical models. To help conceptualize a complete view, Figure 1 attempts to list the structural information to which each physical scale gives access in order to have a fairly complete description of this phenomenon. Each scale tends to adapt its features to the initial effect of the change in the electronic coordination of the metal by accommodating the change generated at the lower physical scale. Finally, this interconnection of behaviour between different physical scales is quite common within a solid, especially molecular, but what makes it both rich and more specific in the case of SCO is the reciprocal nature of influences between scales. Indeed, if, as we have seen, information about change due to SCO spreads from the smallest to the largest scale, carrying with it its share of modifications, a structural feature at a given scale can also have an influence on smaller scales. For example, the fine description of the distortion of the cation polyhedron at the SCO that is easily accessible by variable temperature structural investigation [20] and is known to be crucial for the photo-induced physical properties [21], can be influenced by upper scales, even the crystal packing one. This is largely documented by the comparison of true polymorphs that, by definition, only differ from their crystal packing and can show very different polyhedron distortions at the SCO. Polymorphism that represents a great chance in the study of SCO materials are very often used to indeed highlight scale effects [22]. It could be argued that the causality between differences in distortions and crystal-packings is close to the chicken-and-egg problem, but . other facts abound in the direction of the influence of the upper scales on the lower ones. For example, the particle size reduction by grinding involves significant modifications to smaller physical sizes resulting in the alteration of the SCO features [23]. Even more impressively, the morphological characteristics of the macroscopic crystalline sample could decide the start of the SCO at the atomic scales [24].

The concept of multiscale in SCO can be imaged by a domino effect blended to a Russian dolls architecture. The domino effect is a chain reaction that occurs when a change causes an identical change in close proximity, which will cause another similar change, and so on. The domino effect refers to the spin conversion reaction chain from one metal site to another driven by the first ions that undergo a transition. The analogy of Russian dolls, can be used to account for all the physical scales. Indeed, the investigation of any one of them cannot give a complete picture and is insufficient to explain the modification of the physical properties of the sample in the SCO, one view hiding the other one like one of the Russian doll hides the smaller ones. Note that the Russian dolls analogy gives only a partial picture because in reality each scale may influence the others. Therefore if this image of the multi-scale SCO concept is probably a matter of popularizing science, it also conveys for specialists the message that all events and characteristics related to each of the physical scales must be taken into account. This appears crucial not only for a fundamental understanding but also for any development of a reliable application using SCO. Conceptual view of all scales playing a crucial and complex role on the spin-crossover (SCO) process into a material. From the atomic ion and its polyhedron to the device, each scale reacts and provide significant changes, with or without links to others. The useful structural data that can be retrieved from each scale notably through crystallography analysis are emphasized here, which includes modifications due to SCO. The structure-property pattern is clearly reciprocal at each scale since structural properties depends on the SCO features but SCO features can also depend on concerned structural properties, the whole defining a Russian dolls domino effect.

Figure 1 .

 1 Figure 1.Conceptual view of all scales playing a crucial and complex role on the spin-crossover (SCO) process into a material. From the atomic ion and its polyhedron to the device, each scale reacts and provide significant changes, with or without links to others. The useful structural data that can be retrieved from each scale notably through crystallography analysis are emphasized here, which includes modifications due to SCO. The structure-property pattern is clearly reciprocal at each scale since structural properties depends on the SCO features but SCO features can also depend on concerned structural properties, the whole defining a Russian dolls domino effect.

Although of purely atomic origin, the Spin CrossOver spreads like a cascade of dominoes to all the dimensions of a material which fit together like Russian dolls with not only extremely different effects in nature and in amplitude but also with a mutual inter dependence. The multi-scale description is then the only way to understand the whole impact of a SCO on a material, incidentally showing the power of the crystallography approach. This concept could be extended to many other molecular phenomena.

Keywords: spin crossover • volume • physical scale • cooperativity • mechanism


V Bulanin
email: v.bulanin@spbstu.ru

E Gusakov

V Gusev

C Lechte

S Heuraux

V Minaev

A Petrov

Yu Petrov

A Yashin

N Sakharov

N Teplova

G Zadvitskiy

Full Wave Modeling of Doppler Backscattering from Filaments

Modeling of Doppler backscattering from filaments was carried out using finite-difference time-domain code IPF-FD3D in slab geometry. In the simulation artificial filament-like perturbations were used, the parameters of which varied over a wide range. Modeling DBS signal was focused on the identification of the influence of the amplitude of the filament and its size on the DBS.first,

It is recognized that the filaments have a significant effect on the anomalous energy and particle transport in the tokamak periphery [1,2]. They are actively investigated using various diagnostics in this regard. Recently three studies of filaments using the Doppler backscattering (DBS) method have been performed in Globus-M [3,4] and ASDEX-Upgrade [START_REF] Hennequin | 44th EPS Conference on Plasma Physics[END_REF][START_REF] Trier | 45th EPS Conference on Plasma Physics[END_REF]. The results of backscattering from filaments can be easily interpreted within the framework of the linear backscattering or Born approximation. However, the description of the experimental data under the transition from linear to non-linear backscattering is a rather complicated task that could be solved with the help of full-wave simulations.

Our simulation was carried out using finitedifference time-domain 2D code IPF-FD3D in slab geometry [START_REF] Lechte | [END_REF]. We did not resort to using well-known non-linear MHD codes to determine filament parameters. In the simulation artificially created filament-like perturbations were used, the parameters of which varied over a wide range. Modeling DBS signal was focused on the identification of the influence of the amplitude of the filament and its size on the shape and size of the DBS output signal. The filament amplitudes with a Gaussian cross-section were varied from 0.1% upto 150% of density at cut off of the probing wave. The parameters of the computations are as following: antenna tilt angle α = 13°, antenna horn mouth 5,5 cm, Computations have been carried out for the frequencies 16GHz, 24 GHz, 32GHz, 40GHz, 48GHz, 56GHz, 64GHz of O-mode propagation. Gaussian beam with flat wave front in the antenna mouth. This dependency of the IQ (in-phase (I) and The most interesting result relates to the case when the filament with a diameter of π/2ki·sinα moves along the cutoff (See Fig. 1) (Here: ki is free space wave number of probing beam). Remarcable that with an increase in the filament amplitude from 0.1% to 100% of the critical density, the signals of the IQ detector retain approximately the same with the waveform and duration of bursts of quasi-coherent fluctuations (BQFs). Figure 2 shows an example of the simulation for the both linear and non-linear cases. The result obtained indicates that even with strongly nonlinear scattering, the response of the IQ detector is represented as BQF. It is important that similar bursts were observed on both tokamaks, despite the possible significant difference in the amplitude of the filaments. [1][2][3][4].While maintaining the shape similarity, the amplitude of the signals nonlinearly increases with filament amplitude increasing. As soon as the signal amplitude is usualy measured in experiment in arbitrary units it is not possible to determine the real degree of nonlinearity of the process of Doppler bacscattering from filaments.

Figure 2 .

 2 Figure 2. 1.5cm circular filament. (a) Calculated Q(t) signals for linear (blue), and nonlinear(red), regimes; (b) normalized calculated signals;

Proceedings of the International Conference on Advances and Applications in Plasma Physics (AAPP 2019) AIP Conf. Proc. 2179, 020003-1-020003-2; https://doi.org/10.1063/1.5135476 Published by AIP Publishing. 978-0-7354-1926-1/$30.00


K Crombé

A Kostic

A Nikiforov

I Shesterikov

M Usoltceva

H Faugel

H Fünfgelder

S Heuraux

R Ochoukov

J-M Noterdaeme

Ishtar Team

Plasma operation and electric field measurements in IShTAR

The overall goal of the IShTAR (Ion cyclotron Sheath Test ARrangement) project is to study antenna near-fields in the presence of a plasma and magnetic field to assess theoretical predictions on radio frequency (RF) sheaths and to guide theoretical modelling [START_REF] Crombé | IShTAR: a helicon plasma source to characterize the interactions between ICRF and plasma[END_REF][START_REF] Crombé | [END_REF][START_REF] Crombé | A Test Facility to Investigate Sheath Effects During Ion Cyclotron Resonance Heating[END_REF]. For Ion Cyclotron Radio Frequency (ICRF) antenna applications it is favourable to operate at tokamak edge-like conditions for density and temperature. A helicon antenna at a frequency of 11.76

MHz and with power up to 3kW, is used to create argon or helium plasmas in IShTAR. Technicalities and capabilities of the IShTAR device have been described in [START_REF] Crombé | IShTAR: a helicon plasma source to characterize the interactions between ICRF and plasma[END_REF][START_REF] Crombé | A Test Facility to Investigate Sheath Effects During Ion Cyclotron Resonance Heating[END_REF]. Plasmas have now been characterised in a systematic way in order to obtain reproducible density profiles.

IShTAR plasmas operations

An extensive exploration of the discharge parameters (such as the neutral gas pressure, the gas type, the helicon antenna power and the magnetic field topology) has been performed [START_REF] Shesterikov | IShTAR: a test facility to study the interaction between RF wave and edge plasmas[END_REF]. A selection of resulting radial density profiles is presented in figure 1. They have been obtained by an array of Langmuir probes and crossed checked with measurements from an interferometer.

A number of techniques have been developed to adapt the traditional single Langmuir probe for measurements in RF discharges [START_REF] Shesterikov | IShTAR: a test facility to study the interaction between RF wave and edge plasmas[END_REF]5]. The profiles have been documented in a database, which can be directly used for future operations. It has been found that a high edge plasma density in front of the ICRF antenna can be obtained if the magnetic topology is optimised by adapting the currents in the coils surrounding the main chamber and plasma source, denoted as I big and I source respectively. The basic observation is that for high magnetic fields in the main chamber, corresponding to high values of I big , also high fields in the plasma source are required, as can be seen in the three plots in figure 1. The resulting magnetic topology then expands the plasma profile and increases the edge plasma density.

For the RF sheath studies the behaviour of the slow wave is of particular interest. The slow wave perpendicular component of the refraction coefficient in a magnetised argon plasma for an antenna spectrum with k = 10 m -1 is shown in figure 2. Results are based on radial plasma density profiles as presented in fig. 1. Each column corresponds to a fixed value of I big . The wave frequency is 6 MHz, routinely used in IShTAR. The sharp transition of N 2 ⊥ for slow waves from the red to the blue region corresponds to the position of the Lower Hybrid (LH) resonance. These results suggest that the optimum condition to shift the resonance layer in the direct vicinity of the ICRF antenna launcher would be I big > 3000 A and I source > 500A.

Electric field measurements

Furthermore, progress was made for electric (E) field measurements using passive optical emission spectroscopy. An ANDOR monochromator "Shamrock 750", with a focal length of approximately 738 mm and aperture of f/9.7 is used, in combination with an ANDOR intensifier camera from the series "IStar 334T", which provides high resolution and high sensitivity as well as fast acquisition rates. The monochromator, in a Czerny-Turner optical mount, is equipped with three interchangeable gratings: (i) a 600 l/mm grating with blaze angle at 500 nm; (ii) a 2400 l/mm, holographic grating optimised for the range 190-800 nm; and (iii) a grating with line density of 3600 l/mm, also holographic and optimised for 180-500 nm. A new gas injection system has been implemented, which allows for a local gas puff of helium in the vicinity of the ICRF antenna in order to increase the emission intensity of the spectral lines at the location of the sheath. Indeed, with the local injection of helium, argon can be chosen as main operating gas. It was found previously that argon plasmas in IShTAR have densities typically about ten times higher than in pure helium. A schematic of the system is depicted in figure 3. For high Efields (above 1 kV/cm) Stark effects can be observed on the helium spectra as they are resolved by the IShTAR spectroscopic system. Typically He I at 474.1 nm (4 3 D -2 3 P) is selected. A line shift up to 0.002 nm was measured at the metal walls of the antenna box, corresponding to an E-field of 2.56 kV/cm. More details on the E-field measurements are presented in various publications [START_REF] Kostic | Feasibility study of Passive Optical Emission Spectroscopy for the electric field measurements in IShTAR[END_REF]8,[START_REF] Kostic | Direct local electric field measurements in the sheaths of ICRF antenna in IShTAR[END_REF]. Recently a fibre bundle has been installed to complement the single fibre observation point, with the aim to resolve the E-field evolution inside the sheath. The array focuses 7 fibres onto a 1 cm spot at the edge of the ICRF antenna. The fibres are stacked on top of each other at the entrance slit of the high-resolution spectrometer. The fibre array will give information on the evolution of the electric field in the direct vicinity of the antenna box and inside the sheath [START_REF] Kostic | Polarization Stark spectroscopy for spatially resolved measurements of electric fields in the sheaths of ICRF antenna[END_REF].

Conclusions

IShTAR is a suitable environment to study RF sheaths and develop diagnostics. Interferometer and probes have been used for an improved characterisation of the operation of IShTAR. A sensitivity to the magnetic topology has been observed. Density profiles can be tailored to bring the lower hybrid resonance layer close to the ICRF launcher. In that way optimal condition for sheath studies are created. Successful electric field measurements by passive optical emission spectroscopy have been obtained close to the antenna box. The signal to noise ratio was improved by installing a local gas-puff for helium at the antenna view-point. The installation of a fibre bundle has been completed, it will allow for sheath resolved E-field profiles [START_REF] Kostic | Polarization Stark spectroscopy for spatially resolved measurements of electric fields in the sheaths of ICRF antenna[END_REF]. Future plans also include a feasibility study for active Doppler-Free Saturation Spectroscopy in the IShTAR device [START_REF] Martin | Electric field measurements of the capacitively coupled magnetized RF sheath utilizing passive optical emission spectroscopy[END_REF][START_REF] Martin | [END_REF].

Figure 1 :

 1 Figure 1: Radial plasma density profiles for various currents in the coils surrounding the main chamber (I big ) and plasma source (I source ). The radial position of the ICRF antenna is specified by a vertical green line.

Figure 2 :

 2 Figure 2: Perpendicular component of the refraction coefficients for the slow wave in a magnetised Ar plasma for k = 10 m -1 , a frequency of 6 MHz and typical IShTAR density profiles as presented in fig. 1.

Figure 3 :

 3 Figure 3: Set-up of the passive optical emission spectroscopy system and measured He I spectral line at 474.1 nm.

  46 th EPS Conference on Plasma Physics P1.1014

th EPS Conference on Plasma Physics P1.1014