feat(lang): add Yield scheduler and structural lemmas

[elefthei]

Summary

Adds the Yield language, cooperative scheduler, scheduler bisimulation proof layer, and TICL-facing structural lemma surface for source-level Yield reasoning.

Changes

• Add Yield syntax, events, finite-pool helpers, flow-sensitive denotation, scheduler, erased/visible interpreters, and umbrella exports.
• Implement YFork body as a single-body spawn where child execution remains separate from the parent continuation.
• Add scheduler-visible regressions and strong-bisimulation preservation for scheduled Yield computations.
• Add generic TICL structural lemmas for expressions, assignment, fallthrough-aware sequencing, conditionals, while unrolling/invariance, erased yield, and generalized fork/spawn behavior.
• Preserve zero proof debt: no Admitted, admit, or Axiom in theories/Lang/Yield.

Validation

• dune build theories/Lang/Yield/Ticl.vo theories/Lang/Yield/SBisim.vo theories/Lang/Yield.vo
• dune build
• rg -n "Admitted\\.|admit\\b|Axiom\\b" theories/Lang/Yield --glob '!_build/**' (no matches; exit 1)
• git diff --check origin/main

Notes

Untracked local planning/research documents remain in specs/ and research/; they were inspected for PR prep and intentionally not staged into this code PR.

[elefthei]

Implementation Notes

Task: Implement research/docs/2026-06-01-yield2-cooperative-multithreading-ictrees.md work on new branch lang/yield

Running Notes

• Record implementation decisions, deviations from the spec, tradeoffs, blockers, validation notes, and anything else the user should know.

Iteration 1 Notes

• Branch: created/switched to local lang/yield from the current checkout. The repository remains behind origin/main by 10 commits per preflight; no rebase/merge was performed.
• Project preflight: this is a Rocq/Coq formalization built with Dune/Make/opam (make delegates to dune build). The checkout was present but dependencies were initially incomplete.
• Dependency setup attempted: delegated setup installed non-downgrading packages in the active opam switch: coq-ext-lib.0.13.0, rocq-equations.1.3.1+9.1, and rocq-coinduction.1.21. This resolved the original missing ExtLib build blocker. The documented/opam dependency name rocq-ext-lib was not available in configured repos, while coq-ext-lib provides the needed ExtLib theory.
• Environment tradeoff: active switch is Rocq/Coq 9.1.0 while project docs indicate Rocq 9.0.x. The setup subagent avoided destructive downgrades/removals in the shared switch.
• Remaining global validation blocker: full make/dune build now fails before reaching most Yield files because TICL imports From Coinduction Require Import coinduction, but installed rocq-coinduction.1.21 does not provide Coinduction/coinduction.v. A sibling /home/eioannidis/git/coinduction checkout appears to provide the expected old/forked module, but installing it through opam would downgrade the shared switch, so it was not installed.
• Implemented iteration-1 semantic core only, not the full RFC proof stack. Added theories/Lang/Yield/{Events,Syntax,Vec,Denote,Scheduler,Interp,Ticl}.v and umbrella theories/Lang/Yield.v.
• Deliberate scope deferrals: full scheduler transition lemmas, Choice.v, SBisim.v, schedule_permutation, StImp-parity TICL structural lemma families, and representative examples were deferred to later iterations. This keeps iteration 1 to a small semantic scaffold as recommended by analysis.
• Event design decision: used current TICL plain event types plus Encode instances for yieldE, forkE, and spawnE, rather than old Type -> Type event families from origin/yield2.
• Memory design decision: used stateE Ctx with Ctx := alist string nat, matching StImp/current instrumentation, instead of porting old branch MemE read/write events.
• Variable-read semantics: preserved the RFC-required successful-read cooperative yield: state is read, lookup succeeds, Yield is triggered, then the value is returned. Missing variables use StImp-compatible stuck rather than origin/yield2 default-zero reads.
• Erasure design decision: kept spawn and yield erasure as explicit named views in Interp.v rather than silently erasing scheduler events in the scheduler or primary definitions.
• Implementation fix decisions: nested event sums were parenthesized as yieldE + (forkE + E) and yieldE + (spawnE + E) to match handlers/scheduler cases. Local concrete triggers were used in denotation to avoid adding broad global/transitive ReSum instances. Scheduler VisF matching was made dependent so continuation argument types refine correctly.
• Finite-pool fix: Vec.v dependent Fin.t helpers were adjusted to carry/cast hidden size equalities and use Fin.caseS', fixing the reported Fin.t mismatch at theories/Lang/Yield/Vec.v:15 under Rocq 9.1.
• Validation outcomes: dune build theories/Lang/Yield/Vec.vo passes after the Yield fixes. dune build theories/Lang/Yield/Scheduler.vo, dune build theories/Lang/Yield.vo, and make remain blocked by the repository-level Coinduction module mismatch before reaching Yield. A delegated isolated stubbed coqc check of the actual Yield files (Syntax, Vec, Events, Scheduler, Denote, Interp, Ticl, umbrella) succeeded, which distinguishes the remaining full-build blocker from the Yield source fixes.
• Working tree note: new Yield files are currently untracked. Pre-existing untracked .atomic/, research/, and specs/ directories were left untouched.

Iteration 2 Notes

• Preflight reconfirmed this checkout as a Rocq/Coq formalization built by Dune/Make/opam. The branch was still stale relative to origin/main and had stale Coq package/CI files, missing theories/Lang/HeapImp.v relative to origin/main, untracked Yield files, and a source-tree generated artifact theories/ICTree/.Core.aux.
• Integration decision: instead of a full rebase, the implementation subagent performed targeted reconciliation by restoring the relevant current-main Rocq package/CI/build files and theories/Lang/HeapImp.v from origin/main. This avoids broad merge churn while satisfying the iteration-2 package/CI/HeapImp requirements locally.
• Packaging changes: restored/adopted .github/workflows/rocq.yml, rocq-ticl.opam, dune-project, theories/dune, Makefile, and examples/dune from origin/main; removed stale .github/workflows/coq.yml and coq-ticl.opam. examples/dune was included because after switching to (using rocq 0.11), its stale coq.theory/coq-ticl stanza blocked focused Dune builds before Yield typechecking.
• Source hygiene: removed theories/ICTree/.Core.aux; validation found no .aux or .glob artifacts under theories or examples afterward.
• Source tracking: staged theories/Lang/Yield.v and all theories/Lang/Yield/*.v so the Yield implementation is no longer merely untracked working-tree state. Stale package/workflow deletions were also staged in a follow-up; unrelated untracked .atomic/, progress.md, research docs, and specs were left untracked.
• Yield semantics decision: no denotation or scheduler algorithm changes were made in iteration 2. The existing event/syntax/denotation/scheduler behavior from iteration 1 was preserved.
• API decision: added scheduled_visible as the primary scheduler-visible statement view exposing yieldE + (spawnE + Mem) directly. This implements the RFC's minimal visible-ICTree option and defers a combined visible writer API (instr_stmt_visible/YieldObs) to a later proof-focused iteration.
• Erasure API decision: added explicit erased names interp_scheduled_erased, instr_exp_erased, and instr_stmt_erased. Kept compatibility aliases scheduled, interp_scheduled, instr_exp, and instr_stmt, with comments documenting that interp_scheduled/instr_stmt are erased state-only tiers.
• TICL facade: expanded theories/Lang/Yield/Ticl.v to document and re-export raw, scheduler-visible, and erased proof tiers (Events, Syntax, Denote, Scheduler, Interp). No StImp-parity structural lemma families were added in this iteration.
• Validation outcomes: repository-state validation passed for staged Yield files, preservation of HeapImp.v vs origin/main, package/CI path alignment with origin/main, absence of generated source artifacts, and absence of stale package strings (coq-ticl, coq-ctree, coq.theory, using coq) outside markdown/build/git directories.
• Build blocker: focused dune build theories/Lang/Yield/Interp.vo theories/Lang/Yield/Ticl.vo still fails before reaching Yield-specific typechecking. Dune invokes /home/eioannidis/.opam/5.3.0/bin/rocq --config; installed Rocq 9.0.1 reports Unknown subcommand --config, so Dune skips installed theories and cannot find Stdlib/ExtLib. This is a local Rocq/Dune toolchain discovery issue after the packaging migration, distinct from the earlier stale Coinduction path error.
• Unexpected side effect: the analysis subagent wrote an untracked progress.md note while investigating. It was not staged and is unrelated to the implementation changes.

Iteration 3 Notes

• Orchestration: used delegated subagents for project preflight/setup discovery, proof-surface analysis, implementation, and validation. The spec file at /home/eioannidis/git/ticl/specs/2026-06-01-implement-research-docs-2026-06-01-yield2-cooperative-multithreading-ictrees-md.md remained the authoritative plan.
• Preflight reconfirmed the checkout as a Rocq/Dune/opam proof project on branch lang/yield, with dune-project using (using rocq 0.11), package rocq-ticl, rocq-ticl.opam, rocq.theory stanzas, and .github/workflows/rocq.yml. No submodules were detected. The active local setup still does not appear CI-equivalent.
• Documentation cleanup: changed README and INSTALL dependency references from coq-equations to rocq-equations; changed README generated-documentation wording from coqdoc to rocqdoc.
• Ignore-file cleanup: restored .rocq-native in theories/.gitignore. Kept .coq-native as a deliberate legacy/native-artifact compatibility ignore rather than removing it.
• Generated artifact cleanup: implementation ran deletion for source-tree *.glob and *.aux under theories/ and examples/; validation found no such artifacts afterward.
• Proof-surface decision: added the first lightweight regression layer directly in theories/Lang/Yield/Ticl.v instead of creating a new proof/example module, preserving the existing facade role and avoiding Dune/module churn.
• Added baseline Yield facts in Ticl.v: expression and statement denotation constructor unfold lemmas, scheduler one-step/case facts for empty/no-focus/focused ret/branch/guard/yield/fork/user-event cases, concrete scheduler-visible examples for YYield and YFork YSkip YSkip, erasure handler/unfold lemmas, and alias lemmas documenting that compatibility APIs (interp_scheduled, instr_exp, instr_stmt) are erased views.
• Deliberate deferrals: did not add scheduler permutation, sbisim_schedule, fairness/liveness claims, visible writer-world instrumentation, deep state/writer trace proofs, or full StImp-parity theorem families. The current iteration prioritizes reviewer-visible cleanup and small one-step regression facts.
• Validation outcomes: git diff --check origin/main passed; production stale-name scans found no active coq-equations, coqdoc, coq-ctree, coq-ticl, using coq, or coq.theory regressions in the expected package/docs/build files; .rocq-native is present; Yield files are tracked; git diff --name-status origin/main does not delete theories/Lang/HeapImp.v.
• Build blocker: focused dune build theories/Lang/Yield/Ticl.vo still fails before Yield-specific typechecking. Dune invokes /home/eioannidis/.opam/5.3.0/bin/rocq --config, but local Rocq 9.0.1 reports Unknown subcommand --config; Dune then cannot find the Rocq standard library or theory ExtLib. The local switch also lacks rocq-ext-lib (only earlier coq-ext-lib evidence was observed), while CI targets Rocq 9.1 and pinned Rocq-family dependencies. The new Ticl.v lemmas therefore remain best-effort pending validation in a CI-equivalent Rocq/opam environment.
• Cleanup note: subagent output report files accidentally written to the repository root (preflight-report.md, proof-analysis-report.md, implementation-report.md, validation-report.md) were removed; unrelated pre-existing untracked .atomic/, progress.md, research/, and specs/ items were left untouched.

Iteration 4 Notes

• Scope: implemented proof-surface changes only; no scheduler semantic changes were made.
• Finite-pool laws: added replace_pool_hit, replace_pool_miss, cons_pool_head, and cons_pool_tail in theories/Lang/Yield/Vec.v. Did not add pool_ext because the new regressions only need slot-level facts.
• Ticl façade: explicitly exports Lang.Yield.Vec so the pool laws are part of the visible Yield proof surface.
• Singleton examples: strengthened scheduled_visible_yyield_one_step and scheduled_visible_yfork_skip_skip_one_step so their RHS keeps the scheduler's exact replace_pool terms instead of presenting normalized singleton constant pools.
• Non-degenerate scheduler regressions: added two-thread yield facts proving the focused yield slot updates to its continuation and the other thread is preserved. Added distinguishable fork facts proving Fin.F1 = child, Fin.FS Fin.F1 = parent, and Fin.FS (Fin.FS Fin.F1) = other, with the one-step lemma also recording the shifted parent focus Some (Fin.FS Fin.F1).
• Validation passed: manual rocq compile smoke check of theories/Lang/Yield/Vec.v; temporary /tmp/test_vec_laws.v smoke proof against the new pool laws; git diff --check origin/main; and no source-tree *.glob/*.aux artifacts under theories or examples.
• Validation blocker: dune build theories/Lang/Yield/Ticl.vo remains blocked before Yield proof-checking by the local Rocq/Dune discovery issue: Dune invokes /home/eioannidis/.opam/5.3.0/bin/rocq --config, but local rocq --config reports Unknown subcommand --config, after which Dune cannot find the Rocq standard library or theory ExtLib from theories/dune:5.
• Report written to /tmp/iter4-implementation-report.md.

Iteration 4 Notes

• Orchestration: read the authoritative spec at /home/eioannidis/git/ticl/specs/2026-06-01-implement-research-docs-2026-06-01-yield2-cooperative-multithreading-ictrees-md.md and delegated preflight, proof-surface analysis, implementation, and validation to subagents. The active todo ledger entries for iteration 4 were all resolved before final reporting.
• Preflight reconfirmed this checkout as a Rocq/Coq proof development using Dune/Rocq (dune-project with (using rocq 0.11)), Makefile, rocq-ticl.opam, and the Rocq CI workflow. .gitmodules has no active submodules. _build/ exists from previous work. No dependency installation or destructive setup was attempted because the documented install path is external/opam-oriented and the checkout already contains in-progress changes.
• Finite-pool proof-surface decision: added generic slot-level laws in theories/Lang/Yield/Vec.v rather than normalizing whole finite pools. Added replace_pool_hit, replace_pool_miss, cons_pool_head, and cons_pool_tail. Did not add pool_ext because the iteration-4 regressions only needed per-index facts.
• Scheduler semantics were intentionally left unchanged. The changes are proof/API-surface regressions only.
• theories/Lang/Yield/Ticl.v now exports Lang.Yield.Vec, strengthens the singleton scheduled_visible examples so their RHS keeps the exact scheduler replace_pool terms, and adds non-degenerate two-thread scheduler regressions.
• Added yield regressions proving the focused source-yield step uses replace_pool, clears focus, updates the focused slot, and preserves the unrelated slot.
• Added fork regressions with distinguishable child, parent, and other threads proving scheduler-visible Spawn, child placement at the new head, parent placement at the shifted old focused slot, preservation of an unrelated old thread, and focus on Some (Fin.FS Fin.F1).
• Validation passed for repository hygiene: git diff --check origin/main, no source-tree *.glob/*.aux artifacts, Yield files tracked, stale coq-equations/coqdoc references absent from README/INSTALL, expected rocq-equations/rocqdoc references present, and .rocq-native present in theories/.gitignore.
• Diff against origin/main is scoped to theories/.gitignore and the Yield modules. README.md, INSTALL.md, package, and CI files still appear in local git status because the branch is behind and has staged/catch-up changes, but they have no remaining diff against origin/main in validation.
• Focused build validation remains blocked locally before Yield source compilation: dune build theories/Lang/Yield/Ticl.vo fails because Dune invokes /home/eioannidis/.opam/5.3.0/bin/rocq --config, while local Rocq 9.0.1 reports Unknown subcommand --config; Dune then cannot discover the Rocq standard library or ExtLib. This is classified as the existing local Rocq/Dune toolchain discovery blocker, not a demonstrated Yield code failure.
• Recommended acceptance gate remains a clean CI-equivalent Rocq/opam environment where dune build theories/Lang/Yield/Ticl.vo and preferably broader dune build can run with Stdlib, ExtLib, Equations, and Coinduction discoverable.

Iteration 5 Notes

• Orchestration: read the authoritative spec at /home/eioannidis/git/ticl/specs/2026-06-01-implement-research-docs-2026-06-01-yield2-cooperative-multithreading-ictrees-md.md and delegated preflight, impact analysis, implementation, follow-on proof repair, and validation to subagents. The iteration-5 todo ledger entries were resolved before final reporting.
• Preflight reconfirmed the checkout as an initialized Rocq/Coq proof development using Dune/opam/Make (dune-project with (using rocq 0.11), rocq-ticl.opam, theories/dune, and .github/workflows/rocq.yml). No submodules or generated-source setup were required, and no destructive global opam/toolchain setup was attempted.
• Primary reviewer-a fix: in theories/Lang/Yield/Ticl.v, qualified both unfold-lemma truthiness checks in denote_stmt_yif and denote_stmt_ywhile as YieldSyntax.is_true condition_value. This preserves YieldSyntax.is_true : nat -> bool, Utils.is_true : bool -> Prop, current imports, and denotation/scheduler semantics.
• Follow-on proof-surface repairs were required after the original is_true blocker was removed. schedule_empty_none and the nonempty no-focus scheduler fact now state one-step observations (observe ... = RetF/VisF ...) rather than propositional equality of the guarded cofixpoint tree. This aligns them with the existing focused scheduler one-step lemmas without changing Scheduler.v.
• Focused scheduler proof scripts in Ticl.v were repaired by explicitly unfolding one guarded scheduler step and rewriting observe (v i) hypotheses; their theorem statements and scheduler semantics were left unchanged.
• The singleton scheduled_visible_yfork_skip_skip_one_step regression was adjusted to retain the exact fork bind residual (ICtree.subst' ... (RetF in_child)) instead of over-normalizing child/parent continuations to Ret tt. This keeps the Spawn, child/parent polarity, and replace_pool regression shape while avoiding an overly strong propositional tree-equality assumption.
• Files touched in iteration 5: theories/Lang/Yield/Ticl.v only. theories/Lang/Yield/Scheduler.v was inspected by a subagent but not edited.
• Validation passed after follow-on repairs: dune build theories/Lang/Yield/Vec.vo theories/Lang/Yield/Denote.vo theories/Lang/Yield/Scheduler.vo theories/Lang/Yield/Interp.vo; dune build theories/Lang/Yield/Ticl.vo; dune build theories/Lang/Yield.vo; full dune build; git diff --check origin/main; generated-artifact scan for *.glob/*.aux; and Yield tracked-file scan.
• No remaining blocker was reported by validation. The earlier local Rocq/Dune discovery blocker from previous iterations did not recur in this validation pass.

[elefthei]

Implementation Notes

Task: Complete specs/2026-06-02-complete-specs-2026-06-02-sbisim-schedule-proof-md.md using the rocq skill

Iteration 1/10 — 2026-06-02

Orchestration deviation

• User explicitly deleted the project coq-prover subagent mid-run and directed:
  "only use the rocq skill". The .atomic/agents/coq-prover.md agent was deleted.
  All further work was done directly via the rocq skill (coqc / dune build,
  bundled scripts) rather than subagent delegation.
• NOTE for future iterations: do NOT recreate or use coq-prover; use the rocq
  skill directly.

State found at start of iteration

• theories/Lang/Yield/SBisim.v already contained (compiling, 0 admits) the
  Phase-1 pool algebra + 6 transition constructors from the predecessor spec.
• The now-deleted coq-prover agent had ALSO already written and left compiling
  (in the working tree, exit 0) the following BEFORE it was deleted:
  • Phase 2 constructors: trans_schedule_empty_ret,
    trans_schedule_focused_ret, trans_schedule_focused_guard
    (stated as ≅ unfolding equivalences, not tau-step lemmas).
  • Phase 3 inversions: trans_schedule_no_focus_inv,
    trans_schedule_focused_inv (full 6-way disjunction on observe (v i)),
    plus helper schedule_no_focus_equ.
  • Extra (not in spec but useful): pool_equ algebra (replace/remove/cons_pool_equ)
    and schedule_pool_proper — a strong-equ (≅) congruence of schedule
    over pointwise-≅ pools, in every focus, proved by coinduction.

Design decisions / spec resolutions realised in the landed code

• §9.7 (focused-return label shape): the landed code exposes the focused-return
  and focused-guard cases as ≅ Guard (...) unfolding equivalences
  (e.g. schedule (S n) v (Some i) ≅ Guard (schedule n (remove_pool v i) None))
  rather than as collapsed tau-step trans lemmas. The inversions then use
  trans_guard_inv to strip the guard. This is a reasonable resolution of the
  open question and keeps the residual pool transformation explicit.

Validation outcomes (this iteration)

• dune build theories/Lang/Yield/SBisim.vo → exit 0.
• dune build theories/Lang/Yield.vo (re-export check) → exit 0.
• Whole-tree dune build → TIMED OUT at 1200s/1800s (large project; not a
  failure of the Yield layer). Targeted builds above are green.
• admitted_analyzer.py … --format=summary → Admitted: 0.
• check_axioms.sh → "Standard axioms only".
• grep for BrD/brD_bound/Admitted/admit/Axiom in SBisim.v → none.

NOT completed this iteration (deferred to iteration 2+)

• Phase 4: match_focused_thread_step (focused-thread matching bridge).
• Phase 5: sbisim_schedule (the headline coinductive theorem).
• Phase 6: sbisim_scheduled_visible corollary.

Precise technical blocker for Phase 4/5 (handoff)

The Some-focus simulation case cannot be discharged with the currently-available
ICTree lemmas without new infrastructure:

• schedule (S n) v2 (Some i) reads observe (v2 i). Given only v1 i ~ v2 i,
  v2 i need NOT be structurally a Vis/Ret/Br — it may sit behind
  Guards. sbisim_vis_invE/invT and sbisim_br_inv (SBisim/Core.v:1167–1191)
  require BOTH sides to be literally Vis e k / Br n k; they do not absorb
  leading guards.
• The Fork case is the sharpest: the scheduler consumes the FULL continuation
  k2 at BOTH true and false (cons_pool (k true) (replace_pool v i (k false))),
  so single-step transition matching (sbisim_trans) is insufficient — it only
  exposes the taken branch.
• A search of theories/ICTree/SBisim/* and Trans.v found NO epsilon /
  productive / wtrans / guard-normalization ("any t ~ Vis e k1 equals
  guards-over-Vis e k2 with k1 x ~ k2 x") lemma. That normal-form lemma (or
  an equivalent transition-matching coinduction that follows v2's guards) is the
  missing piece and is the recommended first task for iteration 2.

No secrets/credentials involved (proof-only change).

Iteration 2/10 — 2026-06-04

Orchestration

• P0 (delete Scratch.v) and all independent validation done directly by the
  orchestrator. Phase 4/5/6 proof authoring delegated to the rocq skill agent
  (NOT the deleted coq-prover) with a precise roadmap
  (phase45-roadmap.md) and a hard no-Admitted/keep-green contract. Subagent
  result captured in phase45-result.md. All subagent claims were
  independently re-verified by the orchestrator (clean rebuild + gates).

P0 RESOLVED

• Deleted theories/Lang/Yield/Scratch.v (was untracked). It is gone from
  git status. The non-terminating engineB_val (induction TR) no longer
  wedges the build. Confirmed: whole-tree dune build now exits 0 in <600s
  (previously hung / timed out at 1200-1800s). Its salvageable value-step
  content was rebuilt structurally as schedule_lift_ret inside SBisim.v
  (via the trans_ derivation, not induction TR).

Iteration-1 "blocker" was INACCURATE — corrected

• Iteration 1 claimed no epsilon/guard-normalization infra exists, making
  Phase 4/5 infeasible. WRONG: trans_ (Trans.v:51-69) peels Guard via the
  Stepguard constructor, so trans already absorbs leading guards. sbisim_trans
  (ICTree/SBisim.v:35) gives plain simulation at L:=eq. No epsilon lemma needed.
  The Fork two-branch concern is handled by recovering k0 c ~ k2 c for both
  branches via reverse sbisim_trans + trans_vis_inv, not trans-determinism.

Phases 4/5/6 — COMPLETE (verified)

• SBisim.v: 412 -> 954 lines. Added (all proven, 0 Admitted):
  • Phase 4 lift engine: schedule_lift_{yield,user,tau,fork,ret} + small pool
    helpers (pool_equ_refl, replace_pool_idem_equ, remove_pool_agree,
    remove_replace_pool_equ, cast_refl, ...). Each proven by induction on the
    thread trans_ derivation: Stepguard case reuses
    trans_schedule_focused_guard + IH on replace_pool v i g; base constructor
    reuses the matching trans_schedule_focused_* constructor.
  • Phase 5: schedule_match (L660, ~255 lines) — a single direction-agnostic
    per-step simulation engine inducting on the LEFT scheduler trans_ derivation,
    reused for both sb legs (leg 2 via pool_sbisim_sym + symmetry). Design B
    (inline matching) chosen over a standalone match_focused_thread_step to avoid
    ~250 lines of duplication.
  • Theorem sbisim_schedule (L915) — statement matches the spec verbatim.
  • Phase 6: Corollary sbisim_scheduled_visible (L946), 3-line proof.
• Added 2 imports (Lang.Yield.Denote, Lang.Yield.Interp) for Phase 6 names;
  acyclic (neither imports SBisim). No existing statement/import meaning changed.

Design decisions / deviations from spec

• §9.5 RESOLVED: chose Design B (matching inlined in schedule_match), not a
  separate Yield-local match_focused_thread_step. Cleaner, no duplication.
• §9.7 RESOLVED: focused-Ret is NOT a scheduler val step; the Guard collapses
  into schedule (remove_pool v i) None, so schedule_lift_ret concludes an
  sbisim (~) equality, transported via sbisim_trans. No raw induction TR.
• Induction is on the trans_ derivation (not on n): makes focused-Guard (same n)
  and focused-Ret (smaller n) both terminate as strict sub-derivations.
• Axiom hygiene: deliberately avoided functional_extensionality by stating pool
  idempotence facts as pointwise pool_equ pushed through schedule_pool_proper.

Validation outcomes (orchestrator-verified, not just subagent-claimed)

• rm SBisim.vo && dune build theories/Lang/Yield/SBisim.vo -> exit 0.
• dune build theories/Lang/Yield.vo (re-export) -> exit 0.
• Whole-tree dune build -> exit 0 (<600s; P0 acceptance criterion met).
• admitted_analyzer.py … --format=summary -> Admitted: 0.
• check_axioms.sh -> "Standard axioms only".
• grep -E 'Admitted|admit|BrD|brD_bound|Axiom' SBisim.v -> none.
• Print Assumptions sbisim_schedule / sbisim_scheduled_visible -> only
  Eqdep.Eq_rect_eq.eq_rect_eq (pre-existing baseline from dependent destruction; same as existing schedule_pool_proper). Zero NEW axioms.

State / not committed

• Per spec §8.1 nothing was staged or committed. git status:
  ?? theories/Lang/Yield/SBisim.v, M theories/Lang/Yield.v, Scratch.v gone.
• The spec's full deliverable (P0 + Phases 4/5/6) is now landed. Remaining
  spec items are explicitly DEFERRED non-goals: schedule_permutation (§9.6),
  erased corollaries (§9.4).

[elefthei]

Implementation Notes

Task: Implement the change in specs/2026-06-04-yfork-single-body.md

Running Notes

• Record implementation decisions, deviations from the spec, tradeoffs, blockers, validation notes, and anything else the user should know.

Iteration 1 Notes

• Preflight found this checkout is a Rocq/Coq project using Dune/opam (dune-project, rocq-ticl.opam, Makefile, CI workflow). The checkout appeared initialized enough to proceed; _build/ already existed and no submodules were configured.
• Implemented the selected minimal design: source YFork is now single-body, denotation maps the raw fork result true to the child body and false to Ret tt, and the raw event/scheduler/proof boundary was preserved.
• Files changed: theories/Lang/Yield/Syntax.v, theories/Lang/Yield/Denote.v, theories/Lang/Yield/Ticl.v, and a comment-only terminology update in theories/Lang/Yield/Interp.v.
• Ticl.v exported regression was renamed/retargeted from the old scheduled_visible_yfork_skip_skip_one_step over YFork YSkip YSkip to scheduled_visible_yfork_yield_one_step over YFork YYield, matching the spec preference for a non-trivial child continuation.
• No semantic edits were made to Events.v, Scheduler.v, Vec.v, or SBisim.v; generic scheduler fork lemmas remained unchanged.
• Tradeoff retained from the spec: YSeq (YFork body) rest continues to use ordinary monadic bind, so the child continuation includes body ;; rest and the parent continuation includes rest; this iteration does not implement strict structured-spawn delimiting.
• Raw unscheduled interpretation still resolves Fork to false; the comment now describes this as the parent/no-child branch rather than the old active branch terminology.
• Validation passed: targeted Yield build, full dune build, YFork/static stale-reference checks, proof-debt grep, and git diff --check.
• No blockers encountered.

Iteration 2 Notes

• Preflight was delegated to codebase-locator. It confirmed the checkout is an initialized Rocq/Coq project built with Dune/opam (dune-project, rocq-ticl.opam, _CoqProject, CI workflow, _build, generated docs). No setup command was run because required artifacts/tooling evidence was already present and no submodules were configured.
• Codebase analysis/pattern discovery was delegated before implementation. The analysis identified Denote.v and Ticl.v as the required implementation/proof touchpoints and expected Events.v, Scheduler.v, Vec.v, and SBisim.v to remain unchanged if denote_stmt : YStmt -> ictree YEff unit stayed stable.
• Implemented the iteration-2 semantic fix in theories/Lang/Yield/Denote.v: introduced internal YStmtFlow with Fallthrough | HaltThread, added denote_stmt_flow, made YSeq apply its suffix only on Fallthrough, made YFork child branch run the body then return HaltThread, made the parent branch return Fallthrough, and made YWhile stop child threads from inheriting later loop iterations.
• Preserved the public raw-thread API by redefining denote_stmt as a wrapper that erases the internal flow marker to unit; no scheduler/event/pool/proof-boundary changes were needed.
• Updated theories/Lang/Yield/Ticl.v to replace semantically invalid direct unfold facts such as ordinary-bind denote_stmt_yseq with flow-level unfold facts, adapt the standalone fork regression, and add a regression for scheduled_visible (YSeq (YFork YSkip) YYield) with child-done and parent-yields observations.
• Tradeoff: YStmtFlow / denote_stmt_flow are now part of the visible proof surface from Denote.v/Ticl.v; they should be treated as implementation-level denotation helpers rather than source-language syntax. This keeps exact reflexivity-style facts practical while preserving the public denote_stmt API.
• Validation passed in both implementation and independent validation subagents: targeted Dune builds for Syntax.vo, Denote.vo, Ticl.vo, SBisim.vo, Yield.vo, full dune build, YFork reference grep with no stale two-argument constructors visible, proof-debt grep with no matches, and git diff --check.
• No blockers encountered. A stale attention notification for the implementation subagent was checked after completion; the run status was not available as an async run, but the foreground subagent had already returned a successful completion report.

Iteration 3 Notes

• Restored the minimal public Yield API lemma denote_stmt_yfork in theories/Lang/Yield/Ticl.v, placed immediately after denote_stmt_flow_yfork and before denote_stmt_flow_yskip.
• The lemma uses the exact flow-sensitive equality from the iteration-3 spec/analyzer: denote_stmt (YFork body) unfolds through denote_stmt_flow, the child branch runs denote_stmt_flow body then returns HaltThread, and the parent branch returns Fallthrough before the public wrapper returns tt.
• No changes were made to Syntax.v, Denote.v, Events.v, Scheduler.v, Vec.v, Interp.v, or SBisim.v; existing flow-sensitive semantics and scheduler/event/pool boundaries were preserved.
• Preflight was delegated to codebase-locator and setup verification to debugger. The checkout was confirmed as a Rocq/Coq project built with Dune/opam; the active environment already had dune 3.22.0 and Rocq 9.1.1 available, and a focused dune build theories/Lang/Yield/Ticl.vo passed before implementation, so no setup/bootstrap commands were run.
• Validation passed in the implementation subagent: dune build theories/Lang/Yield/Ticl.vo; public import check via coqtop -quiet -Q _build/default/theories TICL confirmed both denote_stmt_yfork and denote_stmt_flow_yfork; admitted_analyzer.py theories/Lang/Yield/Ticl.v --format=summary --report-only reported Admitted: 0; check_axioms.sh theories/Lang/Yield/Ticl.v --report-only reported standard axioms only; git diff --check -- theories/Lang/Yield/Ticl.v passed.
• Independent validation passed after implementation: dune build theories/Lang/Yield/Ticl.vo, dune build theories/Lang/Yield.vo, full dune build, git diff --check, public API checks via both Lang.Yield.Ticl and umbrella Lang.Yield, proof-debt grep over theories/Lang/Yield with no matches, and rg -n '\bdenote_stmt_yfork\b' theories/Lang/Yield/Ticl.v finding the lemma at line 130.
• Tradeoff: the restored public lemma exposes the flow-sensitive RHS (denote_stmt_flow, Fallthrough, HaltThread) rather than adding a separate branch-erased semantic corollary. This matches the minimal P2 API restoration and avoids extra proof/API expansion.
• Note: the working-tree diff relative to HEAD still includes prior iteration files (Denote.v, Interp.v, Syntax.v, and Ticl.v), but iteration 3 itself only edited theories/Lang/Yield/Ticl.v.
• No blockers encountered.

Iteration 4 Notes

• Preflight was delegated to codebase-analyzer after an initial locator delegation returned no actionable report. It confirmed the checkout is a Rocq/Coq project built with Dune/opam (dune-project, theories/dune, Makefile, README/INSTALL), appears initialized enough for implementation, and had no staged files or setup blocker.
• The active iteration-4 change was repository hygiene rather than Rocq semantics. No tracked Rocq source files were edited in this iteration; the existing tracked modified source files remain theories/Lang/Yield/Syntax.v, theories/Lang/Yield/Denote.v, theories/Lang/Yield/Interp.v, and theories/Lang/Yield/Ticl.v from prior semantic iterations.
• Addressed reviewer-b's hygiene finding by adding local-only ignore rules in .git/info/exclude for .atomic/, progress.md, and rocq-ticl.install; deleting progress.md; and deleting the generated rocq-ticl.install manifest.
• Tradeoff: .atomic/ was preserved on disk because it contains the active Atomic todo ledger required by this orchestration, but it is now locally excluded so it is not shown by git status --short --untracked-files=all and cannot be swept up by broad staging. This avoids a committed .gitignore policy change for project-level Atomic or Dune install artifacts.
• Validation passed: dune build theories/Lang/Yield/Ticl.vo, full dune build, git diff --check, proof-debt grep over theories/Lang/Yield with no Admitted., admit, or Axiom matches, public-name grep found denote_stmt_flow_yfork, denote_stmt_yfork, and scheduled_visible_yseq_yfork_skip_yield_one_step in Ticl.v.
• Git hygiene validation passed: git diff --cached --name-status is empty; .atomic/, progress.md, and rocq-ticl.install are not listed or staged. .atomic/ exists but is ignored via .git/info/exclude; progress.md and rocq-ticl.install are absent. Remaining visible untracked files are specs/research markdown documents and should be staged only explicitly if maintainers want them in the patch.
• No blockers encountered.

[elefthei]

Implementation Notes

Task: Implement specs/2026-06-04-yield-structural-lemma-plan.md, take as much time as needed to prove everything. No admitted!

Running Notes

• Record implementation decisions, deviations from the spec, tradeoffs, blockers, validation notes, and anything else the user should know.

Iteration 1/20 notes — 2026-06-05

Preflight and setup

• Confirmed repository is a Rocq/Dune project from dune-project, rocq-ticl.opam, theories/dune, CI workflow, and docs.
• Local toolchain validated by subagents: Rocq 9.1.1 and Dune 3.22.0.
• Repaired the build-blocking syntax issue in theories/Lang/Yield/Interp.v by removing the stray standalone . after Definition interp_scheduled.
• Did not touch untracked specs/ or research/ directories.

Implementation decisions

• Kept the first structural proof slice in theories/Lang/Yield/Ticl.v instead of introducing a new module, matching the spec's minimal-blast-radius recommendation.
• Added local TICL/ICTree proof imports and a local heterogeneous interp congruence helper in Ticl.v so erased expression proofs can normalize through nested interpreters without changing core ICTree modules globally.
• Added no-admit erased expression/state facts:
  • axr_yexp_ylit
  • axr_yexp_yvar_some with the required lookup name ctx = Some value premise
  • axr_yexp_yplus_ylit_ylit
  • axr_yexp_yminus_ylit_ylit
  • axr_yexp_ymult_ylit_ylit
• Renamed the arithmetic facts to _ylit_ylit rather than exporting broad axr_yexp_yplus/yminus/ymult names with narrow literal/literal statements. This is a deliberate API-honesty deviation from the draft checklist; generalized arithmetic over arbitrary operand expression facts remains deferred.
• Added no-admit erased statement facts:
  • axr_ystmt_yskip_erased
  • axax_ystmt_yyield_erased
• Did not add a one-step axr_ystmt_yyield_erased: debugger analysis showed that statement is false at the scheduled statement layer because source yield erasure still passes through scheduler Guard/singleton Br structure. The truthful theorem is AX AX done.
• Added no-admit literal-RHS assignment update lemmas:
  • aur_ystmt_yassign_ylit_erased
  • aul_ystmt_yassign_ylit_erased
• Fully general assignment lemmas over arbitrary RHS expressions remain deferred because instr_exp_erased evaluates raw expression threads directly, while instr_stmt_erased routes expression evaluation through the scheduler; a bridge/normalization layer is needed before a clean general theorem can be stated and proved.

Validation outcomes

Independent validation passed:

• coqc --version reported Rocq 9.1.1.
• dune build theories/Lang/Yield/Interp.vo theories/Lang/Yield/Ticl.vo theories/Lang/Yield/SBisim.vo theories/Lang/Yield.vo passed.
• Full dune build passed.
• rg -n "Admitted\\.|admit\\b|Axiom\\b|Parameter\\b" theories/Lang/Yield --glob '!_build/**' produced no matches.
• /tmp Rocq symbol checks passed for existing regression symbols and new symbols including axr_yexp_yvar_some, axax_ystmt_yyield_erased, aur_ystmt_yassign_ylit_erased, and aul_ystmt_yassign_ylit_erased.
• Optional Rocq helper scripts (admitted_analyzer.py, check_axioms.sh) were reported unavailable by the independent validation subagent, so the final independent gate used Dune, direct rg, and coqc symbol checks.

Residual work / deferred items

• General arithmetic lemmas axr_yexp_yplus, axr_yexp_yminus, and axr_yexp_ymult over arbitrary operand-expression premises are deferred pending a reusable erased-expression bind-normalization layer.
• General aur_ystmt_yassign / aul_ystmt_yassign over arbitrary RHS expressions are deferred pending a bridge between raw erased expression evaluation and scheduled statement execution.
• Fork/spawn split lemmas, sequence/fallthrough lemmas, conditionals, while invariance, and scheduler permutation remain intentionally out of scope for iteration 1.

Worktree summary

• Tracked files modified: theories/Lang/Yield/Interp.v, theories/Lang/Yield/Ticl.v.
• No files staged.
• Residual untracked directories research/ and specs/ remain present and were not modified by this iteration.

Iteration 3/20 notes — 2026-06-05

Preflight and setup

• Delegated project initialization preflight confirmed this is a Rocq/Dune/opam proof project (dune-project, rocq-ticl.opam, theories/dune, CI workflow).
• Local toolchain remains usable: Rocq 9.1.1, Dune 3.22.0, opam 2.5.1.
• No checkout initialization or submodule setup was required; targeted baseline Yield build passed before implementation.
• The worktree was already dirty before this iteration: theories/Lang/Yield/Ticl.v modified, plus untracked research/ and specs/ directories. No files were staged.

Analysis decisions

• Analyzer found that the dirty Ticl.v already contained most of the iteration-3 public proof surface: generic expression arithmetic, generic assignment, flow-aware sequence facts, branch facts, while unrolling facts, generalized fork/spawn split facts, and aur_ystmt_yyield_erased.
• The main missing spec-level item was ag_ystmt_ywhile or a deliberately named invariant equivalent.
• Existing proof surface intentionally uses flow-aware/raw layers in several places (instr_stmt_flow_erased or denote_stmt_flow) rather than forcing all structural facts through scheduled instr_stmt_erased. This preserves Fallthrough/HaltThread honesty.

Implementation decisions

• Added the missing while invariant door in theories/Lang/Yield/Ticl.v rather than reorganizing modules.
• Added proof helper ywhile_iteration to expose one raw source-flow while-loop iteration.
• Added public theorem ag_ystmt_ywhile at the raw source-flow layer over denote_stmt_flow, matching the existing while unrolling theorem family.
• The ag_ystmt_ywhile theorem does not claim erased/instrumented state behavior. Callers supply an invariant predicate over worlds and a per-iteration premise that preserves the invariant on continuing (inl) loop iterations.
• No semantic definitions were changed, and no Admitted, admit, or Axiom was introduced.

Validation outcomes

• dune build theories/Lang/Yield/Ticl.vo passed.
• dune build theories/Lang/Yield/SBisim.vo theories/Lang/Yield.vo passed.
• Full dune build passed.
• rg -n "Admitted\\.|admit\\b|Axiom\\b" theories/Lang/Yield --glob '!_build/**' found no matches.
• Rocq admitted analyzer reported Admitted: 0 for theories/Lang/Yield.
• A /tmp Rocq public Check suite passed for required iteration-3 and regression names, including the new ag_ystmt_ywhile.

Residual risks / deferred work

• The public Check suite is currently a scratch validation artifact, not a committed regression test.
• The total diff summary for theories/Lang/Yield/Ticl.v versus HEAD is large (885 insertions, 2 deletions) because it includes pre-existing dirty proof-surface work in addition to this iteration's added while-invariant door.
• Some public theorem names intentionally target instr_stmt_flow_erased or raw denote_stmt_flow, not scheduled instr_stmt_erased; this is a semantic tradeoff to keep Yield flow boundaries explicit and may require downstream bridge lemmas later if clients need scheduled-unit forms.