From 43dfe5b6dec6deae65ca0fe5299301f661e90580 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sat, 31 Oct 2026 10:45:10 +0000 Subject: [PATCH 1/2] refactor(Crypto): replace projection chains across MPC, GMW, and SigmaProtocol modules (#1764) --- .../Encryption/EncryptThenMAC.lean | 10 ++-- .../Crypto/Computational/GMW/PolyTime.lean | 20 ++++--- .../Crypto/Computational/GMW/Simulator.lean | 23 +++++--- .../Crypto/Protocols/Cipher/EvenMansour.lean | 2 +- .../Crypto/Protocols/MAC/CarterWegman.lean | 56 ++++++++++--------- .../Crypto/Protocols/MPC/CircuitEval.lean | 9 +-- .../Crypto/Protocols/MPC/Composition.lean | 18 +++--- Complexity/Crypto/Protocols/MPC/PolyTime.lean | 12 ++-- .../Crypto/Protocols/MPC/SharedMul.lean | 44 +++++++-------- .../Crypto/Protocols/SigmaProtocol/Abort.lean | 2 +- .../Crypto/Protocols/SigmaProtocol/Basic.lean | 3 +- .../Protocols/SigmaProtocol/Composition.lean | 9 +-- .../Protocols/SigmaProtocol/FiatShamir.lean | 37 +++++++++--- .../Protocols/SigmaProtocol/Linear.lean | 9 +-- .../Lyubashevsky/NativeExtract.lean | 13 +++-- 15 files changed, 152 insertions(+), 115 deletions(-) diff --git a/Complexity/Crypto/Computational/Encryption/EncryptThenMAC.lean b/Complexity/Crypto/Computational/Encryption/EncryptThenMAC.lean index dc0b185de0..ec8221026a 100644 --- a/Complexity/Crypto/Computational/Encryption/EncryptThenMAC.lean +++ b/Complexity/Crypto/Computational/Encryption/EncryptThenMAC.lean @@ -219,7 +219,7 @@ noncomputable def encryptThenMAC (E : SymmetricCipher) (M : MACScheme) none keyGen_ppt := by have hpost : ComputableInPolyTime - (fun p : (ℕ × List Bool) × List Bool => encPair encBits encBits (p.1.2, p.2)) + (fun p : (ℕ × List Bool) × List Bool => encPair encBits encBits (Prod.snd p.1, p.2)) (encPair (encPair encUnary encBits) encBits) encBits := ComputableInPolyTime.encoding_comp (((ComputableInPolyTime.snd encUnary encBits).comp @@ -240,7 +240,7 @@ noncomputable def encryptThenMAC (E : SymmetricCipher) (M : MACScheme) (ComputableInPolyTime.snd I encBits) have hpost : ComputableInPolyTime (fun p : ((ℕ × List Bool × List Bool) × List Bool) × List Bool => - encPair encBits encBits (p.1.2, p.2)) + encPair encBits encBits (Prod.snd p.1, p.2)) (encPair (encPair I encBits) encBits) encBits := ComputableInPolyTime.encoding_comp (((ComputableInPolyTime.snd I encBits).comp @@ -2117,12 +2117,12 @@ noncomputable def prfCipher (family : List Bool → List Bool → List Bool) decrypt_polyTime := by have hfamTidy := hpoly.tidy have hcond : ComputableTidilyInPolyTime - (fun p : ℕ × List Bool × List Bool => p.2.2.length == 2 * p.1) + (fun p : ℕ × List Bool × List Bool => (Prod.snd p.2).length == 2 * p.1) (encPair encUnary (encPair encBits encBits)) encBool := by polytime have hyes : ComputableTidilyInPolyTime (fun p : ℕ × List Bool × List Bool => - (some (List.zipWith xor (family p.2.1 (p.2.2.take p.1)) (p.2.2.drop p.1)) : - Option (List Bool))) + (some (List.zipWith xor (family (Prod.fst p.2) ((Prod.snd p.2).take p.1)) + ((Prod.snd p.2).drop p.1)) : Option (List Bool))) (encPair encUnary (encPair encBits encBits)) (encOption encBits) := by polytime have hno : ComputableTidilyInPolyTime (fun _ : ℕ × List Bool × List Bool => (none : Option (List Bool))) diff --git a/Complexity/Crypto/Computational/GMW/PolyTime.lean b/Complexity/Crypto/Computational/GMW/PolyTime.lean index 1fbf5a5f7d..58cb29a175 100644 --- a/Complexity/Crypto/Computational/GMW/PolyTime.lean +++ b/Complexity/Crypto/Computational/GMW/PolyTime.lean @@ -517,7 +517,7 @@ theorem isPPTOn_runTwoRound {α Caller : Type} {enc : α ↪ List Bool} {input : {reply1 reply2 : Caller × List Bool → List Bool} {bound : Caller → ℕ} (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits - (fun p => Vstar p.1 p.2.1 p.2.2)) + (fun p => Vstar p.1 (Prod.fst p.2) (Prod.snd p.2))) (hprep : ComputableInPolyTime prepare input (encPair encUnary (encPair enc encBits))) (hr1 : ComputableInPolyTime reply1 (encPair input encBits) encBits) (hr2 : ComputableInPolyTime reply2 (encPair input encBits) encBits) @@ -526,7 +526,8 @@ theorem isPPTOn_runTwoRound {α Caller : Type} {enc : α ↪ List Bool} {input : (hle2 : ∀ c q, (reply2 (c, q)).length ≤ bound c) : IsPPTOn input (encPair encBits (encPair encUnary encBits)) (fun c => runTwoRound (fun q => reply1 (c, q)) (fun q => reply2 (c, q)) - (Vstar (prepare c).1 (prepare c).2.1 (prepare c).2.2) (0, [false, false, false])) := by + (Vstar (prepare c).1 (Prod.fst (prepare c).2) (Prod.snd (prepare c).2)) + (0, [false, false, false])) := by have hprep := hprep.tidy have hr1 := hr1.tidy have hr2 := hr2.tidy @@ -578,7 +579,7 @@ theorem isPPTOn_runTwoRound_prover {α Caller : Type} {enc : α ↪ List Bool} {openFlags bits ch_guess : Caller → List Bool} {seeds pads : Caller → List (List Bool)} (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits - (fun p => Vstar p.1 p.2.1 p.2.2)) + (fun p => Vstar p.1 (Prod.fst p.2) (Prod.snd p.2))) (hg : ComputableInPolyTime generator encBits encBits) (hn : ComputableInPolyTime n input encUnary) (hs : ComputableInPolyTime s input encUnary) @@ -670,7 +671,7 @@ noncomputable def gmwSimWithPads (generator : List Bool → List Bool) (s m : (fun r => proverReply1 generator m r (allOpenFlags φ ch_guess coins.1) coins.1 coins.2 pads) (fun _ => proverReply2 s φ ch_guess coins.1 coins.2) prog (0, [false, false, false]) - return if p.2.2 == ch_guess then true :: p.1 else [] + return if Prod.snd p.2 == ch_guess then true :: p.1 else [] /-- One attempt of the GMW zero-knowledge simulator (without any witness). -/ noncomputable def gmwSimAttempt (generator : List Bool → List Bool) (s m : ℕ) (φ : CNF ℕ) @@ -742,10 +743,10 @@ theorem isPPTOn_gmwSimulator {α : Type} {enc : α ↪ List Bool} (hlen : ∀ s, (generator s).length = length s.length) (hf : ComputableInPolyTime f enc encCNF) (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits - (fun p => Vstar p.1 p.2.1 p.2.2)) : + (fun p => Vstar p.1 (Prod.fst p.2) (Prod.snd p.2))) : IsPPTOn (encPair encUnary (encPair enc encBits)) encBits (fun p : ℕ × α × List Bool => - gmwSimulator generator length f Vstar p.1 p.2.1 p.2.2) := by + gmwSimulator generator length f Vstar p.1 (Prod.fst p.2) (Prod.snd p.2)) := by have hg := hg.tidy have hf := hf.tidy have hattempt := isPPTOn_gmwSimAttempt hg hlen hf hV @@ -827,11 +828,12 @@ theorem isPPTOn_gmwInteract {α : Type} {enc : α ↪ List Bool} (hlen : ∀ s, (generator s).length = length s.length) (hf : ComputableInPolyTime f enc encCNF) (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits - (fun p => Vstar p.1 p.2.1 p.2.2)) : + (fun p => Vstar p.1 (Prod.fst p.2) (Prod.snd p.2))) : IsPPTOn (encPair encUnary (encPair enc (encPair encBits encBits))) encBits (fun p : ℕ × α × List Bool × List Bool => - gmwInteract generator (p.1 + 7) (length (p.1 + 7)) (f p.2.1) p.2.2.1 - (Vstar p.1 p.2.1 p.2.2.2)) := by + gmwInteract generator (p.1 + 7) (length (p.1 + 7)) (f (Prod.fst p.2)) + (Prod.fst (Prod.snd p.2)) + (Vstar p.1 (Prod.fst p.2) (Prod.snd (Prod.snd p.2)))) := by have hgPlain := hg have hfPlain := hf have hg := hg.tidy diff --git a/Complexity/Crypto/Computational/GMW/Simulator.lean b/Complexity/Crypto/Computational/GMW/Simulator.lean index c365b4c3d6..0f956fdb9c 100644 --- a/Complexity/Crypto/Computational/GMW/Simulator.lean +++ b/Complexity/Crypto/Computational/GMW/Simulator.lean @@ -478,7 +478,7 @@ noncomputable def gmwRealWithPads (generator : List Bool → List Bool) (s m : (fun r => proverReply1 generator m r openFlags bits seeds pads) (fun _ => proverReply2 s φ ch_guess bits seeds) prog (0, [false, false, false]) - return if p.2.2 == ch_guess then true :: p.1 else [] + return if Prod.snd p.2 == ch_guess then true :: p.1 else [] /-- Single-attempt hybrid with pseudorandom unopened pads. -/ noncomputable def gmwRealPRGPads (generator : List Bool → List Bool) (s m : ℕ) (φ : CNF ℕ) @@ -918,14 +918,17 @@ theorem isPPTOn_gmwViewReduction {α : Type} {enc : α ↪ List Bool} (hlen : ∀ s, (generator s).length = length s.length) (hf : ComputableInPolyTime f enc encCNF) (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits - (fun p => Vstar p.1 p.2.1 p.2.2)) + (fun p => Vstar p.1 (Prod.fst p.2) (Prod.snd p.2))) (hadv : IsPPTOn (encPair (encPair encUnary (encPair enc encBits)) encBits) encBool - (fun p => adversary p.1.1 p.1.2.1 p.1.2.2 p.2)) : + (fun p => adversary (Prod.fst p.1) (Prod.fst (Prod.snd p.1)) + (Prod.snd (Prod.snd p.1)) p.2)) : IsPPTOn (encPair (encPair encUnary (encPair enc (encPair encBits encBits))) encBits) encBool (fun p : (ℕ × (α × (List Bool × List Bool))) × List Bool => gmwViewReduction generator length f Vstar adversary - p.1.1 p.1.2.1 p.1.2.2.1 p.1.2.2.2 p.2) := by + (Prod.fst p.1) (Prod.fst (Prod.snd p.1)) + (Prod.fst (Prod.snd (Prod.snd p.1))) + (Prod.snd (Prod.snd (Prod.snd p.1))) p.2) := by have hgPlain := hg have hfPlain := hf have hg := hg.tidy @@ -1027,9 +1030,10 @@ theorem gmwView_negligible_of_advice_prg {α : Type} {enc : α ↪ List Bool} (hlen : ∀ s, (generator s).length = length s.length) (hf : ComputableInPolyTime f enc encCNF) (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits - (fun p => Vstar p.1 p.2.1 p.2.2)) + (fun p => Vstar p.1 (Prod.fst p.2) (Prod.snd p.2))) (hadv : IsPPTOn (encPair (encPair encUnary (encPair enc encBits)) encBits) encBool - (fun p => adversary p.1.1 p.1.2.1 p.1.2.2 p.2)) + (fun p => adversary (Prod.fst p.1) (Prod.fst (Prod.snd p.1)) + (Prod.snd (Prod.snd p.1)) p.2)) (hPRG : ∀ test : (ℕ × (α × (List Bool × List Bool))) × List Bool → ProbComp Bool, IsPPTOn (encPair (encPair encUnary (encPair enc (encPair encBits encBits))) encBits) @@ -1111,9 +1115,10 @@ theorem AdvicePRG.gmwView_negligible {α : Type} {enc : α ↪ List Bool} (hAdv : AdvicePRG enc generator length) (hf : ComputableInPolyTime f enc encCNF) (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits - (fun p => Vstar p.1 p.2.1 p.2.2)) + (fun p => Vstar p.1 (Prod.fst p.2) (Prod.snd p.2))) (hadv : IsPPTOn (encPair (encPair encUnary (encPair enc encBits)) encBits) encBool - (fun p => adversary p.1.1 p.1.2.1 p.1.2.2 p.2)) + (fun p => adversary (Prod.fst p.1) (Prod.fst (Prod.snd p.1)) + (Prod.snd (Prod.snd p.1)) p.2)) {a : ℕ → α} {w z : ℕ → List Bool} (ha : PolynomiallyBounded (fun n => (enc (a n)).length)) (hw : PolynomiallyBounded (fun n => (w n).length)) @@ -1139,7 +1144,7 @@ theorem gmwView_indistinguishable_gmwSimulator {α : Type} {enc : α ↪ List Bo {f : α → CNF ℕ} (hf : ComputableInPolyTime f enc encCNF) {Vstar : ℕ → α → List Bool → WordOracleComp Unit (List Bool)} (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits - (fun p => Vstar p.1 p.2.1 p.2.2)) + (fun p => Vstar p.1 (Prod.fst p.2) (Prod.snd p.2))) {a : ℕ → α} {w z : ℕ → List Bool} (ha : ComputableInPolyTime a encUnary enc) (hw_comp : ComputableInPolyTime w encUnary encBits) diff --git a/Complexity/Crypto/Protocols/Cipher/EvenMansour.lean b/Complexity/Crypto/Protocols/Cipher/EvenMansour.lean index ca41828a6f..a1c9a956b6 100644 --- a/Complexity/Crypto/Protocols/Cipher/EvenMansour.lean +++ b/Complexity/Crypto/Protocols/Cipher/EvenMansour.lean @@ -1672,7 +1672,7 @@ theorem run_idealLazyHandler_good_le_realLazyHandler {α : Type} (program : OracleComp (EvenMansourSpec G) α) (P : α → Prop) (k : G × G) {c_e c_π c : Cache G} (hrel : CacheRel k c_e c_π c) : ((OracleComp.interpret idealLazyHandler program).run (c_e, c_π)).toOuterMeasure - {res | P res.1 ∧ isBadEvenMansourKey res.2.1 res.2.2 k = false} ≤ + {res | P res.1 ∧ isBadEvenMansourKey (Prod.fst res.2) (Prod.snd res.2) k = false} ≤ ((OracleComp.interpret (realLazyHandler k) program).run c).toOuterMeasure {res | P res.1} := by induction program generalizing c_e c_π c with diff --git a/Complexity/Crypto/Protocols/MAC/CarterWegman.lean b/Complexity/Crypto/Protocols/MAC/CarterWegman.lean index 42a50c10db..492754a01c 100644 --- a/Complexity/Crypto/Protocols/MAC/CarterWegman.lean +++ b/Complexity/Crypto/Protocols/MAC/CarterWegman.lean @@ -2885,13 +2885,13 @@ noncomputable def carterWegmanNonceMAC (msgLen : ℕ → ℕ) have hfamily_tidy := hfamily.tidy have hprf : ComputableTidilyInPolyTime (fun p : List Bool × List Bool × List Bool => - prfOracle family (dropFrame p.1).length (dropFrame p.1) p.2.2) + prfOracle family (dropFrame p.1).length (dropFrame p.1) (Prod.snd p.2)) (encPair encBits (encPair encBits encBits)) encBits := by have heq : (fun p : List Bool × List Bool × List Bool => - prfOracle family (dropFrame p.1).length (dropFrame p.1) p.2.2) = + prfOracle family (dropFrame p.1).length (dropFrame p.1) (Prod.snd p.2)) = (fun p : List Bool × List Bool × List Bool => - if p.2.2.length == (dropFrame p.1).length then - family (dropFrame p.1) p.2.2 + if (Prod.snd p.2).length == (dropFrame p.1).length then + family (dropFrame p.1) (Prod.snd p.2) else []) := by funext p @@ -2903,8 +2903,9 @@ noncomputable def carterWegmanNonceMAC (msgLen : ℕ → ℕ) let k := unframe p.1 let prfKey := dropFrame p.1 let n := prfKey.length - if (p.2.1.length == msgLen n) && (p.2.2.length == n) then - BitString.listXor n [hash n k p.2.1, (prfOracle family n prfKey p.2.2).take n] + if ((Prod.fst p.2).length == msgLen n) && ((Prod.snd p.2).length == n) then + BitString.listXor n + [hash n k (Prod.fst p.2), (prfOracle family n prfKey (Prod.snd p.2)).take n] else []) (encPair encBits (encPair encBits encBits)) encBits := by @@ -2913,9 +2914,10 @@ noncomputable def carterWegmanNonceMAC (msgLen : ℕ → ℕ) let k := unframe p.1 let prfKey := dropFrame p.1 let n := prfKey.length - if (p.2.1.length == msgLen n) && (p.2.2.length == n) then + if ((Prod.fst p.2).length == msgLen n) && ((Prod.snd p.2).length == n) then (pure (BitString.listXor n - [hash n k p.2.1, (prfOracle family n prfKey p.2.2).take n]) : ProbComp (List Bool)) + [hash n k (Prod.fst p.2), + (prfOracle family n prfKey (Prod.snd p.2)).take n]) : ProbComp (List Bool)) else pure []) = (fun p : List Bool × List Bool × List Bool => @@ -2923,8 +2925,9 @@ noncomputable def carterWegmanNonceMAC (msgLen : ℕ → ℕ) let k := unframe p.1 let prfKey := dropFrame p.1 let n := prfKey.length - if (p.2.1.length == msgLen n) && (p.2.2.length == n) then - BitString.listXor n [hash n k p.2.1, (prfOracle family n prfKey p.2.2).take n] + if ((Prod.fst p.2).length == msgLen n) && ((Prod.snd p.2).length == n) then + BitString.listXor n + [hash n k (Prod.fst p.2), (prfOracle family n prfKey (Prod.snd p.2)).take n] else [])) := by funext p @@ -2938,13 +2941,13 @@ noncomputable def carterWegmanNonceMAC (msgLen : ℕ → ℕ) have hfamily_tidy := hfamily.tidy have hprf : ComputableTidilyInPolyTime (fun p : List Bool × List Bool × List Bool × List Bool => - prfOracle family (dropFrame p.1).length (dropFrame p.1) p.2.2.1) + prfOracle family (dropFrame p.1).length (dropFrame p.1) (Prod.fst (Prod.snd p.2))) (encPair encBits (encPair encBits (encPair encBits encBits))) encBits := by have heq : (fun p : List Bool × List Bool × List Bool × List Bool => - prfOracle family (dropFrame p.1).length (dropFrame p.1) p.2.2.1) = + prfOracle family (dropFrame p.1).length (dropFrame p.1) (Prod.fst (Prod.snd p.2))) = (fun p : List Bool × List Bool × List Bool × List Bool => - if p.2.2.1.length == (dropFrame p.1).length then - family (dropFrame p.1) p.2.2.1 + if (Prod.fst (Prod.snd p.2)).length == (dropFrame p.1).length then + family (dropFrame p.1) (Prod.fst (Prod.snd p.2)) else []) := by funext p @@ -4716,13 +4719,13 @@ noncomputable def carterWegmanRandomMAC (msgLen : ℕ → ℕ) have hfamily_tidy := hfamily.tidy have hprf : ComputableTidilyInPolyTime (fun p : (List Bool × List Bool) × List Bool => - prfOracle family (dropFrame p.1.1).length (dropFrame p.1.1) p.2) + prfOracle family (dropFrame (Prod.fst p.1)).length (dropFrame (Prod.fst p.1)) p.2) (encPair (encPair encBits encBits) encBits) encBits := by have heq : (fun p : (List Bool × List Bool) × List Bool => - prfOracle family (dropFrame p.1.1).length (dropFrame p.1.1) p.2) = + prfOracle family (dropFrame (Prod.fst p.1)).length (dropFrame (Prod.fst p.1)) p.2) = (fun p : (List Bool × List Bool) × List Bool => - if p.2.length == (dropFrame p.1.1).length then - family (dropFrame p.1.1) p.2 + if p.2.length == (dropFrame (Prod.fst p.1)).length then + family (dropFrame (Prod.fst p.1)) p.2 else []) := by funext p @@ -4731,12 +4734,13 @@ noncomputable def carterWegmanRandomMAC (msgLen : ℕ → ℕ) polytime have hbody : ComputableTidilyInPolyTime (fun p : (List Bool × List Bool) × List Bool => - let k := unframe p.1.1 - let prfKey := dropFrame p.1.1 + let k := unframe (Prod.fst p.1) + let prfKey := dropFrame (Prod.fst p.1) let n := prfKey.length - if p.1.2.length == msgLen n then + if (Prod.snd p.1).length == msgLen n then encPair encBits encBits - (p.2, BitString.listXor n [hash n k p.1.2, (prfOracle family n prfKey p.2).take n]) + (p.2, BitString.listXor n + [hash n k (Prod.snd p.1), (prfOracle family n prfKey p.2).take n]) else []) (encPair (encPair encBits encBits) encBits) encBits := by @@ -4748,13 +4752,13 @@ noncomputable def carterWegmanRandomMAC (msgLen : ℕ → ℕ) have hfamily_tidy := hfamily.tidy have hprf : ComputableTidilyInPolyTime (fun p : List Bool × List Bool × List Bool => - prfOracle family (dropFrame p.1).length (dropFrame p.1) (unframe p.2.2)) + prfOracle family (dropFrame p.1).length (dropFrame p.1) (unframe (Prod.snd p.2))) (encPair encBits (encPair encBits encBits)) encBits := by have heq : (fun p : List Bool × List Bool × List Bool => - prfOracle family (dropFrame p.1).length (dropFrame p.1) (unframe p.2.2)) = + prfOracle family (dropFrame p.1).length (dropFrame p.1) (unframe (Prod.snd p.2))) = (fun p : List Bool × List Bool × List Bool => - if (unframe p.2.2).length == (dropFrame p.1).length then - family (dropFrame p.1) (unframe p.2.2) + if (unframe (Prod.snd p.2)).length == (dropFrame p.1).length then + family (dropFrame p.1) (unframe (Prod.snd p.2)) else []) := by funext p diff --git a/Complexity/Crypto/Protocols/MPC/CircuitEval.lean b/Complexity/Crypto/Protocols/MPC/CircuitEval.lean index 204a62be58..e803b2e2e9 100644 --- a/Complexity/Crypto/Protocols/MPC/CircuitEval.lean +++ b/Complexity/Crypto/Protocols/MPC/CircuitEval.lean @@ -148,7 +148,7 @@ and applying `finish` at `.done`. -/ .message (sender := p.1) (receiver := p.2) (fun st => st.1 p.2) ((msgStepsWith finish L).mapState fun i st => - (st.1.1, st.1.2 + extractMsg p i st.2)) + (Prod.fst st.1, Prod.snd st.1 + extractMsg p i st.2)) /-- All-to-all message exchange: party `s` sends `toSend s r` to party `r`, and party `i` applies `finish i` to the vector `fun s => toSend s i` of received messages. -/ @@ -642,12 +642,13 @@ applying `finish` at `.done`. -/ (r : Fin m) (finish : (i : Fin m) → State i → Bool → Out i) : (S : List (Fin m)) → Steps (fun i => State i × Bool × Bool) Out (gatherSchedule m (spec := spec) r S) - | [] => .done (fun i st => finish i st.1 st.2.2) + | [] => .done (fun i st => finish i st.1 (Prod.snd st.2)) | s :: S => .message (sender := s) (receiver := r) - (fun st => st.2.1) + (fun st => Prod.fst st.2) ((gatherStepsWith r finish S).mapState fun i st => - (st.1.1, st.1.2.1, st.1.2.2 + extractBitFor s r i st.2)) + (Prod.fst st.1, Prod.fst (Prod.snd st.1), + Prod.snd (Prod.snd st.1) + extractBitFor s r i st.2)) /-- Sum of party `i`'s received bits along `gatherSchedule m r S`. -/ @[expose] def sumGatherBits {m : ℕ} {spec : MultiOracleSpec} (r : Fin m) : diff --git a/Complexity/Crypto/Protocols/MPC/Composition.lean b/Complexity/Crypto/Protocols/MPC/Composition.lean index 57b3c57250..aaf7234e3e 100644 --- a/Complexity/Crypto/Protocols/MPC/Composition.lean +++ b/Complexity/Crypto/Protocols/MPC/Composition.lean @@ -429,15 +429,15 @@ first state component. -/ .message (sender := parties s₀) (receiver := parties r₀) (fun st_sender => send (st_sender.2 s₀ rfl)) ((Steps.embed parties Outer next).mapState fun _ st_i => - (st_i.1.1, fun s hs => - (st_i.1.2 s hs, + (Prod.fst st_i.1, fun s hs => + (Prod.snd st_i.1 s hs, pullRoundReceived parties (.message s₀ r₀ Msg) hs st_i.2))) | .oracle (op := op) (parties := subParties) query next => .oracle (op := op) (parties := subParties.trans parties) (fun t st_party => query t (st_party.2 (subParties t) rfl)) ((Steps.embed parties Outer next).mapState fun _ st_i => - (st_i.1.1, fun s hs => - (st_i.1.2 s hs, + (Prod.fst st_i.1, fun s hs => + (Prod.snd st_i.1 s hs, pullRoundReceived parties (.oracle op subParties) hs st_i.2))) @[simp] private theorem outputAt_embed {k m : ℕ} {spec : MultiOracleSpec} @@ -515,16 +515,16 @@ execution of `(Sub op).steps` along `parties`. -/ .message (sender := s₀) (receiver := r₀) (fun st_sender => send st_sender.1) ((Steps.compose Sub next).mapState fun _ st_i => - ((st_i.1.1, st_i.2), st_i.1.2)) + ((Prod.fst st_i.1, st_i.2), Prod.snd st_i.1)) | .oracle (op := op) (parties := parties) (sc := rest) query next => (((Steps.embed parties (fun i => State i × Schedule.SubCoins Coins₂ rest i) (Sub op).steps).mapState - (fun i st_i => - ((st_i.1, st_i.2.2), + (fun i (st_i : State i × Schedule.SubCoins Coins₂ (.oracle op parties :: rest) i) => + ((st_i.1, Prod.snd st_i.2), fun (s : Fin (spec₁.arity op)) (hs : parties s = i) => - (query s (hs.symm ▸ st_i.1), st_i.2.1 s hs)))).append + (query s (hs.symm ▸ st_i.1), Prod.fst st_i.2 s hs)))).append ((Steps.compose Sub next).mapState fun _ st_i => - ((st_i.1.1, st_i.2), st_i.1.2))) + ((Prod.fst st_i.1, st_i.2), Prod.snd st_i.1))) /-- Expand a simulated outer execution along `steps : Steps State Out sc₁` by invoking the inner simulator `S₂ op (subCoalition parties I)` at every `.oracle op parties` round (Goldreich Theorem diff --git a/Complexity/Crypto/Protocols/MPC/PolyTime.lean b/Complexity/Crypto/Protocols/MPC/PolyTime.lean index a6f99a722e..fb1c4c878c 100644 --- a/Complexity/Crypto/Protocols/MPC/PolyTime.lean +++ b/Complexity/Crypto/Protocols/MPC/PolyTime.lean @@ -357,8 +357,9 @@ packed coalition input bits `extendCoalitionBits I xI` and output bits def encFamilySimInput {α : Type} (enc : α ↪ List Bool) (m : ℕ) (n k : α → ℕ) (I : Finset (Fin m)) : FamilySimInput α m n k I ↪ List Bool where toFun inp := + let xy := inp.2 encPair enc (encPair encBits encBits) - (inp.1, (extendCoalitionBits I inp.2.1, extendCoalitionBits I inp.2.2)) + (inp.1, (extendCoalitionBits I xy.1, extendCoalitionBits I xy.2)) inj' := by rintro ⟨a₁, x₁, y₁⟩ ⟨a₂, x₂, y₂⟩ h obtain ⟨ha, hxy⟩ := Prod.ext_iff.1 ((encPair enc (encPair encBits encBits)).injective h) @@ -504,8 +505,9 @@ def encGMWPartyView (m coins n k : ℕ) (encPair encBits (encPair encBits encBits)) (((List.ofFn v.input, List.ofFn v.coins.1), (List.ofFn - ((Cslib.BitString.blocksEquiv (α := Bool) (m := N) (k := m - 1)).symm v.coins.2.1.1), - encOTSubCoins _ i v.coins.2.2)), + ((Cslib.BitString.blocksEquiv (α := Bool) (m := N) (k := m - 1)).symm + (Prod.fst (Prod.fst v.coins.2))), + encOTSubCoins _ i (Prod.snd v.coins.2))), (encPairsMsgReceived i (GMWCircuit.allPairs m) r_in, (encOTOracleAnswers _ i v.received, encOutCoordsMsgReceived i (GMWCircuit.outCoords m k) r_out))) @@ -5963,7 +5965,7 @@ theorem isPPTOn_gmwOT14RandomizedSim {α : Type} {enc : α ↪ List Bool} encodeCoalitionView (encGMWPartyView m (coins inp.1) (n inp.1) (k inp.1) (C inp.1)) I <$> gmwOT14RandomizedSim m (coins inp.1) (n inp.1) (k inp.1) - (C inp.1) I inp.2.1 inp.2.2) := by + (C inp.1) I (Prod.fst inp.2) (Prod.snd inp.2)) := by have hD := computableInPolyTime_code_comp_xorPreludeCircuit m hn hcoins hC exact (PolyTimeRunner.isPPTOn_simRunWord m I hcoins.tidy hn.tidy hk.tidy hD.tidy).congr (PolyTimeRunner.eval_simRunWord_eq_gmwOT14RandomizedSim m coins n k C I) @@ -6012,7 +6014,7 @@ theorem exists_perfectSemiHonestPrivate_ot14_of_polyTime {α : Type} {enc : α encodeCoalitionView (encGMWPartyView m (coins inp.1) (n inp.1) (k inp.1) (C inp.1)) I <$> gmwOT14RandomizedSim m (coins inp.1) (n inp.1) (k inp.1) - (C inp.1) I inp.2.1 inp.2.2)) := by + (C inp.1) I (Prod.fst inp.2) (Prod.snd inp.2))) := by have h_in : ComputableInPolyTime (fun a => m * n a + coins a) enc encUnary := by have hmn := ComputableTidilyInPolyTime.comp' ComputableTidilyInPolyTime.unary_mul ((ComputableTidilyInPolyTime.const m).prod hn.tidy) diff --git a/Complexity/Crypto/Protocols/MPC/SharedMul.lean b/Complexity/Crypto/Protocols/MPC/SharedMul.lean index 4e4e42de4e..bb09a9963f 100644 --- a/Complexity/Crypto/Protocols/MPC/SharedMul.lean +++ b/Complexity/Crypto/Protocols/MPC/SharedMul.lean @@ -171,7 +171,7 @@ def twoPartyMulOutput (i : Fin 2) (st : ((Bool × Bool) × Fin.cases Bool (fun _ => Unit) i) × (Round.oracle (spec := ot14Spec) () (Function.Embedding.refl (Fin 2))).Received i) : Bool := Fin.cases - (fun (st : ((Bool × Bool) × Bool) × _) => st.1.2) + (fun (st : ((Bool × Bool) × Bool) × _) => Prod.snd st.1) (fun j st => st.2 j.succ rfl) i st /-- Construction 7.3.7 (p. 643): 2-party shared multiplication in the `ot14Spec`-hybrid model. @@ -304,7 +304,7 @@ abbrev OrderedPair (m : ℕ) : Type := /-- Embedding of `Fin 2` into `Fin m` sending `0 ↦ p.1.1` and `1 ↦ p.1.2` for an ordered pair `p : OrderedPair m`. -/ def pairEmbedding {m : ℕ} (p : OrderedPair m) : Fin 2 ↪ Fin m where - toFun := Fin.cases p.1.1 (fun _ => p.1.2) + toFun := Fin.cases p.val.1 (fun _ => p.val.2) inj' a b h := by fin_cases a <;> fin_cases b · rfl @@ -313,10 +313,10 @@ def pairEmbedding {m : ℕ} (p : OrderedPair m) : Fin 2 ↪ Fin m where · rfl @[simp] theorem pairEmbedding_zero {m : ℕ} (p : OrderedPair m) : - pairEmbedding p 0 = p.1.1 := rfl + pairEmbedding p 0 = p.val.1 := rfl @[simp] theorem pairEmbedding_one {m : ℕ} (p : OrderedPair m) : - pairEmbedding p 1 = p.1.2 := rfl + pairEmbedding p 1 = p.val.2 := rfl /-- Joint 2-party shared-multiplication oracle round for `p : OrderedPair m`. -/ @[reducible] def pairRound {m : ℕ} (p : OrderedPair m) : Round m (sharedMulSpec 2) := @@ -325,7 +325,7 @@ def pairEmbedding {m : ℕ} (p : OrderedPair m) : Fin 2 ↪ Fin m where /-- A party `i` that is neither `p.1.1` nor `p.1.2` receives a subsingleton record in `pairRound p`. -/ theorem subsingleton_received_pairRound {m : ℕ} (p : OrderedPair m) {i : Fin m} - (h1 : i ≠ p.1.1) (h2 : i ≠ p.1.2) : Subsingleton ((pairRound p).Received i) := by + (h1 : i ≠ p.val.1) (h2 : i ≠ p.val.2) : Subsingleton ((pairRound p).Received i) := by refine ⟨fun r₁ r₂ => Round.received_oracle_ext fun s hs => ?_⟩ fin_cases s · exact (h1 hs.symm).elim @@ -351,9 +351,9 @@ def orderedPairs (m : ℕ) : List (OrderedPair m) := two participating parties `p.1.1` or `p.1.2`). -/ def extractPairShare {m : ℕ} (p : OrderedPair m) (i : Fin m) (r : (pairRound p).Received i) : Bool := - if h0 : p.1.1 = i then + if h0 : p.val.1 = i then r 0 h0 - else if h1 : p.1.2 = i then + else if h1 : p.val.2 = i then r 1 h1 else 0 @@ -369,8 +369,8 @@ def pairsSteps {m : ℕ} : | p :: L => .oracle (op := ()) (parties := pairEmbedding p) (fun _ st => st.1) - ((pairsSteps L).mapState fun i st => - (st.1.1, st.1.2 + extractPairShare p i st.2)) + ((pairsSteps L).mapState fun i (st : ((Bool × Bool) × Bool) × (pairRound p).Received i) => + (Prod.fst st.1, Prod.snd st.1 + extractPairShare p i st.2)) /-- Construction 7.5.8 (p. 704): `m`-party shared multiplication in the 2-ary `sharedMulSpec 2`-hybrid model, invoking `sharedMulSpec 2` once for each pair `i < j`. @@ -383,7 +383,7 @@ def multiPartyMulProtocol (m : ℕ) : sampleCoins _ := pure () steps := (pairsSteps (orderedPairs m)).mapState fun _ st => - (st.1, m • (st.1.1 * st.1.2)) + (st.1, m • (Prod.fst st.1 * Prod.snd st.1)) namespace MultiPartyMul @@ -414,7 +414,7 @@ theorem outputOfView_multiPartyMulProtocol {m : ℕ} (i : Fin m) pairwise shares `row_i : Fin m → Bool`. -/ def receivedPairOfRow {m : ℕ} (p : OrderedPair m) (i : Fin m) (row_i : Fin m → Bool) : (pairRound p).Received i := - fun s _ => Fin.cases (row_i p.1.2) (fun _ => row_i p.1.1) s + fun s _ => Fin.cases (row_i p.val.2) (fun _ => row_i p.val.1) s /-- Construct party `i`'s received transcript along `pairsSchedule L` from party `i`'s row of pairwise shares `row_i : Fin m → Bool`. -/ @@ -426,8 +426,8 @@ def receivedScheduleOfRow {m : ℕ} (i : Fin m) (row_i : Fin m → Bool) : theorem extractPairShare_receivedPairOfRow {m : ℕ} (p : OrderedPair m) (i : Fin m) (row_i : Fin m → Bool) : extractPairShare p i (receivedPairOfRow p i row_i) = - (if p.1.1 = i then row_i p.1.2 else 0) + - (if p.1.2 = i then row_i p.1.1 else 0) := by + (if p.val.1 = i then row_i p.val.2 else 0) + + (if p.val.2 = i then row_i p.val.1 else 0) := by dsimp [extractPairShare, receivedPairOfRow] by_cases h0 : p.1.1 = i · have h1 : p.1.2 ≠ i := fun h => ne_of_lt p.2 (h0.trans h.symm) @@ -644,7 +644,7 @@ def viewOfRow {m : ℕ} (i : Fin m) (xi : Bool × Bool) (row_i : Fin m → Bool) /-- 2-party oracle answer tuple for pair `p` on input `x` and coin `b : Bool`. -/ def pairAnswer {m : ℕ} (x : Fin m → Bool × Bool) (p : OrderedPair m) (b : Bool) : Fin 2 → Bool := - completeShares 2 (pairTarget x p.1.1 p.1.2) (fun _ => b) + completeShares 2 (pairTarget x p.val.1 p.val.2) (fun _ => b) theorem deliverOracle_pairAnswer_eq_receivedPairOfRow {m : ℕ} (x : Fin m → Bool × Bool) (r : OrderedPair m → Bool) (p : OrderedPair m) (i : Fin m) : @@ -797,17 +797,17 @@ theorem evalWith_multiPartyMulProtocol (m : ℕ) (x : Fin m → Bool × Bool) : /-- Coin adjustment supported on pairs incident to the pivot party `ℓ : Fin m`. -/ def delta {m : ℕ} (ℓ : Fin m) (w : Fin m → Bool) (p : OrderedPair m) : Bool := - if p.1.1 = ℓ then w p.1.2 - else if p.1.2 = ℓ then w p.1.1 + if p.val.1 = ℓ then w p.val.2 + else if p.val.2 = ℓ then w p.val.1 else 0 /-- Restriction-based presentation of `delta ℓ` depending only on `Finset.univ.erase ℓ`. -/ def deltaErase {m : ℕ} (ℓ : Fin m) (u : (i : Finset.univ.erase ℓ) → Bool) (p : OrderedPair m) : Bool := - if h1 : p.1.1 = ℓ then - u ⟨p.1.2, Finset.mem_erase.mpr ⟨ne_of_gt (h1 ▸ p.2), Finset.mem_univ _⟩⟩ - else if h2 : p.1.2 = ℓ then - u ⟨p.1.1, Finset.mem_erase.mpr ⟨ne_of_lt (h2 ▸ p.2), Finset.mem_univ _⟩⟩ + if h1 : p.val.1 = ℓ then + u ⟨p.val.2, Finset.mem_erase.mpr ⟨ne_of_gt (h1 ▸ p.2), Finset.mem_univ _⟩⟩ + else if h2 : p.val.2 = ℓ then + u ⟨p.val.1, Finset.mem_erase.mpr ⟨ne_of_lt (h2 ▸ p.2), Finset.mem_univ _⟩⟩ else 0 theorem delta_eq_deltaErase_restrict {m : ℕ} (ℓ : Fin m) (w : Fin m → Bool) : @@ -912,8 +912,8 @@ def extendOut {m : ℕ} (I : Finset (Fin m)) (yI : (i : I) → Bool) (j : Fin m) `matrixOfCoins (extendIn I (I.restrict x)) r i` for all `i ∈ I`. -/ def sigmaShift {m : ℕ} (I : Finset (Fin m)) (x : Fin m → Bool × Bool) (p : OrderedPair m) : Bool := - if p.1.2 ∈ I then - pairTarget x p.1.2 p.1.1 + pairTarget (extendIn I (I.restrict x)) p.1.2 p.1.1 + if p.val.2 ∈ I then + pairTarget x p.val.2 p.val.1 + pairTarget (extendIn I (I.restrict x)) p.val.2 p.val.1 else 0 diff --git a/Complexity/Crypto/Protocols/SigmaProtocol/Abort.lean b/Complexity/Crypto/Protocols/SigmaProtocol/Abort.lean index f6c4055806..2653b9ebb5 100644 --- a/Complexity/Crypto/Protocols/SigmaProtocol/Abort.lean +++ b/Complexity/Crypto/Protocols/SigmaProtocol/Abort.lean @@ -77,7 +77,7 @@ noncomputable def acceptedTranscript (x : X) (y : Y) (c : C) : PMF (Option (T × /-- An honest conversation with a uniform challenge, or `none` if the prover aborts. -/ noncomputable def acceptedConversation [Fintype C] [Nonempty C] (x : X) (y : Y) : PMF (Option (T × C × Z)) := - (P.conversation x y).map fun tcz => tcz.2.2.map fun z => (tcz.1, tcz.2.1, z) + (P.conversation x y).map fun tcz => (Prod.snd tcz.2).map fun z => (tcz.1, Prod.fst tcz.2, z) /-- Completeness up to aborts: for every witness-statement pair in `R` and every challenge, every honest transcript in which the prover does not abort is accepting. -/ diff --git a/Complexity/Crypto/Protocols/SigmaProtocol/Basic.lean b/Complexity/Crypto/Protocols/SigmaProtocol/Basic.lean index e8b48e8d24..05ec070425 100644 --- a/Complexity/Crypto/Protocols/SigmaProtocol/Basic.lean +++ b/Complexity/Crypto/Protocols/SigmaProtocol/Basic.lean @@ -191,7 +191,8 @@ variable {P} /-- Every honest conversation is accepting: the verifier always accepts the honest prover. -/ theorem Complete.accepts_of_mem_support_conversation [Fintype C] [Nonempty C] (h : P.Complete R) {x : X} {y : Y} (hxy : R x y) {tcz : T × C × Z} - (htcz : tcz ∈ (P.conversation x y).support) : P.Accepts y tcz.1 tcz.2.1 tcz.2.2 := by + (htcz : tcz ∈ (P.conversation x y).support) : + P.Accepts y tcz.1 (Prod.fst tcz.2) (Prod.snd tcz.2) := by rw [conversation_eq_bind_transcript] at htcz simp only [PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, PMF.mem_support_bind_iff, PMF.mem_support_pure_iff] at htcz diff --git a/Complexity/Crypto/Protocols/SigmaProtocol/Composition.lean b/Complexity/Crypto/Protocols/SigmaProtocol/Composition.lean index 1004242401..d7cd45552b 100644 --- a/Complexity/Crypto/Protocols/SigmaProtocol/Composition.lean +++ b/Complexity/Crypto/Protocols/SigmaProtocol/Composition.lean @@ -176,15 +176,16 @@ noncomputable def orProof (P₀ : SigmaProtocol X₀ Y₀ T₀ C Z₀) (P₁ : S respond _ y s c := match s with | .inl (x, s₀, c₁, z₁) => (c - c₁, P₀.respond x y.1 s₀ (c - c₁), z₁) | .inr (x, s₁, c₀, z₀) => (c₀, z₀, P₁.respond x y.2 s₁ (c - c₀)) - verify y t c z := P₀.verify y.1 t.1 z.1 z.2.1 && P₁.verify y.2 t.2 (c - z.1) z.2.2 + verify y t c z := + P₀.verify y.1 t.1 z.1 (Prod.fst z.2) && P₁.verify y.2 t.2 (c - z.1) (Prod.snd z.2) /-- The OR extractor uses the first side when the first side's challenges differ, and the second side otherwise. -/ def orExtract [DecidableEq C] (extract₀ : Y₀ → T₀ → C → Z₀ → C → Z₀ → X₀) (extract₁ : Y₁ → T₁ → C → Z₁ → C → Z₁ → X₁) (y : Y₀ × Y₁) (t : T₀ × T₁) (c : C) (z : C × Z₀ × Z₁) (c' : C) (z' : C × Z₀ × Z₁) : X₀ ⊕ X₁ := - if z.1 = z'.1 then .inr (extract₁ y.2 t.2 (c - z.1) z.2.2 (c' - z'.1) z'.2.2) - else .inl (extract₀ y.1 t.1 z.1 z.2.1 z'.1 z'.2.1) + if z.1 = z'.1 then .inr (extract₁ y.2 t.2 (c - z.1) (Prod.snd z.2) (c' - z'.1) (Prod.snd z'.2)) + else .inl (extract₀ y.1 t.1 z.1 (Prod.fst z.2) z'.1 (Prod.fst z'.2)) /-- The OR simulator splits the challenge uniformly and simulates both sides. -/ noncomputable def orSimulate (simulate₀ : Y₀ → C → PMF (T₀ × Z₀)) @@ -203,7 +204,7 @@ variable {P₀ : SigmaProtocol X₀ Y₀ T₀ C Z₀} {P₁ : SigmaProtocol X₁ side accepts at `c₀` and the second at `c - c₀`. -/ @[simp] theorem orProof_accepts_iff {y : Y₀ × Y₁} {t : T₀ × T₁} {c : C} {z : C × Z₀ × Z₁} : (orProof P₀ P₁ simulate₀ simulate₁).Accepts y t c z ↔ - P₀.Accepts y.1 t.1 z.1 z.2.1 ∧ P₁.Accepts y.2 t.2 (c - z.1) z.2.2 := by + P₀.Accepts y.1 t.1 z.1 (Prod.fst z.2) ∧ P₁.Accepts y.2 t.2 (c - z.1) (Prod.snd z.2) := by simp only [Accepts, orProof, Bool.and_eq_true] /-- With a witness for the first statement, the OR prover simulates the second side at a diff --git a/Complexity/Crypto/Protocols/SigmaProtocol/FiatShamir.lean b/Complexity/Crypto/Protocols/SigmaProtocol/FiatShamir.lean index 39a83a0cbe..e45844e432 100644 --- a/Complexity/Crypto/Protocols/SigmaProtocol/FiatShamir.lean +++ b/Complexity/Crypto/Protocols/SigmaProtocol/FiatShamir.lean @@ -158,8 +158,9 @@ noncomputable def reductionHandler : (ForgerSpec M (M × T) (T × Z) C q) | .inl m => fun st => let v := st.transcripts.headD (Classical.arbitrary _) - pure ((v.1, v.2.2), - ⟨((m, v.1), v.2.1, none) :: st.table, m :: st.signed, st.count, st.transcripts.tail⟩) + let cz := v.2 + pure ((v.1, cz.2), + ⟨((m, v.1), cz.1, none) :: st.table, m :: st.signed, st.count, st.transcripts.tail⟩) | .inr x => fun st => match st.table.lookup x with | some entry => pure (entry.1, ⟨st.table, st.signed, st.count, st.transcripts.tail⟩) @@ -172,18 +173,26 @@ the position of the query for `(m, t)`. The verdict records the point, the chall response. -/ def verdict (P : SigmaProtocol X Y T C Z) (y : Y) (forged : (M × (T × Z)) × ReductionState M T C Z) (c : C) (position : Option ℕ) : Option ℕ × Bool × (M × T) × C × Z := - (if P.verify y forged.1.2.1 c forged.1.2.2 && !forged.2.signed.contains forged.1.1 then position - else none, P.verify y forged.1.2.1 c forged.1.2.2 && !forged.2.signed.contains forged.1.1, - (forged.1.1, forged.1.2.1), c, forged.1.2.2) + let sig := forged.1 + let m := sig.1 + let tz := sig.2 + let t := tz.1 + let z := tz.2 + (if P.verify y t c z && !forged.2.signed.contains m then position + else none, P.verify y t c z && !forged.2.signed.contains m, + (m, t), c, z) /-- Check a forgery, querying its point when the table lacks it. -/ noncomputable def finish (P : SigmaProtocol X Y T C Z) (y : Y) (forged : (M × (T × Z)) × ReductionState M T C Z) : OracleComp (fun _ : M × T => C) (Option ℕ × Bool × (M × T) × C × Z) := - match forged.2.table.lookup (forged.1.1, forged.1.2.1) with + let sig := forged.1 + let tz := sig.2 + let pt := (sig.1, tz.1) + match forged.2.table.lookup pt with | some entry => pure (verdict P y forged entry.1 entry.2) | none => (fun c => verdict P y forged c (some forged.2.count)) <$> - OracleComp.query (forged.1.1, forged.1.2.1) + OracleComp.query pt /-- The forger, with simulated signing, as a program over the hash oracle with explicit coins: the statement, the forger's coins and the simulated transcripts. It names the query of the forgery's @@ -191,7 +200,8 @@ point when the forger wins. -/ noncomputable def forkingProgram (P : SigmaProtocol X Y T C Z) (A : Forger Y M (T × Z) (M × T) C) (s : Y × A.Coins × List (T × C × Z)) : OracleComp (fun _ : M × T => C) (Option ℕ × Bool × (M × T) × C × Z) := - (interpret reductionHandler (A.forge s.1 s.2.1)).run ⟨[], [], 0, s.2.2⟩ >>= finish P s.1 + let rest := s.2 + (interpret reductionHandler (A.forge s.1 rest.1)).run ⟨[], [], 0, rest.2⟩ >>= finish P s.1 /-- The coins of the forking program for the statement `y`: the forger's coins and `Q` simulated transcripts. -/ @@ -214,7 +224,16 @@ noncomputable def reduction [Nonempty X] (P : SigmaProtocol X Y T C Z) match result with | none => Classical.arbitrary X | some (_, out, out') => - extract y out.1.2.2.1.2 out.1.2.2.2.1 out.1.2.2.2.2 out'.1.2.2.2.1 out'.1.2.2.2.2 + let v := out.1 + let bptcz := v.2 + let ptcz := bptcz.2 + let pt := ptcz.1 + let cz := ptcz.2 + let v' := out'.1 + let bptcz' := v'.2 + let ptcz' := bptcz'.2 + let cz' := ptcz'.2 + extract y pt.2 cz.1 cz.2 cz'.1 cz'.2 end FiatShamir diff --git a/Complexity/Crypto/Protocols/SigmaProtocol/Linear.lean b/Complexity/Crypto/Protocols/SigmaProtocol/Linear.lean index 51b1e28c6d..0fadbc2d47 100644 --- a/Complexity/Crypto/Protocols/SigmaProtocol/Linear.lean +++ b/Complexity/Crypto/Protocols/SigmaProtocol/Linear.lean @@ -221,23 +221,24 @@ noncomputable def chaumPedersen (g : G) : SigmaProtocol (ZMod q) (G × G × G) ( ([BonehShoup2023], Section 19.5.2). -/ @[simp] theorem chaumPedersen_accepts_iff {s : G × G × G} {t : G × G} {c : C} {z : ZMod q} : (chaumPedersen ι g).Accepts s t c z ↔ - z • g = t.1 + ι c • s.2.1 ∧ z • s.1 = t.2 + ι c • s.2.2 := by + z • g = t.1 + ι c • Prod.fst s.2 ∧ z • s.1 = t.2 + ι c • Prod.snd s.2 := by simp [chaumPedersen, Prod.ext_iff] /-- Theorem 19.10 of [BonehShoup2023]: completeness. -/ theorem chaumPedersen_complete : - (chaumPedersen ι g).Complete fun β s => β • g = s.2.1 ∧ β • s.1 = s.2.2 := + (chaumPedersen ι g).Complete fun β s => β • g = Prod.fst s.2 ∧ β • s.1 = Prod.snd s.2 := (linear_complete _ _ ι).mono fun _ _ h => by simpa [Prod.ext_iff] using h /-- Theorem 19.10 of [BonehShoup2023]: special soundness. -/ theorem chaumPedersen_specialSoundness [Fact q.Prime] : - (chaumPedersen ι g).SpecialSoundness (fun β s => β • g = s.2.1 ∧ β • s.1 = s.2.2) + (chaumPedersen ι g).SpecialSoundness + (fun β s => β • g = Prod.fst s.2 ∧ β • s.1 = Prod.snd s.2) (linearExtract ι) := (linear_specialSoundness _ _ ι).mono fun _ _ h => by simpa [Prod.ext_iff] using h /-- Theorem 19.10 of [BonehShoup2023]: special honest-verifier zero knowledge. -/ theorem chaumPedersen_specialHVZK : - (chaumPedersen ι g).SpecialHVZK (fun β s => β • g = s.2.1 ∧ β • s.1 = s.2.2) + (chaumPedersen ι g).SpecialHVZK (fun β s => β • g = Prod.fst s.2 ∧ β • s.1 = Prod.snd s.2) (linearSimulate (fun s => (LinearMap.toSpanSingleton (ZMod q) G g).prod (LinearMap.toSpanSingleton (ZMod q) G s.1)) Prod.snd ι) := (linear_specialHVZK _ _ ι).mono fun _ _ h => by simpa [Prod.ext_iff] using h diff --git a/Complexity/Crypto/Protocols/SigmaProtocol/Lyubashevsky/NativeExtract.lean b/Complexity/Crypto/Protocols/SigmaProtocol/Lyubashevsky/NativeExtract.lean index 1f2f26dcff..a855bd8d6d 100644 --- a/Complexity/Crypto/Protocols/SigmaProtocol/Lyubashevsky/NativeExtract.lean +++ b/Complexity/Crypto/Protocols/SigmaProtocol/Lyubashevsky/NativeExtract.lean @@ -94,15 +94,16 @@ theorem computableInPolyTime_decodeLyubashevskyExtractInput : /-- Compute `z-z′` first, then the SIGNED challenge difference `c′-c`. The unary dimensions control both output segments; optional responses default to zero coordinatewise. -/ def lyubashevskyExtractList (input : LyubashevskyExtractInput) : List ℤ := - ((List.range input.1.1).map fun i => - (input.2.1.2.getD []).getD i 0 - (input.2.2.2.getD []).getD i 0) ++ - ((List.range input.1.2).map fun i => - (if input.2.2.1.getD i false then (1 : ℤ) else 0) - - (if input.2.1.1.getD i false then (1 : ℤ) else 0)) + ((List.range (Prod.fst input.1)).map fun i => + ((Prod.snd (Prod.fst input.2)).getD []).getD i 0 - + ((Prod.snd (Prod.snd input.2)).getD []).getD i 0) ++ + ((List.range (Prod.snd input.1)).map fun i => + (if (Prod.fst (Prod.snd input.2)).getD i false then (1 : ℤ) else 0) - + (if (Prod.fst (Prod.fst input.2)).getD i false then (1 : ℤ) else 0)) /-- Extraction always writes the two declared segments, even on malformed-length inputs. -/ @[simp] theorem length_lyubashevskyExtractList (input : LyubashevskyExtractInput) : - (lyubashevskyExtractList input).length = input.1.1 + input.1.2 := by + (lyubashevskyExtractList input).length = Prod.fst input.1 + Prod.snd input.1 := by simp [lyubashevskyExtractList] /-- One native extractor handles runtime dimensions and all binary integer magnitudes. -/ From b20babb49bec39a3825b441beb09b9b3240560bf Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Mon, 2 Nov 2026 16:13:13 +0000 Subject: [PATCH 2/2] refactor(Crypto): address review feedback on projection chains (#1764) --- .../Encryption/EncryptThenMAC.lean | 10 +-- .../Computational/Encryption/PolyTime.lean | 2 +- .../Encryption/PublicKeyReplacement.lean | 2 +- .../Crypto/Computational/GMW/PolyTime.lean | 34 +++++----- .../Crypto/Computational/GMW/Simulator.lean | 33 +++++----- .../Crypto/Protocols/Cipher/EvenMansour.lean | 22 ++++++- .../Crypto/Protocols/MAC/CarterWegman.lean | 56 ++++++++--------- .../Crypto/Protocols/MPC/CircuitEval.lean | 11 ++-- .../Crypto/Protocols/MPC/Composition.lean | 27 ++++---- Complexity/Crypto/Protocols/MPC/PolyTime.lean | 15 ++--- .../Crypto/Protocols/MPC/SharedMul.lean | 62 +++++++++++-------- .../Crypto/Protocols/SigmaProtocol/Abort.lean | 2 +- .../Crypto/Protocols/SigmaProtocol/Basic.lean | 10 ++- .../Protocols/SigmaProtocol/Composition.lean | 16 +++-- .../Protocols/SigmaProtocol/FiatShamir.lean | 44 +++++-------- .../Protocols/SigmaProtocol/Linear.lean | 16 +++-- .../Lyubashevsky/NativeExtract.lean | 33 +++++++--- 17 files changed, 224 insertions(+), 171 deletions(-) diff --git a/Complexity/Crypto/Computational/Encryption/EncryptThenMAC.lean b/Complexity/Crypto/Computational/Encryption/EncryptThenMAC.lean index ec8221026a..dc0b185de0 100644 --- a/Complexity/Crypto/Computational/Encryption/EncryptThenMAC.lean +++ b/Complexity/Crypto/Computational/Encryption/EncryptThenMAC.lean @@ -219,7 +219,7 @@ noncomputable def encryptThenMAC (E : SymmetricCipher) (M : MACScheme) none keyGen_ppt := by have hpost : ComputableInPolyTime - (fun p : (ℕ × List Bool) × List Bool => encPair encBits encBits (Prod.snd p.1, p.2)) + (fun p : (ℕ × List Bool) × List Bool => encPair encBits encBits (p.1.2, p.2)) (encPair (encPair encUnary encBits) encBits) encBits := ComputableInPolyTime.encoding_comp (((ComputableInPolyTime.snd encUnary encBits).comp @@ -240,7 +240,7 @@ noncomputable def encryptThenMAC (E : SymmetricCipher) (M : MACScheme) (ComputableInPolyTime.snd I encBits) have hpost : ComputableInPolyTime (fun p : ((ℕ × List Bool × List Bool) × List Bool) × List Bool => - encPair encBits encBits (Prod.snd p.1, p.2)) + encPair encBits encBits (p.1.2, p.2)) (encPair (encPair I encBits) encBits) encBits := ComputableInPolyTime.encoding_comp (((ComputableInPolyTime.snd I encBits).comp @@ -2117,12 +2117,12 @@ noncomputable def prfCipher (family : List Bool → List Bool → List Bool) decrypt_polyTime := by have hfamTidy := hpoly.tidy have hcond : ComputableTidilyInPolyTime - (fun p : ℕ × List Bool × List Bool => (Prod.snd p.2).length == 2 * p.1) + (fun p : ℕ × List Bool × List Bool => p.2.2.length == 2 * p.1) (encPair encUnary (encPair encBits encBits)) encBool := by polytime have hyes : ComputableTidilyInPolyTime (fun p : ℕ × List Bool × List Bool => - (some (List.zipWith xor (family (Prod.fst p.2) ((Prod.snd p.2).take p.1)) - ((Prod.snd p.2).drop p.1)) : Option (List Bool))) + (some (List.zipWith xor (family p.2.1 (p.2.2.take p.1)) (p.2.2.drop p.1)) : + Option (List Bool))) (encPair encUnary (encPair encBits encBits)) (encOption encBits) := by polytime have hno : ComputableTidilyInPolyTime (fun _ : ℕ × List Bool × List Bool => (none : Option (List Bool))) diff --git a/Complexity/Crypto/Computational/Encryption/PolyTime.lean b/Complexity/Crypto/Computational/Encryption/PolyTime.lean index bc39f26ff1..174c4d9285 100644 --- a/Complexity/Crypto/Computational/Encryption/PolyTime.lean +++ b/Complexity/Crypto/Computational/Encryption/PolyTime.lean @@ -113,7 +113,7 @@ theorem INDCPAOf.indcpaOn {Msg : Type} {encMsg : Msg ↪ List Bool} {encrypt : ℕ → List Bool → Msg → ProbComp (List Bool)} (h : INDCPAOf encMsg keyGen encrypt) (hvalid : ComputableInPolyTime - (fun p : ℕ × List Bool × Msg × Msg => valid p.1 p.2.1 p.2.2.1 p.2.2.2) + (fun (n, pk, m₀, m₁) => valid n pk m₀ m₁) (encPair encUnary (encPair encBits (encPair encMsg encMsg))) encBool) : INDCPAOn valid encMsg keyGen encrypt := by intro adversary hadversary diff --git a/Complexity/Crypto/Computational/Encryption/PublicKeyReplacement.lean b/Complexity/Crypto/Computational/Encryption/PublicKeyReplacement.lean index cf206bc652..9c6cd71616 100644 --- a/Complexity/Crypto/Computational/Encryption/PublicKeyReplacement.lean +++ b/Complexity/Crypto/Computational/Encryption/PublicKeyReplacement.lean @@ -80,7 +80,7 @@ are certified on their complete inputs. -/ theorem isPPT_keyDistinguisher {encrypt : ℕ → List Bool → Bool → ProbComp (List Bool)} {adversary : Adversary} (hencrypt : IsPPTOn (encPair encUnary (encPair encBits encBool)) encBits - (fun input => encrypt input.1 input.2.1 input.2.2)) + (fun (n, pk, m) => encrypt n pk m)) (hadversary : adversary.IsPPT) : IsPPT encBool (keyDistinguisher encrypt adversary) := by let choiceEncoding := encPair (encPair encBool encBool) encBits let baseEncoding := encPair encUnary encBits diff --git a/Complexity/Crypto/Computational/GMW/PolyTime.lean b/Complexity/Crypto/Computational/GMW/PolyTime.lean index 58cb29a175..28f9dede98 100644 --- a/Complexity/Crypto/Computational/GMW/PolyTime.lean +++ b/Complexity/Crypto/Computational/GMW/PolyTime.lean @@ -517,7 +517,7 @@ theorem isPPTOn_runTwoRound {α Caller : Type} {enc : α ↪ List Bool} {input : {reply1 reply2 : Caller × List Bool → List Bool} {bound : Caller → ℕ} (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits - (fun p => Vstar p.1 (Prod.fst p.2) (Prod.snd p.2))) + (fun (n, a, z) => Vstar n a z)) (hprep : ComputableInPolyTime prepare input (encPair encUnary (encPair enc encBits))) (hr1 : ComputableInPolyTime reply1 (encPair input encBits) encBits) (hr2 : ComputableInPolyTime reply2 (encPair input encBits) encBits) @@ -526,8 +526,7 @@ theorem isPPTOn_runTwoRound {α Caller : Type} {enc : α ↪ List Bool} {input : (hle2 : ∀ c q, (reply2 (c, q)).length ≤ bound c) : IsPPTOn input (encPair encBits (encPair encUnary encBits)) (fun c => runTwoRound (fun q => reply1 (c, q)) (fun q => reply2 (c, q)) - (Vstar (prepare c).1 (Prod.fst (prepare c).2) (Prod.snd (prepare c).2)) - (0, [false, false, false])) := by + (Vstar (prepare c).1 (prepare c).2.1 (prepare c).2.2) (0, [false, false, false])) := by have hprep := hprep.tidy have hr1 := hr1.tidy have hr2 := hr2.tidy @@ -579,7 +578,7 @@ theorem isPPTOn_runTwoRound_prover {α Caller : Type} {enc : α ↪ List Bool} {openFlags bits ch_guess : Caller → List Bool} {seeds pads : Caller → List (List Bool)} (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits - (fun p => Vstar p.1 (Prod.fst p.2) (Prod.snd p.2))) + (fun (n, a, z) => Vstar n a z)) (hg : ComputableInPolyTime generator encBits encBits) (hn : ComputableInPolyTime n input encUnary) (hs : ComputableInPolyTime s input encUnary) @@ -661,6 +660,10 @@ theorem isPPTOn_gmwSampleSimCoins {α : Type} {input : α ↪ List Bool} · fun_prop · fun_prop +/-- Verifier challenge component of a `runTwoRound` output `(view, round, challenge)`. -/ +abbrev twoRoundChallenge {α β γ : Type*} (p : α × β × γ) : γ := + p.2.2 + /-- Run one simulated GMW attempt with pre-sampled unopened pads `pads` (without any witness). -/ noncomputable def gmwSimWithPads (generator : List Bool → List Bool) (s m : ℕ) (φ : CNF ℕ) (prog : WordOracleComp Unit (List Bool)) (pads : List (List Bool)) : @@ -671,7 +674,7 @@ noncomputable def gmwSimWithPads (generator : List Bool → List Bool) (s m : (fun r => proverReply1 generator m r (allOpenFlags φ ch_guess coins.1) coins.1 coins.2 pads) (fun _ => proverReply2 s φ ch_guess coins.1 coins.2) prog (0, [false, false, false]) - return if Prod.snd p.2 == ch_guess then true :: p.1 else [] + return if twoRoundChallenge p == ch_guess then true :: p.1 else [] /-- One attempt of the GMW zero-knowledge simulator (without any witness). -/ noncomputable def gmwSimAttempt (generator : List Bool → List Bool) (s m : ℕ) (φ : CNF ℕ) @@ -694,7 +697,7 @@ private theorem isPPTOn_gmwSimWithPads {α : Type} {enc : α ↪ List Bool} (hlen : ∀ s, (generator s).length = length s.length) (hf : ComputableTidilyInPolyTime f enc encCNF) (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits - (fun p => Vstar p.1 p.2.1 p.2.2)) : + (fun (n, a, z) => Vstar n a z)) : IsPPTOn (encPair (encPair encUnary (encPair enc encBits)) (encList encBits)) encBits (fun p : (ℕ × α × List Bool) × List (List Bool) => gmwSimWithPads generator (p.1.1 + 7) (length (p.1.1 + 7)) @@ -702,7 +705,7 @@ private theorem isPPTOn_gmwSimWithPads {α : Type} {enc : α ↪ List Bool} have hgPlain := ComputableInPolyTime.of_tidy hg have hfPlain := ComputableInPolyTime.of_tidy hf have hlength := PRG.polyTime_length hgPlain hlen - dsimp only [gmwSimWithPads] + dsimp only [gmwSimWithPads, twoRoundChallenge] apply IsPPTOn.bind_with (left := encBits) · exact (ComputableInPolyTime.const 3).sampleList apply IsPPTOn.bind_with (left := encPair encBits (encList encBits)) @@ -720,7 +723,7 @@ private theorem isPPTOn_gmwSimAttempt {α : Type} {enc : α ↪ List Bool} (hlen : ∀ s, (generator s).length = length s.length) (hf : ComputableTidilyInPolyTime f enc encCNF) (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits - (fun p => Vstar p.1 p.2.1 p.2.2)) : + (fun (n, a, z) => Vstar n a z)) : IsPPTOn (encPair encUnary (encPair enc encBits)) encBits (fun p : ℕ × α × List Bool => gmwSimAttempt generator (p.1 + 7) (length (p.1 + 7)) @@ -743,10 +746,10 @@ theorem isPPTOn_gmwSimulator {α : Type} {enc : α ↪ List Bool} (hlen : ∀ s, (generator s).length = length s.length) (hf : ComputableInPolyTime f enc encCNF) (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits - (fun p => Vstar p.1 (Prod.fst p.2) (Prod.snd p.2))) : + (fun (n, a, z) => Vstar n a z)) : IsPPTOn (encPair encUnary (encPair enc encBits)) encBits - (fun p : ℕ × α × List Bool => - gmwSimulator generator length f Vstar p.1 (Prod.fst p.2) (Prod.snd p.2)) := by + (fun (n, a, z) => + gmwSimulator generator length f Vstar n a z) := by have hg := hg.tidy have hf := hf.tidy have hattempt := isPPTOn_gmwSimAttempt hg hlen hf hV @@ -795,7 +798,7 @@ private theorem isPPTOn_runTwoRound_honest {α Caller : Type} {enc : α ↪ List {n s m : Caller → ℕ} {a : Caller → α} {z : Caller → List Bool} {φ : Caller → CNF ℕ} {coins : Caller → List Bool × List (List Bool)} (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits - (fun p => Vstar p.1 p.2.1 p.2.2)) + (fun (n, a, z) => Vstar n a z)) (hg : ComputableTidilyInPolyTime generator encBits encBits) (hn : ComputableTidilyInPolyTime n input encUnary) (hs : ComputableTidilyInPolyTime s input encUnary) @@ -828,12 +831,11 @@ theorem isPPTOn_gmwInteract {α : Type} {enc : α ↪ List Bool} (hlen : ∀ s, (generator s).length = length s.length) (hf : ComputableInPolyTime f enc encCNF) (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits - (fun p => Vstar p.1 (Prod.fst p.2) (Prod.snd p.2))) : + (fun (n, a, z) => Vstar n a z)) : IsPPTOn (encPair encUnary (encPair enc (encPair encBits encBits))) encBits (fun p : ℕ × α × List Bool × List Bool => - gmwInteract generator (p.1 + 7) (length (p.1 + 7)) (f (Prod.fst p.2)) - (Prod.fst (Prod.snd p.2)) - (Vstar p.1 (Prod.fst p.2) (Prod.snd (Prod.snd p.2)))) := by + gmwInteract generator (p.1 + 7) (length (p.1 + 7)) (f p.2.1) p.2.2.1 + (Vstar p.1 p.2.1 p.2.2.2)) := by have hgPlain := hg have hfPlain := hf have hg := hg.tidy diff --git a/Complexity/Crypto/Computational/GMW/Simulator.lean b/Complexity/Crypto/Computational/GMW/Simulator.lean index 0f956fdb9c..a56b3447c6 100644 --- a/Complexity/Crypto/Computational/GMW/Simulator.lean +++ b/Complexity/Crypto/Computational/GMW/Simulator.lean @@ -478,7 +478,7 @@ noncomputable def gmwRealWithPads (generator : List Bool → List Bool) (s m : (fun r => proverReply1 generator m r openFlags bits seeds pads) (fun _ => proverReply2 s φ ch_guess bits seeds) prog (0, [false, false, false]) - return if Prod.snd p.2 == ch_guess then true :: p.1 else [] + return if twoRoundChallenge p == ch_guess then true :: p.1 else [] /-- Single-attempt hybrid with pseudorandom unopened pads. -/ noncomputable def gmwRealPRGPads (generator : List Bool → List Bool) (s m : ℕ) (φ : CNF ℕ) @@ -862,7 +862,7 @@ private theorem isPPTOn_gmwRealWithPads {α Param : Type} {enc : α ↪ List Boo {φ : Param → CNF ℕ} {pads : Param → List (List Bool)} (hg : ComputableTidilyInPolyTime generator encBits encBits) (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits - (fun p => Vstar p.1 p.2.1 p.2.2)) + (fun (n, a, z) => Vstar n a z)) (hn : ComputableTidilyInPolyTime n input encUnary) (hs : ComputableTidilyInPolyTime s input encUnary) (hm : ComputableTidilyInPolyTime m input encUnary) @@ -918,17 +918,13 @@ theorem isPPTOn_gmwViewReduction {α : Type} {enc : α ↪ List Bool} (hlen : ∀ s, (generator s).length = length s.length) (hf : ComputableInPolyTime f enc encCNF) (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits - (fun p => Vstar p.1 (Prod.fst p.2) (Prod.snd p.2))) + (fun (n, a, z) => Vstar n a z)) (hadv : IsPPTOn (encPair (encPair encUnary (encPair enc encBits)) encBits) encBool - (fun p => adversary (Prod.fst p.1) (Prod.fst (Prod.snd p.1)) - (Prod.snd (Prod.snd p.1)) p.2)) : + (fun ((n, a, z), view) => adversary n a z view)) : IsPPTOn (encPair (encPair encUnary (encPair enc (encPair encBits encBits))) encBits) encBool - (fun p : (ℕ × (α × (List Bool × List Bool))) × List Bool => - gmwViewReduction generator length f Vstar adversary - (Prod.fst p.1) (Prod.fst (Prod.snd p.1)) - (Prod.fst (Prod.snd (Prod.snd p.1))) - (Prod.snd (Prod.snd (Prod.snd p.1))) p.2) := by + (fun ((n, a, w, z), challenge) => + gmwViewReduction generator length f Vstar adversary n a w z challenge) := by have hgPlain := hg have hfPlain := hf have hg := hg.tidy @@ -1030,10 +1026,9 @@ theorem gmwView_negligible_of_advice_prg {α : Type} {enc : α ↪ List Bool} (hlen : ∀ s, (generator s).length = length s.length) (hf : ComputableInPolyTime f enc encCNF) (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits - (fun p => Vstar p.1 (Prod.fst p.2) (Prod.snd p.2))) + (fun (n, a, z) => Vstar n a z)) (hadv : IsPPTOn (encPair (encPair encUnary (encPair enc encBits)) encBits) encBool - (fun p => adversary (Prod.fst p.1) (Prod.fst (Prod.snd p.1)) - (Prod.snd (Prod.snd p.1)) p.2)) + (fun ((n, a, z), view) => adversary n a z view)) (hPRG : ∀ test : (ℕ × (α × (List Bool × List Bool))) × List Bool → ProbComp Bool, IsPPTOn (encPair (encPair encUnary (encPair enc (encPair encBits encBits))) encBits) @@ -1064,8 +1059,9 @@ theorem gmwView_negligible_of_advice_prg {α : Type} {enc : α ↪ List Bool} have hf := hf.tidy have hclock := isPPTOn_gmwViewReduction (.of_tidy hg) hlen (.of_tidy hf) hV hadv have hneg := hPRG - (fun p => gmwViewReduction generator length f Vstar adversary - p.1.1 p.1.2.1 p.1.2.2.1 p.1.2.2.2 p.2) hclock a w z ha hw hz + (fun ((n, a, w, z), challenge) => + gmwViewReduction generator length f Vstar adversary n a w z challenge) + hclock a w z ha hw hz have hcount : ComputableTidilyInPolyTime (fun a => totalLen (f a)) enc encUnary := (computableInPolyTime_totalLen (.of_tidy hf)).tidy have hsize : PolyBounded id (fun n => (enc (a n)).length) := @@ -1115,10 +1111,9 @@ theorem AdvicePRG.gmwView_negligible {α : Type} {enc : α ↪ List Bool} (hAdv : AdvicePRG enc generator length) (hf : ComputableInPolyTime f enc encCNF) (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits - (fun p => Vstar p.1 (Prod.fst p.2) (Prod.snd p.2))) + (fun (n, a, z) => Vstar n a z)) (hadv : IsPPTOn (encPair (encPair encUnary (encPair enc encBits)) encBits) encBool - (fun p => adversary (Prod.fst p.1) (Prod.fst (Prod.snd p.1)) - (Prod.snd (Prod.snd p.1)) p.2)) + (fun ((n, a, z), view) => adversary n a z view)) {a : ℕ → α} {w z : ℕ → List Bool} (ha : PolynomiallyBounded (fun n => (enc (a n)).length)) (hw : PolynomiallyBounded (fun n => (w n).length)) @@ -1144,7 +1139,7 @@ theorem gmwView_indistinguishable_gmwSimulator {α : Type} {enc : α ↪ List Bo {f : α → CNF ℕ} (hf : ComputableInPolyTime f enc encCNF) {Vstar : ℕ → α → List Bool → WordOracleComp Unit (List Bool)} (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits - (fun p => Vstar p.1 (Prod.fst p.2) (Prod.snd p.2))) + (fun (n, a, z) => Vstar n a z)) {a : ℕ → α} {w z : ℕ → List Bool} (ha : ComputableInPolyTime a encUnary enc) (hw_comp : ComputableInPolyTime w encUnary encBits) diff --git a/Complexity/Crypto/Protocols/Cipher/EvenMansour.lean b/Complexity/Crypto/Protocols/Cipher/EvenMansour.lean index a1c9a956b6..b4d1890b6b 100644 --- a/Complexity/Crypto/Protocols/Cipher/EvenMansour.lean +++ b/Complexity/Crypto/Protocols/Cipher/EvenMansour.lean @@ -1672,9 +1672,17 @@ theorem run_idealLazyHandler_good_le_realLazyHandler {α : Type} (program : OracleComp (EvenMansourSpec G) α) (P : α → Prop) (k : G × G) {c_e c_π c : Cache G} (hrel : CacheRel k c_e c_π c) : ((OracleComp.interpret idealLazyHandler program).run (c_e, c_π)).toOuterMeasure - {res | P res.1 ∧ isBadEvenMansourKey (Prod.fst res.2) (Prod.snd res.2) k = false} ≤ + {(r, c_e', c_π') : α × Cache G × Cache G | + P r ∧ isBadEvenMansourKey c_e' c_π' k = false} ≤ ((OracleComp.interpret (realLazyHandler k) program).run c).toOuterMeasure {res | P res.1} := by + have hset : + {(r, c_e', c_π') : α × Cache G × Cache G | + P r ∧ isBadEvenMansourKey c_e' c_π' k = false} = + {res | P res.1 ∧ isBadEvenMansourKey res.2.1 res.2.2 k = false} := by + ext ⟨_, _, _⟩ + simp + rw [hset] induction program generalizing c_e c_π c with | pure a => change (PMF.pure (a, (c_e, c_π))).toOuterMeasure @@ -1910,8 +1918,16 @@ private theorem idealGame_apply_le_realGame_add_of_keyDist (keyDist : PMF (G × MeasureTheory.measure_union_le _ _ _ ≤ ((OracleComp.interpret (realLazyHandler k) program).run []).toOuterMeasure (Prod.fst ⁻¹' {b}) + - M_ideal.toOuterMeasure {res | isBadEvenMansourKey res.2.1 res.2.2 k = true} := - add_le_add + M_ideal.toOuterMeasure {res | isBadEvenMansourKey res.2.1 res.2.2 k = true} := by + have hset : + {res : Bool × (Cache G × Cache G) | + res.1 = b ∧ isBadEvenMansourKey res.2.1 res.2.2 k = false} = + {(r, c_e', c_π') : Bool × Cache G × Cache G | + r = b ∧ isBadEvenMansourKey c_e' c_π' k = false} := by + ext ⟨_, _, _⟩ + simp + rw [hset] + exact add_le_add (run_idealLazyHandler_good_le_realLazyHandler program (· = b) k (cacheRel_nil k)) le_rfl have hsum_ideal : ∑' k : G × G, keyDist k * evenMansourIdealGame program b = diff --git a/Complexity/Crypto/Protocols/MAC/CarterWegman.lean b/Complexity/Crypto/Protocols/MAC/CarterWegman.lean index 492754a01c..42a50c10db 100644 --- a/Complexity/Crypto/Protocols/MAC/CarterWegman.lean +++ b/Complexity/Crypto/Protocols/MAC/CarterWegman.lean @@ -2885,13 +2885,13 @@ noncomputable def carterWegmanNonceMAC (msgLen : ℕ → ℕ) have hfamily_tidy := hfamily.tidy have hprf : ComputableTidilyInPolyTime (fun p : List Bool × List Bool × List Bool => - prfOracle family (dropFrame p.1).length (dropFrame p.1) (Prod.snd p.2)) + prfOracle family (dropFrame p.1).length (dropFrame p.1) p.2.2) (encPair encBits (encPair encBits encBits)) encBits := by have heq : (fun p : List Bool × List Bool × List Bool => - prfOracle family (dropFrame p.1).length (dropFrame p.1) (Prod.snd p.2)) = + prfOracle family (dropFrame p.1).length (dropFrame p.1) p.2.2) = (fun p : List Bool × List Bool × List Bool => - if (Prod.snd p.2).length == (dropFrame p.1).length then - family (dropFrame p.1) (Prod.snd p.2) + if p.2.2.length == (dropFrame p.1).length then + family (dropFrame p.1) p.2.2 else []) := by funext p @@ -2903,9 +2903,8 @@ noncomputable def carterWegmanNonceMAC (msgLen : ℕ → ℕ) let k := unframe p.1 let prfKey := dropFrame p.1 let n := prfKey.length - if ((Prod.fst p.2).length == msgLen n) && ((Prod.snd p.2).length == n) then - BitString.listXor n - [hash n k (Prod.fst p.2), (prfOracle family n prfKey (Prod.snd p.2)).take n] + if (p.2.1.length == msgLen n) && (p.2.2.length == n) then + BitString.listXor n [hash n k p.2.1, (prfOracle family n prfKey p.2.2).take n] else []) (encPair encBits (encPair encBits encBits)) encBits := by @@ -2914,10 +2913,9 @@ noncomputable def carterWegmanNonceMAC (msgLen : ℕ → ℕ) let k := unframe p.1 let prfKey := dropFrame p.1 let n := prfKey.length - if ((Prod.fst p.2).length == msgLen n) && ((Prod.snd p.2).length == n) then + if (p.2.1.length == msgLen n) && (p.2.2.length == n) then (pure (BitString.listXor n - [hash n k (Prod.fst p.2), - (prfOracle family n prfKey (Prod.snd p.2)).take n]) : ProbComp (List Bool)) + [hash n k p.2.1, (prfOracle family n prfKey p.2.2).take n]) : ProbComp (List Bool)) else pure []) = (fun p : List Bool × List Bool × List Bool => @@ -2925,9 +2923,8 @@ noncomputable def carterWegmanNonceMAC (msgLen : ℕ → ℕ) let k := unframe p.1 let prfKey := dropFrame p.1 let n := prfKey.length - if ((Prod.fst p.2).length == msgLen n) && ((Prod.snd p.2).length == n) then - BitString.listXor n - [hash n k (Prod.fst p.2), (prfOracle family n prfKey (Prod.snd p.2)).take n] + if (p.2.1.length == msgLen n) && (p.2.2.length == n) then + BitString.listXor n [hash n k p.2.1, (prfOracle family n prfKey p.2.2).take n] else [])) := by funext p @@ -2941,13 +2938,13 @@ noncomputable def carterWegmanNonceMAC (msgLen : ℕ → ℕ) have hfamily_tidy := hfamily.tidy have hprf : ComputableTidilyInPolyTime (fun p : List Bool × List Bool × List Bool × List Bool => - prfOracle family (dropFrame p.1).length (dropFrame p.1) (Prod.fst (Prod.snd p.2))) + prfOracle family (dropFrame p.1).length (dropFrame p.1) p.2.2.1) (encPair encBits (encPair encBits (encPair encBits encBits))) encBits := by have heq : (fun p : List Bool × List Bool × List Bool × List Bool => - prfOracle family (dropFrame p.1).length (dropFrame p.1) (Prod.fst (Prod.snd p.2))) = + prfOracle family (dropFrame p.1).length (dropFrame p.1) p.2.2.1) = (fun p : List Bool × List Bool × List Bool × List Bool => - if (Prod.fst (Prod.snd p.2)).length == (dropFrame p.1).length then - family (dropFrame p.1) (Prod.fst (Prod.snd p.2)) + if p.2.2.1.length == (dropFrame p.1).length then + family (dropFrame p.1) p.2.2.1 else []) := by funext p @@ -4719,13 +4716,13 @@ noncomputable def carterWegmanRandomMAC (msgLen : ℕ → ℕ) have hfamily_tidy := hfamily.tidy have hprf : ComputableTidilyInPolyTime (fun p : (List Bool × List Bool) × List Bool => - prfOracle family (dropFrame (Prod.fst p.1)).length (dropFrame (Prod.fst p.1)) p.2) + prfOracle family (dropFrame p.1.1).length (dropFrame p.1.1) p.2) (encPair (encPair encBits encBits) encBits) encBits := by have heq : (fun p : (List Bool × List Bool) × List Bool => - prfOracle family (dropFrame (Prod.fst p.1)).length (dropFrame (Prod.fst p.1)) p.2) = + prfOracle family (dropFrame p.1.1).length (dropFrame p.1.1) p.2) = (fun p : (List Bool × List Bool) × List Bool => - if p.2.length == (dropFrame (Prod.fst p.1)).length then - family (dropFrame (Prod.fst p.1)) p.2 + if p.2.length == (dropFrame p.1.1).length then + family (dropFrame p.1.1) p.2 else []) := by funext p @@ -4734,13 +4731,12 @@ noncomputable def carterWegmanRandomMAC (msgLen : ℕ → ℕ) polytime have hbody : ComputableTidilyInPolyTime (fun p : (List Bool × List Bool) × List Bool => - let k := unframe (Prod.fst p.1) - let prfKey := dropFrame (Prod.fst p.1) + let k := unframe p.1.1 + let prfKey := dropFrame p.1.1 let n := prfKey.length - if (Prod.snd p.1).length == msgLen n then + if p.1.2.length == msgLen n then encPair encBits encBits - (p.2, BitString.listXor n - [hash n k (Prod.snd p.1), (prfOracle family n prfKey p.2).take n]) + (p.2, BitString.listXor n [hash n k p.1.2, (prfOracle family n prfKey p.2).take n]) else []) (encPair (encPair encBits encBits) encBits) encBits := by @@ -4752,13 +4748,13 @@ noncomputable def carterWegmanRandomMAC (msgLen : ℕ → ℕ) have hfamily_tidy := hfamily.tidy have hprf : ComputableTidilyInPolyTime (fun p : List Bool × List Bool × List Bool => - prfOracle family (dropFrame p.1).length (dropFrame p.1) (unframe (Prod.snd p.2))) + prfOracle family (dropFrame p.1).length (dropFrame p.1) (unframe p.2.2)) (encPair encBits (encPair encBits encBits)) encBits := by have heq : (fun p : List Bool × List Bool × List Bool => - prfOracle family (dropFrame p.1).length (dropFrame p.1) (unframe (Prod.snd p.2))) = + prfOracle family (dropFrame p.1).length (dropFrame p.1) (unframe p.2.2)) = (fun p : List Bool × List Bool × List Bool => - if (unframe (Prod.snd p.2)).length == (dropFrame p.1).length then - family (dropFrame p.1) (unframe (Prod.snd p.2)) + if (unframe p.2.2).length == (dropFrame p.1).length then + family (dropFrame p.1) (unframe p.2.2) else []) := by funext p diff --git a/Complexity/Crypto/Protocols/MPC/CircuitEval.lean b/Complexity/Crypto/Protocols/MPC/CircuitEval.lean index e803b2e2e9..5bf3b0e44f 100644 --- a/Complexity/Crypto/Protocols/MPC/CircuitEval.lean +++ b/Complexity/Crypto/Protocols/MPC/CircuitEval.lean @@ -148,7 +148,8 @@ and applying `finish` at `.done`. -/ .message (sender := p.1) (receiver := p.2) (fun st => st.1 p.2) ((msgStepsWith finish L).mapState fun i st => - (Prod.fst st.1, Prod.snd st.1 + extractMsg p i st.2)) + let (toSend, acc) := st.1 + (toSend, acc + extractMsg p i st.2)) /-- All-to-all message exchange: party `s` sends `toSend s r` to party `r`, and party `i` applies `finish i` to the vector `fun s => toSend s i` of received messages. -/ @@ -642,13 +643,13 @@ applying `finish` at `.done`. -/ (r : Fin m) (finish : (i : Fin m) → State i → Bool → Out i) : (S : List (Fin m)) → Steps (fun i => State i × Bool × Bool) Out (gatherSchedule m (spec := spec) r S) - | [] => .done (fun i st => finish i st.1 (Prod.snd st.2)) + | [] => .done (fun i (state, _, acc) => finish i state acc) | s :: S => .message (sender := s) (receiver := r) - (fun st => Prod.fst st.2) + (fun (_, myShare, _) => myShare) ((gatherStepsWith r finish S).mapState fun i st => - (Prod.fst st.1, Prod.fst (Prod.snd st.1), - Prod.snd (Prod.snd st.1) + extractBitFor s r i st.2)) + let (state, myShare, acc) := st.1 + (state, myShare, acc + extractBitFor s r i st.2)) /-- Sum of party `i`'s received bits along `gatherSchedule m r S`. -/ @[expose] def sumGatherBits {m : ℕ} {spec : MultiOracleSpec} (r : Fin m) : diff --git a/Complexity/Crypto/Protocols/MPC/Composition.lean b/Complexity/Crypto/Protocols/MPC/Composition.lean index aaf7234e3e..8c07557aeb 100644 --- a/Complexity/Crypto/Protocols/MPC/Composition.lean +++ b/Complexity/Crypto/Protocols/MPC/Composition.lean @@ -429,16 +429,18 @@ first state component. -/ .message (sender := parties s₀) (receiver := parties r₀) (fun st_sender => send (st_sender.2 s₀ rfl)) ((Steps.embed parties Outer next).mapState fun _ st_i => - (Prod.fst st_i.1, fun s hs => - (Prod.snd st_i.1 s hs, - pullRoundReceived parties (.message s₀ r₀ Msg) hs st_i.2))) + let ((out_i, st_k_i), recv_i) := st_i + (out_i, fun s hs => + (st_k_i s hs, + pullRoundReceived parties (.message s₀ r₀ Msg) hs recv_i))) | .oracle (op := op) (parties := subParties) query next => .oracle (op := op) (parties := subParties.trans parties) (fun t st_party => query t (st_party.2 (subParties t) rfl)) ((Steps.embed parties Outer next).mapState fun _ st_i => - (Prod.fst st_i.1, fun s hs => - (Prod.snd st_i.1 s hs, - pullRoundReceived parties (.oracle op subParties) hs st_i.2))) + let ((out_i, st_k_i), recv_i) := st_i + (out_i, fun s hs => + (st_k_i s hs, + pullRoundReceived parties (.oracle op subParties) hs recv_i))) @[simp] private theorem outputAt_embed {k m : ℕ} {spec : MultiOracleSpec} (parties : Fin k ↪ Fin m) (Outer : Fin m → Type) @@ -515,16 +517,19 @@ execution of `(Sub op).steps` along `parties`. -/ .message (sender := s₀) (receiver := r₀) (fun st_sender => send st_sender.1) ((Steps.compose Sub next).mapState fun _ st_i => - ((Prod.fst st_i.1, st_i.2), Prod.snd st_i.1)) + let ((state_i, coins_i), recv_i) := st_i + ((state_i, recv_i), coins_i)) | .oracle (op := op) (parties := parties) (sc := rest) query next => (((Steps.embed parties (fun i => State i × Schedule.SubCoins Coins₂ rest i) (Sub op).steps).mapState - (fun i (st_i : State i × Schedule.SubCoins Coins₂ (.oracle op parties :: rest) i) => - ((st_i.1, Prod.snd st_i.2), + (fun i st_i => + let (state_i, slotCoins_i, restCoins_i) := st_i + ((state_i, restCoins_i), fun (s : Fin (spec₁.arity op)) (hs : parties s = i) => - (query s (hs.symm ▸ st_i.1), Prod.fst st_i.2 s hs)))).append + (query s (hs.symm ▸ state_i), slotCoins_i s hs)))).append ((Steps.compose Sub next).mapState fun _ st_i => - ((Prod.fst st_i.1, st_i.2), Prod.snd st_i.1))) + let ((state_i, restCoins_i), subOut_i) := st_i + ((state_i, subOut_i), restCoins_i))) /-- Expand a simulated outer execution along `steps : Steps State Out sc₁` by invoking the inner simulator `S₂ op (subCoalition parties I)` at every `.oracle op parties` round (Goldreich Theorem diff --git a/Complexity/Crypto/Protocols/MPC/PolyTime.lean b/Complexity/Crypto/Protocols/MPC/PolyTime.lean index fb1c4c878c..c448b1ebfb 100644 --- a/Complexity/Crypto/Protocols/MPC/PolyTime.lean +++ b/Complexity/Crypto/Protocols/MPC/PolyTime.lean @@ -357,9 +357,9 @@ packed coalition input bits `extendCoalitionBits I xI` and output bits def encFamilySimInput {α : Type} (enc : α ↪ List Bool) (m : ℕ) (n k : α → ℕ) (I : Finset (Fin m)) : FamilySimInput α m n k I ↪ List Bool where toFun inp := - let xy := inp.2 + let ⟨a, xI, yI⟩ := inp encPair enc (encPair encBits encBits) - (inp.1, (extendCoalitionBits I xy.1, extendCoalitionBits I xy.2)) + (a, (extendCoalitionBits I xI, extendCoalitionBits I yI)) inj' := by rintro ⟨a₁, x₁, y₁⟩ ⟨a₂, x₂, y₂⟩ h obtain ⟨ha, hxy⟩ := Prod.ext_iff.1 ((encPair enc (encPair encBits encBits)).injective h) @@ -500,14 +500,15 @@ def encGMWPartyView (m coins n k : ℕ) let (_, r_out) := splitOTMulCompose (GMWCircuit.progSchedule m D.program) (GMWCircuit.outputSchedule m k) i r_prog_out + let (preludeCoins, (circuitCoins, _), otSubCoins) := v.coins encPair (encPair (encPair encBits encBits) (encPair encBits encBits)) (encPair encBits (encPair encBits encBits)) - (((List.ofFn v.input, List.ofFn v.coins.1), + (((List.ofFn v.input, List.ofFn preludeCoins), (List.ofFn ((Cslib.BitString.blocksEquiv (α := Bool) (m := N) (k := m - 1)).symm - (Prod.fst (Prod.fst v.coins.2))), - encOTSubCoins _ i (Prod.snd v.coins.2))), + circuitCoins), + encOTSubCoins _ i otSubCoins)), (encPairsMsgReceived i (GMWCircuit.allPairs m) r_in, (encOTOracleAnswers _ i v.received, encOutCoordsMsgReceived i (GMWCircuit.outCoords m k) r_out))) @@ -5965,7 +5966,7 @@ theorem isPPTOn_gmwOT14RandomizedSim {α : Type} {enc : α ↪ List Bool} encodeCoalitionView (encGMWPartyView m (coins inp.1) (n inp.1) (k inp.1) (C inp.1)) I <$> gmwOT14RandomizedSim m (coins inp.1) (n inp.1) (k inp.1) - (C inp.1) I (Prod.fst inp.2) (Prod.snd inp.2)) := by + (C inp.1) I inp.2.1 inp.2.2) := by have hD := computableInPolyTime_code_comp_xorPreludeCircuit m hn hcoins hC exact (PolyTimeRunner.isPPTOn_simRunWord m I hcoins.tidy hn.tidy hk.tidy hD.tidy).congr (PolyTimeRunner.eval_simRunWord_eq_gmwOT14RandomizedSim m coins n k C I) @@ -6014,7 +6015,7 @@ theorem exists_perfectSemiHonestPrivate_ot14_of_polyTime {α : Type} {enc : α encodeCoalitionView (encGMWPartyView m (coins inp.1) (n inp.1) (k inp.1) (C inp.1)) I <$> gmwOT14RandomizedSim m (coins inp.1) (n inp.1) (k inp.1) - (C inp.1) I (Prod.fst inp.2) (Prod.snd inp.2))) := by + (C inp.1) I inp.2.1 inp.2.2)) := by have h_in : ComputableInPolyTime (fun a => m * n a + coins a) enc encUnary := by have hmn := ComputableTidilyInPolyTime.comp' ComputableTidilyInPolyTime.unary_mul ((ComputableTidilyInPolyTime.const m).prod hn.tidy) diff --git a/Complexity/Crypto/Protocols/MPC/SharedMul.lean b/Complexity/Crypto/Protocols/MPC/SharedMul.lean index bb09a9963f..87ded645d3 100644 --- a/Complexity/Crypto/Protocols/MPC/SharedMul.lean +++ b/Complexity/Crypto/Protocols/MPC/SharedMul.lean @@ -171,7 +171,7 @@ def twoPartyMulOutput (i : Fin 2) (st : ((Bool × Bool) × Fin.cases Bool (fun _ => Unit) i) × (Round.oracle (spec := ot14Spec) () (Function.Embedding.refl (Fin 2))).Received i) : Bool := Fin.cases - (fun (st : ((Bool × Bool) × Bool) × _) => Prod.snd st.1) + (fun (((_, c₀), _) : ((Bool × Bool) × Bool) × _) => c₀) (fun j st => st.2 j.succ rfl) i st /-- Construction 7.3.7 (p. 643): 2-party shared multiplication in the `ot14Spec`-hybrid model. @@ -301,10 +301,18 @@ theorem perfectSemiHonestPrivate_twoPartyMul : abbrev OrderedPair (m : ℕ) : Type := { p : Fin m × Fin m // p.1 < p.2 } -/-- Embedding of `Fin 2` into `Fin m` sending `0 ↦ p.1.1` and `1 ↦ p.1.2` for an ordered pair +/-- First party `i` of an ordered pair `(i, j)` in `OrderedPair m`. -/ +abbrev OrderedPair.first {m : ℕ} (p : OrderedPair m) : Fin m := + p.val.1 + +/-- Second party `j` of an ordered pair `(i, j)` in `OrderedPair m`. -/ +abbrev OrderedPair.second {m : ℕ} (p : OrderedPair m) : Fin m := + p.val.2 + +/-- Embedding of `Fin 2` into `Fin m` sending `0 ↦ p.first` and `1 ↦ p.second` for an ordered pair `p : OrderedPair m`. -/ def pairEmbedding {m : ℕ} (p : OrderedPair m) : Fin 2 ↪ Fin m where - toFun := Fin.cases p.val.1 (fun _ => p.val.2) + toFun := Fin.cases p.first (fun _ => p.second) inj' a b h := by fin_cases a <;> fin_cases b · rfl @@ -313,19 +321,19 @@ def pairEmbedding {m : ℕ} (p : OrderedPair m) : Fin 2 ↪ Fin m where · rfl @[simp] theorem pairEmbedding_zero {m : ℕ} (p : OrderedPair m) : - pairEmbedding p 0 = p.val.1 := rfl + pairEmbedding p 0 = p.first := rfl @[simp] theorem pairEmbedding_one {m : ℕ} (p : OrderedPair m) : - pairEmbedding p 1 = p.val.2 := rfl + pairEmbedding p 1 = p.second := rfl /-- Joint 2-party shared-multiplication oracle round for `p : OrderedPair m`. -/ @[reducible] def pairRound {m : ℕ} (p : OrderedPair m) : Round m (sharedMulSpec 2) := .oracle () (pairEmbedding p) -/-- A party `i` that is neither `p.1.1` nor `p.1.2` receives a subsingleton record in +/-- A party `i` that is neither `p.first` nor `p.second` receives a subsingleton record in `pairRound p`. -/ theorem subsingleton_received_pairRound {m : ℕ} (p : OrderedPair m) {i : Fin m} - (h1 : i ≠ p.val.1) (h2 : i ≠ p.val.2) : Subsingleton ((pairRound p).Received i) := by + (h1 : i ≠ p.first) (h2 : i ≠ p.second) : Subsingleton ((pairRound p).Received i) := by refine ⟨fun r₁ r₂ => Round.received_oracle_ext fun s hs => ?_⟩ fin_cases s · exact (h1 hs.symm).elim @@ -348,12 +356,12 @@ def orderedPairs (m : ℕ) : List (OrderedPair m) := pairsSchedule (orderedPairs m) /-- Extract party `i`'s oracle answer share from `pairRound p` (`0` if `i` is not one of the -two participating parties `p.1.1` or `p.1.2`). -/ +two participating parties `p.first` or `p.second`). -/ def extractPairShare {m : ℕ} (p : OrderedPair m) (i : Fin m) (r : (pairRound p).Received i) : Bool := - if h0 : p.val.1 = i then + if h0 : p.first = i then r 0 h0 - else if h1 : p.val.2 = i then + else if h1 : p.second = i then r 1 h1 else 0 @@ -369,8 +377,9 @@ def pairsSteps {m : ℕ} : | p :: L => .oracle (op := ()) (parties := pairEmbedding p) (fun _ st => st.1) - ((pairsSteps L).mapState fun i (st : ((Bool × Bool) × Bool) × (pairRound p).Received i) => - (Prod.fst st.1, Prod.snd st.1 + extractPairShare p i st.2)) + ((pairsSteps L).mapState fun i st => + let (xy, acc) := st.1 + (xy, acc + extractPairShare p i st.2)) /-- Construction 7.5.8 (p. 704): `m`-party shared multiplication in the 2-ary `sharedMulSpec 2`-hybrid model, invoking `sharedMulSpec 2` once for each pair `i < j`. @@ -383,7 +392,8 @@ def multiPartyMulProtocol (m : ℕ) : sampleCoins _ := pure () steps := (pairsSteps (orderedPairs m)).mapState fun _ st => - (st.1, m • (Prod.fst st.1 * Prod.snd st.1)) + let (a, b) := st.1 + ((a, b), m • (a * b)) namespace MultiPartyMul @@ -414,7 +424,7 @@ theorem outputOfView_multiPartyMulProtocol {m : ℕ} (i : Fin m) pairwise shares `row_i : Fin m → Bool`. -/ def receivedPairOfRow {m : ℕ} (p : OrderedPair m) (i : Fin m) (row_i : Fin m → Bool) : (pairRound p).Received i := - fun s _ => Fin.cases (row_i p.val.2) (fun _ => row_i p.val.1) s + fun s _ => Fin.cases (row_i p.second) (fun _ => row_i p.first) s /-- Construct party `i`'s received transcript along `pairsSchedule L` from party `i`'s row of pairwise shares `row_i : Fin m → Bool`. -/ @@ -426,8 +436,8 @@ def receivedScheduleOfRow {m : ℕ} (i : Fin m) (row_i : Fin m → Bool) : theorem extractPairShare_receivedPairOfRow {m : ℕ} (p : OrderedPair m) (i : Fin m) (row_i : Fin m → Bool) : extractPairShare p i (receivedPairOfRow p i row_i) = - (if p.val.1 = i then row_i p.val.2 else 0) + - (if p.val.2 = i then row_i p.val.1 else 0) := by + (if p.first = i then row_i p.second else 0) + + (if p.second = i then row_i p.first else 0) := by dsimp [extractPairShare, receivedPairOfRow] by_cases h0 : p.1.1 = i · have h1 : p.1.2 ≠ i := fun h => ne_of_lt p.2 (h0.trans h.symm) @@ -477,7 +487,7 @@ theorem sumReceivedShares_receivedScheduleOfRow {m : ℕ} (i : Fin m) | nil => rfl | cons p L ih => simp [sumReceivedShares, receivedScheduleOfRow, ih] rw [hL, sum_map_orderedPairs] - simp only [extractPairShare_receivedPairOfRow, dite_eq_ite] + simp only [extractPairShare_receivedPairOfRow, OrderedPair.first, OrderedPair.second, dite_eq_ite] have hsplit : ∀ u v : Fin m, (if u < v then (if u = i then row_i v else 0) + (if v = i then row_i u else 0) @@ -644,7 +654,7 @@ def viewOfRow {m : ℕ} (i : Fin m) (xi : Bool × Bool) (row_i : Fin m → Bool) /-- 2-party oracle answer tuple for pair `p` on input `x` and coin `b : Bool`. -/ def pairAnswer {m : ℕ} (x : Fin m → Bool × Bool) (p : OrderedPair m) (b : Bool) : Fin 2 → Bool := - completeShares 2 (pairTarget x p.val.1 p.val.2) (fun _ => b) + completeShares 2 (pairTarget x p.first p.second) (fun _ => b) theorem deliverOracle_pairAnswer_eq_receivedPairOfRow {m : ℕ} (x : Fin m → Bool × Bool) (r : OrderedPair m → Bool) (p : OrderedPair m) (i : Fin m) : @@ -797,17 +807,17 @@ theorem evalWith_multiPartyMulProtocol (m : ℕ) (x : Fin m → Bool × Bool) : /-- Coin adjustment supported on pairs incident to the pivot party `ℓ : Fin m`. -/ def delta {m : ℕ} (ℓ : Fin m) (w : Fin m → Bool) (p : OrderedPair m) : Bool := - if p.val.1 = ℓ then w p.val.2 - else if p.val.2 = ℓ then w p.val.1 + if p.first = ℓ then w p.second + else if p.second = ℓ then w p.first else 0 /-- Restriction-based presentation of `delta ℓ` depending only on `Finset.univ.erase ℓ`. -/ def deltaErase {m : ℕ} (ℓ : Fin m) (u : (i : Finset.univ.erase ℓ) → Bool) (p : OrderedPair m) : Bool := - if h1 : p.val.1 = ℓ then - u ⟨p.val.2, Finset.mem_erase.mpr ⟨ne_of_gt (h1 ▸ p.2), Finset.mem_univ _⟩⟩ - else if h2 : p.val.2 = ℓ then - u ⟨p.val.1, Finset.mem_erase.mpr ⟨ne_of_lt (h2 ▸ p.2), Finset.mem_univ _⟩⟩ + if h1 : p.first = ℓ then + u ⟨p.second, Finset.mem_erase.mpr ⟨ne_of_gt (h1 ▸ p.2), Finset.mem_univ _⟩⟩ + else if h2 : p.second = ℓ then + u ⟨p.first, Finset.mem_erase.mpr ⟨ne_of_lt (h2 ▸ p.2), Finset.mem_univ _⟩⟩ else 0 theorem delta_eq_deltaErase_restrict {m : ℕ} (ℓ : Fin m) (w : Fin m → Bool) : @@ -912,8 +922,8 @@ def extendOut {m : ℕ} (I : Finset (Fin m)) (yI : (i : I) → Bool) (j : Fin m) `matrixOfCoins (extendIn I (I.restrict x)) r i` for all `i ∈ I`. -/ def sigmaShift {m : ℕ} (I : Finset (Fin m)) (x : Fin m → Bool × Bool) (p : OrderedPair m) : Bool := - if p.val.2 ∈ I then - pairTarget x p.val.2 p.val.1 + pairTarget (extendIn I (I.restrict x)) p.val.2 p.val.1 + if p.second ∈ I then + pairTarget x p.second p.first + pairTarget (extendIn I (I.restrict x)) p.second p.first else 0 diff --git a/Complexity/Crypto/Protocols/SigmaProtocol/Abort.lean b/Complexity/Crypto/Protocols/SigmaProtocol/Abort.lean index 2653b9ebb5..3620cc4763 100644 --- a/Complexity/Crypto/Protocols/SigmaProtocol/Abort.lean +++ b/Complexity/Crypto/Protocols/SigmaProtocol/Abort.lean @@ -77,7 +77,7 @@ noncomputable def acceptedTranscript (x : X) (y : Y) (c : C) : PMF (Option (T × /-- An honest conversation with a uniform challenge, or `none` if the prover aborts. -/ noncomputable def acceptedConversation [Fintype C] [Nonempty C] (x : X) (y : Y) : PMF (Option (T × C × Z)) := - (P.conversation x y).map fun tcz => (Prod.snd tcz.2).map fun z => (tcz.1, Prod.fst tcz.2, z) + (P.conversation x y).map fun tcz => (convResponse tcz).map fun z => (tcz.1, convChallenge tcz, z) /-- Completeness up to aborts: for every witness-statement pair in `R` and every challenge, every honest transcript in which the prover does not abort is accepting. -/ diff --git a/Complexity/Crypto/Protocols/SigmaProtocol/Basic.lean b/Complexity/Crypto/Protocols/SigmaProtocol/Basic.lean index 05ec070425..44e5d61b35 100644 --- a/Complexity/Crypto/Protocols/SigmaProtocol/Basic.lean +++ b/Complexity/Crypto/Protocols/SigmaProtocol/Basic.lean @@ -188,11 +188,19 @@ theorem conversation_eq_bind_transcript [Fintype C] [Nonempty C] (x : X) (y : Y) variable {P} +/-- Challenge component `c` of a conversation transcript `(t, c, z)`. -/ +abbrev convChallenge {T C Z : Type*} (tcz : T × C × Z) : C := + tcz.2.1 + +/-- Response component `z` of a conversation transcript `(t, c, z)`. -/ +abbrev convResponse {T C Z : Type*} (tcz : T × C × Z) : Z := + tcz.2.2 + /-- Every honest conversation is accepting: the verifier always accepts the honest prover. -/ theorem Complete.accepts_of_mem_support_conversation [Fintype C] [Nonempty C] (h : P.Complete R) {x : X} {y : Y} (hxy : R x y) {tcz : T × C × Z} (htcz : tcz ∈ (P.conversation x y).support) : - P.Accepts y tcz.1 (Prod.fst tcz.2) (Prod.snd tcz.2) := by + P.Accepts y tcz.1 (convChallenge tcz) (convResponse tcz) := by rw [conversation_eq_bind_transcript] at htcz simp only [PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, PMF.mem_support_bind_iff, PMF.mem_support_pure_iff] at htcz diff --git a/Complexity/Crypto/Protocols/SigmaProtocol/Composition.lean b/Complexity/Crypto/Protocols/SigmaProtocol/Composition.lean index d7cd45552b..2da07ced49 100644 --- a/Complexity/Crypto/Protocols/SigmaProtocol/Composition.lean +++ b/Complexity/Crypto/Protocols/SigmaProtocol/Composition.lean @@ -154,6 +154,14 @@ def orRelation (R₀ : X₀ → Y₀ → Prop) (R₁ : X₁ → Y₁ → Prop) : variable [AddCommGroup C] [Fintype C] +/-- First-side response `z₀` of an OR-proof response `(c₀, z₀, z₁)`. -/ +abbrev orResp₀ {C Z₀ Z₁ : Type*} (z : C × Z₀ × Z₁) : Z₀ := + z.2.1 + +/-- Second-side response `z₁` of an OR-proof response `(c₀, z₀, z₁)`. -/ +abbrev orResp₁ {C Z₀ Z₁ : Type*} (z : C × Z₀ × Z₁) : Z₁ := + z.2.2 + /-- The OR-proof ([BonehShoup2023], Section 19.7.2). With a witness for one side, the prover simulates the other side at a uniform challenge `c'`, commits honestly on its own side, and answers the verifier's challenge `c` on its own side at `c - c'`. The response @@ -177,15 +185,15 @@ noncomputable def orProof (P₀ : SigmaProtocol X₀ Y₀ T₀ C Z₀) (P₁ : S | .inl (x, s₀, c₁, z₁) => (c - c₁, P₀.respond x y.1 s₀ (c - c₁), z₁) | .inr (x, s₁, c₀, z₀) => (c₀, z₀, P₁.respond x y.2 s₁ (c - c₀)) verify y t c z := - P₀.verify y.1 t.1 z.1 (Prod.fst z.2) && P₁.verify y.2 t.2 (c - z.1) (Prod.snd z.2) + P₀.verify y.1 t.1 z.1 (orResp₀ z) && P₁.verify y.2 t.2 (c - z.1) (orResp₁ z) /-- The OR extractor uses the first side when the first side's challenges differ, and the second side otherwise. -/ def orExtract [DecidableEq C] (extract₀ : Y₀ → T₀ → C → Z₀ → C → Z₀ → X₀) (extract₁ : Y₁ → T₁ → C → Z₁ → C → Z₁ → X₁) (y : Y₀ × Y₁) (t : T₀ × T₁) (c : C) (z : C × Z₀ × Z₁) (c' : C) (z' : C × Z₀ × Z₁) : X₀ ⊕ X₁ := - if z.1 = z'.1 then .inr (extract₁ y.2 t.2 (c - z.1) (Prod.snd z.2) (c' - z'.1) (Prod.snd z'.2)) - else .inl (extract₀ y.1 t.1 z.1 (Prod.fst z.2) z'.1 (Prod.fst z'.2)) + if z.1 = z'.1 then .inr (extract₁ y.2 t.2 (c - z.1) (orResp₁ z) (c' - z'.1) (orResp₁ z')) + else .inl (extract₀ y.1 t.1 z.1 (orResp₀ z) z'.1 (orResp₀ z')) /-- The OR simulator splits the challenge uniformly and simulates both sides. -/ noncomputable def orSimulate (simulate₀ : Y₀ → C → PMF (T₀ × Z₀)) @@ -204,7 +212,7 @@ variable {P₀ : SigmaProtocol X₀ Y₀ T₀ C Z₀} {P₁ : SigmaProtocol X₁ side accepts at `c₀` and the second at `c - c₀`. -/ @[simp] theorem orProof_accepts_iff {y : Y₀ × Y₁} {t : T₀ × T₁} {c : C} {z : C × Z₀ × Z₁} : (orProof P₀ P₁ simulate₀ simulate₁).Accepts y t c z ↔ - P₀.Accepts y.1 t.1 z.1 (Prod.fst z.2) ∧ P₁.Accepts y.2 t.2 (c - z.1) (Prod.snd z.2) := by + P₀.Accepts y.1 t.1 z.1 (orResp₀ z) ∧ P₁.Accepts y.2 t.2 (c - z.1) (orResp₁ z) := by simp only [Accepts, orProof, Bool.and_eq_true] /-- With a witness for the first statement, the OR prover simulates the second side at a diff --git a/Complexity/Crypto/Protocols/SigmaProtocol/FiatShamir.lean b/Complexity/Crypto/Protocols/SigmaProtocol/FiatShamir.lean index e45844e432..0c0260d785 100644 --- a/Complexity/Crypto/Protocols/SigmaProtocol/FiatShamir.lean +++ b/Complexity/Crypto/Protocols/SigmaProtocol/FiatShamir.lean @@ -157,10 +157,9 @@ noncomputable def reductionHandler : (q : M ⊕ (M × T)) → StateT (ReductionState M T C Z) (OracleComp (fun _ : M × T => C)) (ForgerSpec M (M × T) (T × Z) C q) | .inl m => fun st => - let v := st.transcripts.headD (Classical.arbitrary _) - let cz := v.2 - pure ((v.1, cz.2), - ⟨((m, v.1), cz.1, none) :: st.table, m :: st.signed, st.count, st.transcripts.tail⟩) + let (t, c, z) := st.transcripts.headD (Classical.arbitrary _) + pure ((t, z), + ⟨((m, t), c, none) :: st.table, m :: st.signed, st.count, st.transcripts.tail⟩) | .inr x => fun st => match st.table.lookup x with | some entry => pure (entry.1, ⟨st.table, st.signed, st.count, st.transcripts.tail⟩) @@ -173,26 +172,20 @@ the position of the query for `(m, t)`. The verdict records the point, the chall response. -/ def verdict (P : SigmaProtocol X Y T C Z) (y : Y) (forged : (M × (T × Z)) × ReductionState M T C Z) (c : C) (position : Option ℕ) : Option ℕ × Bool × (M × T) × C × Z := - let sig := forged.1 - let m := sig.1 - let tz := sig.2 - let t := tz.1 - let z := tz.2 - (if P.verify y t c z && !forged.2.signed.contains m then position - else none, P.verify y t c z && !forged.2.signed.contains m, + let ((m, t, z), state) := forged + (if P.verify y t c z && !state.signed.contains m then position + else none, P.verify y t c z && !state.signed.contains m, (m, t), c, z) /-- Check a forgery, querying its point when the table lacks it. -/ noncomputable def finish (P : SigmaProtocol X Y T C Z) (y : Y) (forged : (M × (T × Z)) × ReductionState M T C Z) : OracleComp (fun _ : M × T => C) (Option ℕ × Bool × (M × T) × C × Z) := - let sig := forged.1 - let tz := sig.2 - let pt := (sig.1, tz.1) - match forged.2.table.lookup pt with + let ((m, t, _), state) := forged + match state.table.lookup (m, t) with | some entry => pure (verdict P y forged entry.1 entry.2) - | none => (fun c => verdict P y forged c (some forged.2.count)) <$> - OracleComp.query pt + | none => (fun c => verdict P y forged c (some state.count)) <$> + OracleComp.query (m, t) /-- The forger, with simulated signing, as a program over the hash oracle with explicit coins: the statement, the forger's coins and the simulated transcripts. It names the query of the forgery's @@ -200,8 +193,8 @@ point when the forger wins. -/ noncomputable def forkingProgram (P : SigmaProtocol X Y T C Z) (A : Forger Y M (T × Z) (M × T) C) (s : Y × A.Coins × List (T × C × Z)) : OracleComp (fun _ : M × T => C) (Option ℕ × Bool × (M × T) × C × Z) := - let rest := s.2 - (interpret reductionHandler (A.forge s.1 rest.1)).run ⟨[], [], 0, rest.2⟩ >>= finish P s.1 + let (y, c, transcripts) := s + (interpret reductionHandler (A.forge y c)).run ⟨[], [], 0, transcripts⟩ >>= finish P y /-- The coins of the forking program for the statement `y`: the forger's coins and `Q` simulated transcripts. -/ @@ -224,16 +217,9 @@ noncomputable def reduction [Nonempty X] (P : SigmaProtocol X Y T C Z) match result with | none => Classical.arbitrary X | some (_, out, out') => - let v := out.1 - let bptcz := v.2 - let ptcz := bptcz.2 - let pt := ptcz.1 - let cz := ptcz.2 - let v' := out'.1 - let bptcz' := v'.2 - let ptcz' := bptcz'.2 - let cz' := ptcz'.2 - extract y pt.2 cz.1 cz.2 cz'.1 cz'.2 + let (_, _, (_, t), c, z) := out.1 + let (_, _, _, c', z') := out'.1 + extract y t c z c' z' end FiatShamir diff --git a/Complexity/Crypto/Protocols/SigmaProtocol/Linear.lean b/Complexity/Crypto/Protocols/SigmaProtocol/Linear.lean index 0fadbc2d47..521b965b2b 100644 --- a/Complexity/Crypto/Protocols/SigmaProtocol/Linear.lean +++ b/Complexity/Crypto/Protocols/SigmaProtocol/Linear.lean @@ -217,28 +217,36 @@ noncomputable def chaumPedersen (g : G) : SigmaProtocol (ZMod q) (G × G × G) ( linear (fun s => (LinearMap.toSpanSingleton (ZMod q) G g).prod (LinearMap.toSpanSingleton (ZMod q) G s.1)) Prod.snd ι +/-- First group element `v` of a Chaum–Pedersen statement `(u, v, w)`. -/ +abbrev cpStatementV {G : Type*} (s : G × G × G) : G := + s.2.1 + +/-- Second group element `w` of a Chaum–Pedersen statement `(u, v, w)`. -/ +abbrev cpStatementW {G : Type*} (s : G × G × G) : G := + s.2.2 + /-- The Chaum–Pedersen verification equations `z • g = t₁ + c • v` and `z • u = t₂ + c • w` ([BonehShoup2023], Section 19.5.2). -/ @[simp] theorem chaumPedersen_accepts_iff {s : G × G × G} {t : G × G} {c : C} {z : ZMod q} : (chaumPedersen ι g).Accepts s t c z ↔ - z • g = t.1 + ι c • Prod.fst s.2 ∧ z • s.1 = t.2 + ι c • Prod.snd s.2 := by + z • g = t.1 + ι c • cpStatementV s ∧ z • s.1 = t.2 + ι c • cpStatementW s := by simp [chaumPedersen, Prod.ext_iff] /-- Theorem 19.10 of [BonehShoup2023]: completeness. -/ theorem chaumPedersen_complete : - (chaumPedersen ι g).Complete fun β s => β • g = Prod.fst s.2 ∧ β • s.1 = Prod.snd s.2 := + (chaumPedersen ι g).Complete fun β (u, v, w) => β • g = v ∧ β • u = w := (linear_complete _ _ ι).mono fun _ _ h => by simpa [Prod.ext_iff] using h /-- Theorem 19.10 of [BonehShoup2023]: special soundness. -/ theorem chaumPedersen_specialSoundness [Fact q.Prime] : (chaumPedersen ι g).SpecialSoundness - (fun β s => β • g = Prod.fst s.2 ∧ β • s.1 = Prod.snd s.2) + (fun β (u, v, w) => β • g = v ∧ β • u = w) (linearExtract ι) := (linear_specialSoundness _ _ ι).mono fun _ _ h => by simpa [Prod.ext_iff] using h /-- Theorem 19.10 of [BonehShoup2023]: special honest-verifier zero knowledge. -/ theorem chaumPedersen_specialHVZK : - (chaumPedersen ι g).SpecialHVZK (fun β s => β • g = Prod.fst s.2 ∧ β • s.1 = Prod.snd s.2) + (chaumPedersen ι g).SpecialHVZK (fun β (u, v, w) => β • g = v ∧ β • u = w) (linearSimulate (fun s => (LinearMap.toSpanSingleton (ZMod q) G g).prod (LinearMap.toSpanSingleton (ZMod q) G s.1)) Prod.snd ι) := (linear_specialHVZK _ _ ι).mono fun _ _ h => by simpa [Prod.ext_iff] using h diff --git a/Complexity/Crypto/Protocols/SigmaProtocol/Lyubashevsky/NativeExtract.lean b/Complexity/Crypto/Protocols/SigmaProtocol/Lyubashevsky/NativeExtract.lean index a855bd8d6d..450ad26491 100644 --- a/Complexity/Crypto/Protocols/SigmaProtocol/Lyubashevsky/NativeExtract.lean +++ b/Complexity/Crypto/Protocols/SigmaProtocol/Lyubashevsky/NativeExtract.lean @@ -94,16 +94,25 @@ theorem computableInPolyTime_decodeLyubashevskyExtractInput : /-- Compute `z-z′` first, then the SIGNED challenge difference `c′-c`. The unary dimensions control both output segments; optional responses default to zero coordinatewise. -/ def lyubashevskyExtractList (input : LyubashevskyExtractInput) : List ℤ := - ((List.range (Prod.fst input.1)).map fun i => - ((Prod.snd (Prod.fst input.2)).getD []).getD i 0 - - ((Prod.snd (Prod.snd input.2)).getD []).getD i 0) ++ - ((List.range (Prod.snd input.1)).map fun i => - (if (Prod.fst (Prod.snd input.2)).getD i false then (1 : ℤ) else 0) - - (if (Prod.fst (Prod.fst input.2)).getD i false then (1 : ℤ) else 0)) + let ((m, k), (c, z), (c', z')) := input + ((List.range m).map fun i => + (z.getD []).getD i 0 - (z'.getD []).getD i 0) ++ + ((List.range k).map fun i => + (if c'.getD i false then (1 : ℤ) else 0) - + (if c.getD i false then (1 : ℤ) else 0)) + +/-- First unary dimension `m` (response dimension) of a `LyubashevskyExtractInput`. -/ +abbrev extractDimM (input : LyubashevskyExtractInput) : ℕ := + input.1.1 + +/-- Second unary dimension `k` (challenge dimension) of a `LyubashevskyExtractInput`. -/ +abbrev extractDimK (input : LyubashevskyExtractInput) : ℕ := + input.1.2 /-- Extraction always writes the two declared segments, even on malformed-length inputs. -/ @[simp] theorem length_lyubashevskyExtractList (input : LyubashevskyExtractInput) : - (lyubashevskyExtractList input).length = Prod.fst input.1 + Prod.snd input.1 := by + (lyubashevskyExtractList input).length = extractDimM input + extractDimK input := by + rcases input with ⟨⟨m, k⟩, ⟨c, z⟩, ⟨c', z'⟩⟩ simp [lyubashevskyExtractList] /-- One native extractor handles runtime dimensions and all binary integer magnitudes. -/ @@ -112,7 +121,15 @@ theorem computableInPolyTime_lyubashevskyExtractList : ComputableInPolyTime lyubashevskyExtractList encLyubashevskyExtractInput (encList encIntBin) := by apply ComputableInPolyTime.of_tidy - unfold lyubashevskyExtractList encLyubashevskyExtractInput + change ComputableTidilyInPolyTime + (fun input : LyubashevskyExtractInput => + ((List.range input.1.1).map fun i => + (input.2.1.2.getD []).getD i 0 - (input.2.2.2.getD []).getD i 0) ++ + ((List.range input.1.2).map fun i => + (if input.2.2.1.getD i false then (1 : ℤ) else 0) - + (if input.2.1.1.getD i false then (1 : ℤ) else 0))) + encLyubashevskyExtractInput (encList encIntBin) + unfold encLyubashevskyExtractInput fun_prop private theorem getD_optional_ofFn {m : ℕ} (z : Option (Fin m → ℤ)) (i : Fin m) :