primality constraint #882
primality constraint #882
Conversation
|
The primality constraint and prime field inverses are now fully implemented. Remaining tasks are to add some unit tests and documentation. |
|
Do the changes to the |
Yeah, that might make sense. I was planning to also unify some of the What4 and SBV code paths, and maybe all of that makes more sense as separate PR. |
robdockins
force-pushed
the
primes2
branch
2 times, most recently
from
d3a1fa8
to
1f5b892
Compare
robdockins
force-pushed
the
primes2
branch
2 times, most recently
from
09283bb
to
515a9da
Compare
There was a problem hiding this comment.
Looks good to me. At first I was a bit unsure about using a trie to cache primality checks; is the time savings worth the memory cost? But considering the typical use case, it probably is: Users will have a few fixed (probably large) prime constants in their source files, and you'll have to discharge primality constraints on the same numbers every time you use one of the overloaded primitives.
and the What4 symbolic simulator. We use the EGCD algorithm to compute inverses for concrete values. For symbolic values, we posit a multiplicitive inverse via a defining equation. To get this to work, we needed to fix a bug in the equation definition code for What4; it was asserting definitions with the wrong polarity for "prove" calls.
This involves adding the ability to assert definitional relations, and porting the What4 method for modular inverse.
modular inverse computations instead of using the arithmoi and semiring packages.
and finite field inverse computations.
Tracks the changes in Cryptol from GaloisInc/cryptol#882 which adds primality testing to the Cryptol type system, and implements field operations for `Z p`. Currently, we don't represent the primality test in SAWCore, but we might revisit this aspect in the future.
Dust off some experimental work on a type-level primality constraint, and push it forward.
This PR implements a primality constraint, which is implemented in the typechecker via a probable prime test. The type
Z pis added to theFieldclass under the constraintprime p, andrecipis defined viaEGCDfor concrete values. For symbolic values, the What4 backend posits the multiplicative inverse via a defining equation. The SBV backend needs to be enhanced with the same definition equation capability the What4 backend has to complete this work.