FEAT-085 (#113): lattice laws for the bits domain, checked up to γ - #158
Merged
Conversation
…gamma scry#113 says the analyzer's frontend is unguarded. Measured: 18 join/meet functions across 8 domains, exactly ONE domain (octagon) has any lattice-law test, and it checks commutativity plus top-absorption on hand-picked values. No proptest/quickcheck/arbitrary/cargo-fuzz anywhere in the workspace. First slice: scry-sai-bits — 6 of the 18 functions, the most intricate arithmetic (CRT, mod_inverse), and the domain scry#105 already flags. CHECKED UP TO GAMMA, NEVER STRUCTURALLY, and that choice is the point. Two encodings can denote the same set, so `==` on representations is too strong — and this project has been bitten by exactly that: the Verus join proof (FEAT-012) was FALSE and unverified for months because it asserted `join(a,b) == join(b,a)` structurally, which fails for distinct bottom encodings. These assert the semantic version over the exhaustive [0,256) domain the crate already sweeps. The soundness-critical law is join_is_an_upper_bound_up_to_gamma: if a join drops an element, every fixpoint built on it under-approximates and the analyzer can report PROVEN-SAFE for something reachable. Commutativity, associativity and idempotence are hygiene; that one is the product. Its dual catches a meet that INVENTS an element. MUTATION-CHECKED SURGICALLY. Forcing `meet` to return TOP kills exactly meet_is_a_lower_bound_up_to_gamma plus one pre-existing test, and nothing else. A broad mutation (join returns self) also fires but is uninformative, because `alpha` is itself built from join — so the surgical one is the evidence. No new dependency: the crate already has an alpha/contains/sweep idiom, reused rather than adding proptest to a published crate. Credit: prompted by the Wasm Research Day Q&A, where a Binaryen engineer reported good luck fuzzing their own abstract domains for exactly this — independent corroboration from a second group, which beats an in-house opinion that fuzzing would be good. ALSO FIXES A PRE-EXISTING CLIPPY ERROR that blocked local verification here: a doc line beginning `> 2^63` read as an unterminated Markdown blockquote. Confirmed pre-existing by stashing and re-running on a clean tree — main fails identically. CI never saw it because the Clippy job covers only four packages, the same four the Test job used before scry#141. Filed as scry#157, with the lesson that widening one per-package gate did not fix the pattern. HONEST SCOPE: one domain. 12 of the 18 functions — interval, pentagon, float, handle, segment, poly, viz — remain unguarded. This does not make scry#113 done. tests=0 clippy=0 fmt=0 rivet=0 claim-check=0. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc
📐 rivet artifact deltaPR: #158 Base SHA: Validationhead — `rivet validate` resultbase — `rivet validate` result (for comparison)Artifact stats
full stats — headDiff (base → head)AADL model — headPosted by the |
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
1 participant
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.
First slice of #113. Also surfaces a second gate-coverage defect — filed as #157.
The gap, measured
18
join/meetfunctions across 8 domains. Exactly one domain (octagon) has any lattice-law test, and it checks commutativity + top-absorption on hand-picked values. Noproptest/quickcheck/arbitrary/cargo-fuzzin the workspace.This slice takes
scry-sai-bits— 6 of the 18, the most intricate arithmetic (CRT,mod_inverse), already flagged by #105.Checked up to γ, never structurally — and that's the point
Two encodings can denote the same set, so
==on representations is too strong. This project has already been bitten by exactly that: the Verus join proof (FEAT-012) was false and unverified for months because it assertedjoin(a,b) == join(b,a)structurally, which fails for distinct bottom encodings.These assert the semantic version over the exhaustive
[0,256)domain the crate already sweeps.The soundness-critical law is
join_is_an_upper_bound_up_to_gamma. If a join drops an element, every fixpoint built on it under-approximates and the analyzer can report PROVEN-SAFE for something reachable. Commutativity, associativity, idempotence are hygiene; that one is the product. Its dual catches ameetthat invents an element.Mutation-checked surgically
The surgical one is the evidence; I'm reporting the broad one as uninformative rather than counting it.
No new dependency — the crate's existing
alpha/contains/sweepidiom is reused rather than adding proptest to a published crate.Credit: prompted by the Wasm Research Day Q&A, where a Binaryen engineer reported good luck fuzzing their own abstract domains for exactly this. Independent corroboration from a second group beats an in-house opinion that fuzzing would be good.
It also unearthed #157
Local verification was blocked by a pre-existing clippy error on
main— a doc line beginning> 2^63, read as an unterminated blockquote. Confirmed pre-existing by stashing and re-running clean: main fails identically.CI never saw it because the Clippy job covers four packages — the same four the Test job used before #141. Widening one per-package gate did not fix the pattern; I checked
cargo testbecause that was the reported symptom and didn't ask the same question of the gate three lines above it.Fixed here since it blocks this branch; the scope defect is #157.
Honest scope
One domain. 12 of the 18 functions — interval, pentagon, float, handle, segment, poly, viz — remain unguarded. This does not make #113 done.
tests 0 · clippy 0 · fmt 0 ·
rivet validate0 · claim-check 0.