various cleanup: typos, whitespace, comments, etc

bedrock2/src/bedrock2/FE310CSemantics.v

@@ -49,20 +49,20 @@ Section WithParameters.
     intros.
     all :
     repeat match goal with
-        | H : context[(?x =? ?y)%string] |- _ =>
-            destruct (x =? y)%string in *
-        | H: exists _, _ |- _ => destruct H
-        | H: _ /\ _ |- _ => destruct H
-        | H: False |- _ => destruct H
-        end; subst;
-      repeat match goal with
-        | H: _ :: _ = _ :: _ |- _ => injection H; intros; subst; clear H
-        end;
-      eauto 8 using Properties.map.same_domain_refl.
+      | H : context[(?x =? ?y)%string] |- _ =>
+          destruct (x =? y)%string in *
+      | H: exists _, _ |- _ => destruct H
+      | H: _ /\ _ |- _ => destruct H
+      | H: False |- _ => destruct H
+    end; subst;
+    repeat match goal with
+      | H: _ :: _ = _ :: _ |- _ => injection H; intros; subst; clear H
+    end;
+    eauto 8 using Properties.map.same_domain_refl.
   Qed.
 
   Global Instance ext_spec : Semantics.ExtSpec := deleakaged_ext_spec.
-  Global Instance ext_spec_ok : Semantics.ext_spec.ok sem_ext_spec := deleakaged_ext_spec_ok.
+  Global Instance ext_spec_ok : Semantics.ext_spec.ok ext_spec := deleakaged_ext_spec_ok.
 
   Global Instance locals: Interface.map.map String.string word := SortedListString.map _.
   Global Instance env: Interface.map.map String.string (list String.string * list String.string * cmd) :=

bedrock2/src/bedrock2/MetricLeakageSemantics.v

@@ -2,6 +2,7 @@ Require Import coqutil.sanity coqutil.Byte.
 Require Import coqutil.Tactics.fwd.
 Require Import coqutil.Map.Properties.
 Require coqutil.Map.SortedListString.
+Require Import coqutil.Z.Lia.
 Require Import bedrock2.Syntax coqutil.Map.Interface coqutil.Map.OfListWord.
 Require Import BinIntDef coqutil.Word.Interface coqutil.Word.Bitwidth.
 Require Export bedrock2.Memory.
@@ -261,8 +262,6 @@ Module exec. Section WithParams.
         eauto 10.
   Qed.
 
-    Require Import coqutil.Z.Lia.
-
   Lemma eval_expr_extends_trace :
     forall e0 m l mc k v mc' k',
     eval_expr m l e0 k mc = Some (v, k', mc') ->
@@ -401,7 +400,6 @@ Module exec. Section WithParams.
     (forall k', pick_sp1 (k' ++ k) = pick_sp2 (k' ++ k)) ->
     exec (pick_sp := pick_sp2) s k t m l mc post.
   Proof.
-    Set Printing Implicit.
     intros H1 pick_sp2. induction H1; intros; try solve [econstructor; eauto].
     - econstructor; eauto. intros. replace (pick_sp1 k) with (pick_sp2 k) in *.
       { subst a. eapply weaken.
@@ -640,7 +638,7 @@ Section WithParams.
       destruct IHarges as (mc'' & IH). rewrite IH. eauto.
   Qed.
 
-  Definition deleakaged_ext_spec :=
+  Definition deleakaged_ext_spec : Semantics.ExtSpec :=
     fun t mGive a args post => ext_spec t mGive a args (fun mReceive resvals klist => post mReceive resvals).
 
   Lemma deleakaged_ext_spec_ok {ext_spec_ok: ext_spec.ok ext_spec}:
@@ -652,7 +650,8 @@ Section WithParams.
   Qed.    
 
   Context (e: env).
-  Instance sem_ext_spec : Semantics.ExtSpec := deleakaged_ext_spec.
+  Existing Instance deleakaged_ext_spec.
+  Existing Instance deleakaged_ext_spec_ok.
 
   Lemma to_plain_exec: forall c t m l post,
       Semantics.exec e c t m l post ->

bedrock2/src/bedrock2Examples/ct.v

@@ -20,7 +20,7 @@ Import LeakageProgramLogic.Coercions.
 Section WithParameters.
   Context {word: word.word 32} {mem: Interface.map.map word Byte.byte}.
   Context {word_ok : word.ok word} {mem_ok : Interface.map.ok mem}.
-  Context {pick_sp: PickSp}. Locate "fnspec!".
+  Context {pick_sp: PickSp}.
 
 #[global] Instance ctspec_of_div3329 : spec_of "div3329" :=
     fnspec! exists f, "div3329" x ~> ret,

compiler/src/compiler/DeadCodeElim.v

@@ -174,8 +174,7 @@ Section WithArguments1.
         * eapply H7p0p1.
         * solve_compile_post.
           -- agree_on_solve. repeat listset_to_set. subset_union_solve.
-          -- simpl. rewrite H0. 
-                 rewrite H7p5. reflexivity.
+          -- simpl. rewrite H0. rewrite H7p5. reflexivity.
     - intros.
       eapply agree_on_find in H3; fwd.
       destr (existsb (eqb x) used_after); fwd.
@@ -308,7 +307,7 @@ Section WithArguments1.
         unfold compile_post in *.
         fwd.
         apply agree_on_eval_bcond.
-        repeat listset_to_set. Check agree_on_union.
+        repeat listset_to_set.
         apply agree_on_union in H4p1.
         fwd.
         eapply agree_on_subset; [ | eapply H4p1p1 ].
@@ -318,7 +317,7 @@ Section WithArguments1.
       destruct (eval_bcond l' cond) as [b|] eqn:E; try congruence. exists b.
       split; [reflexivity|]. split.
       { intros. subst. solve_compile_post. rewrite <- app_assoc. simpl. rewrite H4p5.
-        cbv [CustomFix.Let_In_pf_nd]. rewrite List.skipn_app_r by reflexivity.
+        cbv [FixEq.Let_In_pf_nd]. rewrite List.skipn_app_r by reflexivity.
         simpl. rewrite <- app_assoc. reflexivity. }
       { intros. subst.
         eapply exec.weaken.
@@ -329,7 +328,7 @@ Section WithArguments1.
           - intros. rewrite associate_one_left. rewrite app_assoc. rewrite H8.
             repeat (rewrite rev_app_distr || cbn [rev List.app] || rewrite <- app_assoc).
             rewrite dfix_step. cbn [stmt_leakage_body]. rewrite H4p5.
-            cbv [CustomFix.Let_In_pf_nd]. rewrite List.skipn_app_r by reflexivity.
+            cbv [FixEq.Let_In_pf_nd]. rewrite List.skipn_app_r by reflexivity.
             reflexivity.
         }
         cbv beta. intros. fwd.
@@ -338,12 +337,12 @@ Section WithArguments1.
           intros. rewrite associate_one_left. repeat rewrite app_assoc. rewrite H8.
           repeat (rewrite rev_app_distr || cbn [rev List.app] || rewrite <- app_assoc).
           f_equal. f_equal. rewrite dfix_step. cbn [stmt_leakage_body]. rewrite H4p5.
-          cbv [CustomFix.Let_In_pf_nd]. rewrite List.skipn_app_r by reflexivity.
+          cbv [FixEq.Let_In_pf_nd]. rewrite List.skipn_app_r by reflexivity.
           f_equal. f_equal. rewrite H6p5. rewrite List.skipn_app_r by reflexivity.
           reflexivity. }
         cbv beta. intros. fwd. solve_compile_post. cbn [stmt_leakage_body].
         repeat (rewrite rev_app_distr || cbn [rev List.app] || rewrite <- app_assoc).
-        rewrite H4p5. f_equal. cbv [CustomFix.Let_In_pf_nd].
+        rewrite H4p5. f_equal. cbv [FixEq.Let_In_pf_nd].
         rewrite List.skipn_app_r by reflexivity. f_equal. rewrite H6p5.
         rewrite List.skipn_app_r by reflexivity. rewrite H6p9. reflexivity. }
     - intros.

compiler/src/compiler/DeadCodeElimDef.v

@@ -1,3 +1,6 @@
+Require Import Coq.Init.Wf Wellfounded.
+Require Import compiler.FixEq.
+Require Import bedrock2.LeakageSemantics.
 Require Import compiler.FlatImp.
 Require Import Coq.Lists.List. Import ListNotations.
 Require Import bedrock2.Syntax.
@@ -15,8 +18,6 @@ Require Import coqutil.Tactics.fwd.
 Require Import Coq.Logic.PropExtensionality.
 Require Import Coq.Logic.FunctionalExtensionality.
 
-Require Import compiler.CustomFix.
-
 Section WithArguments1.
   Context {width: Z}.
   Context {BW: Bitwidth.Bitwidth width }.
@@ -468,12 +469,13 @@ Section WithArguments1.
           SSkip
     | SStackalloc x n body =>
         SStackalloc x n (dce body u)
-        (* The below optimization probably can be made to work;
-           on past attempt, got stuck at goals about `Memory.anybytes n a map.empty` *)
-        (* if (existsb (eqb x) (live body u)) then
-          SStackalloc x n (dce body u)
-        else
-          (dce body u) *)
+    (* Finite address spaces are subtle, so the below optimization is unsound.  See
+       https://github.com/mit-plv/bedrock2/pull/393#discussion_r1685645179*)
+
+    (* if (existsb (eqb x) (live body u)) then
+       SStackalloc x n (dce body u)
+       else
+       (dce body u) *)
     | SLit x _ =>
         if (existsb (eqb x) u) then
           s
@@ -505,9 +507,6 @@ Section WithArguments1.
     | SSkip => SSkip
     end.
 
-  Require Import compiler.CustomFix.
-  Require Import bedrock2.LeakageSemantics.
-  Require Import Coq.Init.Wf Wellfounded.
   Definition tuple : Type := leakage * stmt var * list var * (leakage (*skip*) -> leakage (*everything*)).
   Definition project_tuple (tup : tuple) :=
     let '(kH, s, u, f) := tup in (length kH, s).
@@ -519,26 +518,6 @@ Section WithArguments1.
     cbv [lt_tuple]. apply wf_inverse_image. apply lt_tuple'_wf.
   Defined.
 
-  (*Because high-level pick_sp is always the result of applying low-level pick_sp to
-    low-level trace, this function doesn't need to return a triple
-    (high-level-trace-to-skip, low-level-trace-so-far, high-level-pick-sp-output),
-    like the FlatToRiscv function does.  It suffices to return the first two elts
-    of the tuple.  Nope never mind, we still need the triple, because we need to exit
-    immediately upon hitting a stackalloc; can't continue adding on low-level trace.
-    The third element of the triple could just be an 'error'/'quit'/'exit' boolean,
-    I suppose.  I guess I'll do that?
-
-    We wouldn't have this problem if this thing were written in CPS...
-    But that comes with its own inconveniences in proof-writing:
-    I recall a lot of fumbling around with existential arguments to the continuation.
-    Also I would have to use the custom fix thing (or unnecessarily use functional
-    extensionality) to prove the fixpoint equation.  And I suppose it makes the thing
-    harder to understand for no good reason.
-
-    I guess the best option is the 'error'/short_circuit boolean.
-
-    Nope, I changed my mind.  CPS is good.
-   *)
   Definition stmt_leakage_body
     (e: env)
     (tup : leakage * stmt var * list var * (leakage -> leakage))
@@ -600,14 +579,14 @@ Section WithArguments1.
                     | leak_unit :: kH' =>
                         fun _ => leak_unit :: dtransform_stmt_trace (kH', body, u,
                                   fun skip => f (leak_unit :: skip)) _
-                    | _ => fun _ => nil (*we don't call the continuation here.  wow, that was so much easier than carrying around the 'error' flag*)
+                    | _ => fun _ => nil
                     end eq_refl
               | SLit x _ => fun _ => f nil
               | SOp x op _ _ =>
                   fun _ =>
                     (*copied from spilling.
-                      I should do a leak_list for ops (or just make every op leak two words)
-                      so I don't have to deal with this nonsense*)
+                      Maybe I should do a leak_list for ops (or just make every op leak two words)
+                      to avoid this awkwardness*)
                     let skip :=
                       match op with
                       | Syntax.bopname.divu