## Variations on Semantics of Programming Languages

This example provides solutions to exercises proposed by Olivier Danvy. It proposes several variations around different ways of defining the semantics of a language. It is presented in the paper Formalizing semantics with an automatic program verifier.

Auteurs: Claude Marché / Martin Clochard

Catégories: Semantics of languages / Inductive predicates

Outils: Why3

see also the index (by topic, by tool, by reference, by year)

# Defunctionalization

This is inspired from student exercises proposed by Olivier Danvy at the JFLA 2014 conference

## Simple Arithmetic Expressions

```module Expr

use export int.Int

```

Grammar of expressions

```n  :  int

e  :  expression
e ::= n | e - e

p  :  program
p ::= e
```

```type expr = Cte int | Sub expr expr

type prog = expr

```

Examples:

```p0 = 0
p1 = 10 - 6
p2 = (10 - 6) - (7 - 2)
p3 = (7 - 2) - (10 - 6)
p4 = 10 - (2 - 3)
```

```let constant p0 : prog = Cte 0

let constant p1 : prog = Sub (Cte 10) (Cte 6)

let constant p2 : prog = Sub (Sub (Cte 10) (Cte 6)) (Sub (Cte 7) (Cte 2))

let constant p3 : prog = Sub (Sub (Cte 7) (Cte 2)) (Sub (Cte 10) (Cte 6))

let constant p4 : prog = Sub (Cte 10) (Sub (Cte 2) (Cte 3))

end

```

## Direct Semantics

```module DirectSem

use Expr

```

Values:

```v  :  value
v ::= n
```
Expressible Values:
```ve  :  expressible_value
ve ::= v
```
Interpretation:
```------
n => n

e1 => n1   e2 => n2   n1 - n2 = n3
----------------------------------
e1 - e2 => n3
```
A program e is interpreted into a value n if judgement
```  e => n
```
holds.

#### Exercise 0.0

Program the interpreter above and test it on the examples.

```  eval_0 : expression -> expressible_value
interpret_0 : program -> expressible_value
```

```(* Note: Why3 definitions introduced by "function" belong to the logic
part of Why3 language *)

let rec function eval_0 (e:expr) : int =
match e with
| Cte n -> n
| Sub e1 e2 -> eval_0 e1 - eval_0 e2
end

let function interpret_0 (p:prog) : int = eval_0 p

```

Tests, can be replayed using

```  why3 defunctionalization.mlw --exec DirectSem.test
```
(Why3 version at least 0.82 required)

```let test () =
interpret_0 p0,
interpret_0 p1,
interpret_0 p2,
interpret_0 p3,
interpret_0 p4

constant v3 : int = eval_0 p3

goal eval_p3 : v3 = 1

end

```

## CPS: Continuation Passing Style

```module CPS

use Expr

```

#### Exercise 0.1

CPS-transform (call by value, left to right) the function `eval_0`, and call it from the main interpreter with the identity function as initial continuation

```      eval_1 : expression -> (expressible_value -> 'a) -> 'a
interpret_1 : program -> expressible_value
```

```use DirectSem

let rec eval_1 (e:expr) (k: int->'a) : 'a
variant { e }
ensures { result = k (eval_0 e) }
= match e with
| Cte n -> k n
| Sub e1 e2 ->
eval_1 e1 (fun v1 -> eval_1 e2 (fun v2 -> k (v1 - v2)))
end

let interpret_1 (p : prog) : int
ensures { result = eval_0 p }
= eval_1 p (fun n -> n)

end

```

## Defunctionalization

```module Defunctionalization

use Expr
use DirectSem

```

#### Exercise 0.2

De-functionalize the continuation of `eval_1`.

```         cont ::= ...

continue_2 : cont -> value -> value
eval_2 : expression -> cont -> value
interpret_2 : program -> value
```
The data type `cont` represents the grammar of contexts.

The two mutually recursive functions `eval_2` and `continue_2` implement an abstract machine, that is a state transition system.

```type cont = A1 expr cont | A2 int cont | I

```

One would want to write in Why:

```function eval_cont (c:cont) (v:int) : int =
match c with
| A1 e2 k ->
let v2 = eval_0 e2 in
eval_cont (A2 v k) v2
| A2 v1 k -> eval_cont k (v1 - v)
| I -> v
end
```
But since the recursion is not structural, Why3 kernel rejects it (definitions in the logic part of the language must be total)

We replace that with a relational definition, an inductive one.

```inductive eval_cont cont int int =
| a1 :
forall e2:expr, k:cont, v:int, r:int.
eval_cont (A2 v k) (eval_0 e2) r -> eval_cont (A1 e2 k) v r
| a2 :
forall v1:int, k:cont, v:int, r:int.
eval_cont k (v1 - v) r -> eval_cont (A2 v1 k) v r
| a3 :
forall v:int. eval_cont I v v

```

Some functions to serve as measures for the termination proof

```function size_e (e:expr) : int =
match e with
| Cte _ -> 1
| Sub e1 e2 -> 3 + size_e e1 + size_e e2
end

lemma size_e_pos: forall e: expr. size_e e >= 1

function size_c (c:cont) : int =
match c with
| I -> 0
| A1 e2 k -> 2 + size_e e2 + size_c k
| A2 _ k -> 1 + size_c k
end

lemma size_c_pos: forall c: cont. size_c c >= 0

```

WhyML programs (declared with `let` instead of `function`), mutually recursive, resulting from de-functionalization

```let rec continue_2 (c:cont) (v:int) : int
variant { size_c c }
ensures { eval_cont c v result }
=
match c with
| A1 e2 k -> eval_2 e2 (A2 v k)
| A2 v1 k -> continue_2 k (v1 - v)
| I -> v
end

with eval_2 (e:expr) (c:cont) : int
variant { size_c c + size_e e }
ensures { eval_cont c (eval_0 e) result }
=
match e with
| Cte n -> continue_2 c n
| Sub e1 e2 -> eval_2 e1 (A1 e2 c)
end

```

The interpreter. The post-condition specifies that this program computes the same thing as `eval_0`

```let interpret_2 (p:prog) : int
ensures { result = eval_0 p }
= eval_2 p I

let test () =
interpret_2 p0,
interpret_2 p1,
interpret_2 p2,
interpret_2 p3,
interpret_2 p4

end

```

## Defunctionalization with an algebraic variant

```module Defunctionalization2

use Expr
use DirectSem

```

#### Exercise 0.2

De-functionalize the continuation of `eval_1`.

```         cont ::= ...

continue_2 : cont -> value -> value
eval_2 : expression -> cont -> value
interpret_2 : program -> value
```
The data type `cont` represents the grammar of contexts.

The two mutually recursive functions `eval_2` and `continue_2` implement an abstract machine, that is a state transition system.

```type cont = A1 expr cont | A2 int cont | I

```

One would want to write in Why:

```function eval_cont (c:cont) (v:int) : int =
match c with
| A1 e2 k ->
let v2 = eval_0 e2 in
eval_cont (A2 v k) v2
| A2 v1 k -> eval_cont k (v1 - v)
| I -> v
end
```
But since the recursion is not structural, Why3 kernel rejects it (definitions in the logic part of the language must be total)

We replace that with a relational definition, an inductive one.

```inductive eval_cont cont int int =
| a1 :
forall e2:expr, k:cont, v:int, r:int.
eval_cont (A2 v k) (eval_0 e2) r -> eval_cont (A1 e2 k) v r
| a2 :
forall v1:int, k:cont, v:int, r:int.
eval_cont k (v1 - v) r -> eval_cont (A2 v1 k) v r
| a3 :
forall v:int. eval_cont I v v

```

Peano naturals to serve as the measure for the termination proof

```type nat = S nat | O

function size_e (e:expr) (acc:nat) : nat =
match e with
| Cte _ -> S acc
| Sub e1 e2 -> S (size_e e1 (S (size_e e2 (S acc))))
end

function size_c (c:cont) (acc:nat) : nat =
match c with
| I -> acc
| A1 e2 k -> S (size_e e2 (S (size_c k acc)))
| A2 _ k -> S (size_c k acc)
end

```

WhyML programs (declared with `let` instead of `function`), mutually recursive, resulting from de-functionalization

```let rec continue_2 (c:cont) (v:int) : int
variant { size_c c O }
ensures { eval_cont c v result }
=
match c with
| A1 e2 k -> eval_2 e2 (A2 v k)
| A2 v1 k -> continue_2 k (v1 - v)
| I -> v
end

with eval_2 (e:expr) (c:cont) : int
variant { size_e e (size_c c O) }
ensures { eval_cont c (eval_0 e) result }
=
match e with
| Cte n -> continue_2 c n
| Sub e1 e2 -> eval_2 e1 (A1 e2 c)
end

```

The interpreter. The post-condition specifies that this program computes the same thing as `eval_0`

```let interpret_2 (p:prog) : int
ensures { result = eval_0 p }
= eval_2 p I

let test () =
interpret_2 p0,
interpret_2 p1,
interpret_2 p2,
interpret_2 p3,
interpret_2 p4

end

```

## Semantics with errors

```module SemWithError

use Expr

```

Errors:

```s  :  error
```
Expressible values:
```ve  :  expressible_value
ve ::= v | s
```

```type value = Vnum int | Underflow
(* in (Vnum n), n should always be >= 0 *)

```

Interpretation:

```------
n => n

e1 => s
------------
e1 - e2 => s

e1 => n1   e2 => s
------------------
e1 - e2 => s

e1 => n1   e2 => n2   n1 < n2
-----------------------------
e1 - e2 => "underflow"

e1 => n1   e2 => n2   n1 >= n2   n1 - n2 = n3
---------------------------------------------
e1 - e2 => n3
```
We interpret the program `e` into value `n` if the judgement
```  e => n
```
holds, and into error `s` if the judgement
```  e => s
```
holds.

#### Exercise 1.0

Program the interpreter above and test it on the examples.

```  eval_0 : expr -> expressible_value
interpret_0 : program -> expressible_value
```

```function eval_0 (e:expr) : value =
match e with
| Cte n -> if n >= 0 then Vnum n else Underflow
| Sub e1 e2 ->
match eval_0 e1 with
| Underflow -> Underflow
| Vnum v1 ->
match eval_0 e2 with
| Underflow -> Underflow
| Vnum v2 ->
if v1 >= v2 then Vnum (v1 - v2) else Underflow
end
end
end

function interpret_0 (p:prog) : value = eval_0 p

```

#### Exercise 1.1

CPS-transform (call by value, from left to right) the function `eval_0`, call it from the main interpreter with the identity function as initial continuation.

```      eval_1 : expr -> (expressible_value -> 'a) -> 'a
interpret_1 : program -> expressible_value
```

```function eval_1 (e:expr) (k:value -> 'a) : 'a =
match e with
| Cte n -> k (if n >= 0 then Vnum n else Underflow)
| Sub e1 e2 ->
eval_1 e1 (fun v1 ->
match v1 with
| Underflow -> k Underflow
| Vnum v1 ->
eval_1 e2 (fun v2 ->
match v2 with
| Underflow -> k Underflow
| Vnum v2 -> k (if v1 >= v2 then Vnum (v1 - v2) else Underflow)
end)
end)
end

function interpret_1 (p : prog) : value = eval_1 p (fun n ->  n)

lemma cps_correct_expr:
forall e: expr. forall k:value -> 'a. eval_1 e k = k (eval_0 e)

lemma cps_correct: forall p. interpret_1 p = interpret_0 p

```

#### Exercise 1.2

Divide the continuation

```    expressible_value -> 'a
```
in two:
```    (value -> 'a) * (error -> 'a)
```
and adapt `eval_1` and `interpret_1` as
```       eval_2 : expr -> (value -> 'a) -> (error -> 'a) -> 'a
interpret_2 : program -> expressible_value
```

```(*
function eval_2 (e:expr) (k:int -> 'a) (kerr: unit -> 'a) : 'a =
match e with
| Cte n -> if n >= 0 then k n else kerr ()
| Sub e1 e2 ->
eval_2 e1 (fun v1 ->
eval_2 e2 (fun v2 ->
if v1 >= v2 then k (v1 - v2) else kerr ())
kerr) kerr
end
*)

function eval_2 (e:expr) (k:int -> 'a) (kerr: unit -> 'a) : 'a =
match e with
| Cte n -> if n >= 0 then k n else kerr ()
| Sub e1 e2 ->
eval_2 e1 (eval_2a e2 k kerr) kerr
end

with eval_2a (e2:expr) (k:int -> 'a) (kerr : unit -> 'a) : int -> 'a =
(fun v1 ->  eval_2 e2 (eval_2b v1 k kerr) kerr)

with eval_2b (v1:int) (k:int -> 'a) (kerr : unit -> 'a) : int -> 'a =
(fun v2 ->  if v1 >= v2 then k (v1 - v2) else kerr ())

function interpret_2 (p : prog) : value =
eval_2 p (fun n ->  Vnum n) (fun _ ->  Underflow)

lemma cps2_correct_expr_aux:
forall k: int -> 'a, e1 e2, kerr: unit -> 'a.
eval_2 (Sub e1 e2) k kerr = eval_2 e1 (eval_2a e2 k kerr) kerr

lemma cps2_correct_expr:
forall e, kerr: unit->'a, k:int -> 'a. eval_2 e k kerr =
match eval_0 e with Vnum n -> k n | Underflow -> kerr () end

lemma cps2_correct: forall p. interpret_2 p = interpret_0 p

```

#### Exercise 1.3

Specialize the codomain of the continuations and of the evaluation function so that it is not polymorphic anymore but is `expressible_value`, and then short-circuit the second continuation to stop in case of error

```       eval_3 : expr -> (value -> expressible_value) -> expressible_value
interpret_3 : program -> expressible_value
```
NB: Now there is only one continuation and it is applied only in absence of error.

```function eval_3 (e:expr) (k:int -> value) : value =
match e with
| Cte n -> if n >= 0 then k n else Underflow
| Sub e1 e2 ->
eval_3 e1 (eval_3a e2 k)
end

with eval_3a (e2:expr) (k:int -> value) : int -> value =
(fun v1 ->  eval_3 e2 (eval_3b v1 k))

with eval_3b (v1:int) (k:int -> value) : int -> value =
(fun v2 ->  if v1 >= v2 then k (v1 - v2) else Underflow)

function interpret_3 (p : prog) : value = eval_3 p (fun n ->  Vnum n)

let rec lemma cps3_correct_expr (e:expr) : unit
variant { e }
ensures { forall k. eval_3 e k =
match eval_0 e with Vnum n -> k n | Underflow -> Underflow end }
= match e with
| Cte _ -> ()
| Sub e1 e2 ->
cps3_correct_expr e1;
cps3_correct_expr e2;
assert {forall k. eval_3 e k = eval_3 e1 (eval_3a e2 k) }
end

lemma cps3_correct: forall p. interpret_3 p = interpret_0 p

```

#### Exercise 1.4

De-functionalize the continuation of `eval_3`.

```         cont ::= ...

continue_4 : cont -> value -> expressible_value
eval_4 : expr -> cont -> expressible_value
interprete_4 : program -> expressible_value
```
The data type `cont` represents the grammar of contexts. (NB. has it changed w.r.t to previous exercise?)

The two mutually recursive functions `eval_4` and `continue_4` implement an abstract machine, that is a transition system that stops immediately in case of error, or and the end of computation.

```type cont = I | A expr cont | B int cont

end
</pre></blockquote>}
But since the recursion is not structural, Why3 kernel rejects it
(definitions in the logic part of the language must be total)
```

One would want to write in Why:

```function eval_cont (c:cont) (v:value) : value =
match v with
| Underflow -> Underflow
| Vnum v ->
match c with
| A e2 k -> eval_cont (B (Vnum v) k) (eval_0 e2)
| B v1 k -> eval_cont k (if v1 >= v then Vnum (v1 - v) else Underflow)
| I -> Vnum v (* v >= 0 by construction
```
```We replace that with a relational definition, an inductive one.

*)

inductive eval_cont cont value value =
| underflow :
forall k:cont. eval_cont k Underflow Underflow
| a1 :
forall e2:expr, k:cont, v:int, r:value.
eval_cont (B v k) (eval_0 e2) r -> eval_cont (A e2 k) (Vnum v) r
| a2 :
forall v1:int, k:cont, v:int, r:value.
eval_cont k (if v1 >= v then Vnum (v1 - v) else Underflow) r
-> eval_cont (B v1 k) (Vnum v) r
| a3 :
forall v:int. eval_cont I (Vnum v) (Vnum v)

```

Some functions to serve as measures for the termination proof

```function size_e (e:expr) : int =
match e with
| Cte _ -> 1
| Sub e1 e2 -> 3 + size_e e1 + size_e e2
end

lemma size_e_pos: forall e: expr. size_e e >= 1

use Defunctionalization as D

function size_c (c:cont) : int =
match c with
| I -> 0
| A e2 k -> 2 + D.size_e e2 + size_c k
| B _ k -> 1 + size_c k
end

lemma size_c_pos: forall c: cont. size_c c >= 0

let rec continue_4 (c:cont) (v:int) : value
requires { v >= 0 }
variant { size_c c }
ensures { eval_cont c (Vnum v) result }
=
match c with
| A e2 k -> eval_4 e2 (B v k)
| B v1 k -> if v1 >= v then continue_4 k (v1 - v) else Underflow
| I -> Vnum v
end

with eval_4 (e:expr) (c:cont) : value
variant { size_c c + D.size_e e }
ensures { eval_cont c (eval_0 e) result }
=
match e with
| Cte n -> if n >= 0 then continue_4 c n else Underflow
| Sub e1 e2 -> eval_4 e1 (A e2 c)
end

```

The interpreter. The post-condition specifies that this program computes the same thing as `eval_0`

```let interpret_4 (p:prog) : value
ensures { result = eval_0 p }
= eval_4 p I

let test () =
interpret_4 p0,
interpret_4 p1,
interpret_4 p2,
interpret_4 p3,
interpret_4 p4

end

```

## Reduction Semantics

```module ReductionSemantics

```

A small step semantics, defined iteratively with reduction contexts

```  use Expr
use DirectSem

```

Expressions:

```n  :  int

e  :  expression
e ::= n | e - e

p  :  program
p ::= e
```

Values:

```v  :  value
v ::= n
```

Potential Redexes:

```  rp ::= n1 - n2
```

Reduction Rule:

```  n1 - n2 -> n3
```
(in the case of relative integers Z, all potential redexes are true redexes; but for natural numbers, not all of them are true ones:
```   n1 - n2 -> n3   if n1 >= n2
```
a potential redex that is not a true one is stuck.)

Contraction Function:

```  contract : redex_potentiel -> expression + stuck
contract (n1 - n2) = n3   si n3 = n1 - n2
```
and if there are only non-negative numbers:
```  contract (n1 - n2) = n3     if n1 >= n2 and n3 = n1 - n2
contract (n1 - n2) = stuck  if n1 < n2
```

```predicate is_a_redex (e:expr) =
match e with
| Sub (Cte _) (Cte _) -> true
| _ -> false
end

let contract (e:expr) : expr
requires { is_a_redex e }
ensures { eval_0 result = eval_0 e }
=
match e with
| Sub (Cte v1) (Cte v2) -> Cte (v1 - v2)
| _ -> absurd
end

```

Reduction Contexts:

```C  : cont
C ::= [] | [C e] | [v C]
```

```type context = Empty | Left context expr | Right int context

```

Recomposition:

```             recompose : cont * expression -> expression
recompose ([], e) = e
recompose ([C e2], e1) = recompose (C, e1 - e2)
recompose ([n1 C], e2) = recompose (C, n1 - e2)
```

```let rec function recompose (c:context) (e:expr) : expr =
match c with
| Empty -> e
| Left c e2 -> recompose c (Sub e e2)
| Right n1 c -> recompose c (Sub (Cte n1) e)
end

let rec lemma recompose_values (c:context) (e1 e2:expr) : unit
requires { eval_0 e1 = eval_0 e2 }
variant  { c }
ensures  { eval_0 (recompose c e1) = eval_0 (recompose c e2) }
= match c with
| Empty -> ()
| Left c e -> recompose_values c (Sub e1 e) (Sub e2 e)
| Right n c -> recompose_values c (Sub (Cte n) e1) (Sub (Cte n) e2)
end

(* not needed anymore
let rec lemma recompose_inversion (c:context) (e:expr)
requires {
match c with Empty -> false | _ -> true end \/
match e with Cte _ -> false | Sub _ _ -> true end }
variant { c }
ensures {  match recompose c e with
Cte _ -> false | Sub _ _ -> true end }
= match c with
| Empty -> ()
| Left c e2 -> recompose_inversion c (Sub e e2)
| Right n1 c -> recompose_inversion c (Sub (Cte n1) e)
end
*)

```

Decomposition:

```dec_or_val = (C, rp) | v
```
Decomposition function:
```             decompose_term : expression * cont -> dec_or_val
decompose_term (n, C) = decompose_cont (C, n)
decompose_term (e1 - e2, C) = decompose_term (e1, [C e2])

decompose_cont : cont * value -> dec_or_val
decompose_cont ([], n) = n
decompose_cont ([C e], n) = decompose_term (e, [n c])
decompose_term ([n1 C], n2) = (C, n1 - n2)

decompose : expression -> dec_or_val
decompose e = decompose_term (e, [])
```

```exception Stuck

predicate is_a_value (e:expr) =
match e with
| Cte _ -> true
| _ -> false
end

predicate is_empty_context (c:context) =
match c with
| Empty -> true
| _ -> false
end

use Defunctionalization as D (* for size_e *)

function size_e (e:expr) : int = D.size_e e

function size_c (c:context) : int =
match c with
| Empty -> 0
| Left c e -> 2 + size_c c + size_e e
| Right _ c -> 1 + size_c c
end

lemma size_c_pos: forall c: context. size_c c >= 0

let rec decompose_term (e:expr) (c:context) : (context, expr)
variant { size_e e + size_c c }
ensures { let c1,e1 = result in
recompose c1 e1 = recompose c e /\
is_a_redex e1 }
raises { Stuck -> is_empty_context c /\ is_a_value e }
(* raises { Stuck -> is_a_value (recompose c e) } *)
=
match e with
| Cte n -> decompose_cont c n
| Sub e1 e2 -> decompose_term e1 (Left c e2)
end

with decompose_cont (c:context) (n:int) : (context, expr)
variant { size_c c }
ensures { let c1,e1 = result in
recompose c1 e1 = recompose c (Cte n)  /\
is_a_redex e1 }
raises { Stuck -> is_empty_context c }
(*  raises { Stuck -> is_a_value (recompose c (Cte n)) } *)
=
match c with
| Empty -> raise Stuck
| Left c e -> decompose_term e (Right n c)
| Right n1 c -> c, Sub (Cte n1) (Cte n)
end

let decompose (e:expr) : (context, expr)
ensures { let c1,e1 = result in recompose c1 e1 = e  /\
is_a_redex e1 }
raises { Stuck -> is_a_value e }
=
decompose_term e Empty

```

One reduction step:

```reduce : expression -> expression + stuck

if decompose e = v
then reduce e = stuck

if decompose e = (C, rp)
and contract rp = stuck
then reduce e = stuck

if decompose e = (C, rp)
and contract rp = c
then reduce e = recompose (C, c)
```

#### Exercise 2.0

Implement the reduction semantics above and test it

```let reduce (e:expr) : expr
ensures { eval_0 result = eval_0 e }
raises { Stuck -> is_a_value e }
=
let c,r = decompose e in
recompose c (contract r)

```

Evaluation based on iterated reduction:

```itere : red_ou_val -> value + erreur

itere v = v

if contract rp = stuck
then itere (C, rp) = stuck

if contract rp = c
then itere (C, rp) = itere (decompose (recompose (C, c)))
```

```let rec itere (e:expr) : int
diverges (* termination could be proved but that's not the point *)
ensures { eval_0 e = result }
=
match reduce e with
| e' -> itere e'
| exception Stuck ->
match e with
| Cte n -> n
| _ -> absurd
end
end

```

#### Exercise 2.1

Optimize the step recomposition / decomposition into a single function `refocus`.

```let refocus c e
ensures { let c1,e1 = result in
recompose c1 e1 = recompose c e /\
is_a_redex e1 }
raises { Stuck -> is_empty_context c /\ is_a_value e }
= decompose_term e c

let rec itere_opt (c:context) (e:expr) : int
diverges
ensures { result = eval_0 (recompose c e) }
= match refocus c e with
| c, r -> itere_opt c (contract r)
| exception Stuck ->
assert { is_empty_context c };
match e with
| Cte n -> n
| _ -> absurd
end
end

let rec normalize (e:expr)
diverges
ensures { result = eval_0 e }
= itere_opt Empty e

```

#### Exercise 2.2

Derive an abstract machine

```(c,Cte n)_1 -> (c,n)_2
(c,Sub e1 e2)_1 -> (Left c e2,e1)_1
(Empty,n)_2 -> stop with result = n
(Left c e,n)_2 -> (Right n c,e)_1
(Right n1 c,n)_2 -> (c,Cte (n1 - n))_1
```

```let rec eval_1 c e
variant { 2 * (size_c c + size_e e) }
ensures { result = eval_0 (recompose c e) }
= match e with
| Cte n -> eval_2 c n
| Sub e1 e2 -> eval_1 (Left c e2) e1
end

with eval_2 c n
variant { 1 + 2 * size_c c }
ensures { result = eval_0 (recompose c (Cte n)) }
= match c with
| Empty -> n
| Left c e -> eval_1 (Right n c) e
| Right n1 c -> eval_1 c (Cte (n1 - n))
end

let interpret p
ensures { result = eval_0 p }
= eval_1 Empty p

let test () =
interpret p0,
interpret p1,
interpret p2,
interpret p3,
interpret p4

end

module RWithError

use Expr
use SemWithError

```

#### Exercise 2.3

An abstract machine for the case with errors

```(c,Cte n)_1 -> stop on Underflow if  n < 0
(c,Cte n)_1 -> (c,n)_2 if n >= 0
(c,Sub e1 e2)_1 -> (Left c e2,e1)_1
(Empty,n)_2 -> stop on Vnum n
(Left c e,n)_2 -> (Right n c,e)_1
(Right n1 c,n)_2 -> stop on Underflow if n1 < n
(Right n1 c,n)_2 -> (c,Cte (n1 - n))_1 if n1 >= n
```

```type context = Empty | Left context expr | Right int context

use Defunctionalization as D (* for size_e *)

function size_e (e:expr) : int = D.size_e e

function size_c (c:context) : int =
match c with
| Empty -> 0
| Left c e -> 2 + size_c c + size_e e
| Right _ c -> 1 + size_c c
end

lemma size_c_pos: forall c: context. size_c c >= 0

function recompose (c:context) (e:expr) : expr =
match c with
| Empty -> e
| Left c e2 -> recompose c (Sub e e2)
| Right n1 c -> recompose c (Sub (Cte n1) e)
end

let rec lemma recompose_values (c:context) (e1 e2:expr) : unit
requires { eval_0 e1 = eval_0 e2 }
variant  { c }
ensures  { eval_0 (recompose c e1) = eval_0 (recompose c e2) }
= match c with
| Empty -> ()
| Left c e -> recompose_values c (Sub e1 e) (Sub e2 e)
| Right n c -> recompose_values c (Sub (Cte n) e1) (Sub (Cte n) e2)
end

let rec lemma recompose_underflow (c:context) (e:expr) : unit
requires { eval_0 e = Underflow }
variant { c }
ensures { eval_0 (recompose c e) = Underflow }
= match c with
| Empty -> ()
| Left c e1 -> recompose_underflow c (Sub e e1)
| Right n c -> recompose_underflow c (Sub (Cte n) e)
end

let rec eval_1 c e
variant { 2 * (size_c c + size_e e) }
ensures { result = eval_0 (recompose c e) }
= match e with
| Cte n -> if n >= 0 then eval_2 c n else Underflow
| Sub e1 e2 -> eval_1 (Left c e2) e1
end

with eval_2 c n
variant { 1 + 2 * size_c c }
requires { n >= 0 }
ensures { result = eval_0 (recompose c (Cte n)) }
= match c with
| Empty -> Vnum n
| Left c e -> eval_1 (Right n c) e
| Right n1 c -> if n1 >= n then eval_1 c (Cte (n1 - n)) else Underflow
end

let interpret p
ensures { result = eval_0 p }
= eval_1 Empty p

let test () =
interpret p0,
interpret p1,
interpret p2,
interpret p3,
interpret p4

end
```