Adding states to exec monad natively #1

Nils-Lauermann · 2025-01-29T16:32:15Z

No description provided.

tperami

This is good! If the whole Common lib doesn't build with that change, fix it, otherwise wait until tomorrow before fixing the rest of the codebase

tperami · 2025-01-29T16:41:33Z

Common/Exec.v

 Proof. unfold_decide. Qed.

 (** Create an execution from a set of results, e.g. to convert from pure
    non-determinism to Exec *)
-Definition Results {E A C} `{Elements A C} (s : C) : t E A := make (elements s) [].
+Definition Results {E A C} `{Elements A C} (s : C) : res () E A := make (map ((),.) (elements s)) [].


Looking at how this is used (in 2 places), this might be better if this was of type Exec.t St E A and forwarded the state into each result

tperami · 2025-01-29T16:43:36Z

Common/Exec.v

  make (e1.(results) ++ e2.(results)) (e1.(errors) ++ e2.(errors)).
 #[global] Typeclasses Opaque merge.
 Arguments merge : simpl never.

 (** Convert an execution into a list of results *)
-Definition to_result_list `(e : t E A) : list (result E A) :=
+Definition to_result_list `(e : res St E A) : list (result (St * E) (St * A)) :=
  map Ok e.(results) ++ map Error e.(errors).


This will generate a list (result (St * E) (St * A)), I think it would be better if it was list (St * result E A)

tperami · 2025-01-29T16:45:57Z

Common/Exec.v

-#[global] Instance choose_inst {E} : MChoose (t E) :=
-  λ '(ChooseFin n), make (enum (fin n)) [].
+#[global] Instance choose_inst {St E} : MChoose (t St E) :=
+  λ '(ChooseFin n) st, make (map (st,.) (enum (fin n))) [].


Now that this is a bit more complicated, maybe the implementation should just be Results (enum (fin n)). This would avoid duplicating the logic

tperami · 2025-01-29T17:20:37Z

Common/Exec.v

+  UnfoldElemOf x ((f <$> e) st) (∃ st' y, P (st', y) ∧ x = (st', f y)).
+Proof. tcclean. unfold elem_of, elem_of_results, fmap, fmap_inst.
+  destruct (e st) as [l es]. cbn. set_unfold.
+  cdestruct |- *** #CDestrSplitGoal; repeat eexists; eauto; naive_solver.


repeat eexists before eauto should not be necessary. Also having eauto in non-terminating position is not great. Doesn't naive_solver work alone? (It does on my machine)

tperami

LGTM except we need to think together how to update the promising part

tperami · 2025-02-10T13:05:06Z

Common/Exec.v

+  map (λ '(st,r), (st, Ok r)) e.(results) ++ map (λ '(st,err), (st, Error err)) e.(errors).
+
+Definition t {St E A} := St → res St E A.
+Arguments t : clear implicits.


You can remove the { and the Arguments here

tperami · 2025-02-10T13:08:28Z

Common/Exec.v

+
+(** Create an execution from a set of results, e.g. to convert from pure
+    non-determinism to Exec *)
+Definition Results {St E A C} `{Elements A C} (s : C) : t St E A := λ st, make (map (st,.) (elements s)) [].


tperami · 2025-02-10T13:08:42Z

Common/Exec.v

-#[global] Instance mbind_inst {E} : MBind (t E) :=
-  λ _ _ f e, foldr merge (make [] e.(errors)) (map f e.(results)).
+#[global] Instance mbind_inst {St E} : MBind (t St E) :=
+  λ _ _ f e st, let est := e st in foldr merge (make [] est.(errors)) (map (λ '(st', r), f r st') est.(results)).


tperami · 2025-02-10T13:10:01Z

Common/Exec.v

+#[global] Instance throw_inst {St E} : MThrow E (t St E) := λ _ e st, make [] [(st,e)].
+
+#[global] Instance choose_inst {St E} : MChoose (t St E) :=
+λ '(ChooseFin n), @Results _ _ (Fin.t n) _ _ (enum (fin n)).


Please use fin and not Fin.t everywhere for consistency

tperami · 2025-02-10T13:11:28Z

Common/Exec.v

+| MGet => λ s, (mret s : t St E St) s
+end.
+
+Lemma mdiscard_eq {St E A} : mdiscard =@{t St E A} (λ st, make [] []).


Ordering remark: This should be kept close to choose_inst, because it's derived from it directly

tperami · 2025-02-10T13:14:41Z

Common/Exec.v

+match eff with
+| MSet s => λ _, (mret () : t St E ()) s
+| MGet => λ s, (mret s : t St E St) s
+end.


Indentation should be 2 spaces here. Also, it might be nicer to have the inlined version here as this is a primitive effect of the monad e.g. λ _, make [(s, ())] [] instead of λ _, mret () s).

tperami · 2025-02-10T13:25:03Z

GenModels/TermModels.v

@@ -281,9 +281,9 @@ Module TermModels (IWA : InterfaceWithArch). (* to be imported *)
      End MR.
      Arguments t : clear implicits.

-      Definition from_exec {n} (e : Exec.t string (MState.final n)) :
+      Definition from_exec {St n} (e : Exec.t St string (MState.final n)) (st : St) :


If the original didn't have a stateT than this should take an Exec.res rather than do the application itself

tperami · 2025-02-10T13:27:41Z

promising-arm/GenPromising.v

@@ -170,17 +170,17 @@ Module Gen (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
          set.*)
      promise_select :
        (* fuel *) nat -> (* tid *) nat → memoryMap → pModel.(tState) →
-        PromMemory.t pModel.(mEvent) → Exec.t string pModel.(mEvent);
+        PromMemory.t pModel.(mEvent) → Exec.t (pModel.(tState) * PromMemory.t pModel.(mEvent) * pModel.(iis)) string pModel.(mEvent);


Again if there was not StateT it should become a Exec.res

tperami · 2025-02-10T15:08:30Z

promising-arm/GenPromising.v

+        init |>
+          (ist ←@{(Exec.t (tState * PromMemory.t mEvent * iis prom) string)} cinterp handler sem;
+          λ '(ts, mem, iis),
+          st |> setv (tstate tid) ts
+             |> setv (istate tid) ist
+             |> setv events mem
+             |> λ st', (mret st' : Exec.t (tState * PromMemory.t mEvent * Gen.iis prom) string t) (ts, mem, iis)).


The original was horrible to read, but now it's even worse, we need to have a function to lift an Exec monad into another exec monad with a different state. I'll add the required boilerplate to the Setter set-up for that, and then we'll need to add a step function

tperami reviewed Jan 29, 2025

View reviewed changes

tperami reviewed Feb 10, 2025

View reviewed changes

Nils-Lauermann force-pushed the stateful_exec branch from 141209f to 74b6d3e Compare February 13, 2025 17:41

Nils-Lauermann added 8 commits February 18, 2025 16:18

Modify Exec to include a state (especially also in the errors)

22d38f5

Adapt more definitions

d4e806d

Introduce monadic instances for res with state unit

ebb1b01

Finish redefinition of Exec monad with states

90f974a

Improve definitions and proofs

f068d31

Fix small issues

a4ad45e

Fix GenModels

75e1ecb

Try to adapt promising

5884913

Nils-Lauermann force-pushed the stateful_exec branch from 74b6d3e to 5884913 Compare February 18, 2025 16:20

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Adding states to exec monad natively #1

Adding states to exec monad natively #1

Nils-Lauermann commented Jan 29, 2025

tperami left a comment

tperami Jan 29, 2025

tperami Jan 29, 2025

tperami Jan 29, 2025

tperami Jan 29, 2025

tperami left a comment

tperami Feb 10, 2025

tperami Feb 10, 2025

tperami Feb 10, 2025

tperami Feb 10, 2025

tperami Feb 10, 2025

tperami Feb 10, 2025

tperami Feb 10, 2025

tperami Feb 10, 2025

tperami Feb 10, 2025

Adding states to exec monad natively #1

Are you sure you want to change the base?

Adding states to exec monad natively #1

Conversation

Nils-Lauermann commented Jan 29, 2025

tperami left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tperami left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment