Repository navigation
feat(provider): judge authored effect programs in the lowerer and verifier - #935
flyingrobots wants to merge 1 commit into
Conversation
…ifier
Echo's runtime was the only component that judged an authored effect
program. The provider lowerer and verifier now each judge one themselves,
sharing no code with the runtime or each other:
- binding to the program's own Core, Target IR and exports;
- the pinned lawpack, adapter, target profile and intrinsic catalog that
authorize each effect;
- each effect's runtime ABI, write class and failure contract through the
intrinsic-scoped failure table, with one declared obstruction per arm;
- node-for-node Core and Target IR correspondence;
- the body's types, proven ranges (input constraints dominate, let caps
carry, a require proves nothing) and declared budget under each
component's own cost model.
effect_publication::encode_effect_publication runs the lowerer's judgment
before serializing and refuses unsafe programs with UnsupportedProgram;
effect_publication::judge_effect_program exposes it. The verifier's
effect_package::verify_effect_package also binds every identity the package
claims, its operation, output and footprint contract to the program it
carries.
warp-core generates and pins a verdict corpus from its own fixture builders
and asserts the runtime's verdict on each entry; the lowerer and verifier
reach the same verdicts on the same bytes. The providers' cost models are
stricter than the runtime's meter, so the captured node-atom read's 1 MiB
step budget and the synthetic wire control's one-step budget are refused
before installation; the wire control now declares 1,024 steps and the
retained publication controls are re-emitted.
Both components' Core type readers now accept an unsigned width named
directly in a type table ({ kind: "U32" }), as Core and the runtime do.
|
Important Review skippedAuto reviews are disabled on base/target branches other than the default branch. Please check the settings in the CodeRabbit UI or the ⚙️ Run configuration
You can disable this status message by setting the Use the checkbox below for a quick retry:
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 |
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. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 0c522565ef
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
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".
| for (value, expected) in [ | ||
| (get(closure, "core_identity", E)?, &judged.core_identity), |
There was a problem hiding this comment.
Changing only semantic_closure.canonical_meaning_identity in an accepted corpus package to an unrelated digest still returns Ok(()): this loop checks core_identity but never checks the separate canonical meaning claim. The lowerer sets both identities to the Core digest, and warp-core/src/echo_operation.rs subsequently uses canonical_meaning_identity as the installed operation's semantic identity and carries it into receipts. Consequently, verification accepts an executable attributed to a meaning it does not implement. Require this field to equal judged.core_identity and add it to the identity-mutation tests.
Useful? React with 👍 / 👎.
| for constraint in list(get(intent, "inputConstraints")?)? { | ||
| cost = cost.plus( | ||
| self.predicate(get(constraint, "predicate")?, &scope, true, 0)? | ||
| .0, | ||
| )?; | ||
| self.proven.push(get(constraint, "predicate")?); |
There was a problem hiding this comment.
Publishing each constraint immediately lets later input constraints use earlier ones as range proofs. For example, adding a second constraint that evaluates isUtf8(slice(text, 0, at)) after the existing at <= length(text) constraint in slice-proven is accepted by the lowerer. However, warp-core/src/edict_effects/instruction_relation.rs:51–58 checks every input constraint with an empty fact set and only then publishes their facts, so runtime preparation rejects that same program for an unproven slice. The verifier's new effect_intent loop has the same discrepancy. Audit all constraints first, then expose their predicates to the body, preserving sequential proof propagation only within an all predicate.
Useful? React with 👍 / 👎.
| if conforming && unit { | ||
| Ok(Cost { | ||
| steps: 1, | ||
| bytes: 64, | ||
| }) |
There was a problem hiding this comment.
For mutation programs with a tight maxAllocatedBytes, the ABI charge includes only the 64-byte unit result and omits the additional 280 bytes that warp-core/src/edict_effects/frame.rs::charge_emission reserves for every emitted mutation. The verifier's ABI cost has the same omission. Rebinding ensure-node-control with a Core allocation budget of 3,978 bytes is accepted by both providers, but an allowed input containing 1,024 atom bytes consumes that budget plus the unaccounted reservation and fails during execution despite passing the static budget judgment. Include the emission reservation in both cost models and add a tight-allocation mutation witness.
Useful? React with 👍 / 👎.
1 participant
Summary
Until now only Echo's runtime judged an authored effect program. The provider lowerer and verifier now each judge one themselves, sharing no code with the runtime or with each other. This meets the ruling's requirement that the lowerer and verifier independently establish that the executable respects its contract.
Each component establishes:
letcaps carry forward, earlier conjuncts prove later ones, and arequireproves nothing.Where it runs:
encode_effect_publicationjudges before serializing and refuses unsafe programs withUnsupportedProgram.judge_effect_programexposes the same judgment.effect_package::verify_effect_packagealso binds every identity the package claims, its operation, its output type and its footprint contract to the program it carries (InvalidBinding).Evidence
warp-core generates a verdict corpus from its own effect-package builders, asserts the runtime's verdict on every entry, and pins the bytes under
crates/echo-edict-provider-lowerer/tests/fixtures/effect-programs. The lowerer and verifier tests embed the same bytes and must reach the same verdicts.I traced the refusing stage for every entry in both components, so each forgery is refused by the check it targets. Every refused entry other than the two budget cases carries an ample budget.
The verifier tests also cover:
Behaviour changes, please review
read-captured-budget.{ kind: "U32" }), as Core and the runtime already do. This changes the components, so they are re-promoted..ban-nondeterminism-allowlistentry for the corpus's explicit, ignored regeneration test.Test plan
native_rule_bootstrap,trusted_runtime,host_test,delta_validate(corpus verdicts, every existing suite)cargo clippy --workspace --all-targets -D warnings, plus warp-core with its test featuresscripts/ban-globals.sh,scripts/ban-nondeterminism.sh, Prettier, markdownlint, pre-push gate