Commit c87c1e9a authored by Léon Gondelman's avatar Léon Gondelman

mini-compiler: aexpr & bexpr proved

parent 5fd9aede
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require map.Map.
Require int.Int.
Require bool.Bool.
Axiom map : forall (a:Type) (b:Type), Type.
Parameter map_WhyType : forall (a:Type) {a_WT:WhyType a}
(b:Type) {b_WT:WhyType b}, WhyType (map a b).
Existing Instance map_WhyType.
Parameter get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b.
Parameter set: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b -> (map a b).
Axiom Select_eq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) ->
((get (set m a1 b1) a2) = b1).
Axiom Select_neq : forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, forall (m:(map a b)), forall (a1:a) (a2:a),
forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1) a2) = (get m a2)).
Parameter const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
b -> (map a b).
Axiom Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (b1:b) (a1:a), ((get (const b1: (map a b)) a1) = b1).
(* Why3 assumption *)
Inductive id :=
| Id : Z -> id.
Axiom id_WhyType : WhyType id.
Existing Instance id_WhyType.
(* Why3 assumption *)
Definition state := (map id Z).
(* Why3 assumption *)
Inductive aexpr :=
| Anum : Z -> aexpr
| Avar : id -> aexpr
| Aadd : aexpr -> aexpr -> aexpr
| Asub : aexpr -> aexpr -> aexpr
| Amul : aexpr -> aexpr -> aexpr.
Axiom aexpr_WhyType : WhyType aexpr.
Existing Instance aexpr_WhyType.
(* Why3 assumption *)
Inductive bexpr :=
| Btrue : bexpr
| Bfalse : bexpr
| Band : bexpr -> bexpr -> bexpr
| Bnot : bexpr -> bexpr
| Beq : aexpr -> aexpr -> bexpr
| Ble : aexpr -> aexpr -> bexpr.
Axiom bexpr_WhyType : WhyType bexpr.
Existing Instance bexpr_WhyType.
(* Why3 assumption *)
Inductive com :=
| Cskip : com
| Cassign : id -> aexpr -> com
| Cseq : com -> com -> com
| Cif : bexpr -> com -> com -> com
| Cwhile : bexpr -> com -> com.
Axiom com_WhyType : WhyType com.
Existing Instance com_WhyType.
(* Why3 assumption *)
Fixpoint aeval (st:(map id Z)) (e:aexpr) {struct e}: Z :=
match e with
| (Anum n) => n
| (Avar x) => (get st x)
| (Aadd e1 e2) => ((aeval st e1) + (aeval st e2))%Z
| (Asub e1 e2) => ((aeval st e1) - (aeval st e2))%Z
| (Amul e1 e2) => ((aeval st e1) * (aeval st e2))%Z
end.
Parameter beval: (map id Z) -> bexpr -> bool.
Axiom beval_def : forall (st:(map id Z)) (b:bexpr),
match b with
| Btrue => ((beval st b) = true)
| Bfalse => ((beval st b) = false)
| (Bnot b') => ((beval st b) = (Init.Datatypes.negb (beval st b')))
| (Band b1 b2) => ((beval st b) = (Init.Datatypes.andb (beval st
b1) (beval st b2)))
| (Beq a1 a2) => (((aeval st a1) = (aeval st a2)) -> ((beval st
b) = true)) /\ ((~ ((aeval st a1) = (aeval st a2))) -> ((beval st
b) = false))
| (Ble a1 a2) => (((aeval st a1) <= (aeval st a2))%Z -> ((beval st
b) = true)) /\ ((~ ((aeval st a1) <= (aeval st a2))%Z) -> ((beval st
b) = false))
end.
Axiom inversion_beval_t : forall (a1:aexpr) (a2:aexpr) (m:(map id Z)),
((beval m (Beq a1 a2)) = true) -> ((aeval m a1) = (aeval m a2)).
Axiom inversion_beval_f : forall (a1:aexpr) (a2:aexpr) (m:(map id Z)),
((beval m (Beq a1 a2)) = false) -> ~ ((aeval m a1) = (aeval m a2)).
(* Why3 assumption *)
Inductive ceval: (map id Z) -> com -> (map id Z) -> Prop :=
| E_Skip : forall (m:(map id Z)), (ceval m Cskip m)
| E_Ass : forall (m:(map id Z)) (a:aexpr) (n:Z) (x:id), ((aeval m
a) = n) -> (ceval m (Cassign x a) (set m x n))
| E_Seq : forall (cmd1:com) (cmd2:com) (m0:(map id Z)) (m1:(map id Z))
(m2:(map id Z)), (ceval m0 cmd1 m1) -> ((ceval m1 cmd2 m2) -> (ceval m0
(Cseq cmd1 cmd2) m2))
| E_IfTrue : forall (m0:(map id Z)) (m1:(map id Z)) (cond:bexpr) (cmd1:com)
(cmd2:com), ((beval m0 cond) = true) -> ((ceval m0 cmd1 m1) -> (ceval
m0 (Cif cond cmd1 cmd2) m1))
| E_IfFalse : forall (m0:(map id Z)) (m1:(map id Z)) (cond:bexpr)
(cmd1:com) (cmd2:com), ((beval m0 cond) = false) -> ((ceval m0 cmd2
m1) -> (ceval m0 (Cif cond cmd1 cmd2) m1))
| E_WhileEnd : forall (cond:bexpr) (m:(map id Z)) (body:com), ((beval m
cond) = false) -> (ceval m (Cwhile cond body) m)
| E_WhileLoop : forall (mi:(map id Z)) (mj:(map id Z)) (mf:(map id Z))
(cond:bexpr) (body:com), ((beval mi cond) = true) -> ((ceval mi body
mj) -> ((ceval mj (Cwhile cond body) mf) -> (ceval mi (Cwhile cond
body) mf))).
Require Import Why3.
Ltac cvc := why3 "CVC4,1.4,".
(* Why3 goal *)
Theorem ceval_deterministic : forall (c:com) (mi:(map id Z)) (mf1:(map id Z))
(mf2:(map id Z)), (ceval mi c mf1) -> ((ceval mi c mf2) -> (mf1 = mf2)).
intros c mi mf1 mf2 h1 h2.
generalize dependent mf2.
induction h1;intros mf2 h2; inversion h2; cvc.
Qed.
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.4pl2" timelimit="5" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<file name="../imp.why" expanded="true">
<theory name="Imp" sum="939397712f6415b10da2ec9b4ffeab30" expanded="true">
<goal name="inversion_beval_t" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inversion_beval_f" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="ceval_deterministic" expanded="true">
<proof prover="0" edited="imp_Imp_ceval_deterministic_1.v"><result status="valid" time="2.36"/></proof>
</goal>
</theory>
</file>
</why3session>
module Compiler_logic
use import int.Int
use import list.List
use import list.Length
use import list.Append
use import vm.Vm
use import state.State
use import HighOrd
function fst (p: ('a,'b)) : 'a =
let (x,_) = p in x
meta rewrite_def function fst
function snd (p: ('a,'b)) : 'b =
let (_,y) = p in y
meta rewrite_def function snd
(* Unary predicates over machine states *)
type pred = machine_state -> bool
(* Postcondition type (first argument is old state) *)
type post = machine_state -> pred
(* Hoare triples with explicit pre & post *)
type hl 'a =
{ code: code;
ghost pre : 'a -> pos -> pred;
ghost post: 'a -> pos -> post }
(* Code with weakest precondition wp_correctness. *)
type wp 'a =
{ wcode : code;
ghost wp : 'a -> pos -> pred -> pred }
(* Machine transition independence for a piece of code with respect
to the rest of the code. *)
predicate contextual_irrelevance (c : code) (p: pos) (ms1 ms2 : machine_state)
= forall c_global: code.
codeseq_at c_global p c ->
transition_star c_global ms1 ms2
(* (Total) correctness for hoare triple. *)
predicate hl_correctness (cs : hl 'a) =
forall x:'a, p: pos, ms : machine_state. cs.pre x p ms ->
exists ms' : machine_state.
cs.post x p ms ms' /\ contextual_irrelevance cs.code p ms ms'
(* Invariant for code with WP wp_correctness. *)
predicate wp_correctness (code : wp 'a) =
forall x:'a, p: pos, post : pred, ms: machine_state.
(code.wp x p post) ms ->
exists ms' : machine_state.
(post ms') /\ contextual_irrelevance code.wcode p ms ms'
(* WP combinator for sequence. *)
function seq_wp (s1 : wp 'a) (s2: wp ('a, machine_state)) : 'a -> pos -> pred -> pred =
\x p q ms. s1.wp x p (s2.wp (x,ms) (p + s1.wcode.length) q) ms
lemma seq_wp_lemma :
forall s1: wp 'a, s2 x p q ms.
seq_wp s1 s2 x p q ms = s1.wp x p (s2.wp (x,ms) (p + s1.wcode.length) q) ms
meta rewrite prop seq_wp_lemma
(* Code combinator for sequence, with wp. *)
let (~) (s1 : wp 'a) (s2 : wp ('a, machine_state)) : wp 'a
requires { wp_correctness s1 /\ wp_correctness s2 }
ensures { result.wcode.length = s1.wcode.length + s2.wcode.length }
ensures { result.wp = seq_wp s1 s2 /\ wp_correctness result }
= let wcode = s1.wcode ++ s2.wcode in
let res =
{ wcode = wcode ;
wp = any 'a -> pos -> pred -> pred ensures {result = seq_wp s1 s2 } }
in assert {
forall x: 'a, p: pos, post : pred, ms: machine_state. (res.wp x p post) ms ->
not ( exists ms' : machine_state. (post ms')
/\ contextual_irrelevance res.wcode p ms ms') ->
(forall ms' : machine_state.
((s2.wp (x,ms) (p + s1.wcode.length) post) ms')
/\ contextual_irrelevance res.wcode p ms ms' -> false)
&& false };
res
function fork_wp (s2: wp 'a) (exn: 'a -> pos -> pred) : 'a -> pos -> pred -> pred =
\x p q ms.
( exn x p ms -> q ms)
/\ (not exn x p ms -> s2.wp x p q ms)
lemma fork_wp_lemma:
forall s2: wp 'a, exn x p q ms.
fork_wp s2 exn x p q ms =
( ( exn x p ms -> q ms)
/\ (not exn x p ms -> s2.wp x p q ms))
meta rewrite prop fork_wp_lemma
(* Code combinator for sequence, with wp. *)
let (%) (s: wp 'a) (exn: 'a -> pos -> pred) : wp 'a
requires { wp_correctness s }
ensures { result.wp = fork_wp s exn /\ result.wcode.length = s.wcode.length }
ensures { wp_correctness result }
= { wcode = s.wcode ;
wp = any 'a -> pos -> pred -> pred ensures {result = fork_wp s exn } }
(* WP transformer for hoare triples. *)
function towp_wp (c : hl 'a) : 'a -> pos -> pred -> pred =
\ x p q ms. c.pre x p ms && (forall ms'. c.post x p ms ms' -> q ms')
lemma towp_wp_lemma:
forall c, x:'a, p q ms. towp_wp c x p q ms =
(c.pre x p ms && (forall ms'. c.post x p ms ms' -> q ms'))
meta rewrite prop towp_wp_lemma
(* Unwrap code with hoare triple into code with wp.
Analogous to function call/abstract block. *)
let ($_) (c: hl 'a) : wp 'a
requires { hl_correctness c }
ensures { result.wcode.length = c.code.length /\ result.wp = towp_wp c}
ensures { wp_correctness result }
= { wcode = c.code;
wp = any 'a -> pos -> pred -> pred ensures {result = towp_wp c}}
(* Equip code with pre/post-condition. That is here that proof happen.
(P -> wp (c,Q)). Anologous to checking function/abstract block
specification. *)
let hoare (ghost pre: 'a -> pos -> pred) (c: wp 'a) (ghost post: 'a -> pos -> post) : hl 'a
requires { wp_correctness c }
requires { forall x p ms. pre x p ms -> (c.wp x p (post x p ms)) ms }
ensures { result.pre = pre /\ result.post = post }
ensures { result.code.length = c.wcode.length /\ hl_correctness result}
= { code = c.wcode ; pre = pre; post = post }
function trivial_pre : 'a -> pos -> pred = \x p ms.
match ms with
| VMS p' _ _ -> p = p'
end
lemma trivial_pre_lemma:
forall x:'a, p ms. trivial_pre x p ms =
match ms with
| VMS p' _ _ -> p = p'
end
meta rewrite prop trivial_pre_lemma
end
(*
Local Variables:
compile-command: "why3 ide -L . logic.mlw"
End:
*)
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.3" timelimit="5" memlimit="1000"/>
<file name="../logic.mlw" expanded="true">
<theory name="Compiler_logic" sum="9dcaf842383ff8f3b36434fd4a939892" expanded="true">
<goal name="seq_wp_lemma">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter infix ~" expl="VC for infix ~" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter infix ~.1" expl="1. assertion" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter infix ~.1.1" expl="1. assertion">
<proof prover="1"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="WP_parameter infix ~.1.2" expl="2. assertion" expanded="true">
<transf name="simplify_trivial_quantification_in_goal" expanded="true">
<goal name="WP_parameter infix ~.1.2.1" expl="1." expanded="true">
<transf name="compute_specified" expanded="true">
<goal name="WP_parameter infix ~.1.2.1.1" expl="1.">
<proof prover="1"><result status="valid" time="0.23"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="WP_parameter infix ~.2" expl="2. postcondition">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter infix ~.3" expl="3. postcondition">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
<goal name="fork_wp_lemma" expanded="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter infix %" expl="VC for infix %">
<transf name="split_goal_wp">
<goal name="WP_parameter infix %.1" expl="1. postcondition">
<proof prover="0"><result status="valid" time="0.10"/></proof>
</goal>
</transf>
</goal>
<goal name="towp_wp_lemma">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter prefix $" expl="VC for prefix $">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter hoare" expl="VC for hoare">
<transf name="split_goal_wp">
<goal name="WP_parameter hoare.1" expl="1. postcondition">
<proof prover="0"><result status="valid" time="0.07"/></proof>
<proof prover="2"><result status="valid" time="0.07"/></proof>
</goal>
</transf>
</goal>
<goal name="trivial_pre_lemma">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
</theory>
</file>
</why3session>
This diff is collapsed.
This diff is collapsed.
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