{-# LANGUAGE NoImplicitPrelude #-} {-# LANGUAGE OverloadedStrings #-} -- | Groth16/BLS12-381 verification over CIP-381 builtins. -- -- This is the REAL verifier: it parses the compressed verifying key and -- proof (the exact wire format produced by the Go prover in -- @proto/vending/prover/serialize.go@) and runs the Groth16 pairing check -- through the Plutus BLS12-381 builtins. The same code path serves the small -- off-chain fixture (VerifySpec) and the big-RAM Recovery proof — only the -- bytes differ. -- -- Wire format (compressed ZCash/IETF points, MSB flag bits intact): -- -- Proof (192 bytes): A(G1)[0:48] | B(G2)[48:144] | C(G1)[144:192] -- VK (432 bytes): alpha(G1)[0:48] | beta(G2)[48:144] | gamma(G2)[144:240] -- | delta(G2)[240:336] | IC0(G1)[336:384] | IC1(G1)[384:432] -- -- Public input: the 'Scalar' carries the raw 32-byte Blake2b-256 digest. We -- read it LITTLE-ENDIAN and reduce mod r (the BLS12-381 scalar-field order), -- matching the circuit's @bytesToFieldLE@ / @RefPub@ reduction. With one -- public input the IC layout is (IC0, IC1) and -- @vk_x = IC0 + pub * IC1@. -- -- Check (gnark's Groth16 verify equation): -- e(A,B) == e(alpha,beta) * e(vk_x,gamma) * e(C,delta) -- expressed through finalVerify as -- finalVerify (millerLoop A B) -- (millerLoop alpha beta * millerLoop vk_x gamma * millerLoop C delta) module Recovery.Verify ( groth16Verify , groth16VerifyCommitted ) where import PlutusTx.Prelude import PlutusTx.Builtins ( bls12_381_G1_uncompress , bls12_381_G2_uncompress , bls12_381_G1_add , bls12_381_G1_neg , bls12_381_G1_scalarMul , bls12_381_millerLoop , bls12_381_mulMlResult , bls12_381_finalVerify , byteStringToInteger , integerToByteString , xorByteString , sha2_256 , consByteString , modInteger , sliceByteString , indexByteString , lengthOfByteString , ByteOrder (BigEndian, LittleEndian) ) import Recovery.Types -- | BLS12-381 scalar-field order r. The public input is reduced mod r so that -- the recovered field element equals the one gnark committed to. {-# INLINABLE blsScalarFieldOrder #-} blsScalarFieldOrder :: Integer blsScalarFieldOrder = 52435875175126190479447740508185965837690552500527637822603658699938581184513 -- | Fold a bytestring into an Integer, LITTLE-ENDIAN: byte i has weight 256^i. -- This matches the circuit's @bytesToFieldLE@ packing of the digest. {-# INLINABLE leBytesToInteger #-} leBytesToInteger :: BuiltinByteString -> Integer leBytesToInteger bs = go 0 0 1 where n = lengthOfByteString bs go i acc mul | i >= n = acc | otherwise = go (i + 1) (acc + indexByteString bs i * mul) (mul * 256) {-# INLINABLE groth16Verify #-} groth16Verify :: VerifyingKey -> Proof -> Scalar -> Bool groth16Verify (VerifyingKey vk) (Proof p) (Scalar pubBytes) = let -- verifying-key points alpha = bls12_381_G1_uncompress (sliceByteString 0 48 vk) beta = bls12_381_G2_uncompress (sliceByteString 48 96 vk) gamma = bls12_381_G2_uncompress (sliceByteString 144 96 vk) delta = bls12_381_G2_uncompress (sliceByteString 240 96 vk) ic0 = bls12_381_G1_uncompress (sliceByteString 336 48 vk) ic1 = bls12_381_G1_uncompress (sliceByteString 384 48 vk) -- proof points a = bls12_381_G1_uncompress (sliceByteString 0 48 p) b = bls12_381_G2_uncompress (sliceByteString 48 96 p) c = bls12_381_G1_uncompress (sliceByteString 144 48 p) -- public input: LE digest reduced into Fr pub = leBytesToInteger pubBytes `modInteger` blsScalarFieldOrder vkX = ic0 `bls12_381_G1_add` (pub `bls12_381_G1_scalarMul` ic1) -- pairing check: e(A,B) == e(alpha,beta)*e(vk_x,gamma)*e(C,delta) lhs = bls12_381_millerLoop a b rhs = bls12_381_millerLoop alpha beta `bls12_381_mulMlResult` bls12_381_millerLoop vkX gamma `bls12_381_mulMlResult` bls12_381_millerLoop c delta in bls12_381_finalVerify lhs rhs -- --------------------------------------------------------------------------- -- Commitment-aware verifier (gnark BSB22 Pedersen, ONE commitment) -- --------------------------------------------------------------------------- -- -- The production Recovery circuit's lookup-table hashing (std/math/uints in -- every Blake2b/SHA512/ed25519 gadget) forces a single gnark Pedersen -- commitment. The vanilla A|B|C verifier above drops it; this function consumes -- the extended wire format produced by @prover.SerializeVKCommitment@ / -- @SerializeProofCommitment@ and reproduces gnark's full verify (verify.go): -- -- VK (672B): [0:432) vanilla(alpha|beta|gamma|delta|IC0|IC1) -- [432:480) K2 (G1) [480:576) CK.G (G2) [576:672) CK.GSigmaNeg (G2) -- Proof (336B): [0:192) vanilla(A|B|C) -- [192:288) commitment UNCOMPRESSED (X48|Y48) [288:336) PoK (G1) -- -- Steps: -- 1. Reconstruct the compressed commitment from (X, sign-of-Y) per ZCash -- flag rules and uncompress it through the CIP-0381 builtin — this -- VALIDATES on-curve + subgroup and yields the point for the pairings. -- 2. Pedersen PoK: e(commitment, GSigmaNeg) * e(PoK, G) == 1, checked as -- e(PoK, G) == e(-commitment, GSigmaNeg). -- 3. BSB22 commitment challenge e_cmt = expand_message_xmd_SHA256 over the -- 96-byte uncompressed commitment with DST "bsb22-commitment", reduced mod r. -- 4. vk_x = K0 + pub*K1 + e_cmt*K2 + commitment. -- 5. Groth16 final: e(A,B) == e(alpha,beta)*e(vk_x,gamma)*e(C,delta). -- Accepts iff the PoK check AND the Groth16 equation both hold. -- | BLS12-381 base-field order p. Used to pick the compressed-point sort bit: -- the ZCash "largest" flag is set iff y > p - y. {-# INLINABLE blsBaseFieldOrder #-} blsBaseFieldOrder :: Integer blsBaseFieldOrder = 4002409555221667393417789825735904156556882819939007885332058136124031650490837864442687629129015664037894272559787 -- | The 16-byte domain-separation tag gnark uses for the commitment challenge -- (@constraint.CommitmentDst@). {-# INLINABLE commitmentDst #-} commitmentDst :: BuiltinByteString commitmentDst = "bsb22-commitment" -- | RFC 9380 expand_message_xmd over SHA-256 with lenInBytes = 48 (ell = 2, so -- exactly three SHA-256 calls). Returns the 48-byte uniform output. -- -- Z_pad = 0x00 * 64 (SHA-256 block size) -- b0 = SHA256(Z_pad | msg | I2OSP(48,2) | 0x00 | DST | I2OSP(len DST,1)) -- b1 = SHA256(b0 | 0x01 | DST | I2OSP(len DST,1)) -- b2 = SHA256((b0 XOR b1) | 0x02 | DST | I2OSP(len DST,1)) -- out = (b1 | b2)[:48] = b1 (32) | b2[:16] {-# INLINABLE expandMsgXmd48 #-} expandMsgXmd48 :: BuiltinByteString -> BuiltinByteString expandMsgXmd48 msg = let oneB = consByteString 1 emptyByteString -- 0x01 twoB = consByteString 2 emptyByteString -- 0x02 z00 = consByteString 0 emptyByteString -- 0x00 -- I2OSP(len DST, 1) = 0x10 (DST is 16 bytes); DST' = DST | 0x10 dstPrime = commitmentDst <> consByteString 16 emptyByteString zPad = integerToByteString BigEndian 64 0 -- 64 zero bytes -- I2OSP(48, 2) = 0x00 0x30 lib = consByteString 0 (consByteString 48 emptyByteString) b0 = sha2_256 (zPad <> msg <> lib <> z00 <> dstPrime) b1 = sha2_256 (b0 <> oneB <> dstPrime) b2 = sha2_256 (xorByteString False b0 b1 <> twoB <> dstPrime) in b1 <> sliceByteString 0 16 b2 {-# INLINABLE groth16VerifyCommitted #-} groth16VerifyCommitted :: VerifyingKey -> Proof -> Scalar -> Bool groth16VerifyCommitted (VerifyingKey vk) (Proof p) (Scalar pubBytes) = let -- verifying-key points (vanilla prefix) alpha = bls12_381_G1_uncompress (sliceByteString 0 48 vk) beta = bls12_381_G2_uncompress (sliceByteString 48 96 vk) gamma = bls12_381_G2_uncompress (sliceByteString 144 96 vk) delta = bls12_381_G2_uncompress (sliceByteString 240 96 vk) ic0 = bls12_381_G1_uncompress (sliceByteString 336 48 vk) ic1 = bls12_381_G1_uncompress (sliceByteString 384 48 vk) -- commitment extras k2 = bls12_381_G1_uncompress (sliceByteString 432 48 vk) ckG = bls12_381_G2_uncompress (sliceByteString 480 96 vk) ckGSN = bls12_381_G2_uncompress (sliceByteString 576 96 vk) -- proof points (vanilla prefix) a = bls12_381_G1_uncompress (sliceByteString 0 48 p) b = bls12_381_G2_uncompress (sliceByteString 48 96 p) c = bls12_381_G1_uncompress (sliceByteString 144 48 p) -- commitment: 96B uncompressed (X48|Y48) at [192:288); PoK at [288:336) cmtUncompressed = sliceByteString 192 96 p xBytes = sliceByteString 192 48 p yBytes = sliceByteString 240 48 p yInt = byteStringToInteger BigEndian yBytes -- ZCash sort bit: 0x20 iff y is the lexicographically-larger root. sortBit = if yInt > (blsBaseFieldOrder - yInt) then 32 else 0 -- X's top 3 bits are 000 (X < p), so OR-ing the 0x80 compression flag -- (and 0x20 sort) is plain addition on byte 0. comp0 = indexByteString xBytes 0 + 128 + sortBit comp = consByteString comp0 (sliceByteString 1 47 xBytes) -- uncompress VALIDATES on-curve + subgroup and gives the pairing point commitment = bls12_381_G1_uncompress comp pok = bls12_381_G1_uncompress (sliceByteString 288 48 p) -- Pedersen PoK: e(commitment, GSigmaNeg) * e(PoK, G) == 1 -- <=> e(PoK, G) == e(-commitment, GSigmaNeg) pokOk = bls12_381_finalVerify (bls12_381_millerLoop pok ckG) (bls12_381_millerLoop (bls12_381_G1_neg commitment) ckGSN) -- BSB22 commitment challenge e_cmt (mod r) eCmt = byteStringToInteger BigEndian (expandMsgXmd48 cmtUncompressed) `modInteger` blsScalarFieldOrder -- public input: LE digest reduced into Fr pub = byteStringToInteger LittleEndian pubBytes `modInteger` blsScalarFieldOrder -- vk_x = K0 + pub*K1 + e_cmt*K2 + commitment vkX = ic0 `bls12_381_G1_add` (pub `bls12_381_G1_scalarMul` ic1) `bls12_381_G1_add` (eCmt `bls12_381_G1_scalarMul` k2) `bls12_381_G1_add` commitment -- Groth16: e(A,B) == e(alpha,beta)*e(vk_x,gamma)*e(C,delta) lhs = bls12_381_millerLoop a b rhs = bls12_381_millerLoop alpha beta `bls12_381_mulMlResult` bls12_381_millerLoop vkX gamma `bls12_381_mulMlResult` bls12_381_millerLoop c delta mainOk = bls12_381_finalVerify lhs rhs in pokOk && mainOk