fix extraneous unfolding of get in straightline, prove addsub

mit-plv · Jun 27, 2023 · d37488b · d37488b
1 parent 832f47e
commit d37488b
Show file tree

Hide file tree

Showing 5 changed files with 36 additions and 44 deletions.
diff --git a/bedrock2/src/bedrock2/ProgramLogic.v b/bedrock2/src/bedrock2/ProgramLogic.v
@@ -255,7 +255,9 @@ Ltac straightline :=
   | |- dexpr _ _ _ _ => cbv beta delta [dexpr]
   | |- dexprs _ _ _ _ => cbv beta delta [dexprs]
   | |- literal _ _ => cbv beta delta [literal]
-  | |- get _ _ _ => cbv beta delta [get]
+  | |- @get ?w ?W ?L ?l ?x ?P =>
+      let get' := eval cbv [get] in @get in
+      change (get' w W L l x P); cbv beta
   | |- load _ _ _ _ => cbv beta delta [load]
   | |- @Loops.enforce ?width ?word ?locals ?names ?values ?map =>
     let values := eval cbv in values in

diff --git a/bedrock2/src/bedrock2Examples/MultipleReturnValues.v b/bedrock2/src/bedrock2Examples/MultipleReturnValues.v
@@ -1,20 +1,26 @@
-Require Import coqutil.Macros.subst coqutil.Macros.unique bedrock2.Syntax.
-Require Import bedrock2.NotationsCustomEntry Coq.Lists.List.
-
-Import BinInt String ListNotations.
-Local Open Scope string_scope. Local Open Scope Z_scope. Local Open Scope list_scope.
-
-Section MultipleReturnValues.
-  Example addsub := func! (a, b) ~> (x, y) {
-    x = a + b;
-    y = a - b
-  }.
-
-  Example addsub_test := func! () ~> ret {
-    unpack! ret, ret = addsub($14, $7);
-    ret = ret - $7
-  }.
-End MultipleReturnValues.
+From bedrock2 Require Import Syntax NotationsCustomEntry.
+Local Open Scope string_scope. Local Open Scope Z_scope.
+
+Example addsub := func! (a, b) ~> (x, y) {
+  x = a + b;
+  y = a - b
+}.
+
+Example addsub_test := func! () ~> ret {
+  unpack! ret, ret = addsub($14, $7);
+  ret = ret - $7
+}.
+
+From bedrock2 Require Import WeakestPrecondition ProgramLogic BasicC64Semantics.
+Import coqutil.Word.Interface.
+
+Local Instance spec_of_addsub : spec_of "addsub" :=
+  fnspec! "addsub" a b ~> x y,
+  { requires m t := True; ensures M T := m=M /\ t=T /\
+    x = word.add a b /\ y = word.sub a b }.
+
+Lemma addsub_correct : program_logic_goal_for_function! addsub.
+Proof. repeat straightline. Qed.
 
 (*
 Require Import bedrock2.ToCString coqutil.Macros.WithBaseName.

diff --git a/bedrock2/src/bedrock2Examples/SPI.v b/bedrock2/src/bedrock2Examples/SPI.v
@@ -269,8 +269,7 @@ Section WithParameters.
           { ZnWordsL. } }
           { ZnWords. }
           { ZnWords. } }
-      { letexists; split; repeat straightline.
-        eexists (x2 ;++ cons _ nil); split; cbn [app]; eauto.
+      { eexists (x2 ;++ cons _ nil); split; cbn [app]; eauto.
         eexists. split.
         { econstructor; try eassumption; right; eauto. }
         eexists (byte.of_Z (word.unsigned x)), _; split.
@@ -315,10 +314,7 @@ Section WithParameters.
           { econstructor; try eassumption; right; eauto. }
           subst i.
           rewrite Properties.word.unsigned_xor_nowrap, Z.lxor_nilpotent in H1; contradiction. } }
-      { eexists _; split.
-        { repeat straightline. }
-        split; trivial.
-        (* copy-paste from above, trace manipulation *)
+      { (* copy-paste from above, trace manipulation *)
         eexists (x2 ;++ cons _ nil); split; cbn [app]; eauto.
         eexists. split.
         { econstructor; try eassumption; right; eauto. }

diff --git a/bedrock2/src/bedrock2Examples/lightbulb.v b/bedrock2/src/bedrock2Examples/lightbulb.v
@@ -522,29 +522,22 @@ Section WithParameters.
         eapply Z.ltb_nlt in HJ.
         ZnWords. }
       repeat straightline.
-      repeat letexists. split. { repeat straightline. }
-      eexists _, _. split. { exact eq_refl. }
 
-      repeat straightline.
       subst i.
-      match goal with H: _ |- _ =>
-        progress repeat (unshelve erewrite (_ : forall x, word.add x (word.of_Z 0) = x) in H; [intros; ring|]);
-        progress repeat (unshelve erewrite (_ : forall x, word.sub x (word.of_Z 0) = x) in H; [intros; ring|])
-      end.
+      progress replace (Z.to_nat (word.unsigned (word.sub p_addr p_addr) / 1)) with O in * by ZnWords.
+      rewrite ?word.add_0_r, ?word.sub_0_r, ?Z.mul_1_l, ?Nat.add_0_l, ?Z2Nat.id, ?word.of_Z_unsigned in * by apply word.unsigned_range.
+
       eexists; split.
       1: { repeat match goal with |- context [?x] => match type of x with list _ => subst x end end.
         repeat rewrite List.app_assoc. f_equal. }
       eexists; split.
       1:repeat eapply List.Forall2_app; eauto.
       destruct H14; [left|right]; repeat straightline; repeat split; eauto.
-      { trans_ltu.
-        Import eplace.
-        eplace (word.add p_addr _) with (word.add p_addr num_bytes) in * by ZnWords.
-        eplace (Z.to_nat (word.unsigned (word.sub p_addr p_addr) / 1)) with O in * by ZnWords.
+      { progress trans_ltu.
         cbn [List.firstn array] in *.
         replace (word.unsigned (word.of_Z 1521)) with 1521 in *
           by (rewrite word.unsigned_of_Z; exact eq_refl).
-          eexists _, _; repeat split.
+        eexists _, _; repeat split.
         { cbn [seps] in *. SeparationLogic.ecancel_assumption. }
         { revert dependent x2. revert dependent x6. intros.
           destruct H5; repeat straightline; try contradiction.
@@ -563,10 +556,9 @@ Section WithParameters.
         all: try ZnWords.
         }
       { repeat match goal with H : _ |- _ => rewrite H; intro HX; solve[inversion HX] end. }
-      { trans_ltu;
-        replace (word.unsigned (word.of_Z 1521)) with 1521 in * by
+      { progress trans_ltu;
+        progress replace (word.unsigned (word.of_Z 1521)) with 1521 in * by
           (rewrite word.unsigned_of_Z; exact eq_refl).
-        replace (Z.to_nat (word.unsigned (word.sub p_addr p_addr) / 1)) with O in * by ZnWords.
         all : cbn [seps array List.firstn List.skipn] in *.
         eexists _; split; eauto; repeat split; try blia.
         { SeparationLogic.seprewrite_in @bytearray_index_merge H10.
@@ -578,7 +570,6 @@ Section WithParameters.
           rewrite ?Znat.Z2Nat.id by eapply word.unsigned_range; blia. }
         right. right. split; eauto using TracePredicate.any_app_more. } }
 
-    all: repeat letexists; split; repeat straightline.
     all: eexists; split;
       [repeat match goal with |- context [?x] => match type of x with list _ => subst x end end;
       rewrite ?List.app_assoc; eauto|].

diff --git a/bedrock2/src/bedrock2Examples/stackalloc.v b/bedrock2/src/bedrock2Examples/stackalloc.v
@@ -90,10 +90,7 @@ Section WithParameters.
     set [Byte.byte.of_Z (word.unsigned v0); b0; b1; b2] as ss in *.
     assert (length ss = Z.to_nat 4) by reflexivity.
     repeat straightline.
-    cbn.
-    eexists; split; [exact eq_refl|].
-    subst R. subst m1.
-    eexists _, _; Tactics.ssplit; eauto.
+    Tactics.ssplit; eauto.
 
     subst v. subst v1. subst ss.
     eapply Properties.word.unsigned_inj.