fix: EQ over cross-kind SigmaProps throws when the left is a conjecture#888
Open
mwaddip wants to merge 1 commit into
Open
fix: EQ over cross-kind SigmaProps throws when the left is a conjecture#888mwaddip wants to merge 1 commit into
mwaddip wants to merge 1 commit into
Conversation
Scala DataValueComparer.equalSigmaBoolean (DataValueComparer.scala:253) dispatches on the LEFT node: the leaf arms (ProveDlog / ProveDHTuple / TrivialProp) return false on a mismatched right via their inner `case _ => false`, but the conjecture arms are guarded (`case CAND(children) if r.isInstanceOf[CAND]`), so a conjecture left against a different-kind right falls through every arm to the top-level `case _ => sys.error(...)` and script evaluation THROWS. The behavior is asymmetric: `(pkA && pkB) == pkA` throws while `pkA == (pkA && pkB)` is false, and NEQ shares the comparer. Children recurse through equalSigmaBoolean, so nested mismatches inside matching tops throw too. Our Eq/NEq used derive-PartialEq, returning symmetric false everywhere — a guard script the JVM fails-with-exception evaluated to false and validated under sigma-rust. Route SigmaProp = SigmaProp through an equalSigmaBoolean mirror: matched leaves compare structurally; matched conjectures recurse (length mismatch false before children; Cthreshold k mismatch short-circuits before children); on a kind mismatch a leaf left is false and a conjecture left is an EvalError carrying the JVM message. Regression tests drive the four JVM-blessed byte vectors from the conformance corpus (santa-eval EQ_of_SigmaProp_conjecture_mismatch, parse blessed bytes -> eval) plus unit pins for the NEQ twin, the nested throw, structural recursion, and both short-circuits. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
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.
Scala
DataValueComparer.equalSigmaBoolean(DataValueComparer.scala:253) dispatches on the LEFT node: the leaf arms (ProveDlog/ProveDHTuple/TrivialProp) return false on a mismatched right, but the conjecture arms are guarded (case CAND(children) if r.isInstanceOf[CAND]), so a conjecture left vs a different-kind right falls through to the top-levelsys.error— eval THROWS, asymmetrically:(pkA && pkB) == pkAthrows,pkA == (pkA && pkB)is false. NEQ shares the comparer; children recurse, so nested mismatches throw too.Our Eq/NEq used derive-PartialEq (symmetric false): a guard script the JVM rejects-with-exception validated under sigma-rust.
Fix: SigmaProp==SigmaProp goes through an equalSigmaBoolean mirror. Tests drive four JVM-blessed byte vectors plus unit pins.