zenon/formal-methods-fstar
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Add proofs

Browse Source
This commit is contained in:
Tobias Eidelpes 2021-06-03 10:41:21 +02:00
parent b4f23f8247
commit 204ff4fa5b
1 changed files with 10 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
Project2.fst
View File

@ -236,14 +236,19 @@ val order_decreases: (n: nat) -> (te: tenv) -> (cs: callstack{wellformed cs}) ->
Lemma (requires (nsteps n te cs == cs' /\ n > 0 /\ ~ (isFinal cs) )) Lemma (requires (nsteps n te cs == cs' /\ n > 0 /\ ~ (isFinal cs) ))
(ensures (getLexFromList(getDecArgList cs')<< getLexFromList(getDecArgList cs))) (ensures (getLexFromList(getDecArgList cs')<< getLexFromList(getDecArgList cs)))
let rec order_decreases n te cs cs' = let rec order_decreases n te cs cs' =
admit () if n = 1 then ()
else let cs1 = step_simp te cs in
assert (getLexFromList (getDecArgList cs1) << getLexFromList (getDecArgList cs));
if isFinal cs1
then nsteps_stop (n-1) te cs1
else order_decreases (n-1) te cs1 cs'
(* Use the previous Lemma to show that the callstacks during execution are unique *) (* Use the previous Lemma to show that the callstacks during execution are unique *)
val callstacks_unique: (n: nat) -> (te: tenv) -> (cs: callstack{wellformed cs}) -> (cs': callstack) -> val callstacks_unique: (n: nat) -> (te: tenv) -> (cs: callstack{wellformed cs}) -> (cs': callstack) ->
Lemma (requires (nsteps n te cs == cs' /\ n > 0 /\ ~ (isFinal cs) )) Lemma (requires (nsteps n te cs == cs' /\ n > 0 /\ ~ (isFinal cs) ))
(ensures (~ (cs == cs'))) (ensures (~ (cs == cs')))
let rec callstacks_unique n te cs cs' = let rec callstacks_unique n te cs cs' =
admit () order_decreases n te cs cs'
(* 3.5: Exception propagation *) (* 3.5: Exception propagation *)
@ -252,4 +257,6 @@ val exception_prop: (te:tenv) -> (ps:plaincallstack) ->
Lemma (requires (wellformed (Ter ExcState ps))) Lemma (requires (wellformed (Ter ExcState ps)))
(ensures (nsteps (op_Multiply 2 (length ps)) te (Ter ExcState ps) == (Ter ExcState []))) (ensures (nsteps (op_Multiply 2 (length ps)) te (Ter ExcState ps) == (Ter ExcState [])))
let rec exception_prop te ps = let rec exception_prop te ps =
admit () match ps with
| [] -> ()
| _ :: ps' -> exception_prop te ps'