Repository navigation
Implement exact-parent authored graph effects - #921
flyingrobots wants to merge 48 commits into
Conversation
|
Important Draft PR not reviewedDraft PRs are not automatically reviewed by default.
To automatically review draft PRs, update your CodeRabbit configuration: reviews:
auto_review:
drafts: true
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
…nto feat/authored-effect-bridge
|
@codex review |
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
|
Codex Review: Didn't find any major issues. More of your lovely PRs please. Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
|
@codex review |
|
Codex Review: Didn't find any major issues. Already looking forward to the next diff. Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
|
The user confirmed that there are no existing saved histories and directed a single current version of each structure, format and implementation in main crates. Historical versions may exist only in separate upgrade/migration tools. This supersedes the V1-preservation proposal: the parallel V1/V2 catalogs currently on this branch must be replaced before this draft is ready. Commit 48d2d8a records the rule in contributor guidance and current architecture documentation; the plan now requires a coordinated compiler/runtime/consumer cutover. No additional parallel grant-admission path has been added. |
Goal
Implement the generic exact-parent evaluation-to-effect bridge needed by compiler-authored operations. Echo must witness actual reads, authenticate the package's laws, interpret typed instructions, derive its own patch, and publish atomically with receipts/WAL and fresh-engine recovery of the original decision. Application algorithms remain authored outside Echo.
Plan
Current status
Current data-checker checkpoint
cd75aa04makesExecutableOperationPackage::prepareavailable withouttrusted_runtimeornative_rule_bootstrap. It compiles the same current effect/Core/Target/profile checker, keeps trusted helper modules private in that build, and retains all owner-constructor gates. Fresh outer pins cannot admit invalid embedded compiler bytes or a substituted Core closure. Preparation does not authenticate source-to-Core compilation, select an authorized release pin, install a package, or grant invocation rights.Validation passed 97 tests with trusted-host features and the three publication controls with those features disabled. An external client compiles against the preparation API; imports of
TrustedRuntimeHostand the private frame helper are separately refused. Strict Clippy passed in default, trusted-host and bootstrap-only configurations; barewasm32-unknown-unknownlibrary checking and warnings-as-errors documentation generation passed with Rust 1.96. Full SPDX, format and diff checks passed. The fixtures remain explicitly synthetic, and this is not a component build/audit or public compiler proof.Public effect producer/verifier integration remains unfinished. Reusing the checker in the provider guest requires a coherent authenticated toolchain update: the runtime requires Rust 1.96, while component builds remain pinned to Rust 1.90. The previous
09239c7chosted run failed four checks: the lowerer build and G4 comparison rejected the stale checked component, the actual-host generated-helper comparison failed, and the downstream evidence gate failed. Current-head hosted checks are pending. No merge readiness is claimed.Schema checkpoint
09239c7cadmits the native factory's current effect envelope through the provider's owningecho-operation-packageroot. Anchored and effect envelopes reuse a common current field group. Effect closure metadata has no duplicate outer lawpack; anchored projection/lawpack requirements remain intact. The program remains opaque to schema admission. A malformed-program control passes metadata admission but is refused by runtime preparation even with a fresh package pin.A synthetic factory-produced wire control first passed the current runtime decoder and failed owning-root admission, then passed both after the schema change. Current-schema tests cover required fields, 32-byte identities, budget/coordinate types, closed envelopes, unsupported schema versions and extra outer lawpack metadata. Native related validation passes 168 tests across 13 suites with one ignored test, plus strict changed-target Clippy, full SPDX checking, formatting and all artifact/package/asset freshness checks. Schema, helper, provenance, package metadata and digest goldens were regenerated together. Current schema is
167cda41b4dd0b7a4c5f1fd63e9539ea3111027c3a9ea263a6faad789a7dde1d; metadata package issha256:25d2b8a67768b5522ad36b474131da5df4a7b60a9b4e6c269996633ac312400c.The native
effect_publication::encode_effect_publicationfactory preserves the retained compiler bundle and derives embedded identities. It produces untrusted proposals, is not called by the public lowerer yet, and does not verify compiler correspondence, graph-law semantics, policy authority or execution. Synthetic controls are not public compiler outputs or independent verifier results. Runtime decoder dependencies/features remain dev-only for the producer.The preceding catalog-transport checkpoint requires explicit bounded
intrinsicCatalogbytes and checks canonical encoding, root shape and the exact owner-framed reference in the selected target profile. Its refusal controls remain green. Existing exact profile admission and catalog-to-export nominal agreement remain enforced.Publication boundary: current source/helper schema is
167cda41b4dd0b7a4c5f1fd63e9539ea3111027c3a9ea263a6faad789a7dde1d, while the checked lowerer is still the71d70c63component (d9b82fa4...d4450e0) binding the preceding schema. All 44 hosted checks passed for 71d70c6; current-head publication checks are expected to report this known mismatch until the coherent producer/verifier change is published. Main #925 is merged at c4745f8 with all six post-merge workflows green.The PR remains draft. Genuine public effect compilation, validated public producer integration, independent verification, complete authenticated profile/catalog delivery and the remaining runtime acceptance scope below are unfinished. Parallel historical contract/configuration/Target-IR paths remain unfinished under the user's one-current-version policy. No package generated by the public effect compiler path or installed execution is claimed.
One current publication, program sum, semantic closure, admission policy/token, installed record/catalog, invocation and recovery collection serve fixed and authored-effect program kinds. Owner invocation admission independently checks installed meaning, authority/grants, input binding, budgets and the actual parent. Installation recovery works, including fixed-program Action recovery with an effect installation present in either installation order. Superseded structures and decoders were removed without compatibility aliases. The user confirmed there are no saved histories to preserve; historical versions belong only in separate migration tools.
The exact
echo.compiler-produced-effect-program/v1bundle binds canonical Core, ordered Target IR and exports. Bodies with effects additionally require canonical source, lawpack, adapter, target-profile and intrinsic-catalog artifacts. Preparation checks their hash chain, selected intent/output, shared constraints/budgets/basis, complete instruction order, lexical references, adapter authorization and mapped failures. Imported declarations bind to exported definitions; shared inference preserves nominal identities. Concrete single-argument signatures and fault contracts must agree with the catalog. The implemented node-read ABI independently fixes three 32-byte address fields, a bounded direct byte result and four fault tags/classes. The five mutation emitters below are also recognized; further intrinsic families, polymorphism and positional argument unpacking remain unsupported.Private ordered authored evaluation now runs through
EffectEvaluationFrame::evaluate_effect. It requires a runtime-bound frame, exact program/frame footprint-law equality and a valid typed aperture. Typed let/read/require instructions reuse the existing expression/helper evaluator, runtime value checks, cumulative meter and real typed recording adapter. Core/program/frame resource ceilings intersect. Successful node/atom pairs must satisfy the prepared graph schema. False requirements evaluate their terminal payloads; supported zero-argument mapped failure constructors yield their authored source-context name and empty payload. Refusals terminate the frame and retain completed dependencies. Successful calls retain cumulative usage and observations.Five compiler-targeted mutation emitters now buffer typed
EnsureNode,CreateNode,ReplaceAtom,EnsureEdgeandReplaceEdgeintents. They require the explicitcontinuum.profile.graph-effects/v1Core/Target profile, concrete single-record arguments and empty-record results. The runtime fixes their input fields and 32-byte identities independently of metadata, keeps node and atom types distinct, and retains replacement comparisons. Each emission atomically admits one step, 280 logical row bytes and fixed write bytes: 64 plus atom payload length for node/atom effects, or 128 for edges. The already charged payload moves into the typed intent without copying. Only a successful whole authored operation retains its entire buffer; guard/resource/output failure discards its partial intents. Whole authored evaluation requires an unused frame and ends evaluation on success, so another component/program cannot contribute work or append to the result. Read-only profiles cannot authorize emission. The frame exposes a read-only data view, with no public entry point accepting caller-constructed intents as evidence. Emission reads no target state and modifies no frontier, but its fixed write-byte charge applies even when Ensure later resolves identically. A whole operation may emit at most 1,024 effects, including duplicates and later no-ops. The next emission refuses without exposing a partial buffer, while retaining prior successful charges. Proposal resolution still determines actual write slots.A consuming
into_effect_evaluationcrossing now returns one opaqueCompletedEffectEvaluation, retaining the exact producing program identity, canonical-input basis binding, actual output, emitted intents and actual recorded-read image. Program identity and input-basis recipes are shared with the existing program identity and invocation admission code. The input binding must equal the runtime parent's application basis. Changing otherwise valid input cannot yield completion under its old binding. Output storage is borrowed during evaluation and moved into completion with the intent buffer; it is not cloned. Unused/failed/mixed frames and bounded read-export failures cannot deliver this completed value. The sole full parent and usage counters come from the read image. This is execution-origin evidence, not installed-package authority or independent compiler/verifier approval.The runtime owner consumes a completed evaluation and independently admitted invocation to derive a counterfactual patch at the exact unchanged full parent. Both admission and completed evaluation must carry this owner's private process-local evaluation authority, in addition to installation/program/parent checks. An adversarial witness reproduced foreign completion crossing when parent tuples matched but detached store contents differed. The frame now moves its owner binding into opaque completion, and derivation refuses that foreign origin before using its data. Matching reachable-state roots do not establish equal stores. Owned-parts host reconstruction preserves the authority; it is not serialized recovery evidence.
All five effects have operation-shape witnesses. Validation enforces schema, content/mutable-slot identity, comparisons, endpoints, typed permissions and resolved write limits. Idempotent Ensure emits no writes but retains emission costs and still requires write permission. Validation usage includes successful evaluation and resolution prefixes. Prior-read reachability uses canonical read-image slot order. Descendant mutation tests verify one- and two-level alpha-portal dependency slots and exact charges, with forbidden-owner/beta refusal witnesses. Read-only authored work retains its two observed slots in an empty derived patch without recharging. Independent program and application-basis substitutions refuse under the same owner. Competing-failure witnesses cover schema/identity/footprint/precondition phase precedence.
This remains private whole-parent derivation. No operations are applied and installed authored-effect Action dispatch still refuses. Scoped-history admission, same-Tick conflicts, physical allocation guarantees, retained decisions and original-decision recovery remain open. Additional adversarial coverage and the full scoped-history/composition contract remain required before treating the bridge as complete.
The public configuration boundary now recognizes an explicit
edict-effect-program/v1declaration with nonempty encoded graph-schema/footprint-law payloads, identity law 1, bounded input/result/allocation ceilings and explicit I/O/step budget. A fresh unmodified Edict build at1d287efand admitted source-function provider candidates give a controlled witness: identical authored source/lawpack/configuration hashes refuse at05-target-configurationbefore this schema change and reachProviderLowererRefused / UnsupportedSemanticsafterward. An existing public bounded-read control still succeeds with package and independent verifier-report bytes identical to the original provider. No emitted Core or Target IR is rewritten. This does not produce or verify a generic authored-effect package: the lowerer route and target intrinsic/profile/resource work remain open. Existing fixed-operation v1/v2 configuration dispatch is also still noncompliant with the single-current-version rule and must be consolidated.Producer-boundary checkpoint validation: 69 tests across eight Wesley generation/schema/package/corpus suites pass, along with strict changed-target Clippy, formatting/SPDX/feature scheduling and all three artifact/package/assets exact checks. Generated schema, provenance, package manifest and consumer golden pins are refreshed together. Prior runtime-owner checkpoint validation below covers the unchanged runtime code, not a new full core run.
The retained raw public capture has inconsistent lawpack pins, a prior Target IR profile reference and a catalog declaring only the original replace fixture. Positive tests use an explicitly synthetic, coherently repinned read catalog and artifact chain. They do not prove genuine public effect compilation or independent verifier acceptance. Complete source-to-Core proof, graph-schema/export authority, target schema/profile resources, general intrinsic contracts, constructor payload/taxonomy authority and cost/footprint/configuration calculus remain open. Complete pure-main/projection refinement-aware static typing also remains open.
The approved proposal requires emission charges and a 1,024-effect ceiling. The buffering prototype incorrectly deferred write-byte charging and omitted the count ceiling. Those corrected semantics remain enforced during private mutation validation/patch derivation. Fixed step/write/row admission is atomic; a write-budget or row-reservation failure commits none of that emission charge. Earlier expression work and successful emission charges remain consumed even when the operation later fails.
Validation for this checkpoint: all 80 package tests pass. The cross-owner completion witness failed before the owner binding and passed after it. Final-source owner/host-enabled core validation passed 2,164 primary tests, zero failures and nine ignored across 100 primary Cargo groups, including 30 passing doctests and six ignored. Six child-process test results also pass, yielding a raw log total of 2,170 passes across 106 result groups. The count audit selects each top-level harness result once. Final strict all-target owner/host Clippy, formatting, global-state/nondeterminism/serialization guards, SPDX and feature-test scheduling pass.
The trusted-runtime-only library Clippy configuration still reports a dead-code warning in the unchanged
receipt_correlations_for_current_basismethod. New derivation internals are gated consistently with the runtime-owner host. The owner/host-enabled strict all-target configuration passes. Fresh hosted checks must finish for this pushed head. The PR remains a draft.The genuine flat-text capacity probe at
b46455csucceeded through 65,536 bytes but refused at 1,048,576 bytes under the tested allocation/shared-step ceilings. Full-size acceptance, remaining language capabilities, complete AVL acceptance and the final Jim dependency update remain part of the cross-repository objective.