Repository navigation
feat(warp-core): carry proven-range facts through authored effect programs - #934
flyingrobots wants to merge 2 commits into
Conversation
…grams Effect programs were judged with an empty proof, so a runtime slice or subtraction needed literal operands and Jim's isUtf8(slice(text, 0, at)) could not run inside an edit. Preparation now follows Edict's rules: the intent's input constraints dominate the whole body, an unsigned let proven below its width carries that ceiling to later nodes, and an addition bound also uses a dominating fact comparing its term with a constant. Earlier conjuncts of one all still prove later ones. A require proves nothing after it, as in Edict.
|
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 20 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. |
…roofs # Conflicts: # CHANGELOG.md
Summary
Authored effect programs were prepared with an empty proof, so a runtime
core.bytes.sliceorcore.integer.subtractinside an effect program needed literal operands. Jim's flatReplaceRangeneedsisUtf8(slice(text, 0, at))with a runtimeatinside its edit. Preparation now follows Edict's proven-range rules (edict-syntax/src/target_ir/totality.rs), implemented independently in Echo:letproven below its width carries that ceiling to later nodes (counts, literals, sums, or a constraint such asat <= 10).term <= c,term == c, either side), as Edict's do. This also applies to conjunct prefixes inside helper predicates.allprove later ones (unchanged).requireproves nothing after it, matching Edict: it ends evaluation on failure but is not a dominating fact.Only warp-core changes. The provider lowerer and verifier don't judge effect-program bodies yet, so no component promotion is needed.
Tests (
tests/edict_effect_package_tests/proven_ranges.rs, 9)at <= len(text)proves a runtime prefix slice; without it, or with the constraint on another operand, the program is refused at preparation.requireguard before the slice does not prove it (refused).letcount carries its ceiling:count + (u64::MAX - 64)accepted,- 63refused.letand later additions:at <= 10accepts+ (u64::MAX - 10), refuses- 9;at == 10and10 == atdo the same.at <= len(text) && isUtf8(slice(text, 0, at))on"hé"accepts offsets 0, 1, 3 and takes the authoredapp.BadOffsetobstruction for 2 (insideé), 4 andu64::MAX; the same check outside its conjunction is refused before it runs.The three positive cases failed before the change.
Test plan
cargo test -p warp-core --features native_rule_bootstrap,trusted_runtime,host_test,delta_validate(114 suites)cargo clippy -p warp-core --all-targetswith those features,-D warnings(Rust 1.96.0, the pinned toolchain)scripts/ban-globals.sh,scripts/ban-nondeterminism.sh