Experiment with nonterminating programs

bedrock2/src/bedrock2/FE310CSemantics.v

@@ -48,7 +48,7 @@ Section WithParameters.
     split;
     cbv [leakage_ext_spec Morphisms.Proper Morphisms.respectful Morphisms.pointwise_relation Basics.impl];
     intros.
-    all :
+    1,2 :
     repeat match goal with
       | H : context[(?x =? ?y)%string] |- _ =>
           destruct (x =? y)%string in *
@@ -60,6 +60,17 @@ Section WithParameters.
       | H: _ :: _ = _ :: _ |- _ => injection H; intros; subst; clear H
     end;
     eauto 8 using Properties.map.same_domain_refl.
+    repeat match goal with
+           | H: context[(?x =? ?y)%string] |- _ => destruct (x =? y)%string end.
+    - assert (H0 := H O). destruct H0 as (addr & val & H0 & (H1 & H2 & H3) & H4). subst.
+      exists addr, val. intuition auto. specialize (H x).
+      destruct H as (addr' & val' & H0' & (H1' & H2' & H3') & H4'). subst.
+      inversion H0'. subst. assumption.
+    - assert (H0 := H O). destruct H0 as (addr & H0 & (H1 & H2 & H3) & H4). subst.
+      exists addr. intuition auto. specialize (H x).
+      destruct H as (addr' & H0' & (H1' & H2' & H3') & H4'). subst.
+      inversion H0'. subst. auto.
+    - set (x := O). auto.
   Qed.
 
   Global Instance ext_spec : Semantics.ExtSpec := deleakaged_ext_spec.

bedrock2/src/bedrock2/LeakageSemantics.v

@@ -89,11 +89,10 @@ Module ext_spec.
              (ext_spec t mGive act args);
 
     intersect: forall t mGive a args
-                      (post1 post2: mem -> list word -> list word -> Prop),
-        ext_spec t mGive a args post1 ->
-        ext_spec t mGive a args post2 ->
+                      (post : _ -> mem -> list word -> list word -> Prop),
+        (forall x : nat, ext_spec t mGive a args (post x)) ->
         ext_spec t mGive a args (fun mReceive resvals klist =>
-                                   post1 mReceive resvals klist /\ post2 mReceive resvals klist);
+                                   forall x, post x mReceive resvals klist);
   }.
 End ext_spec.
 Arguments ext_spec.ok {_ _ _ _} _.
@@ -289,81 +288,81 @@ Module exec. Section WithParams.
       eauto 10.
   Qed.
 
-  Lemma intersect: forall k t l m s post1,
-      exec s k t m l post1 ->
-      forall post2,
-        exec s k t m l post2 ->
-        exec s k t m l (fun k' t' m' l' => post1 k' t' m' l' /\ post2 k' t' m' l').
-  Proof.
-    induction 1;
-      intros;
-      match goal with
-      | H: exec _ _ _ _ _ _ |- _ => inversion H; subst; clear H
-      end;
-      try match goal with
-      | H1: ?e = Some (?x1, ?y1, ?z1), H2: ?e = Some (?x2, ?y2, ?z2) |- _ =>
-        replace x2 with x1 in * by congruence;
-          replace y2 with y1 in * by congruence;
-          replace z2 with z1 in * by congruence;
-          clear x2 y2 z2 H2
-      end;
-      repeat match goal with
-             | H1: ?e = Some (?v1, ?k1), H2: ?e = Some (?v2, ?k2) |- _ =>
-                 replace v2 with v1 in * by congruence;
-                 replace k2 with k1 in * by congruence;
-                 clear H2
-             end;
-      repeat match goal with
-             | H1: ?e = Some ?v1, H2: ?e = Some ?v2 |- _ =>
-               replace v2 with v1 in * by congruence; clear H2
-             end;
-      try solve [econstructor; eauto | exfalso; congruence].
-
-    - econstructor. 1: eassumption.
-      intros.
-      rename H0 into Ex1, H12 into Ex2.
-      eapply weaken. 1: eapply H1. 1,2: eassumption.
-      1: eapply Ex2. 1,2: eassumption.
-      cbv beta.
-      intros. fwd.
-      lazymatch goal with
-      | A: map.split _ _ _, B: map.split _ _ _ |- _ =>
-        specialize @map.split_diff with (4 := A) (5 := B) as P
-      end.
-      edestruct P; try typeclasses eauto. 2: subst; eauto 10.
-      eapply anybytes_unique_domain; eassumption.
-    - econstructor.
-      + eapply IHexec. exact H5. (* not H *)
-      + simpl. intros *. intros [? ?]. eauto.
-    - eapply while_true. 1, 2: eassumption.
-      + eapply IHexec. exact H9. (* not H1 *)
-      + simpl. intros *. intros [? ?]. eauto.
-    - eapply call. 1, 2, 3: eassumption.
-      + eapply IHexec. exact H16. (* not H2 *)
-      + simpl. intros *. intros [? ?].
-        edestruct H3 as (? & ? & ? & ? & ?); [eassumption|].
-        edestruct H17 as (? & ? & ? & ? & ?); [eassumption|].
-        repeat match goal with
-               | H1: ?e = Some ?v1, H2: ?e = Some ?v2 |- _ =>
-                 replace v2 with v1 in * by congruence; clear H2
-               end.
-        eauto 10.
-    - pose proof ext_spec.mGive_unique as P.
-      specialize P with (1 := H) (2 := H7) (3 := H1) (4 := H14).
-      subst mGive0.
-      destruct (map.split_diff (map.same_domain_refl mGive) H H7) as (? & _).
-      subst mKeep0.
-      eapply interact. 1,2: eassumption.
-      + eapply ext_spec.intersect; [ exact H1 | exact H14 ].
-      + simpl. intros *. intros [? ?].
-        edestruct H2 as (? & ? & ?); [eassumption|].
-        edestruct H15 as (? & ? & ?); [eassumption|].
-        repeat match goal with
-               | H1: ?e = Some ?v1, H2: ?e = Some ?v2 |- _ =>
-                 replace v2 with v1 in * by congruence; clear H2
-               end.
-        eauto 10.
-  Qed.
+  (* Lemma intersect: forall k t l m s post1, *)
+  (*     exec s k t m l post1 -> *)
+  (*     forall post2, *)
+  (*       exec s k t m l post2 -> *)
+  (*       exec s k t m l (fun k' t' m' l' => post1 k' t' m' l' /\ post2 k' t' m' l'). *)
+  (* Proof. *)
+  (*   induction 1; *)
+  (*     intros; *)
+  (*     match goal with *)
+  (*     | H: exec _ _ _ _ _ _ |- _ => inversion H; subst; clear H *)
+  (*     end; *)
+  (*     try match goal with *)
+  (*     | H1: ?e = Some (?x1, ?y1, ?z1), H2: ?e = Some (?x2, ?y2, ?z2) |- _ => *)
+  (*       replace x2 with x1 in * by congruence; *)
+  (*         replace y2 with y1 in * by congruence; *)
+  (*         replace z2 with z1 in * by congruence; *)
+  (*         clear x2 y2 z2 H2 *)
+  (*     end; *)
+  (*     repeat match goal with *)
+  (*            | H1: ?e = Some (?v1, ?k1), H2: ?e = Some (?v2, ?k2) |- _ => *)
+  (*                replace v2 with v1 in * by congruence; *)
+  (*                replace k2 with k1 in * by congruence; *)
+  (*                clear H2 *)
+  (*            end; *)
+  (*     repeat match goal with *)
+  (*            | H1: ?e = Some ?v1, H2: ?e = Some ?v2 |- _ => *)
+  (*              replace v2 with v1 in * by congruence; clear H2 *)
+  (*            end; *)
+  (*     try solve [econstructor; eauto | exfalso; congruence]. *)
+
+  (*   - econstructor. 1: eassumption. *)
+  (*     intros. *)
+  (*     rename H0 into Ex1, H12 into Ex2. *)
+  (*     eapply weaken. 1: eapply H1. 1,2: eassumption. *)
+  (*     1: eapply Ex2. 1,2: eassumption. *)
+  (*     cbv beta. *)
+  (*     intros. fwd. *)
+  (*     lazymatch goal with *)
+  (*     | A: map.split _ _ _, B: map.split _ _ _ |- _ => *)
+  (*       specialize @map.split_diff with (4 := A) (5 := B) as P *)
+  (*     end. *)
+  (*     edestruct P; try typeclasses eauto. 2: subst; eauto 10. *)
+  (*     eapply anybytes_unique_domain; eassumption. *)
+  (*   - econstructor. *)
+  (*     + eapply IHexec. exact H5. (* not H *) *)
+  (*     + simpl. intros *. intros [? ?]. eauto. *)
+  (*   - eapply while_true. 1, 2: eassumption. *)
+  (*     + eapply IHexec. exact H9. (* not H1 *) *)
+  (*     + simpl. intros *. intros [? ?]. eauto. *)
+  (*   - eapply call. 1, 2, 3: eassumption. *)
+  (*     + eapply IHexec. exact H16. (* not H2 *) *)
+  (*     + simpl. intros *. intros [? ?]. *)
+  (*       edestruct H3 as (? & ? & ? & ? & ?); [eassumption|]. *)
+  (*       edestruct H17 as (? & ? & ? & ? & ?); [eassumption|]. *)
+  (*       repeat match goal with *)
+  (*              | H1: ?e = Some ?v1, H2: ?e = Some ?v2 |- _ => *)
+  (*                replace v2 with v1 in * by congruence; clear H2 *)
+  (*              end. *)
+  (*       eauto 10. *)
+  (*   - pose proof ext_spec.mGive_unique as P. *)
+  (*     specialize P with (1 := H) (2 := H7) (3 := H1) (4 := H14). *)
+  (*     subst mGive0. *)
+  (*     destruct (map.split_diff (map.same_domain_refl mGive) H H7) as (? & _). *)
+  (*     subst mKeep0. *)
+  (*     eapply interact. 1,2: eassumption. *)
+  (*     + eapply ext_spec.intersect; [ exact H1 | exact H14 ]. *)
+  (*     + simpl. intros *. intros [? ?]. *)
+  (*       edestruct H2 as (? & ? & ?); [eassumption|]. *)
+  (*       edestruct H15 as (? & ? & ?); [eassumption|]. *)
+  (*       repeat match goal with *)
+  (*              | H1: ?e = Some ?v1, H2: ?e = Some ?v2 |- _ => *)
+  (*                replace v2 with v1 in * by congruence; clear H2 *)
+  (*              end. *)
+  (*       eauto 10. *)
+  (* Qed. *)
 
   End WithEnv.