defunctionalization: simplified proof

parent aa5e2d12
......@@ -160,16 +160,7 @@ function interpret_1 (p : prog) : int = eval_1 p (\ n. n)
use import DirectSem
let rec lemma cps_correct_expr (e:expr) : unit
variant { e }
ensures { forall k:int -> 'a. eval_1 e k = k (eval_0 e) }
= match e with
| Cte _ -> ()
| Sub e1 e2 ->
cps_correct_expr e1;
cps_correct_expr e2
end
lemma cps_correct_expr: forall e:expr, k:int -> 'a. eval_1 e k = k (eval_0 e)
lemma cps_correct: forall p. interpret_1 p = interpret_0 p
......@@ -477,17 +468,14 @@ with eval_2b (v1:int) (k:int -> 'a) (kerr : unit -> 'a) : int -> 'a =
function interpret_2 (p : prog) : value =
eval_2 p (\ n. Vnum n) (\ u. Underflow)
let rec lemma cps2_correct_expr (e:expr) (kerr:unit -> 'a): unit
variant { e }
ensures { forall k. eval_2 e k kerr =
match eval_0 e with Vnum n -> k n | Underflow -> kerr () end }
= match e with
| Cte _ -> ()
| Sub e1 e2 ->
cps2_correct_expr e1 kerr;
cps2_correct_expr e2 kerr;
assert {forall k. eval_2 e k kerr = eval_2 e1 (eval_2a e2 k kerr) kerr }
end
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
......@@ -952,7 +940,8 @@ let rec itere_opt (c:context) (e:expr) : int
let (c,r) = refocus c e in
itere_opt c (contract r)
with Stuck ->
match recompose c e with
assert { match c with Empty -> true | _ -> false end };
match e with
| Cte n -> n
| _ -> absurd
end
......@@ -1088,7 +1077,7 @@ let rec lemma recompose_underflow (c:context) (e:expr) : unit
let rec eval_1 c e
variant { 2 * (size_c c + size_e 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
......@@ -1096,7 +1085,7 @@ let rec eval_1 c e
end
with eval_2 c n
variant { 1 + 2 * size_c c }
variant { 1 + 2 * size_c c }
requires { n >= 0 }
ensures { result = eval_0 (recompose c (Cte n)) }
= match c with
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment