Prove PeerAuthPQ_implies_PeerAuth via definitional refactor#2
Merged
ChristianoBraga merged 1 commit intoBeneficial-AI-Foundation:mainfrom May 3, 2026
Conversation
…l refactor
Converts PeerAuthPQ from an opaque Prop to a def over
`PeerAuth ∧ PQSPKAgreement`, making the implication theorem fall out
as `And.left`.
The previous opaque formulation made the theorem unprovable: Lean
cannot relate two unrelated opaque Props. The docstring already stated
the intended semantics ("PeerAuthPQ = PeerAuth plus PQSPK agreement"),
so this change makes the structure faithful to the spec.
Changes:
- New `opaque PQSPKAgreement` carrying the extra conjunct that
distinguishes Theorem 6 from Theorem 2 (KEM public-key agreement,
established under the SH-CR assumption).
- `PeerAuthPQ` becomes `def ... := PeerAuth ∧ PQSPKAgreement`.
- `PeerAuthPQ_implies_PeerAuth` proved as `And.left` (was `sorry`).
Downstream impact: `PQXDH_KEM_pubkey_agreement` (Theorem 6) still
produces `PeerAuthPQ` — it now has to produce both conjuncts, which
is closer to what its existing (still `sorry`) proof obligation
actually requires. No other callers consume `PeerAuthPQ`.
Build: `lake build` passes (2748 jobs). The previous sorry warning
at SecurityDefs.lean:402 is gone; unrelated PQXDH.lean sorrys
remain unchanged.
verilib probe 'peer_auth_pq_implies_peer_auth' was marked
`effort := "small"`; this matches that sizing.
Contributor
ChristianoBraga
left a comment
ChristianoBraga
left a comment
There was a problem hiding this comment.
Looks good to me too.
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
4 participants
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.
Summary
Closes the
sorryinPeerAuthPQ_implies_PeerAuth(PQXDHLean/SecurityDefs.lean:402) by making the relationship betweenPeerAuthPQandPeerAuthstructural rather than opaque.The previous formulation left both
PeerAuthandPeerAuthPQasopaqueProps, which makes the implication literally unprovable — Lean cannot relate two unrelated opaque declarations. The theorem's docstring, and theverilibprobe metadata (effort := \"small\",priority := \"medium\"), indicate that a small structural change was intended.Change
In
PQXDHLean/SecurityDefs.lean:opaque PQSPKAgreement— the extra conjunct that distinguishes Theorem 6 from Theorem 2 (KEM public-key agreement, established under the SH-CR assumption per §5.3.2 p. 480).opaque PeerAuthPQ→def PeerAuthPQ := PeerAuth ∧ PQSPKAgreement, matching the existing docstring ("Extended peer authentication —PeerAuthplus agreement over the PQSPK").sorrywithAnd.left.Net:
+24 / -5in one file.Fidelity to the spec
The paper (Bhargavan et al., USENIX Security 2024, §5.3.2) defines
PeerAuthPQas strictlyPeerAuthstrengthened with PQSPK agreement. The newdefis the minimal Lean encoding of exactly that statement.PQSPKAgreementremains opaque for the same reasonPeerAuthis — its truth is established externally (via CryptoVerif / the SH-CR reduction), not internally.Downstream impact
PQXDH_KEM_pubkey_agreement(Theorem 6,PQXDHLean/PQXDH.lean:437) producesPeerAuthPQas its conclusion. WithPeerAuthPQnow a conjunction, that theorem's goal unfolds toPeerAuth ∧ PQSPKAgreement— arguably a more honest proof obligation than the opaque form. Its body is stillsorryin the repo; unchanged by this PR.PeerAuthPQ.docs/PQXDHDocs/DocSecurityDefs.lean:134) uses:::definition, which accepts eitheropaqueordef. No docs change required.Verification
Before:
SecurityDefs.lean:402emitteddeclaration uses 'sorry'.After: that warning is gone. The five unrelated sorrys in
PQXDH.lean(258, 298, 371, 408, 437) are unchanged.Test plan
lake buildpasses on Lean v4.28.0 / Mathlib v4.28.0grep -n sorry PQXDHLean/SecurityDefs.leanreturns no hits (was: line 403)defform is acceptable for the Verso blueprint (docs build)