feat(lang): add Yield scheduler and structural lemmas

theories/.gitignore

@@ -21,6 +21,7 @@
 *.vo
 *.vok
 *.vos
+.coq-native
 .rocq-native
 .csdp.cache
 .lia.cache

theories/Lang/Yield.v

@@ -0,0 +1,10 @@
+From TICL Require Export
+  Lang.Yield.Events
+  Lang.Yield.Syntax
+  Lang.Yield.Vec
+  Lang.Yield.Denote
+  Lang.Yield.Scheduler
+  Lang.Yield.Interp
+  Lang.Yield.Ticl
+  Lang.Yield.SBisim
+  Lang.Yield.SchedulerFairness.

theories/Lang/Yield/Denote.v

@@ -0,0 +1,110 @@
+From Stdlib Require Import Nat Strings.String.
+From ExtLib Require Import Data.Map.FMapAList Data.String Structures.Maps.
+From TICL Require Import
+  ICTree.Core
+  Events.StateE
+  Lang.Maps
+  Lang.Yield.Events
+  Lang.Yield.Syntax.
+
+Import ICtree ICTreeNotations.
+Local Open Scope ictree_scope.
+
+Definition Ctx := alist string nat.
+Definition Mem := stateE Ctx.
+
+(** Raw Yield denotations can yield, fork, and access memory. *)
+Definition YEff := yieldE + (forkE + Mem).
+
+Definition ytrigger (e : YEff) : ictree YEff (encode e) :=
+  @ICtree.trigger YEff YEff _ _ ReSum_refl ReSumRet_refl e.
+Definition yget : ictree YEff Ctx := ytrigger (inr (inr Get)).
+Definition yput (m : Ctx) : ictree YEff unit :=
+  ytrigger (inr (inr (Put m))).
+Definition yyield : ictree YEff unit := ytrigger (inl Yield).
+Definition yfork : ictree YEff bool := ytrigger (inr (inl Fork)).
+
+(** Denotation of expressions.  Successful variable reads yield once before
+    returning the value; missing variables remain stuck. *)
+Fixpoint denote_exp (e : YExp) : ictree YEff nat :=
+  match e with
+  | YVar name =>
+      ctx <- yget;;
+      match lookup name ctx with
+      | Some value => yyield;; Ret value
+      | None => stuck
+      end
+  | YLit n => Ret n
+  | YPlus a b =>
+      x <- denote_exp a;;
+      y <- denote_exp b;;
+      Ret (x + y)%nat
+  | YMinus a b =>
+      x <- denote_exp a;;
+      y <- denote_exp b;;
+      Ret (x - y)%nat
+  | YMult a b =>
+      x <- denote_exp a;;
+      y <- denote_exp b;;
+      Ret (x * y)%nat
+  end.
+
+(** Internal result used to prevent child threads from inheriting source
+    continuations outside their fork body.
+
+    [Fallthrough] means the current thread should continue with the enclosing
+    source continuation.  [HaltThread] means a spawned child has finished its
+    declared body and must not inherit enclosing continuations. *)
+Inductive YStmtFlow : Type :=
+| Fallthrough
+| HaltThread.
+
+(** Flow-sensitive denotation of statements. *)
+Fixpoint denote_stmt_flow (s : YStmt) : ictree YEff YStmtFlow :=
+  match s with
+  | YAssign name expr =>
+      value <- denote_exp expr;;
+      ctx <- yget;;
+      yput (add name value ctx);;
+      Ret Fallthrough
+  | YSeq a b =>
+      flow <- denote_stmt_flow a;;
+      match flow with
+      | Fallthrough => denote_stmt_flow b
+      | HaltThread => Ret HaltThread
+      end
+  | YIf test then_branch else_branch =>
+      condition_value <- denote_exp test;;
+      if is_true condition_value then
+        denote_stmt_flow then_branch
+      else
+        denote_stmt_flow else_branch
+  | YWhile test body =>
+      ICtree.iter
+        (fun _ =>
+           condition_value <- denote_exp test;;
+           if is_true condition_value then
+             flow <- denote_stmt_flow body;;
+             match flow with
+             | Fallthrough => Ret (inl tt)
+             | HaltThread => Ret (inr HaltThread)
+             end
+           else
+             Ret (inr Fallthrough)) tt
+  | YFork body =>
+      in_child <- yfork;;
+      if in_child then
+        _ <- denote_stmt_flow body;;
+        Ret HaltThread
+      else
+        Ret Fallthrough
+  | YSkip => Ret Fallthrough
+  | YYield =>
+      yyield;;
+      Ret Fallthrough
+  end.
+
+(** Public denotation of statements to unscheduled Yield threads. *)
+Definition denote_stmt (s : YStmt) : ictree YEff unit :=
+  _ <- denote_stmt_flow s;;
+  Ret tt.

theories/Lang/Yield/Events.v

@@ -0,0 +1,40 @@
+From Stdlib Require Import Fin.
+From TICL Require Import ICTree.Core Events.Core.
+
+Generalizable All Variables.
+
+(** Cooperative scheduling point emitted by source-level [yield]. *)
+Variant yieldE : Type := Yield.
+
+(** Thread-local fork choice.  The scheduler interprets the resulting [bool]
+    to run both continuations. *)
+Variant forkE : Type := Fork.
+
+(** Scheduler-level observation that a fork spawned another runnable thread. *)
+Variant spawnE : Type := Spawn.
+
+#[global] Instance Encode_yieldE : Encode yieldE :=
+  fun e => match e with Yield => unit end.
+#[global] Instance Encode_forkE : Encode forkE :=
+  fun e => match e with Fork => bool end.
+#[global] Instance Encode_spawnE : Encode spawnE :=
+  fun e => match e with Spawn => unit end.
+
+Definition yield {E} `{HE : Encode E} `{RS : ReSum yieldE E}
+           `{RR : @ReSumRet yieldE E Encode_yieldE HE RS} : ictree E unit :=
+  @ICtree.trigger yieldE E Encode_yieldE HE RS RR Yield.
+Definition fork {E} `{HE : Encode E} `{RS : ReSum forkE E}
+           `{RR : @ReSumRet forkE E Encode_forkE HE RS} : ictree E bool :=
+  @ICtree.trigger forkE E Encode_forkE HE RS RR Fork.
+Definition spawn {E} `{HE : Encode E} `{RS : ReSum spawnE E}
+           `{RR : @ReSumRet spawnE E Encode_spawnE HE RS} : ictree E unit :=
+  @ICtree.trigger spawnE E Encode_spawnE HE RS RR Spawn.
+
+(** A runnable source thread may yield, fork, or perform user effects. *)
+Definition thread (E : Type) `{Encode E} := ictree (yieldE + (forkE + E)) unit.
+
+(** A scheduled computation exposes yields and spawns, but no raw forks. *)
+Definition completed (E : Type) `{Encode E} := ictree (yieldE + (spawnE + E)) unit.
+
+(** Finite thread pools are represented as functions from finite indices. *)
+Definition pool (E : Type) `{Encode E} (n : nat) := Fin.t n -> thread E.

theories/Lang/Yield/Interp.v

@@ -0,0 +1,92 @@
+From Stdlib Require Import Fin.
+From ExtLib Require Import
+  Structures.Monad
+  Data.Monads.StateMonad
+  Structures.MonadState
+  Data.Map.FMapAList
+  Data.String.
+From TICL Require Import
+  ICTree.Core
+  ICTree.Interp.Core
+  ICTree.Interp.State
+  ICTree.Events.State
+  ICTree.Events.Writer
+  Events.Core
+  Events.StateE
+  Lang.Maps
+  Lang.Yield.Events
+  Lang.Yield.Syntax
+  Lang.Yield.Denote
+  Lang.Yield.Scheduler.
+
+Import ICtree ICTreeNotations.
+Local Open Scope ictree_scope.
+
+(** Start a source statement as a singleton pool focused on its only thread.
+    This is the scheduler-visible view: source [Fork] events have been
+    scheduled into scheduler [Spawn] observations, and cooperative [Yield]
+    observations remain visible alongside memory effects. *)
+Definition scheduled_visible (s : YStmt) : completed Mem :=
+  schedule 1 (fun _ => denote_stmt s) (Some Fin.F1).
+
+(** Backward-compatible name for the scheduler-visible scheduled computation. *)
+Definition scheduled : YStmt -> completed Mem := scheduled_visible.
+
+(** Erase scheduler spawn observations while preserving yield and memory events. *)
+Definition handle_spawn : (yieldE + (spawnE + Mem)) ~> ictree (yieldE + Mem) :=
+  fun event =>
+    match event with
+    | inl y => ICtree.trigger y
+    | inr (inl Spawn) => Ret tt
+    | inr (inr m) => ICtree.trigger m
+    end.
+Definition interp_spawn {X} (t : ictree (yieldE + (spawnE + Mem)) X) : ictree (yieldE + Mem) X :=
+  interp handle_spawn t.
+
+(** Erase cooperative yield observations, leaving only memory effects. *)
+Definition handle_yield : (yieldE + Mem) ~> ictree Mem :=
+  fun event =>
+    match event with
+    | inl Yield => Ret tt
+    | inr m => ICtree.trigger m
+    end.
+Definition interp_yield {X} (t : ictree (yieldE + Mem) X) : ictree Mem X :=
+  interp handle_yield t.
+
+(** Erased scheduled interpretation: both scheduler [Spawn] and cooperative
+    [Yield] observations are intentionally erased, leaving only memory effects. *)
+Definition interp_scheduled_erased (s : YStmt) : ictree Mem unit :=
+  interp_yield (interp_spawn (scheduled_visible s)).
+
+(** Backward-compatible erased scheduled interpretation.  New concurrency-facing
+    code should choose explicitly between [scheduled_visible] and
+    [interp_scheduled_erased]. *)
+Definition interp_scheduled : YStmt -> ictree Mem unit := interp_scheduled_erased.
+
+(** Interpret a raw thread without scheduling by resolving [Fork] to [false],
+    so a standalone thread behaves as the parent path and never starts the
+    fork body. *)
+Definition handle_thread : YEff ~> ictree (yieldE + Mem) :=
+  fun event =>
+    match event with
+    | inl y => ICtree.trigger y
+    | inr (inl Fork) => Ret false
+    | inr (inr m) => ICtree.trigger m
+    end.
+Definition interp_thread {X} (t : ictree YEff X) : ictree Mem X :=
+  interp_yield (interp handle_thread t).
+
+(** Erased expression instrumentation: raw thread-level [Yield] observations
+    are erased before state instrumentation. *)
+Definition instr_exp_erased (e : YExp) (ctx : Ctx) : ictreeW Ctx (nat * Ctx) :=
+  instr_stateE (interp_thread (denote_exp e)) ctx.
+
+(** Erased statement instrumentation: scheduler [Spawn] and cooperative [Yield]
+    observations are erased before state instrumentation. *)
+Definition instr_stmt_erased (s : YStmt) (ctx : Ctx) : ictreeW Ctx (unit * Ctx) :=
+  instr_stateE (interp_scheduled_erased s) ctx.
+
+(** Backward-compatible erased instrumentation aliases.  These names preserve the
+    iteration-1 API, where instrumentation observed only memory/state effects. *)
+Definition instr_exp : YExp -> Ctx -> ictreeW Ctx (nat * Ctx) := instr_exp_erased.
+Definition instr_stmt : YStmt -> Ctx -> ictreeW Ctx (unit * Ctx) := instr_stmt_erased.