Skip to content

feat(core): define canonical call action and retirement composition - #96

Draft
afflom wants to merge 10 commits into
v01/owned-general-enumerationfrom
v01/canonical-composition
Draft

afflom wants to merge 10 commits into
v01/owned-general-enumerationfrom
v01/canonical-composition

Conversation

@afflom

@afflom afflom commented Nov 5, 2026 •

Copy link
Copy Markdown
Member

The existing canonical helpers left call capture timing, transferred results, remaining-live-binding order and failed-action event order uncomposed. This adds source-owned composition that reuses CanonicalSchedule, CanonicalBindings, CanonicalCost and ReferenceSemantics.

  • Eager captures are resolved once per instruction, including zero loops; Scan observer captures precede updater captures. Each invocation still binds and charges its own parameters.
  • Explicit fresh/transferred completion prevents reallocation for Apply returns, final Fold state and completed Tabulate/Scan output. Equal values and null handles do not infer aliasing or origin.
  • Ascending logical slot keys determine frame retirement, excluding only the returned key and skipping holes.
  • A typed reference action cursor consumes events before index/basis attempts, retains the exact cursor on refusal, and preserves paid attempts across extension. Invalid index emits no byteRead; missing basis still pays its attempted referenceRead. Only success allocates a result and performs last-use release.
  • Loop prelude/finish composition reuses existing growth/state event helpers, with no completed-output-length allocation.

Validation is deliberately scoped: official language1.2 fmt/check and eight-root build pass for all22 modules (10 unchanged authority dependencies plus12 new modules). The65 general relation statements and64 registered controls are SOURCE-VALID, not yet kernel/execution qualified. Kernel qualification stops at the existing ad70 ReferenceSemantics.leaf_index_step_refines_independent_sequence proof (omega/Option observation goals). Six preceding dependency kernels pass; no proof was removed/pruned and no compiler/limit changed. Their exact-AX audit is230/232: RuntimeOpcode.fromCode and operandAt have pre-existing overdeclared Q/P policies. New mutation execution remains pending that dependency.

Official migration on private copies preserves all10 dependency declaration sets exactly. Public authority files, Engine, product language1.1 and release locks are unchanged. The machine owner separately owns instruction-prefix integration; these mathematical list/function carriers are not a shipped runtime fallback or a bounded-Engine acceptance claim.

Base ad70ad9; source29bd9d362f0e45a1e3d32c392d25da20c18925f4. No accepted production export, semantic-budget refinement or locked-SDK release acceptance.

Contract and exact API scope · Source-bound receipt

Authentic full parsed source for all12 new modules is public at tests/canonical-composition/parsed-modules.json (source29bd9d3; SHA256ddd73a21290a3bdad7df31f4f4b2c8d41508695069a9daa169f780dcc0fa56cc). No signatures/traversal were reconstructed. The exact existing blocked theorem IR, unchanged-source qualification command and eight actual omega contexts are public in reference-leaf-failure.json and reference-leaf-eight-contexts.txt. Only the official trace.omega CLI flag was added for diagnosis; original proof/module bytes are unchanged. Coordination separately owns the narrow dependency repair; this branch has no duplicate repair edit.

Actual generated-only experiments are now recorded separately: v1 fails positive with5residuals; v2 passes positive/rejects bothfalse/all79policiesexact; v3 repeats that gate using72metadata-derived constructor rules rather than a hardcoded project constructor. Both successful diagnostic modules evaluate unchanged definitions to the stated counterexamples, preserve the full theorem header, and restore all generated copies byte-exactly to the original eight-error failure. No diagnostic olean is installed as an original qualified foundation. These results establish generated-proof sufficiency only; the65source relations/64controls remain unqualified pending a supported source/official compiler route. No LexLean edit, semantics/SDK pin change or upstream implementation is claimed.

Alexander Flom and others added 10 commits November 5, 2026 01:35
Merge the preceding chain head into v01/canonical-composition and carry this
lane's unintegrated changes forward in SDK 1.2 form.

Verified integrated 1.2 sources owned by this lane:
- src/Uorc/Core/Bytes.lex.tex
- src/Uorc/Core/CanonicalActionComposition.lex.tex
- src/Uorc/Core/CanonicalActionCompositionProofs.lex.tex
- src/Uorc/Core/CanonicalActionCompositionTests.lex.tex
- src/Uorc/Core/CanonicalCallComposition.lex.tex
- src/Uorc/Core/CanonicalCallCompositionProofs.lex.tex
- src/Uorc/Core/CanonicalCallCompositionTests.lex.tex
- src/Uorc/Core/CanonicalComposition.lex.tex
- src/Uorc/Core/CanonicalCompositionProofs.lex.tex
- src/Uorc/Core/CanonicalCompositionTests.lex.tex
- src/Uorc/Core/CanonicalRetirement.lex.tex
- src/Uorc/Core/CanonicalRetirementProofs.lex.tex
- src/Uorc/Core/CanonicalRetirementTests.lex.tex
- src/Uorc/Core/ReferenceSemantics.lex.tex
@afflom
afflom changed the base branch from v01/product-integration to v01/owned-general-enumeration November 6, 2026 06:40
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant