moving the device_implements_state_machine instance for IncrementWait

to the file where the IncrementWait Cava circuit is defined,
splitting up a two-field parameter record along the way to avoid
having to define more parameter rewrapping instances, running into
a nasty usability issue (mit-plv/bedrock2#193)
caused by Hint Mode + on map.map.

investigations/bedrock2/IncrementWait/IncrementWaitProperties.v

@@ -27,9 +27,9 @@ Import Syntax.Coercions List.ListNotations.
 Local Open Scope Z_scope.
 
 Section Proofs.
-  Context {p : parameters} {p_ok : parameters.ok p}
+  Context {word: word.word 32} {word_ok: word.ok word}
+          {mem: map.map word Byte.byte} {mem_ok: Interface.map.ok mem}
           {circuit_spec : circuit_behavior}.
-  Import parameters.
 
   Global Instance spec_of_put_wait_get : spec_of "put_wait_get" :=
     fun function_env =>
@@ -49,8 +49,8 @@ Section Proofs.
                 /\ rets = [proc input]).
 
   Local Ltac simplify_implicits :=
-    change Semantics.word with parameters.word in *;
-    change Semantics.mem with parameters.mem in *;
+    change Semantics.word with word in *;
+    change Semantics.mem with mem in *;
     change Semantics.width with 32 in *.
 
   Lemma execution_unique (t : trace) s1 s2 :

investigations/bedrock2/IncrementWait/IncrementWaitSemantics.v

@@ -26,23 +26,10 @@ Class circuit_behavior :=
   { ncycles_processing : nat
   }.
 
-Module parameters.
-  Class parameters :=
-    { word :> Interface.word.word 32;
-      mem :> Interface.map.map word Byte.byte;
-    }.
-
-  Class ok (p : parameters) :=
-    { word_ok :> word.ok word; (* for impl of mem below *)
-      mem_ok :> Interface.map.ok mem; (* for impl of mem below *)
-    }.
-End parameters.
-Notation parameters := parameters.parameters.
-
 Section WithParameters.
-  Context {p : parameters} {p_ok : parameters.ok p}.
+  Context {word: word.word 32} {word_ok: word.ok word}
+          {mem: map.map word Byte.byte} {mem_ok: Interface.map.ok mem}.
   Context {circuit_spec : circuit_behavior}.
-  Import parameters.
 
   Local Notation bedrock2_event := (mem * string * list word * (mem * list word))%type.
   Local Notation bedrock2_trace := (list bedrock2_event).

investigations/bedrock2/IncrementWait/IncrementWaitToCava.v

@@ -16,11 +16,6 @@ Definition binary: list byte := Eval compute in Pipeline.instrencode put_wait_ge
 
 Axiom TODO: False.
 
-Instance DI:  MMIOToCava.device_implements_state_machine
-             counter_device
-             IncrementWaitSemantics.state_machine_parameters.
-Admitted.
-
 Theorem IncrementWait_end2end_correct: forall p_functions p_call mH Rdata Rexec R (* <-? *)
           (initialL: ExtraRiscvMachine counter_device) input output_placeholder sched,
     -2^19 <= word.signed (word.sub p_functions p_call) < 2^19 ->
@@ -45,7 +40,6 @@ Proof.
   refine (bedrock2_and_cava_system_correct
             _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);
     try eassumption.
-  { exact IncrementWaitSemantics.state_machine_parameters_ok. }
   { apply sameset_ref. }
   { exact funcs_valid. }
   { apply List.dedup_NoDup_iff with (aeqb_spec:=String.eqb_spec). reflexivity. }
@@ -70,7 +64,6 @@ Proof.
     eapply MMIOToCava.initial_state_is_reset_state.
     reflexivity. }
   { refine (@WeakestPreconditionProperties.Proper_cmd _ StateMachineSemantics.ok _ _ _ _ _ _ _ _ _ _ _).
-    1: exact IncrementWaitSemantics.state_machine_parameters_ok.
     1: eapply WeakestPreconditionProperties.Proper_call.
     2: {
       eapply main_correct. 1: eassumption.

investigations/bedrock2/IncrementWait/IncrementWaitToRiscV.v

@@ -36,14 +36,6 @@ Instance p : MMIO.parameters :=
      MMIO.funname_env_ok := SortedListString.ok;
   |}.
 
-Instance semantics_params : IncrementWaitSemantics.parameters := {|
-  IncrementWaitSemantics.parameters.word := MMIO.word;
-  IncrementWaitSemantics.parameters.mem := MMIO.mem |}.
-
-Instance semantics_params_ok : IncrementWaitSemantics.parameters.ok _ := {|
-  IncrementWaitSemantics.parameters.word_ok := _;
-  IncrementWaitSemantics.parameters.mem_ok := _ |}.
-
 Existing Instances Words32 compilation_params FlatToRiscv_params.
 
 Definition heap_start: Utility.word := word.of_Z (4*2^10).

investigations/bedrock2/IncrementWait/IncrementWaitToRiscVProperties.v

@@ -26,14 +26,17 @@ Local Open Scope string_scope.
 Local Hint Resolve FlattenExpr.mk_Semantics_params_ok FlattenExpr_hyps : typeclass_instances.
 
 Definition post_main
-           (input output_placeholder : parameters.word) R
+           (input output_placeholder : Semantics.word) R
            (t' : trace) (m' : Semantics.mem) : Prop :=
   (* trace is valid and leads to IDLE state *)
   execution (p := state_machine_parameters) t' IDLE
   /\ (scalar (word.of_Z input_ptr) input
      * scalar (word.of_Z output_ptr) (proc input)
      * R)%sep m'.
 
+(* https://github.com/mit-plv/bedrock2/issues/193 *)
+Global Hint Mode map.map - - : typeclass_instances.
+
 Lemma main_correct
       fs input output_placeholder
       R (t : @trace semantics_parameters) m l :
@@ -68,7 +71,7 @@ Proof.
   subst a2.
   use_sep_assumption.
   cancel.
-  cancel_seps_at_indices 0%nat 1%nat. 1: reflexivity.
+  cancel_seps_at_indices 0%nat 0%nat. 1: reflexivity.
   reflexivity.
 Qed.
 

investigations/bedrock2/RiscvMachineWithCavaDevice/DetIncrMachine.v

@@ -104,6 +104,8 @@ Require Import coqutil.Map.Interface.
 Require Import coqutil.Map.Properties.
 Require Import Bedrock2Experiments.RiscvMachineWithCavaDevice.InternalMMIOMachine.
 Require Import Bedrock2Experiments.IncrementWait.Constants.
+Require Import Bedrock2Experiments.IncrementWait.IncrementWaitSemantics.
+Require Import Bedrock2Experiments.RiscvMachineWithCavaDevice.MMIOToCava.
 
 Section WithParameters.
   Context {word: Interface.word 32} {word_ok: word.ok word}
@@ -118,4 +120,12 @@ Section WithParameters.
     device.maxRespDelay := 1;
   |}.
 
+  (* conservative upper bound matching the instance given in IncrementWaitToRiscv *)
+  Global Instance circuit_spec : circuit_behavior :=
+  {| ncycles_processing := 15%nat |}.
+
+  Global Instance cava_counter_satisfies_state_machine:
+    device_implements_state_machine counter_device state_machine_parameters.
+  Admitted.
+
 End WithParameters.

investigations/bedrock2/RiscvMachineWithCavaDevice/MMIOToCava.v

@@ -16,7 +16,6 @@ Require Import riscv.Utility.FreeMonad.
 Require Import riscv.Utility.runsToNonDet.
 Require Import riscv.Platform.MetricSane.
 Require Import Bedrock2Experiments.RiscvMachineWithCavaDevice.InternalMMIOMachine.
-Require Import Bedrock2Experiments.RiscvMachineWithCavaDevice.DetIncrMachine.
 Require Import Bedrock2Experiments.StateMachineMMIOSpec.
 
 Class device_implements_state_machine{word: word.word 32}{mem: map.map word Byte.byte}