From 204ff4fa5bfd86437521929e82094ced4a6e7588 Mon Sep 17 00:00:00 2001 From: Tobias Eidelpes Date: Thu, 3 Jun 2021 10:41:21 +0200 Subject: [PATCH] Add proofs --- Project2.fst | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/Project2.fst b/Project2.fst index 4b2ba76..c79797a 100644 --- a/Project2.fst +++ b/Project2.fst @@ -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) )) (ensures (getLexFromList(getDecArgList cs')<< getLexFromList(getDecArgList 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 *) val callstacks_unique: (n: nat) -> (te: tenv) -> (cs: callstack{wellformed cs}) -> (cs': callstack) -> Lemma (requires (nsteps n te cs == cs' /\ n > 0 /\ ~ (isFinal cs) )) (ensures (~ (cs == cs'))) let rec callstacks_unique n te cs cs' = - admit () + order_decreases n te cs cs' (* 3.5: Exception propagation *) @@ -252,4 +257,6 @@ val exception_prop: (te:tenv) -> (ps:plaincallstack) -> Lemma (requires (wellformed (Ter ExcState ps))) (ensures (nsteps (op_Multiply 2 (length ps)) te (Ter ExcState ps) == (Ter ExcState []))) let rec exception_prop te ps = - admit () + match ps with + | [] -> () + | _ :: ps' -> exception_prop te ps'