Repository navigation
Conversation
`FinType.card` was defined as `size enum`. A clone can only override a defined operator by a convertible term, so a `CyclicGroup` could not be given an abstract order: two cyclic groups of the same order `p` sharing one exponent ring, as needed for a pairing, could not be stated. On `main`, `clone CyclicGroup with op order <= p` fails with the anomaly `EcTheoryReplay.CoreIncompatible`. `card` is now an abstract operator specified by `axiom card_spec : card = size enum`. This is a conservative extension: interpreting `card` as `size enum` recovers the previous theory. In `CyclicGroup` the axiom is `order_spec`. Proofs that unfolded or folded `card` (or `order`), explicitly or by conversion, now rewrite with `card_spec` (FinType, Group, Distr, Tuple). Clones under `proof *` that fixed `enum` now also fix `card` and realize `card_spec` (FinProdType, ZModPCyclic, DZmodP, FiniteEager in ROM, the three clones in Word, and the ChaChaPoly and MEE-CBC examples). Clones that already set `card` discharge `card_spec` instead of leaving it as an axiom (Bool, DBool, DWord, BitWord). Downstream developments need the same adaptations: rewrite with `card_spec` (or pass it to `smt`) where `card` was unfolded, and define `card` in `FinType` clones under `proof *`. Test: tests/fintype-shared-card.ec. Co-authored-by: Thomas Haines <907287+gerlion@users.noreply.github.com>
Contributor
|
You can already get this behaviour by introducing an abstract I think that leaving both |
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.
Closes #1223.
What:
FinType.cardis now an abstract operator withaxiom card_spec : card = size enum(order_specinCyclicGroup). This allowsCyclicGroupclones with an abstract order, e.g. two groups sharing one order and oneZModEfor a pairing (tests/fintype-shared-card.ec, which hitsanomaly: CoreIncompatibleonmain).Stdlib adaptations (12 files): proofs that unfolded or folded
card/orderusecard_spec/order_spec;proof *clones that fixedenumalso fixcard; clones that already setcarddischargecard_spec. The commit message lists the affected theories.Testing:
make unit,make stdlibandmake examplespass on this branch and onmain(e704d26) with the provers pinned ineasycrypt.project(CVC5 1.1.2, Z3 4.16.0, Alt-Ergo 2.6.4). The new test passes here and fails onmain.Breaking change / external projects (run locally against each project's current default branch):
Cryptobox.ec:1248) that also occurs withmain, so unrelated.FinTypeclones underproof *that setenumbut notcard; the fix isop card <= size (<same list>)plusrealize card_spec. Two slh-dsa proofs also needcard_specpassed tosmt.The patches are ready; we can send them to the maintainers or provide them as
merge-feat/fintype-abstract-cardbranches, whichever you prefer.