finish leakage loops

bedrock2/src/bedrock2/LeakageLoops.v

@@ -501,46 +501,50 @@ Section Loops.
 
 
   Lemma atleastonce
-    {e c t l} {m : mem}
+    {e c k t l} {m : mem}
     (variables : list String.string)
     {localstuple : tuple word (length variables)}
     {Pl : enforce variables localstuple l}
-    {measure : Type} (invariant:_->_->_->ufunc word (length variables) Prop)
+    {measure : Type} (invariant:_->_->_->_->ufunc word (length variables) Prop)
     lt (Hwf : well_founded lt)
-    {post : _->_->_-> Prop}
-    (Henter : exists br, expr m l e (eq br) /\ (word.unsigned br = 0%Z -> post t m l))
-    (v0 : measure) (Hpre : tuple.apply (invariant v0 t m) localstuple)
-    (Hbody : forall v t m, tuple.foralls (fun localstuple =>
-      tuple.apply (invariant v t m) localstuple ->
-       cmd call c t m (reconstruct variables localstuple) (fun t m l =>
-         exists br, expr m l e (eq br) /\
-         (word.unsigned br <> 0 -> Markers.unique (Markers.left (tuple.existss (fun localstuple => enforce variables localstuple l /\ Markers.right (Markers.unique (exists v', tuple.apply (invariant v' t m) localstuple /\ lt v' v)))))) /\
-         (word.unsigned br =  0 -> post t m l))))
-    : cmd call (cmd.while e c) t m l post.
+    {post : _->_->_->_-> Prop}
+    (v0 : measure)
+    (Henter : exists br k', dexpr m l k e br k' /\
+                         (word.unsigned br = 0%Z -> post (leak_bool false :: k') t m l) /\
+    (word.unsigned br <> 0%Z -> tuple.apply (invariant v0 (leak_bool true :: k') t m) localstuple))
+    (Hbody : forall v k t m, tuple.foralls (fun localstuple =>
+      tuple.apply (invariant v k t m) localstuple ->
+       cmd call c k t m (reconstruct variables localstuple) (fun k t m l =>
+         exists br k', dexpr m l k e br k' /\
+         (word.unsigned br <> 0 -> Markers.unique (Markers.left (tuple.existss (fun localstuple => enforce variables localstuple l /\ Markers.right (Markers.unique (exists v', tuple.apply (invariant v' (leak_bool true :: k') t m) localstuple /\ lt v' v)))))) /\
+         (word.unsigned br =  0 -> post (leak_bool false :: k') t m l))))
+    : cmd call (cmd.while e c) k t m l post.
   Proof.
-    eapply (atleastonce_localsmap (fun v t m l => exists localstuple, Logic.and (enforce variables localstuple l) (tuple.apply (invariant v t m) localstuple))); eauto.
-    intros vi ti mi li (?&X&Y).
-    specialize (Hbody vi ti mi).
+    destruct Henter as (br & k' & Hbr & Henterfalse & Hentertrue).
+    eapply (atleastonce_localsmap (fun v k t m l => exists localstuple, Logic.and (enforce variables localstuple l) (tuple.apply (invariant v k t m) localstuple))); eauto.
+    { eexists. eexists. split; eauto. split; eauto. }
+    intros vi ki ti mi li (?&X&Y).
+    specialize (Hbody vi ki ti mi).
     eapply hlist.foralls_forall in Hbody.
     specialize (Hbody Y).
     rewrite <-(reconstruct_enforce _ _ _ X) in Hbody.
     eapply Proper_cmd; [ |eapply Hbody].
-    intros t' m' l' (?&?&HH&?).
-    eexists; split; eauto.
+    intros k'' t' m' l' (?&?&?&HH&?).
+    eexists; eexists; split; eauto.
     split; intros; eauto.
     specialize (HH ltac:(eauto)).
     eapply hlist.existss_exists in HH; destruct HH as (?&?&?&?&?).
     eexists; split; eauto.
   Qed.
 
-  Lemma while_zero_iterations {e c t l} {m : mem} {post : _->_->_-> Prop}
-    (HCond: expr m l e (eq (word.of_Z 0)))
-    (HPost: post t m l)
-    : cmd call (cmd.while e c) t m l post.
+  Lemma while_zero_iterations {e c k t l} {m : mem} {post : _->_->_->_-> Prop}
+    (HCondPost: exists k', dexpr m l k e (word.of_Z 0) k' /\ post (leak_bool false :: k') t m l)
+    : cmd call (cmd.while e c) k t m l post.
   Proof.
-    eapply (while_localsmap (fun n t' m' l' => t' = t /\ m' = m /\ l' = l) (PeanoNat.Nat.lt_wf 0) 0%nat).
-    1: unfold split; auto. intros *. intros (? & ? & ?). subst.
-    eexists. split. 1: exact HCond.
+    destruct HCondPost as (k' & HCond & Hpost).
+    eapply (while_localsmap (fun n k' t' m' l' => k' = k /\ t' = t /\ m' = m /\ l' = l) (PeanoNat.Nat.lt_wf 0) 0%nat).
+    1: unfold split; auto. intros *. intros (? & ? & ? & ?). subst.
+    eexists. eexists. split. 1: exact HCond.
     rewrite Properties.word.unsigned_of_Z_0.
     split; intros; congruence.
   Qed.
@@ -552,30 +556,30 @@ Section Loops.
   Local Infix "==>" := Lift1Prop.impl1.
 
   Lemma tailrec_sep
-    e c t (m : mem) l (post : _->_->_-> Prop)
+    e c k t (m : mem) l (post : _->_->_->_-> Prop)
     {measure : Type} P Q lt (Hwf : well_founded lt) (v0 : measure) R0
-    (Hpre : (P v0 t l * R0) m)
-    (Hbody : forall v t m l R, (P v t l * R) m ->
-      exists br, expr m l e (eq br) /\
-      (word.unsigned br <> 0%Z -> cmd call c t m l
-        (fun t' m' l' => exists v' dR, (P v' t' l' * (R * dR)) m' /\
+    (Hpre : (P v0 k t l * R0) m)
+    (Hbody : forall v k t m l R, (P v k t l * R) m ->
+      exists br k', dexpr m l k e br k' /\
+      (word.unsigned br <> 0%Z -> cmd call c (leak_bool true :: k') t m l
+        (fun k'' t' m' l' => exists v' dR, (P v' k'' t' l' * (R * dR)) m' /\
           lt v' v /\
-          forall T L, Q v' T L * dR ==> Q v T L)) /\
-      (word.unsigned br = 0%Z -> (Q v t l * R) m))
-    (Hpost : forall t m l, (Q v0 t l * R0) m -> post t m l)
-    : cmd call (cmd.while e c) t m l post.
+          forall K T L, Q v' K T L * dR ==> Q v K T L)) /\
+      (word.unsigned br = 0%Z -> (Q v (leak_bool false :: k') t l * R) m))
+    (Hpost : forall k t m l, (Q v0 k t l * R0) m -> post k t m l)
+    : cmd call (cmd.while e c) k t m l post.
   Proof.
     eapply wp_while.
-    eexists measure, lt, (fun v t m l => exists R, (P v t l * R) m /\
-                          forall T L, Q v T L * R ==> Q v0 T L * R0).
+    eexists measure, lt, (fun v k t m l => exists R, (P v k t l * R) m /\
+                          forall K T L, Q v K T L * R ==> Q v0 K T L * R0).
     split; [assumption|].
     split. { exists v0, R0. split; [assumption|]. intros. reflexivity. }
-    intros vi ti mi li (Ri&?&Qi).
-    destruct (Hbody _ _ _ _ _ ltac:(eassumption)) as (br&?&X); exists br; split; [assumption|].
+    intros vi ki ti mi li (Ri&?&Qi).
+    destruct (Hbody _ _ _ _ _ _ ltac:(eassumption)) as (br&ki'&?&X); exists br, ki'; split; [assumption|].
     destruct X as (Htrue&Hfalse). split; intros Hbr;
       [pose proof(Htrue Hbr)as Hpc|pose proof(Hfalse Hbr)as Hpc]; clear Hbr Htrue Hfalse.
     { eapply Proper_cmd; [ |eapply Hpc].
-      intros tj mj lj (vj&dR&dP&?&dQ).
+      intros kj tj mj lj (vj&dR&dP&?&dQ).
       exists vj; split; [|assumption].
       exists (Ri * dR); split; [assumption|].
       intros. rewrite (sep_comm _ dR), <-(sep_assoc _ dR), dQ; trivial. }