refactor Scalars to use $@

Author: andres-erbsen

rupicola

@@ -639,7 +639,7 @@ Section with_parameters.
                                 (expr.op bopname.add a_var
                                                  (expr.op bopname.mul idx_var sz_word)))
                      scratch.
-  Proof using T_Fits_ok locals_ok mem_ok word_ok.
+  Proof using BW T_Fits_ok locals_ok mem_ok word_ok.
     unfold broadcast_expr; intuition idtac.
     repeat straightline.
     exists a_ptr; intuition idtac.
@@ -703,7 +703,7 @@ Section with_parameters.
            (expr.op bopname.add a_var
               (expr.op bopname.mul idx_var sz_word)))
         a_data.
-  Proof using T_Fits_ok locals_ok mem_ok word_ok.
+  Proof using T_Fits_ok locals_ok mem_ok word_ok BW.
     unfold broadcast_expr; intuition idtac.
     repeat straightline.
     exists a_ptr; intuition idtac.
@@ -799,25 +799,11 @@ Section with_parameters.
       reflexivity.
     }
     intros ptr t m.
-    split.
-    {
-      intro H.
-      unfold  truncated_word, truncated_scalar.
-      cbn.
-      rewrite word.unsigned_of_Z_nowrap.
-      rewrite word.byte_of_Z_unsigned.
-      ecancel_assumption.
-      apply byte_in_word_bounds.
-    }
-    {
-      intro H.
-      unfold truncated_word, truncated_scalar in H.
-      cbn in H.
-      rewrite word.unsigned_of_Z_nowrap in H.
-      rewrite word.byte_of_Z_unsigned in H.
-      ecancel_assumption.
-      apply byte_in_word_bounds.
-    }
+    cbv [truncated_word truncated_scalar].
+    simpl le_split.
+    rewrite word.unsigned_of_Z_nowrap, word.byte_of_Z_unsigned by apply byte_in_word_bounds.
+    rewrite OfListWord.map.of_list_word_singleton.
+    split; cbv [sepclause_of_map ptsto] in *; auto.
   Qed.
 
 

src/Bedrock/End2End/RupicolaCrypto/Broadcast.v

@@ -675,8 +675,10 @@ Section Scalars.
              (LittleEndianList.le_split (Z.to_nat bytes_per_word)
              (word.unsigned x))).
   Proof.
-    unfold scalar, truncated_word, truncated_scalar, littleendian, ptsto_bytes.ptsto_bytes.
-    rewrite HList.tuple.to_list_of_list; reflexivity.
+    unfold scalar, truncated_word, truncated_scalar.
+    symmetry; eapply array1_iff_eq_of_list_word_at; trivial.
+    rewrite length_le_split.
+    case BW as [ [ -> | -> ] ]; cbv; discriminate.
   Qed.
 
   Lemma truncated_scalar_one_ptsto_iff1 :
@@ -685,8 +687,12 @@ Section Scalars.
         (truncated_scalar access_size.one addr x)
         (ptsto addr (Byte.byte.of_Z x)).
   Proof. intros.
-    unfold scalar, truncated_word, truncated_scalar, littleendian, ptsto_bytes.ptsto_bytes.
-    rewrite HList.tuple.to_list_of_list. unfold Memory.bytes_per, le_split, array.
+    unfold scalar, truncated_word, truncated_scalar.
+    etransitivity. {
+      symmetry; eapply array1_iff_eq_of_list_word_at; trivial.
+      rewrite length_le_split.
+      case BW as [ [ -> | -> ] ]; cbv; discriminate. }
+    unfold Memory.bytes_per, le_split, array.
     cancel.
   Qed.
 

src/Bedrock/Field/Common/Util.v

@@ -18,7 +18,7 @@ Require Import Crypto.Bedrock.Field.Common.Arrays.ByteBounds.
 Local Open Scope Z_scope.
 
 Section Bignum.
-  Import bedrock2.Memory bedrock2.ptsto_bytes.
+  Import bedrock2.Memory.
   Context  {width} {word : Interface.word width} {mem : map.map word Init.Byte.byte}.
 
   Local Notation k := (bytes_per_word width).

src/Bedrock/Field/Synthesis/Generic/Bignum.v

@@ -585,11 +585,6 @@ Section FElems.
 
         instantiate (2 := pout). instantiate (1 := Rr).
 
-        About fe25519.
-        Print UnOp.
-        Print Build_UnOp.
-        Search UnOp.
-
         eapply H6.
         compile_step.