Fix some code according to bump of bedrock2

Author: JasonGross

src/Bedrock/Field/Interface/Representation.v

@@ -18,7 +18,8 @@ Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
 
 Section Representation.
   Context {p : Types.parameters} {field_parameters : FieldParameters}
-          {p_ok : Types.ok}.
+          {p_ok : Types.ok}
+          (width_ge_32 : 32 <= Semantics.width).
   Context (n : nat) (weight : nat -> Z)
           (loose_bounds tight_bounds : list (option zrange))
           (relax_bounds :
@@ -73,7 +74,7 @@ Section Representation.
       { match goal with
           | H : Array.array _ _ _ _ _ |- _ =>
             eapply Bignum_of_bytes with (n0:=n) in H;
-              [ destruct H | nia ]
+              [ destruct H | nia.. ]
         end.
         eexists; eauto. }
       {

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

@@ -30,7 +30,8 @@ Section Bignum.
     sep (emp (length x = n_bytes)) (array ptsto (word.of_Z 1) px x).
 
   Section Proofs.
-    Context {ok : Types.ok}.
+    Context {ok : Types.ok}
+            (width_ge_32 : 32 <= Semantics.width).
     Existing Instance semantics_ok.
 
     (* TODO: factor this proof into a more general form that says if subarrays
@@ -50,7 +51,7 @@ Section Bignum.
         cbn [array length] in *. sepsimpl; eauto. }
       { rewrite <-(firstn_skipn (Z.to_nat word_size_in_bytes) bs).
         rewrite array_append.
-        rewrite Scalars.scalar_of_bytes with (l:=List.firstn _ _).
+        rewrite Scalars.scalar_of_bytes with (l:=List.firstn _ _); try assumption.
         2:{
           rewrite word_size_in_bytes_eq in *.
           etransitivity;

src/Bedrock/Field/Translation/Proofs/LoadStoreList.v

@@ -297,7 +297,8 @@ Section LoadStoreList.
     { cbv [Memory.load].
       erewrite load_Z_of_sep; [ reflexivity | ].
       ecancel_assumption. }
-    { rewrite Z.land_ones by auto with zarith.
+    { unfold truncate_Z.
+      rewrite Z.land_ones by auto with zarith.
       rewrite Z.mod_small; [ reflexivity | ].
       rewrite <-hd_skipn_nth_default.
       match goal with H : base_access_sizes_good _ |- _ =>