Skip to content

Plonky3: Modulo Arithmetics Support#52

Open
YunkaiZhang233 wants to merge 15 commits intomainfrom
yunkai@modulo-arithmetics
Open

Plonky3: Modulo Arithmetics Support#52
YunkaiZhang233 wants to merge 15 commits intomainfrom
yunkai@modulo-arithmetics

Conversation

@YunkaiZhang233
Copy link
Collaborator

Started supporting modulo arithmetics with Coqtail

  • refactored MLessEffects so operators are listed in separate files for structure
  • replaced previous axioms with actual theorem proofs
  • completed the lemma in MLessEffects (but temporarily breaking easy tactic in keccak/round_flags due to change of lemma statement)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants