Repository navigation
feat: verify runtime slice and subtraction operands by proven range - #931
Merged
Merged
Conversation
Echo's lowerer, verifier and native helper checker accepted core.bytes.slice and core.integer.subtract only with literal operands, so Jim's isUtf8(slice(text, 0, at)) with a runtime offset could not verify. Each now implements Edict's proven-range rules independently: a slice needs start <= end <= len(bytes) over that same operand, a subtraction needs right <= left, and an order holds for equal terms, a zero right side, ordered constants, an input constraint or an earlier conjunct of the same `all`. Conditional predicates, negations, later conjuncts and helper callers prove nothing. The bounded-read relations type both calls, so a read guard such as `at <= len(text) && isUtf8(slice(text, 0, at))` verifies; short-circuit evaluation sends an out-of-range offset down the authored path. Slices are typed Bytes<max=N> as Edict types them, so isUtf8 of a literal slice type-checks. A Core without a function table that contains either call is now judged in full, including its budget, as addition already was. Refs flyingrobots/amblicit#269
Contributor
|
Warning Review limit reachedYou've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository. Next included review available in 33 minutes. View limit details
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. |
Promotes the byte-identical G4 candidates from det-gates run 39583101692: lowerer sha256:6aed0c24 (491,504 bytes) and verifier sha256:083096b1 (510,119 bytes). Copies them into both provider packages, refreshes the manifest component digests, the provider digest sha256:41a77967 and the manifest raw digest 7e985673 in the package goldens, and the component READMEs. Refs flyingrobots/amblicit#269
Owner
Author
|
@coderabbitai review |
Contributor
|
…at/proven-dynamic-slice # Conflicts: # crates/echo-wesley-gen/assets/v1/edict-provider/package/v1/components/lowerer.echo-dpo.component.wasm # crates/echo-wesley-gen/assets/v1/edict-provider/package/v1/components/verifier.echo-dpo.component.wasm # crates/echo-wesley-gen/assets/v1/edict-provider/package/v1/provider-manifest.echo.json # crates/echo-wesley-gen/tests/provider_package.rs # crates/echo-wesley-gen/tests/provider_package_corpus.rs # schemas/edict-provider/README.md # schemas/edict-provider/components/v1/README.md # schemas/edict-provider/components/v1/lowerer.echo-dpo.component.wasm # schemas/edict-provider/components/v1/verifier.echo-dpo.component.wasm # schemas/edict-provider/package/v1/components/lowerer.echo-dpo.component.wasm # schemas/edict-provider/package/v1/components/verifier.echo-dpo.component.wasm # schemas/edict-provider/package/v1/provider-manifest.echo.json # xtask/src/provider_lowerer_component.rs
…at/proven-dynamic-slice
Promotes the byte-identical G4 candidates from det-gates run 39591924108, built from the merge of feat/byte-count-runtime (named count bounds) with the proven-range slice and subtraction proofs: lowerer sha256:6271a912 (492,758 bytes) and verifier sha256:5b156096 (509,828 bytes). Refreshes both package manifests, the provider digest (sha256:ce95e09c), the manifest raw digest golden, and the component READMEs.
…at/proven-dynamic-slice # Conflicts: # crates/echo-edict-provider-lowerer/src/executable_operation/source_functions/unsigned_addition.rs # crates/echo-edict-provider-verifier/src/executable_operation/source_functions/unsigned_addition.rs # crates/echo-edict-provider-verifier/tests/bounded_read/source_functions.rs # crates/echo-wesley-gen/assets/v1/edict-provider/package/v1/components/lowerer.echo-dpo.component.wasm # crates/echo-wesley-gen/assets/v1/edict-provider/package/v1/components/verifier.echo-dpo.component.wasm # crates/echo-wesley-gen/assets/v1/edict-provider/package/v1/provider-manifest.echo.json # crates/echo-wesley-gen/tests/provider_package.rs # crates/echo-wesley-gen/tests/provider_package_corpus.rs # schemas/edict-provider/README.md # schemas/edict-provider/components/v1/README.md # schemas/edict-provider/components/v1/lowerer.echo-dpo.component.wasm # schemas/edict-provider/components/v1/verifier.echo-dpo.component.wasm # schemas/edict-provider/package/v1/components/lowerer.echo-dpo.component.wasm # schemas/edict-provider/package/v1/components/verifier.echo-dpo.component.wasm # schemas/edict-provider/package/v1/provider-manifest.echo.json # xtask/src/provider_lowerer_component.rs
…ting Promotes the byte-identical G4 candidates from det-gates run 39600796482, built from the merge of feat/byte-count-runtime (count judgment gating and reused addition caps) with the proven-range proofs: lowerer sha256:b52ec57c (493,449 bytes) and verifier sha256:e1426a80 (510,251 bytes). Refreshes both package manifests, the provider digest (sha256:e82a973b), the manifest raw digest golden, and the component READMEs.
Owner
Author
|
@codex review please, focus on the merged judgment gating (add, subtract, slice, count), the combined read fixture helpers, and the promoted component digests |
|
Codex Review: Didn't find any major issues. 👍 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". |
flyingrobots
added a commit
that referenced
this pull request
Oct 21, 2026
Brings in count (#929) and proven-range slice and subtraction (#931). edict_pure::infer and check_predicate keep #921's crate visibility and take main's proof parameter; the effect instruction relation passes Proof::none(), so runtime slices and subtractions in effect programs still need literal operands until effect programs carry their proofs. Provider components and goldens take main's set until re-promotion.
4 of 5 tasks
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Echo's lowerer, verifier and native helper checker accepted
core.bytes.sliceandcore.integer.subtractonly with literal operands, so Jim'sisUtf8(slice(text, 0, at))with a runtime offset could not verify. This implements Edict's existing proven-range semantics, independently in each component, without weakening verification.start <= endandend <= len(bytes)over that same operand, which is its actual length, not its declared maximum. A subtraction needsright <= left. An order holds for equal terms, a zero right side, ordered constants, an input constraint, or an earlier conjunct of the sameall. Conditional predicates, negations, later conjuncts and helper callers prove nothing. Terms are compared by canonical encoding within each component's work ceiling.at <= len(text) && isUtf8(slice(text, 0, at))lowers and verifies. Runtimeallshort-circuits, so an out-of-rangeatmakes the guard false and the program takes its authored path. A program without the guard is refused before installation.Bytes<max=N>(the operand's maximum, no minimum), as Edict types them. Previously a literal slice was narrowed, soisUtf8<Bytes<max=N>>of a literal slice was refused.Finding: retained leaf-slice budget
Jim's compiler-produced leaf-slice package (
crates/warp-core/tests/fixtures/edict-byte-slice) declares a 1,048,576-step budget. Echo's worst-case charge for slicing its whole 1 MiB operand is 1,048,669 steps, 93 over, so both components now refuse that retained package. Edict's static cost model accepted the budget; Echo's says a maximal slice would exhaust it at runtime. The conformance tests here run the same program with a 2 MiB step budget: it is accepted, and refused once itslenconstraint is dropped. Reconciling the two cost models is follow-up work. The runtime evaluation test for that fixture is unchanged and passes.Tests
edict_pure::proven_range_tests(3): admitted guarded prefix, zero and end offsets, guarded suffix, guarded and literal subtraction; refused unguarded, guard after use, guard on another operand, guard on another offset, guard by declared capacity, disjunctive (negated) guard, guard in a conditional, guard in a sibling branch, unguarded, reversed and underflowing subtraction; runtime boundary results at offsets 0 to 4 andu64::MAX, with out-of-range offsets returning the authored result rather than failing.source_functions::proven_ranges(3): the same cases in both judgments, plus an intent-level subtraction proven by an input constraint and refused without it.bounded_read::source_functions::slice(3): guarded runtime slice of a read fact lowers and verifies; unguarded and late-guard forms refused by both.pure_relation(2): Jim's compiler-produced leaf slice is accepted by both when proven by its input constraints. Without its length constraint, the lowerer refuses it, and so does the verifier independently, against an accepted rebinding control.edict_*integration test.Component promotion follows from this PR's det-gates candidates.
Stacked on #929. Refs flyingrobots/amblicit#269.