Commit dec6495c authored by Martin Clochard's avatar Martin Clochard
Browse files

double_wp: fixed coq proof

parent 38d9e475
......@@ -156,6 +156,9 @@ Inductive machine_state :=
Axiom machine_state_WhyType : WhyType machine_state.
Existing Instance machine_state_WhyType.
(* Why3 assumption *)
Definition ofs := Z.
(* Why3 assumption *)
Inductive instr :=
| Iconst : Z -> instr
......@@ -204,24 +207,24 @@ Definition isetvar (x:id): (list instr) :=
(Init.Datatypes.cons (Isetvar x) Init.Datatypes.nil).
(* Why3 assumption *)
Definition ibeq (ofs:Z): (list instr) :=
(Init.Datatypes.cons (Ibeq ofs) Init.Datatypes.nil).
Definition ibeq (ofs1:Z): (list instr) :=
(Init.Datatypes.cons (Ibeq ofs1) Init.Datatypes.nil).
(* Why3 assumption *)
Definition ible (ofs:Z): (list instr) :=
(Init.Datatypes.cons (Ible ofs) Init.Datatypes.nil).
Definition ible (ofs1:Z): (list instr) :=
(Init.Datatypes.cons (Ible ofs1) Init.Datatypes.nil).
(* Why3 assumption *)
Definition ibne (ofs:Z): (list instr) :=
(Init.Datatypes.cons (Ibne ofs) Init.Datatypes.nil).
Definition ibne (ofs1:Z): (list instr) :=
(Init.Datatypes.cons (Ibne ofs1) Init.Datatypes.nil).
(* Why3 assumption *)
Definition ibgt (ofs:Z): (list instr) :=
(Init.Datatypes.cons (Ibgt ofs) Init.Datatypes.nil).
Definition ibgt (ofs1:Z): (list instr) :=
(Init.Datatypes.cons (Ibgt ofs1) Init.Datatypes.nil).
(* Why3 assumption *)
Definition ibranch (ofs:Z): (list instr) :=
(Init.Datatypes.cons (Ibranch ofs) Init.Datatypes.nil).
Definition ibranch (ofs1:Z): (list instr) :=
(Init.Datatypes.cons (Ibranch ofs1) Init.Datatypes.nil).
(* Why3 assumption *)
Inductive transition: (list instr) -> machine_state -> machine_state ->
......@@ -250,49 +253,49 @@ Inductive transition: (list instr) -> machine_state -> machine_state ->
(s:(list Z)) (m:(map id Z)), (transition c (VMS p
(Init.Datatypes.cons n2 (Init.Datatypes.cons n1 s)) m) (VMS (p + 1%Z)%Z
(Init.Datatypes.cons (n1 * n2)%Z s) m))
| trans_beq : forall (c:(list instr)) (p1:Z) (ofs:Z), (codeseq_at c p1
(ibeq ofs)) -> forall (s:(list Z)) (m:(map id Z)) (n1:Z) (n2:Z),
| trans_beq : forall (c:(list instr)) (p1:Z) (ofs1:Z), (codeseq_at c p1
(ibeq ofs1)) -> forall (s:(list Z)) (m:(map id Z)) (n1:Z) (n2:Z),
(n1 = n2) -> (transition c (VMS p1
(Init.Datatypes.cons n2 (Init.Datatypes.cons n1 s)) m)
(VMS ((p1 + 1%Z)%Z + ofs)%Z s m))
| trans_beq1 : forall (c:(list instr)) (p1:Z) (ofs:Z), (codeseq_at c p1
(ibeq ofs)) -> forall (s:(list Z)) (m:(map id Z)) (n1:Z) (n2:Z),
(VMS ((p1 + 1%Z)%Z + ofs1)%Z s m))
| trans_beq1 : forall (c:(list instr)) (p1:Z) (ofs1:Z), (codeseq_at c p1
(ibeq ofs1)) -> forall (s:(list Z)) (m:(map id Z)) (n1:Z) (n2:Z),
(~ (n1 = n2)) -> (transition c (VMS p1
(Init.Datatypes.cons n2 (Init.Datatypes.cons n1 s)) m)
(VMS (p1 + 1%Z)%Z s m))
| trans_bne : forall (c:(list instr)) (p1:Z) (ofs:Z), (codeseq_at c p1
(ibne ofs)) -> forall (s:(list Z)) (m:(map id Z)) (n1:Z) (n2:Z),
| trans_bne : forall (c:(list instr)) (p1:Z) (ofs1:Z), (codeseq_at c p1
(ibne ofs1)) -> forall (s:(list Z)) (m:(map id Z)) (n1:Z) (n2:Z),
(n1 = n2) -> (transition c (VMS p1
(Init.Datatypes.cons n2 (Init.Datatypes.cons n1 s)) m)
(VMS (p1 + 1%Z)%Z s m))
| trans_bne1 : forall (c:(list instr)) (p1:Z) (ofs:Z), (codeseq_at c p1
(ibne ofs)) -> forall (s:(list Z)) (m:(map id Z)) (n1:Z) (n2:Z),
| trans_bne1 : forall (c:(list instr)) (p1:Z) (ofs1:Z), (codeseq_at c p1
(ibne ofs1)) -> forall (s:(list Z)) (m:(map id Z)) (n1:Z) (n2:Z),
(~ (n1 = n2)) -> (transition c (VMS p1
(Init.Datatypes.cons n2 (Init.Datatypes.cons n1 s)) m)
(VMS ((p1 + 1%Z)%Z + ofs)%Z s m))
| trans_ble : forall (c:(list instr)) (p1:Z) (ofs:Z), (codeseq_at c p1
(ible ofs)) -> forall (s:(list Z)) (m:(map id Z)) (n1:Z) (n2:Z),
(VMS ((p1 + 1%Z)%Z + ofs1)%Z s m))
| trans_ble : forall (c:(list instr)) (p1:Z) (ofs1:Z), (codeseq_at c p1
(ible ofs1)) -> forall (s:(list Z)) (m:(map id Z)) (n1:Z) (n2:Z),
(n1 <= n2)%Z -> (transition c (VMS p1
(Init.Datatypes.cons n2 (Init.Datatypes.cons n1 s)) m)
(VMS ((p1 + 1%Z)%Z + ofs)%Z s m))
| trans_ble1 : forall (c:(list instr)) (p1:Z) (ofs:Z), (codeseq_at c p1
(ible ofs)) -> forall (s:(list Z)) (m:(map id Z)) (n1:Z) (n2:Z),
(VMS ((p1 + 1%Z)%Z + ofs1)%Z s m))
| trans_ble1 : forall (c:(list instr)) (p1:Z) (ofs1:Z), (codeseq_at c p1
(ible ofs1)) -> forall (s:(list Z)) (m:(map id Z)) (n1:Z) (n2:Z),
(~ (n1 <= n2)%Z) -> (transition c (VMS p1
(Init.Datatypes.cons n2 (Init.Datatypes.cons n1 s)) m)
(VMS (p1 + 1%Z)%Z s m))
| trans_bgt : forall (c:(list instr)) (p1:Z) (ofs:Z), (codeseq_at c p1
(ibgt ofs)) -> forall (s:(list Z)) (m:(map id Z)) (n1:Z) (n2:Z),
| trans_bgt : forall (c:(list instr)) (p1:Z) (ofs1:Z), (codeseq_at c p1
(ibgt ofs1)) -> forall (s:(list Z)) (m:(map id Z)) (n1:Z) (n2:Z),
(n1 <= n2)%Z -> (transition c (VMS p1
(Init.Datatypes.cons n2 (Init.Datatypes.cons n1 s)) m)
(VMS (p1 + 1%Z)%Z s m))
| trans_bgt1 : forall (c:(list instr)) (p1:Z) (ofs:Z), (codeseq_at c p1
(ibgt ofs)) -> forall (s:(list Z)) (m:(map id Z)) (n1:Z) (n2:Z),
| trans_bgt1 : forall (c:(list instr)) (p1:Z) (ofs1:Z), (codeseq_at c p1
(ibgt ofs1)) -> forall (s:(list Z)) (m:(map id Z)) (n1:Z) (n2:Z),
(~ (n1 <= n2)%Z) -> (transition c (VMS p1
(Init.Datatypes.cons n2 (Init.Datatypes.cons n1 s)) m)
(VMS ((p1 + 1%Z)%Z + ofs)%Z s m))
| trans_branch : forall (c:(list instr)) (p:Z) (ofs:Z), (codeseq_at c p
(ibranch ofs)) -> forall (s:(list Z)) (m:(map id Z)), (transition c
(VMS p s m) (VMS ((p + 1%Z)%Z + ofs)%Z s m)).
(VMS ((p1 + 1%Z)%Z + ofs1)%Z s m))
| trans_branch : forall (c:(list instr)) (p:Z) (ofs1:Z), (codeseq_at c p
(ibranch ofs1)) -> forall (s:(list Z)) (m:(map id Z)), (transition c
(VMS p s m) (VMS ((p + 1%Z)%Z + ofs1)%Z s m)).
(* Why3 assumption *)
Inductive transition_star: (list instr) -> machine_state -> machine_state ->
......@@ -321,10 +324,10 @@ Parameter func_WhyType : forall (a:Type) {a_WT:WhyType a}
Existing Instance func_WhyType.
(* Why3 assumption *)
Definition pred (a:Type) := (func a bool).
Definition pred (a:Type) := (a -> bool).
Parameter infix_at: forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, (func a b) -> a -> b.
{b:Type} {b_WT:WhyType b}, (a -> b) -> a -> b.
(* Why3 assumption *)
Definition fst {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b} (p:(a*
......@@ -339,38 +342,37 @@ Definition snd {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b} (p:(a*
end.
(* Why3 assumption *)
Definition pred1 := (func machine_state bool).
Definition pred1 := (machine_state -> bool).
(* Why3 assumption *)
Definition rel := (func machine_state (func machine_state bool)).
Definition rel := (machine_state -> (machine_state -> bool)).
(* Why3 assumption *)
Definition pre (a:Type) := (func a (func Z (func machine_state bool))).
Definition pre (a:Type) := (a -> (Z -> (machine_state -> bool))).
(* Why3 assumption *)
Definition post (a:Type) := (func a (func Z (func machine_state (func
machine_state bool)))).
Definition post (a:Type) := (a -> (Z -> (machine_state -> (machine_state ->
bool)))).
(* Why3 assumption *)
Inductive hl
(a:Type) :=
| mk_hl : (list instr) -> (func a (func Z (func machine_state bool))) ->
(func a (func Z (func machine_state (func machine_state bool)))) -> hl
a.
| mk_hl : (list instr) -> (a -> (Z -> (machine_state -> bool))) -> (a ->
(Z -> (machine_state -> (machine_state -> bool)))) -> hl a.
Axiom hl_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (hl a).
Existing Instance hl_WhyType.
Implicit Arguments mk_hl [[a]].
(* Why3 assumption *)
Definition post1 {a:Type} {a_WT:WhyType a} (v:(hl a)): (func a (func Z (func
machine_state (func machine_state bool)))) :=
Definition post1 {a:Type} {a_WT:WhyType a} (v:(hl a)): (a -> (Z ->
(machine_state -> (machine_state -> bool)))) :=
match v with
| (mk_hl x x1 x2) => x2
end.
(* Why3 assumption *)
Definition pre1 {a:Type} {a_WT:WhyType a} (v:(hl a)): (func a (func Z (func
machine_state bool))) := match v with
Definition pre1 {a:Type} {a_WT:WhyType a} (v:(hl a)): (a -> (Z ->
(machine_state -> bool))) := match v with
| (mk_hl x x1 x2) => x1
end.
......@@ -381,21 +383,21 @@ Definition code1 {a:Type} {a_WT:WhyType a} (v:(hl a)): (list instr) :=
end.
(* Why3 assumption *)
Definition wp_trans (a:Type) := (func a (func Z (func (func machine_state
bool) (func machine_state bool)))).
Definition wp_trans (a:Type) := (a -> (Z -> ((machine_state -> bool) ->
(machine_state -> bool)))).
(* Why3 assumption *)
Inductive wp
(a:Type) :=
| mk_wp : (list instr) -> (func a (func Z (func (func machine_state bool)
(func machine_state bool)))) -> wp a.
| mk_wp : (list instr) -> (a -> (Z -> ((machine_state -> bool) ->
(machine_state -> bool)))) -> wp a.
Axiom wp_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (wp a).
Existing Instance wp_WhyType.
Implicit Arguments mk_wp [[a]].
(* Why3 assumption *)
Definition wp1 {a:Type} {a_WT:WhyType a} (v:(wp a)): (func a (func Z (func
(func machine_state bool) (func machine_state bool)))) :=
Definition wp1 {a:Type} {a_WT:WhyType a} (v:(wp a)): (a -> (Z ->
((machine_state -> bool) -> (machine_state -> bool)))) :=
match v with
| (mk_wp x x1) => x1
end.
......@@ -413,358 +415,295 @@ Definition contextual_irrelevance (c:(list instr)) (p:Z) (ms1:machine_state)
(* Why3 assumption *)
Definition hl_correctness {a:Type} {a_WT:WhyType a} (cs:(hl a)): Prop :=
forall (x:a) (p:Z) (ms:machine_state),
((infix_at (infix_at (infix_at (pre1 cs) x) p) ms) = true) ->
exists ms':machine_state,
((infix_at (infix_at (infix_at (infix_at (post1 cs) x) p) ms)
ms') = true) /\ (contextual_irrelevance (code1 cs) p ms ms').
forall (x:a) (p:Z) (ms:machine_state), (((((pre1 cs) x) p) ms) = true) ->
exists ms':machine_state, ((((((post1 cs) x) p) ms) ms') = true) /\
(contextual_irrelevance (code1 cs) p ms ms').
(* Why3 assumption *)
Definition wp_correctness {a:Type} {a_WT:WhyType a} (code2:(wp a)): Prop :=
forall (x:a) (p:Z) (post2:(func machine_state bool)) (ms:machine_state),
((infix_at (infix_at (infix_at (infix_at (wp1 code2) x) p) post2)
ms) = true) -> exists ms':machine_state, ((infix_at post2 ms') = true) /\
(contextual_irrelevance (wcode code2) p ms ms').
Parameter seq_wp: forall {a:Type} {a_WT:WhyType a}, Z -> (func a (func Z
(func (func machine_state bool) (func machine_state bool)))) -> (func (a*
machine_state)%type (func Z (func (func machine_state bool) (func
machine_state bool)))) -> (func a (func Z (func (func machine_state bool)
(func machine_state bool)))).
Axiom seq_wp_def : forall {a:Type} {a_WT:WhyType a}, forall (l1:Z) (w1:(func
a (func Z (func (func machine_state bool) (func machine_state bool)))))
(w2:(func (a* machine_state)%type (func Z (func (func machine_state bool)
(func machine_state bool))))) (x:a) (p:Z) (q:(func machine_state bool))
(ms:machine_state), ((infix_at (infix_at (infix_at (infix_at (seq_wp l1 w1
w2) x) p) q) ms) = (infix_at (infix_at (infix_at (infix_at w1 x) p)
(infix_at (infix_at (infix_at w2 (x, ms)) (p + l1)%Z) q)) ms)).
forall (x:a) (p:Z) (post2:(machine_state -> bool)) (ms:machine_state),
((((((wp1 code2) x) p) post2) ms) = true) -> exists ms':machine_state,
((post2 ms') = true) /\ (contextual_irrelevance (wcode code2) p ms ms').
(* Why3 assumption *)
Definition seq_wp {a:Type} {a_WT:WhyType a} (l1:Z) (w1:(a -> (Z ->
((machine_state -> bool) -> (machine_state -> bool))))) (w2:((a*
machine_state)%type -> (Z -> ((machine_state -> bool) -> (machine_state ->
bool))))): (a -> (Z -> ((machine_state -> bool) -> (machine_state ->
bool)))) := fun (x:a) (p:Z) (q:(machine_state -> bool))
(ms:machine_state) => ((((w1 x) p) (((w2 (x, ms)) (p + l1)%Z) q)) ms).
Axiom seq_wp_lemma : forall {a:Type} {a_WT:WhyType a}, forall (l1:Z)
(w1:(func a (func Z (func (func machine_state bool) (func machine_state
bool))))) (w2:(func (a* machine_state)%type (func Z (func (func
machine_state bool) (func machine_state bool))))) (x:a) (p:Z) (q:(func
machine_state bool)) (ms:machine_state),
((infix_at (infix_at (infix_at (infix_at (seq_wp l1 w1 w2) x) p) q)
ms) = (infix_at (infix_at (infix_at (infix_at w1 x) p)
(infix_at (infix_at (infix_at w2 (x, ms)) (p + l1)%Z) q)) ms)).
Parameter fork_wp: forall {a:Type} {a_WT:WhyType a}, (func a (func Z (func
(func machine_state bool) (func machine_state bool)))) -> (func a (func Z
(func machine_state bool))) -> (func a (func Z (func (func machine_state
bool) (func machine_state bool)))).
Axiom fork_wp_def : forall {a:Type} {a_WT:WhyType a}, forall (w:(func a (func
Z (func (func machine_state bool) (func machine_state bool))))) (exn:(func
a (func Z (func machine_state bool)))) (x:a) (p:Z) (q:(func machine_state
bool)) (ms:machine_state),
((infix_at (infix_at (infix_at (infix_at (fork_wp w exn) x) p) q)
ms) = true) <-> ((((infix_at (infix_at (infix_at exn x) p) ms) = true) ->
((infix_at q ms) = true)) /\ ((~ ((infix_at (infix_at (infix_at exn x) p)
ms) = true)) -> ((infix_at (infix_at (infix_at (infix_at w x) p) q)
ms) = true))).
Axiom fork_wp_lemma : forall {a:Type} {a_WT:WhyType a}, forall (w:(func a
(func Z (func (func machine_state bool) (func machine_state bool)))))
(exn:(func a (func Z (func machine_state bool)))) (x:a) (p:Z) (q:(func
machine_state bool)) (ms:machine_state),
((infix_at (infix_at (infix_at (infix_at (fork_wp w exn) x) p) q)
ms) = true) <-> ((((infix_at (infix_at (infix_at exn x) p) ms) = true) ->
((infix_at q ms) = true)) /\ ((~ ((infix_at (infix_at (infix_at exn x) p)
ms) = true)) -> ((infix_at (infix_at (infix_at (infix_at w x) p) q)
ms) = true))).
Parameter towp_wp: forall {a:Type} {a_WT:WhyType a}, (func a (func Z (func
machine_state bool))) -> (func a (func Z (func machine_state (func
machine_state bool)))) -> (func a (func Z (func (func machine_state bool)
(func machine_state bool)))).
Axiom towp_wp_def : forall {a:Type} {a_WT:WhyType a}, forall (pr:(func a
(func Z (func machine_state bool)))) (ps:(func a (func Z (func
machine_state (func machine_state bool))))) (x:a) (p:Z) (q:(func
machine_state bool)) (ms:machine_state),
((infix_at (infix_at (infix_at (infix_at (towp_wp pr ps) x) p) q)
ms) = true) <-> (((infix_at (infix_at (infix_at pr x) p) ms) = true) /\
forall (ms':machine_state), ((infix_at (infix_at (infix_at (infix_at ps x)
p) ms) ms') = true) -> ((infix_at q ms') = true)).
Axiom towp_wp_lemma : forall {a:Type} {a_WT:WhyType a}, forall (pr:(func a
(func Z (func machine_state bool)))) (ps:(func a (func Z (func
machine_state (func machine_state bool))))) (x:a) (p:Z) (q:(func
machine_state bool)) (ms:machine_state),
((infix_at (infix_at (infix_at (infix_at (towp_wp pr ps) x) p) q)
ms) = true) <-> (((infix_at (infix_at (infix_at pr x) p) ms) = true) /\
forall (ms':machine_state), ((infix_at (infix_at (infix_at (infix_at ps x)
p) ms) ms') = true) -> ((infix_at q ms') = true)).
Parameter trivial_pre: forall {a:Type} {a_WT:WhyType a}, (func a (func Z
(func machine_state bool))).
Axiom trivial_pre_def : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (p:Z)
(ms:machine_state), ((infix_at (infix_at (infix_at (trivial_pre : (func a
(func Z (func machine_state bool)))) x) p) ms) = true) <->
match ms with
(w1:(a -> (Z -> ((machine_state -> bool) -> (machine_state -> bool)))))
(w2:((a* machine_state)%type -> (Z -> ((machine_state -> bool) ->
(machine_state -> bool))))) (x:a) (p:Z) (q:(machine_state -> bool))
(ms:machine_state), ((((((seq_wp l1 w1 w2) x) p) q) ms) = ((((w1 x) p)
(((w2 (x, ms)) (p + l1)%Z) q)) ms)).
Parameter fork_wp: forall {a:Type} {a_WT:WhyType a}, (a -> (Z ->
((machine_state -> bool) -> (machine_state -> bool)))) -> (a -> (Z ->
(machine_state -> bool))) -> (a -> (Z -> ((machine_state -> bool) ->
(machine_state -> bool)))).
Axiom fork_wp_def : forall {a:Type} {a_WT:WhyType a}, forall (w:(a -> (Z ->
((machine_state -> bool) -> (machine_state -> bool))))) (cond:(a -> (Z ->
(machine_state -> bool)))) (x:a) (p:Z) (q:(machine_state -> bool))
(ms:machine_state), ((((((fork_wp w cond) x) p) q) ms) = true) <->
(((~ ((((cond x) p) ms) = true)) -> ((q ms) = true)) /\ (((((cond x) p)
ms) = true) -> (((((w x) p) q) ms) = true))).
Axiom fork_wp_lemma : forall {a:Type} {a_WT:WhyType a}, forall (w:(a -> (Z ->
((machine_state -> bool) -> (machine_state -> bool))))) (cond:(a -> (Z ->
(machine_state -> bool)))) (x:a) (p:Z) (q:(machine_state -> bool))
(ms:machine_state), ((((((fork_wp w cond) x) p) q) ms) = true) <->
(((~ ((((cond x) p) ms) = true)) -> ((q ms) = true)) /\ (((((cond x) p)
ms) = true) -> (((((w x) p) q) ms) = true))).
Parameter towp_wp: forall {a:Type} {a_WT:WhyType a}, (a -> (Z ->
(machine_state -> bool))) -> (a -> (Z -> (machine_state ->
(machine_state -> bool)))) -> (a -> (Z -> ((machine_state -> bool) ->
(machine_state -> bool)))).
Axiom towp_wp_def : forall {a:Type} {a_WT:WhyType a}, forall (pr:(a -> (Z ->
(machine_state -> bool)))) (ps:(a -> (Z -> (machine_state ->
(machine_state -> bool))))) (x:a) (p:Z) (q:(machine_state -> bool))
(ms:machine_state), ((((((towp_wp pr ps) x) p) q) ms) = true) <-> (((((pr
x) p) ms) = true) /\ forall (ms':machine_state), (((((ps x) p) ms)
ms') = true) -> ((q ms') = true)).
Axiom towp_wp_lemma : forall {a:Type} {a_WT:WhyType a}, forall (pr:(a ->
(Z -> (machine_state -> bool)))) (ps:(a -> (Z -> (machine_state ->
(machine_state -> bool))))) (x:a) (p:Z) (q:(machine_state -> bool))
(ms:machine_state), ((((((towp_wp pr ps) x) p) q) ms) = true) <-> (((((pr
x) p) ms) = true) /\ forall (ms':machine_state), (((((ps x) p) ms)
ms') = true) -> ((q ms') = true)).
Parameter trivial_pre: forall {a:Type} {a_WT:WhyType a}, (a -> (Z ->
(machine_state -> bool))).
Axiom trivial_pre_def : forall {a:Type} {a_WT:WhyType a}, forall (us:a) (p:Z)
(ms:machine_state), (((((trivial_pre : (a -> (Z -> (machine_state ->
bool)))) us) p) ms) = true) <-> match ms with
| (VMS p' _ _) => (p = p')
end.
(* Why3 assumption *)
Inductive acc {a:Type} {a_WT:WhyType a}: (func a (func a bool)) -> a ->
Prop :=
| Acc : forall (r:(func a (func a bool))) (x:a), (forall (y:a),
((infix_at (infix_at r y) x) = true) -> (acc r y)) -> (acc r x).
Inductive acc {a:Type} {a_WT:WhyType a}: (a -> (a -> bool)) -> a -> Prop :=
| Acc : forall (r:(a -> (a -> bool))) (x:a), (forall (y:a), (((r y)
x) = true) -> (acc r y)) -> (acc r x).
Parameter loop_preservation: forall {a:Type} {a_WT:WhyType a}, (func a (func
Z (func machine_state bool))) -> (func a (func Z (func machine_state
bool))) -> (func a (func Z (func machine_state (func machine_state
bool)))) -> (func a (func Z (func machine_state (func machine_state
bool)))).
Parameter loop_progress: forall {a:Type} {a_WT:WhyType a}, (a -> (Z ->
(machine_state -> bool))) -> (a -> (Z -> (machine_state -> bool))) -> (a ->
(Z -> (machine_state -> (machine_state -> bool)))) -> (a -> (Z ->
(machine_state -> (machine_state -> bool)))).
Axiom loop_preservation_def : forall {a:Type} {a_WT:WhyType a},
forall (inv:(func a (func Z (func machine_state bool)))) (post2:(func a
(func Z (func machine_state bool)))) (var:(func a (func Z (func
machine_state (func machine_state bool))))) (x:a) (p:Z) (ms:machine_state)
(ms':machine_state),
((infix_at (infix_at (infix_at (infix_at (loop_preservation inv post2 var)
x) p) ms) ms') = true) <-> ((((infix_at (infix_at (infix_at inv x) p)
ms') = true) /\ ((infix_at (infix_at (infix_at (infix_at var x) p) ms')
ms) = true)) \/ ((infix_at (infix_at (infix_at post2 x) p) ms') = true)).
Parameter forget_old: forall {a:Type} {a_WT:WhyType a}, (func a (func Z (func
machine_state bool))) -> (func a (func Z (func machine_state (func
machine_state bool)))).
Axiom forget_old_def : forall {a:Type} {a_WT:WhyType a}, forall (post2:(func
a (func Z (func machine_state bool)))) (x:a) (p:Z) (ms:machine_state),
((infix_at (infix_at (infix_at (forget_old post2) x) p)
ms) = (infix_at (infix_at post2 x) p)).
Parameter ifun_post: forall {a:Type} {a_WT:WhyType a}, (func machine_state
machine_state) -> (func a (func Z (func machine_state (func machine_state
bool)))).
Axiom loop_progress_def : forall {a:Type} {a_WT:WhyType a}, forall (inv:(a ->
(Z -> (machine_state -> bool)))) (post2:(a -> (Z -> (machine_state ->
bool)))) (var:(a -> (Z -> (machine_state -> (machine_state -> bool)))))
(x:a) (p:Z) (ms:machine_state) (ms':machine_state), ((((((loop_progress inv
post2 var) x) p) ms) ms') = true) <-> ((((((inv x) p) ms') = true) /\
(((((var x) p) ms') ms) = true)) \/ ((((post2 x) p) ms') = true)).
(* Why3 assumption *)
Definition forget_old {a:Type} {a_WT:WhyType a} (post2:(a -> (Z ->
(machine_state -> bool)))): (a -> (Z -> (machine_state -> (machine_state ->
bool)))) := fun (x:a) (p:Z) (us:machine_state) => ((post2 x) p).
Axiom ifun_post_def : forall {a:Type} {a_WT:WhyType a}, forall (f:(func
machine_state machine_state)) (x:a) (p:Z) (ms:machine_state)
(ms':machine_state),
((infix_at (infix_at (infix_at (infix_at (ifun_post f: (func a (func Z
(func machine_state (func machine_state bool))))) x) p) ms)
ms') = true) <-> (ms' = (infix_at f ms)).
Parameter ifun_post: forall {a:Type} {a_WT:WhyType a}, (machine_state ->
machine_state) -> (a -> (Z -> (machine_state -> (machine_state -> bool)))).
Parameter iconst_post: forall {a:Type} {a_WT:WhyType a}, Z -> (func a (func Z
(func machine_state (func machine_state bool)))).
Axiom ifun_post_def : forall {a:Type} {a_WT:WhyType a},
forall (f:(machine_state -> machine_state)) (us:a) (us1:Z)
(ms:machine_state) (ms':machine_state), ((((((ifun_post f: (a -> (Z ->
(machine_state -> (machine_state -> bool))))) us) us1) ms) ms') = true) <->
(ms' = (f ms)).
Axiom iconst_post_def : forall {a:Type} {a_WT:WhyType a}, forall (n:Z) (x:a)
(p:Z) (ms:machine_state) (ms':machine_state),
((infix_at (infix_at (infix_at (infix_at (iconst_post n: (func a (func Z
(func machine_state (func machine_state bool))))) x) p) ms)
Parameter iconst_post: forall {a:Type} {a_WT:WhyType a}, Z -> (a -> (Z ->
(machine_state -> (machine_state -> bool)))).
Axiom iconst_post_def : forall {a:Type} {a_WT:WhyType a}, forall (n:Z) (us:a)
(p:Z) (ms:machine_state) (ms':machine_state), ((((((iconst_post n: (a ->
(Z -> (machine_state -> (machine_state -> bool))))) us) p) ms)
ms') = true) <-> forall (s:(list Z)) (m:(map id Z)), (ms = (VMS p s m)) ->
(ms' = (VMS (p + 1%Z)%Z (Init.Datatypes.cons n s) m)).
Parameter iconst_fun: Z -> (func machine_state machine_state).
Axiom iconst_fun_def : forall (n:Z) (ms:machine_state),
((infix_at (iconst_fun n)
ms) = match ms with
(* Why3 assumption *)
Definition iconst_fun (n:Z): (machine_state -> machine_state) :=
fun (ms:machine_state) =>
match ms with
| (VMS p s m) => (VMS (p + 1%Z)%Z (Init.Datatypes.cons n s) m)
end).
end.
Parameter ivar_post: forall {a:Type} {a_WT:WhyType a}, id -> (func a (func Z
(func machine_state (func machine_state bool)))).
Parameter ivar_post: forall {a:Type} {a_WT:WhyType a}, id -> (a -> (Z ->
(machine_state -> (machine_state -> bool)))).
Axiom ivar_post_def : forall {a:Type} {a_WT:WhyType a}, forall (x:id) (a1:a)
(p:Z) (ms:machine_state) (ms':machine_state),
((infix_at (infix_at (infix_at (infix_at (ivar_post x: (func a (func Z
(func machine_state (func machine_state bool))))) a1) p) ms)
Axiom ivar_post_def : forall {a:Type} {a_WT:WhyType a}, forall (x:id) (us:a)
(p:Z) (ms:machine_state) (ms':machine_state), ((((((ivar_post x: (a ->
(Z -> (machine_state -> (machine_state -> bool))))) us) p) ms)
ms') = true) <-> forall (s:(list Z)) (m:(map id Z)), (ms = (VMS p s m)) ->
(ms' = (VMS (p + 1%Z)%Z (Init.Datatypes.cons (get m x) s) m)).
Parameter ivar_fun: id -> (func machine_state machine_state).
Axiom ivar_fun_def : forall (x:id) (ms:machine_state),
((infix_at (ivar_fun x)
ms) = match ms with
(* Why3 assumption *)
Definition ivar_fun (x:id): (machine_state -> machine_state) :=
fun (ms:machine_state) =>
match ms with
| (VMS p s m) => (VMS (p + 1%Z)%Z (Init.Datatypes.cons (get m x) s) m)
end).
end.
(* Why3 assumption *)
Definition binop := (func Z (func Z Z)).
Definition binop := (Z -> (Z -> Z)).
Parameter ibinop_pre: forall {a:Type} {a_WT:WhyType a}, (func a (func Z (func