Conversation
…es, examples. Stages 4-6 of enabling (a*b)^x = a^x * b^x: core/public.v, the HeapLang primitives, lib/dh.v and the case studies. Lemmas whose base must now be an atom gained negb (is_mul _) / negb (is_inv _) premises; public_TExp, TExpA, TExpK, TExp_TMulN, TExp_TInv, minted_base_exps and twp_texp stay unconditional. New factor-level API, for protocols that exponentiate an attacker-supplied value and so cannot assume an atomic base: algebra.v is_inv_TExp, TExp_injl, invs_canceled_TExp, factors_TExp subterms.v subterm_factors, subterm_TExp_factors public.v public_TExp_factors The OPAQUE server exercises all of them. It also needs a group-membership check it never had: 1 ^ x = 1 drops the server's ephemeral secret out of the session key, so Server.session now rejects an identity X_u -- the check its own TODO was already asking for. CLAUDE.md records the endomorphism law, the atomic-base wf invariant, and both downstream consequences. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E8khwa8zca1fMdMbwHLikG
PTMul is replaced by PTN of term_opN & list pre_term, mirroring PT0/PT1/PT2. term_opN currently has the single constructor ONMul, with the same derived eqType/choiceType/countType/orderType instances as the other operation types, and PTMul ts becomes a Notation for PTN ONMul ts (alongside PTInv/PTExp). Keeping PTMul as a notation means product-specific matches read as before and, once term_opN gains a constructor, become non-exhaustiveness errors rather than silently taking the product branch. The HeapLang encoding follows the arities too: outer TOpN_tag = 3, inner TMul_tag = 0, PTN o ts represented as (#TOpN_tag, (repr o, repr_list ...)). eq_term, leq_term, hl_is_mul, hl_one, hl_factors and hl_mul_aux are updated accordingly, with eq_term_opN / leq_term_opN and their specs. Order plumbing: leqE's PTN case compares the operation first, as PT1/PT2 do; with_stdpp.v gains int_of_term_opN / opN_le / opN_leE, and pt_order_mul becomes pt_order_N, quantified over the operation. Case patterns in the n-ary branch now destruct the operation -- [] rather than a binder, so is_mul and friends keep reducing as before, and a second n-ary operation fails loudly. Structural functions that ignore the operation (height, tsize, nonces_of_pre_term) match on PTN _ ts; product-specific ones (is_mul, factors, wf, normalize) stay on PTMul. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E8khwa8zca1fMdMbwHLikG
Owner
Author
|
NB As it stands, this doesn't make much sense. Because inverses are total, the group of exponents is a symbolic model of the integers modulo some prime number p. But |
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.
This pull request enables the distributivity equation
(ab) ^ x = a^x b^x. This equation means that the group of exponents is the same group as the Diffie-Hellman group.