Prove source request-trace equivalence for yield lowering

[jasisz]

Follow-up to #1329, after the generated finite-history invariants in #1375.

The missing theorem compares the original direct-style function with its lowered process protocol under the same oracle. For every finite observable prefix they must produce the same ordered (operation, arguments, answer) events, allowing internal yields, and the same result when both reach Done. Equal final results alone are insufficient.

Original implementation prerequisites (source retention and dynamic trace observers are now implemented by #1377/#1378):

• yield_lowering::lower consumes the stamped source functions and retains protocols/signatures, but not source bodies for a second proof model. Preserve the original function and its module ownership before replacing it; do not reconstruct the source side from the generated machine.
• types/checker/effect_lifting.rs primarily assigns static call-site counters. Match arms advance the same compile-time counter, and ordinary helper calls do not return an updated occurrence counter. The special Process.stopRequested path threads a base, but is not a general process trace model. The source observer and protocol driver need dynamic executed-call positions, including repeated requests and in-place effects.
• main/commands.rs deliberately refuses proof export of process cases with process_verification; keep that refusal until the corresponding Oracle model is implemented. The VM driver in yield_lowering/verify.rs already executes the actual generated protocol and uses runtime stub counters; it is not an independent source specification.

Implementation / acceptance:

• Retain independently readable source definitions and precise origin mapping through module loading, including private and imported yielding helpers.
• Define concrete typed request/answer observations and the source and protocol transition semantics in ordinary generated Aver; no public user generics or handwritten example-only Lean companion.
• Thread dynamic Oracle state through branches, helpers and resumes. Internal yields consume no answer. State the in-place-effect and runtime conformance assumptions explicitly.
• Prove local source-to-protocol correspondence and compose it over arbitrary finite derivations/prefixes, with explicit helper-theorem dependencies. Different internal step counts must not be conflated with a common fuel number.
• Check the theorem using normal aver proof --check, with universal manifests and the existing axiom whitelist. Unsupported shapes must be explicit; sampled schedules cannot earn universal credit.
• Cover repeated calls of one kind, mixed kinds, branches, self yields, local/imported nested helpers, early completion, and in-place effects.
• Negative controls must reject dropped, duplicated, reordered and argument/answer-swapped requests even when the final return value remains unchanged; also catch Oracle counter resets across resumes.

The coordinator history laws already established by #1375 remain separate: slot counts, job bounds, and request-instance retirement over the pure transition fold. Provider answer-stability laws have their own consistency premises. Neither is the source request-trace correspondence theorem.

Current implementation slice — PR #1377 (merged)

#1377 retains original module-owned source and adds concrete typed source/protocol observers. Twelve ordinary Aver laws check arbitrary finite prefixes for branches, repeated/mixed requests, Unit/early errors, self yields, local/private/imported finite helpers and local in-place effects. The stateful auxiliary is an explicit dependency of the initial-state law. Six false trace laws remain unproved despite identical return values; VM/WASM and existing proof/history regressions pass locally.

This issue remains open. PR #1378 (merged) adds source tail-entry alignment for finite local and imported helpers. Each Advance resumes a source-defined tail boundary without consuming an answer; helper-local tail positions survive inlining. Eight new laws are universal, including arbitrary initial cursors; two false pause-counter laws fail despite unchanged results and events. PR #1380 (merged) implements local recursive helper/splice laws with explicit parent dependencies. PR #1381 (merged) adds owning-module composition for imported helpers, including finite wrappers around private recursive helpers. Imported in-place effects remain explicitly rejected. Effectful independent products and direct process-stub proof export remain unsupported. Runtime/provider and whole-coordinator conformance are not proved by this slice. Acceptance boxes above remain open until the corresponding scope is merged and complete.

Local recursive composition — PR #1380 (merged)

Local recursive helpers now get independent source/protocol observers in the caller's concrete trace types. Ordinary helper correspondence and per-call splice laws quantify over arbitrary finite input tapes, initial cursors, captured arguments and suspended child outcomes. Parent laws explicitly cite them; omitted citation lists preserve earlier available laws.

Seventeen new fixture laws are universal and axiom-audited: non-tail and tail entry, repeated helpers, nominal arguments, Unit answers, early errors and local in-place observations. Four false laws that preserve return values while corrupting cursor fields remain unproved. All 300 distinct local tests pass (46 proof regressions, 180 Lean exporter units, 74 protocol/runtime tests), as do strict Clippy and formatting. CI, all four Proof shards and selected Certification passed on final head 7d9f989 after integrating Lean 4.34. Squash-merged as 15ca84f.

The local slice is merged; this issue remains open. PR #1381 merged the imported splice/adaptor slice. Imported in-place effects and broader source/driver correspondence remain open; no runtime conformance, fairness or unbounded termination claim is added.

Imported recursive composition — PR #1381 (merged)

Owning modules export ordinary cursor and source-correspondence contracts. The cursor law quantifies over every suspended outcome, finite input tape and initial cursor; a caller-side mapping theorem transports the child's observations while preserving the caller's original input remainder and event prefixes. Ordinary splice laws compose repeated calls, tail entry and finite wrappers around private recursive helpers. Metadata carries theorem identities, not proof credit.

Both new fixtures pass normal Lean 4.34 proof checking: 41 universal laws total, no bounded laws/build errors/sorries, every law axiom-audited. All 336 distinct local tests pass: 10 source-trace proof regressions, 35 explanation/recursive-explanation and Knowledge integration proof regressions, 216 exporter/checker units, and 75 protocol/runtime tests (including VM and wasm-gc). Strict feature-enabled Clippy and formatting pass. CI, all four Proof shards and selected Certification passed on final head 27575d2 before squash merge.

The proof-search improvements work from checked function shapes and explicit citations: predicates of recursive results, list-map transport, summarized adapters, named Bool explanations and constructor-specific continuation equations. No fixture-name dispatch, added axiom, increased proof budget or measured speedup is claimed. A related checker fix prevents cached type stamps from reviving failed inference during retained-source checking.

Next: imported in-place effects, then the remaining source/driver correspondence. The broad acceptance boxes stay open pending complete, merged coverage.

Remaining implementation sequence

1. Imported in-place effects (Prove source request-trace equivalence for yield lowering #1376). Export an owning-module observation interface for actual generated Start/Answer segments. The importing caller maps its typed tape and composes the checked observation while preserving the dynamic operation position, consumed-input count, event prefix and original remainder. Keep the source observer independent. Cover effects before/after a request, repeated imported calls, private recursion, nested imports, early errors and caller-only tokens. Require ordinary Aver laws universally checked by Lean and axiom-audited; negative controls must catch dropped/reordered effects and reset counters even when return values agree. Execute the same observers on VM and wasm-gc. Correct the stale last paragraph of docs/yield-request-traces.md that still calls recursive import composition pending.
2. Close the remaining source/driver correspondence in Prove source request-trace equivalence for yield lowering #1376. Connect the retained-source observer and checked protocol contracts to the execution-driver model over arbitrary finite observable prefixes. State the shared-oracle/runtime-conformance assumptions explicitly and keep them distinct from proved equalities. Audit each acceptance box against a checked theorem or a documented scope boundary; imported-effect support alone does not close the whole issue.

The broader concurrency and proof-performance roadmap is kept in #1329.