bump coqutil

and adapt to rewrite bug that got exposed by not importing Word
mit-plv · Apr 5, 2024 · 75c4008 · 75c4008
1 parent 4421d54
commit 75c4008
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 2 deletions.
diff --git a/compiler/src/compiler/memory_mapped_ext_calls_compiler.v b/compiler/src/compiler/memory_mapped_ext_calls_compiler.v
@@ -520,7 +520,8 @@ Section MMIO.
         - eapply map.disjoint_putmany_l. split. 1: assumption.
           apply map.disjoint_comm. assumption. }
       { cbn. rewrite word.unsigned_of_Z_nowrap by lia.
-        rewrite LittleEndian.split_combine. assumption. }
+        replace (LittleEndian.split n (LittleEndian.combine n v)) with v.
+        1: assumption. symmetry. apply LittleEndian.split_combine. }
       lazymatch goal with
       | HO: outcome _ _, H: forall _ _, outcome _ _ -> _ |- _ =>
           specialize H with (1 := HO); destruct H as (l' & Hp & HPost)

diff --git a/deps/coqutil b/deps/coqutil
diff --git a/processor/src/processor/KamiRiscvStep.v b/processor/src/processor/KamiRiscvStep.v
@@ -38,6 +38,10 @@ Require Import processor.Consistency.
 
 Local Open Scope Z_scope.
 
+(* workaround for `rewrite` bug:
+   https://github.com/coq/coq/issues/1811#issuecomment-1320064508 *)
+Local Set Keyed Unification.
+
 Local Ltac subst_after_destr H ::= idtac.
 
 (** Consistency between the Kami word and the Z-based word *)