workaround needed because itauto lia makes proofs depend on

unused section variables See https://gitlab.inria.fr/fbesson/itauto/-/issues/3
mit-plv · Aug 27, 2020 · 5316184 · 5316184
1 parent db0986f
commit 5316184
Show file tree

Hide file tree

Showing 4 changed files with 58 additions and 48 deletions.
diff --git a/bedrock2/src/bedrock2/Scalars.v b/bedrock2/src/bedrock2/Scalars.v
@@ -37,6 +37,7 @@ Section Scalars.
     (Hsep : sep (truncated_scalar sz addr value) R m)
     : Memory.load_Z sz m addr = Some (Z.land value (Z.ones (Z.of_nat (bytes_per (width:=width) sz)*8))).
   Proof.
+    clear - word_ok mem mem_ok Hsep.
     cbv [load scalar littleendian load_Z] in *.
     erewrite load_bytes_of_sep by exact Hsep; apply f_equal.
     rewrite LittleEndian.combine_split.
@@ -56,6 +57,7 @@ Section Scalars.
     (Hsep : sep (scalar addr value) R m)
     : Memory.load Syntax.access_size.word m addr = Some value.
   Proof.
+    clear - word_ok mem mem_ok Hsep.
     cbv [load].
     erewrite load_Z_of_sep by exact Hsep; f_equal.
     cbv [bytes_per bytes_per_word].
@@ -87,6 +89,7 @@ Section Scalars.
     (Hsep : sep (scalar16 addr value) R m)
     : Memory.load Syntax.access_size.two m addr = Some (word.of_Z (word.unsigned value)).
   Proof.
+    clear - word_ok word16_ok mem mem_ok Hsep.
     cbv [load].
     erewrite load_Z_of_sep by exact Hsep; f_equal.
     cbv [bytes_per].
@@ -99,6 +102,7 @@ Section Scalars.
     (Hsep : sep (scalar32 addr value) R m)
     : Memory.load Syntax.access_size.four m addr = Some (word.of_Z (word.unsigned value)).
   Proof.
+    clear - word_ok word32_ok mem mem_ok Hsep.
     cbv [load].
     erewrite load_Z_of_sep by exact Hsep; f_equal.
     cbv [bytes_per].
@@ -143,6 +147,7 @@ Section Scalars.
     (Hpost : forall m, sep (scalar16 addr (word.of_Z (word.unsigned value))) R m -> post m)
     : exists m1, Memory.store Syntax.access_size.two m addr value = Some m1 /\ post m1.
   Proof.
+    clear - word_ok word16_ok mem mem_ok Hsep Hpost.
     cbv [scalar16 truncated_scalar littleendian ptsto_bytes bytes_per tuple.to_list LittleEndian.split PrimitivePair.pair._1 PrimitivePair.pair._2 array] in Hsep, Hpost.
     eapply (store_bytes_of_sep _ 2 (PrimitivePair.pair.mk _ (PrimitivePair.pair.mk _ tt))); cbn; [ecancel_assumption|].
     cbv [LittleEndian.split].
@@ -161,6 +166,7 @@ Section Scalars.
     (Hpost : forall m, sep (scalar32 addr (word.of_Z (word.unsigned value))) R m -> post m)
     : exists m1, Memory.store Syntax.access_size.four m addr value = Some m1 /\ post m1.
   Proof.
+    clear - word_ok word32_ok mem mem_ok Hsep Hpost.
     cbv [scalar32 truncated_scalar littleendian ptsto_bytes bytes_per tuple.to_list LittleEndian.split PrimitivePair.pair._1 PrimitivePair.pair._2 array] in Hsep, Hpost.
     eapply (store_bytes_of_sep _ 4 (PrimitivePair.pair.mk _ (PrimitivePair.pair.mk _ (PrimitivePair.pair.mk _ (PrimitivePair.pair.mk _ tt))))); cbn; [ecancel_assumption|].
     cbv [LittleEndian.split].
@@ -184,6 +190,7 @@ Section Scalars.
     Lift1Prop.iff1 (array ptsto (word.of_Z 1) a l)
                    (scalar16 a (word.of_Z (LittleEndian.combine _ (HList.tuple.of_list l)))).
   Proof.
+    clear - word_ok word16_ok mem mem_ok H.
     do 2 (destruct l as [|?x l]; [discriminate|]). destruct l; [|discriminate].
     cbv [scalar16 truncated_scalar littleendian ptsto_bytes.ptsto_bytes].
     eapply Morphisms.eq_subrelation; [exact _|].
@@ -200,6 +207,7 @@ Section Scalars.
     Lift1Prop.iff1 (array ptsto (word.of_Z 1) a l)
                    (scalar32 a (word.of_Z (LittleEndian.combine _ (HList.tuple.of_list l)))).
   Proof.
+    clear - word_ok word32_ok mem mem_ok H.
     do 4 (destruct l as [|?x l]; [discriminate|]). destruct l; [|discriminate].
     cbv [scalar32 truncated_scalar littleendian ptsto_bytes.ptsto_bytes].
     eapply Morphisms.eq_subrelation; [exact _|].
@@ -215,6 +223,7 @@ Section Scalars.
     Lift1Prop.iff1 (array ptsto (word.of_Z 1) a l)
                    (scalar a (word.of_Z (LittleEndian.combine _ (HList.tuple.of_list l)))).
   Proof.
+    clear - word_ok mem mem_ok H.
     cbv [scalar truncated_scalar littleendian ptsto_bytes]. subst width.
     replace (bytes_per Syntax.access_size.word) with (length l). 2: {
       unfold bytes_per, bytes_per_word. clear.

diff --git a/compiler/src/compiler/FlatToRiscvCommon.v b/compiler/src/compiler/FlatToRiscvCommon.v
@@ -230,6 +230,34 @@ Section WithParameters.
          stack_needed act <= N *)
       fits_stack M N e (SInteract binds act args).
 
+  Lemma stackalloc_words_nonneg: forall s,
+      0 <= stackalloc_words s.
+  Proof.
+    assert (bytes_per_word = 4 \/ bytes_per_word = 8). {
+      unfold bytes_per_word. destruct width_cases as [E | E]; rewrite E; cbv; auto.
+    }
+    induction s; simpl; Z.div_mod_to_equations; blia.
+  Qed.
+
+  Lemma framesize_nonneg: forall argvars resvars body,
+      0 <= framelength (argvars, resvars, body).
+  Proof.
+    intros. unfold framelength.
+    pose proof (stackalloc_words_nonneg body).
+    assert (bytes_per_word = 4 \/ bytes_per_word = 8). {
+      unfold bytes_per_word. destruct width_cases as [E | E]; rewrite E; cbv; auto.
+    }
+    Z.div_mod_to_equations.
+    blia.
+  Qed.
+
+  Lemma fits_stack_nonneg: forall M N e s,
+      fits_stack M N e s ->
+      0 <= M /\ 0 <= N.
+  Proof.
+    induction 1; try blia. pose proof (@framesize_nonneg argnames retnames body). blia.
+  Qed.
+
   (* Ghost state used to describe low-level state introduced by the compiler.
      Called "ghost constants" because after executing a piece of code emitted by
      the compiler, these values should still be the same.

diff --git a/compiler/src/compiler/FlatToRiscvFunctions.v b/compiler/src/compiler/FlatToRiscvFunctions.v
@@ -48,34 +48,6 @@ Section Proofs.
 
   Local Notation RiscvMachineL := MetricRiscvMachine.
 
-  Lemma stackalloc_words_nonneg: forall s,
-      0 <= stackalloc_words s.
-  Proof.
-    assert (bytes_per_word = 4 \/ bytes_per_word = 8). {
-      unfold bytes_per_word. destruct width_cases as [E | E]; rewrite E; cbv; auto.
-    }
-    induction s; simpl; Z.div_mod_to_equations; blia.
-  Qed.
-
-  Lemma framesize_nonneg: forall argvars resvars body,
-      0 <= framelength (argvars, resvars, body).
-  Proof.
-    intros. unfold framelength.
-    pose proof (stackalloc_words_nonneg body).
-    assert (bytes_per_word = 4 \/ bytes_per_word = 8). {
-      unfold bytes_per_word. destruct width_cases as [E | E]; rewrite E; cbv; auto.
-    }
-    Z.div_mod_to_equations.
-    blia.
-  Qed.
-
-  Lemma fits_stack_nonneg: forall M N e s,
-      fits_stack M N e s ->
-      0 <= M /\ 0 <= N.
-  Proof.
-    induction 1; try blia. pose proof (@framesize_nonneg argnames retnames body). blia.
-  Qed.
-
   (* high stack addresses     | stackframe of main             \
                               ...                               \
     g|                        ---                                }- stuffed into R

diff --git a/processor/src/processor/Consistency.v b/processor/src/processor/Consistency.v
@@ -35,26 +35,6 @@ Qed.
 
 Section FetchOk.
   Local Hint Resolve (@KamiWord.WordsKami width width_cases): typeclass_instances.
-  Context {mem: map.map word byte}.
-
-  (* [instrMemSizeLg] is the log number of instructions in the instruction cache.
-   * If the instruction base address is just 0, then the address range for
-   * the instructions is [0 -- 4 * 2^(instrMemSizeLg)].
-   *)
-  Variables instrMemSizeLg memSizeLg: Z.
-  Hypothesis (HinstrMemBound: 3 <= instrMemSizeLg <= width - 2).
-  Local Notation ninstrMemSizeLg := (Z.to_nat instrMemSizeLg).
-  Local Notation nmemSizeLg := (Z.to_nat memSizeLg).
-  Local Notation nwidth := (Z.to_nat width).
-  Local Notation width_inst_valid := (width_inst_valid HinstrMemBound).
-
-  Definition instrMemSize: nat := NatLib.pow2 (2 + Z.to_nat instrMemSizeLg).
-
-  Definition pc_related (kpc rpc: kword width): Prop :=
-    kpc = rpc.
-
-  Definition AddrAligned (addr: kword width) :=
-    split1 2 (nwidth - 2) addr = WO~0~0.
 
   Fixpoint alignedXAddrsRange (base: nat) (n: nat): XAddrs :=
     match n with
@@ -80,6 +60,27 @@ Section FetchOk.
     - etransitivity; [eauto|blia].
   Qed.
 
+  Context {mem: map.map word byte}.
+
+  (* [instrMemSizeLg] is the log number of instructions in the instruction cache.
+   * If the instruction base address is just 0, then the address range for
+   * the instructions is [0 -- 4 * 2^(instrMemSizeLg)].
+   *)
+  Variables instrMemSizeLg memSizeLg: Z.
+  Hypothesis (HinstrMemBound: 3 <= instrMemSizeLg <= width - 2).
+  Local Notation ninstrMemSizeLg := (Z.to_nat instrMemSizeLg).
+  Local Notation nmemSizeLg := (Z.to_nat memSizeLg).
+  Local Notation nwidth := (Z.to_nat width).
+  Local Notation width_inst_valid := (width_inst_valid HinstrMemBound).
+
+  Definition instrMemSize: nat := NatLib.pow2 (2 + Z.to_nat instrMemSizeLg).
+
+  Definition pc_related (kpc rpc: kword width): Prop :=
+    kpc = rpc.
+
+  Definition AddrAligned (addr: kword width) :=
+    split1 2 (nwidth - 2) addr = WO~0~0.
+
   (* set of executable addresses in the kami processor *)
   Definition kamiXAddrs: XAddrs :=
     alignedXAddrsRange 0 instrMemSize.