From 60b2c8319ac28f43be66faf32f5d93e870da0e0f Mon Sep 17 00:00:00 2001 From: Marios Georgiou Date: Tue, 28 Jan 2025 18:03:44 -0500 Subject: [PATCH 1/5] Create OptimizedSpecification.cry file and import all functions from Specification.cry We also edit ML_DSA.cry to point to the optimized file. We avoid importing private functions or properties as these have already been tested. Looking forward, we will optimize some of these functions and will define equivalence properties. --- .../Asymmetric/Signature/ML_DSA/ML_DSA.cry | 4 +- .../ML_DSA/OptimizedSpecification.cry | 152 ++++++++++++++++++ 2 files changed, 154 insertions(+), 2 deletions(-) create mode 100644 Primitive/Asymmetric/Signature/ML_DSA/OptimizedSpecification.cry diff --git a/Primitive/Asymmetric/Signature/ML_DSA/ML_DSA.cry b/Primitive/Asymmetric/Signature/ML_DSA/ML_DSA.cry index 91dca073..0a13dcc7 100644 --- a/Primitive/Asymmetric/Signature/ML_DSA/ML_DSA.cry +++ b/Primitive/Asymmetric/Signature/ML_DSA/ML_DSA.cry @@ -36,7 +36,7 @@ module Primitive::Asymmetric::Signature::ML_DSA::ML_DSA where import interface Primitive::Asymmetric::Signature::ML_DSA::Parameters as P -import Primitive::Asymmetric::Signature::ML_DSA::Specification { interface P } +import Primitive::Asymmetric::Signature::ML_DSA::OptimizedSpecification { interface P } /** * Generate a public-private key pair. @@ -98,7 +98,7 @@ Verify pk M sigma ctx // We expose the internal functions for testing purposes only. submodule TestAPI where - import Primitive::Asymmetric::Signature::ML_DSA::Specification { interface P } as Spec + import Primitive::Asymmetric::Signature::ML_DSA::OptimizedSpecification { interface P } as Spec KeyGen_internal = Spec::KeyGen_internal Sign_internal = Spec::Sign_internal diff --git a/Primitive/Asymmetric/Signature/ML_DSA/OptimizedSpecification.cry b/Primitive/Asymmetric/Signature/ML_DSA/OptimizedSpecification.cry new file mode 100644 index 00000000..2269dbda --- /dev/null +++ b/Primitive/Asymmetric/Signature/ML_DSA/OptimizedSpecification.cry @@ -0,0 +1,152 @@ +/** + * Optimized implementation of the ML-DSA (CRYSTALS-Dilithium) signature scheme. + * + * This implementation deviates from the specification in favor of performance. + * + * @copyright Galois Inc + * @author Marios Georgiou + */ +module Primitive::Asymmetric::Signature::ML_DSA::OptimizedSpecification where + +import interface Primitive::Asymmetric::Signature::ML_DSA::Parameters as P +import Primitive::Asymmetric::Signature::ML_DSA::Specification { interface P } as Spec + +type q = P::q +type ω = P::ω +type k = P::k +type ell = P::ell +type η = P::η +type λ = P::λ +type γ1 = P::γ1 +type γ2 = P::γ2 + +type Byte = Spec::Byte + +type Tq = Spec::Tq +type R = Spec::R +type R2 = Spec::R2 +type Rq = Spec::Rq + +modPlusMinus : {α} (fin α) => Z q -> Integer +modPlusMinus = Spec::modPlusMinus`{α} + +infNormRq = Spec::infNormRq + +infNormR = Spec::infNormR + +castToRq = Spec::castToRq + +NTT_Vec = Spec::NTT_Vec + +NTTInv_Vec = Spec::NTTInv_Vec + +H = Spec::H + +HBits = Spec::HBits + +G = Spec::G + +ζ = Spec::ζ + +type d = Spec::d + +β = Spec::β + +type PublicKey = Spec::PublicKey + +type PrivateKey = Spec::PrivateKey + +type Signature = Spec::Signature + +KeyGen_internal = Spec::KeyGen_internal + +Sign_internal = Spec::Sign_internal + +Verify_internal = Spec::Verify_internal + +IntegerToBits : {α} (fin α, α > 0) => Integer -> [α] +IntegerToBits = Spec::IntegerToBits + +BitsToInteger = Spec::BitsToInteger + +IntegerToBytes : {α} (fin α, α > 0) => Integer -> [α]Byte +IntegerToBytes = Spec::IntegerToBytes + +BitsToBytes : {α} (fin α) => [α]Bit -> [α /^ 8]Byte +BitsToBytes = Spec::BitsToBytes + +BytesToBits : {α} (fin α) => [α]Byte -> [8 * α]Bit +BytesToBits = Spec::BytesToBits + +B2B2BInverts = Spec::B2B2BInverts + +CoeffFromThreeBytes = Spec::CoeffFromThreeBytes + +CoeffFromHalfByte = Spec::CoeffFromHalfByte + +SimpleBitPack : {b} (fin b, width b > 0) => R -> [32 * width b]Byte +SimpleBitPack x = Spec::SimpleBitPack`{b} x + +BitPack : {a, b} (fin a, fin b, width (a + b) > 0) => + R -> [32 * width (a + b)]Byte +BitPack w = Spec::BitPack`{a, b} w + +SimpleBitUnpack = Spec::SimpleBitUnpack + +BitUnpack = Spec::BitUnpack + +HintBitPack = Spec::HintBitPack + +HintBitUnpack = Spec::HintBitUnpack + +pkEncode = Spec::pkEncode + +pkDecode = Spec::pkDecode + +skEncode = Spec::skEncode + +skDecode = Spec::skDecode + +sigEncode = Spec::sigEncode + +sigDecode = Spec::sigDecode + +w1Encode = Spec::w1Encode + +SampleInBall = Spec::SampleInBall + +RejNTTPoly = Spec::RejNTTPoly + +RejBoundedPoly = Spec::RejBoundedPoly + +ExpandA = Spec::ExpandA + +ExpandS = Spec::ExpandS + +ExpandMask = Spec::ExpandMask + +Power2Round = Spec::Power2Round + +Decompose = Spec::Decompose + +HighBits = Spec::HighBits + +LowBits = Spec::LowBits + +MakeHint = Spec::MakeHint + +UseHint = Spec::UseHint + +NTT = Spec::NTT + +NTTInv = Spec::NTTInv + +AddNTT = Spec::AddNTT + +MultiplyNTT = Spec::MultiplyNTT + +AddVectorNTT = Spec::AddVectorNTT + +ScalarVectorNTT = Spec::ScalarVectorNTT + +MatrixVectorNTT = Spec::MatrixVectorNTT From 98255762079f8189e6a0003cce74ae2e8d99ff9b Mon Sep 17 00:00:00 2001 From: Marios Georgiou Date: Tue, 28 Jan 2025 18:19:02 -0500 Subject: [PATCH 2/5] Implement first level optimizations. In particular, we optimize `IntegerToBits`, `BitsToInteger`, `IntegerToBytes`, `BitsToBytes` and `BytesToBits`. We also add equivalence properties. The updated functions are around 10x faster. --- .../ML_DSA/OptimizedSpecification.cry | 25 +++++++++++++++---- 1 file changed, 20 insertions(+), 5 deletions(-) diff --git a/Primitive/Asymmetric/Signature/ML_DSA/OptimizedSpecification.cry b/Primitive/Asymmetric/Signature/ML_DSA/OptimizedSpecification.cry index 2269dbda..a4a19a5f 100644 --- a/Primitive/Asymmetric/Signature/ML_DSA/OptimizedSpecification.cry +++ b/Primitive/Asymmetric/Signature/ML_DSA/OptimizedSpecification.cry @@ -65,18 +65,33 @@ Sign_internal = Spec::Sign_internal Verify_internal = Spec::Verify_internal IntegerToBits : {α} (fin α, α > 0) => Integer -> [α] -IntegerToBits = Spec::IntegerToBits +IntegerToBits x = reverse (fromInteger x) -BitsToInteger = Spec::BitsToInteger +IntegerToBitsEquivalence : {α} (fin α, α > 0) => Integer -> Bit +property IntegerToBitsEquivalence x = Spec::IntegerToBits`{α} x == IntegerToBits`{α} x + +BitsToInteger y = toInteger (reverse y) + +BitsToIntegerEquivalence : {α} (fin α, α > 0) => [α] -> Bit +property BitsToIntegerEquivalence x = Spec::BitsToInteger x == BitsToInteger x IntegerToBytes : {α} (fin α, α > 0) => Integer -> [α]Byte -IntegerToBytes = Spec::IntegerToBytes +IntegerToBytes x = reverse (split (fromInteger x)) + +IntegerToBytesEquivalence : {α} (fin α, α > 0) => Integer -> Bit +property IntegerToBytesEquivalence x = Spec::IntegerToBytes`{α} x == IntegerToBytes`{α} x BitsToBytes : {α} (fin α) => [α]Bit -> [α /^ 8]Byte -BitsToBytes = Spec::BitsToBytes +BitsToBytes y = map reverse (split (y # zero)) + +BitsToBytesEquivalence : {α} (fin α) => [α]Bit -> Bit +property BitsToBytesEquivalence x = Spec::BitsToBytes x == BitsToBytes x BytesToBits : {α} (fin α) => [α]Byte -> [8 * α]Bit -BytesToBits = Spec::BytesToBits +BytesToBits z = join (map reverse z) + +BytesToBitsEquivalence : {α} (fin α) => [α]Byte -> Bit +property BytesToBitsEquivalence x = Spec::BytesToBits x == BytesToBits x B2B2BInverts = Spec::B2B2BInverts From 5685782a6215b59fc88e1444167205a9c890815c Mon Sep 17 00:00:00 2001 From: Marios Georgiou Date: Tue, 28 Jan 2025 18:31:00 -0500 Subject: [PATCH 3/5] Implement optimized versions of functions at the second dependency level The functions we optimize are: `SimpleBitPack`, `BitPack`, `SimpleBitUnpack` and `BitUnpack`. These functions are now 10x faster than in the specs. We also implement and check equivalence properties. --- .../ML_DSA/OptimizedSpecification.cry | 23 +++++++++++++++---- 1 file changed, 19 insertions(+), 4 deletions(-) diff --git a/Primitive/Asymmetric/Signature/ML_DSA/OptimizedSpecification.cry b/Primitive/Asymmetric/Signature/ML_DSA/OptimizedSpecification.cry index a4a19a5f..d2c5e07a 100644 --- a/Primitive/Asymmetric/Signature/ML_DSA/OptimizedSpecification.cry +++ b/Primitive/Asymmetric/Signature/ML_DSA/OptimizedSpecification.cry @@ -100,15 +100,30 @@ CoeffFromThreeBytes = Spec::CoeffFromThreeBytes CoeffFromHalfByte = Spec::CoeffFromHalfByte SimpleBitPack : {b} (fin b, width b > 0) => R -> [32 * width b]Byte -SimpleBitPack x = Spec::SimpleBitPack`{b} x +SimpleBitPack w = BitsToBytes (join (map IntegerToBits`{width b} w)) + +SimpleBitPackEquivalence : {b} (fin b, width b > 0) => R -> Bit +property SimpleBitPackEquivalence w = Spec::SimpleBitPack`{b} w == SimpleBitPack`{b} w BitPack : {a, b} (fin a, fin b, width (a + b) > 0) => R -> [32 * width (a + b)]Byte -BitPack w = Spec::BitPack`{a, b} w +BitPack w = BitsToBytes (join (map (\x -> IntegerToBits`{width (a + b)} (`b - x)) w)) + +BitPackEquivalence : {a, b} (fin a, fin b, width (a + b) > 0) => R -> Bit +property BitPackEquivalence w = Spec::BitPack`{a, b} w == BitPack`{a, b} w + +SimpleBitUnpack : {b} (fin b, width b > 0) => [32 * width b]Byte -> R +SimpleBitUnpack v = map BitsToInteger (split (BytesToBits v)) + +SimpleBitUnpackEquivalence : {b} (fin b, width b > 0) => [32 * width b]Byte -> Bit +property SimpleBitUnpackEquivalence v = Spec::SimpleBitUnpack`{b} v == SimpleBitUnpack`{b} v -SimpleBitUnpack = Spec::SimpleBitUnpack +BitUnpack : {a, b} (fin a, fin b, width (a + b) > 0) => + [32 * width (a + b)]Byte -> R +BitUnpack v = map (\x -> `b - BitsToInteger x) (split (BytesToBits v)) -BitUnpack = Spec::BitUnpack +BitUnpackEquivalence : {a, b} (fin a, fin b, width (a + b) > 0) => [32 * width (a + b)]Byte -> Bit +property BitUnpackEquivalence v = Spec::BitUnpack`{a, b} v == BitUnpack`{a, b} v HintBitPack = Spec::HintBitPack From 29ca144f2d54713cd096496a25eda75adcff8b38 Mon Sep 17 00:00:00 2001 From: Marios Georgiou Date: Tue, 28 Jan 2025 19:03:07 -0500 Subject: [PATCH 4/5] Implement optimized versions of functions at the third level These definitions are copied and pasted directly from the Specification.cry file. Only tiny edits in the some type parameters are made and are explicitly mentioned in the doc comments. The edited functions are: `KeyGen_internal`, `pkEncode`, `pkDecode`, `skEncode`, `skDecode`, `sigEncode`, `sigDecode`, `w1Encode`, `SampleInBall`, `ExpandA`, `ExpandS` and `ExpandMask` --- .../ML_DSA/OptimizedSpecification.cry | 237 +++++++++++++++++- 1 file changed, 225 insertions(+), 12 deletions(-) diff --git a/Primitive/Asymmetric/Signature/ML_DSA/OptimizedSpecification.cry b/Primitive/Asymmetric/Signature/ML_DSA/OptimizedSpecification.cry index d2c5e07a..a812f92c 100644 --- a/Primitive/Asymmetric/Signature/ML_DSA/OptimizedSpecification.cry +++ b/Primitive/Asymmetric/Signature/ML_DSA/OptimizedSpecification.cry @@ -19,6 +19,7 @@ type η = P::η type λ = P::λ type γ1 = P::γ1 type γ2 = P::γ2 +type τ = P::τ type Byte = Spec::Byte @@ -58,7 +59,39 @@ type PrivateKey = Spec::PrivateKey type Signature = Spec::Signature -KeyGen_internal = Spec::KeyGen_internal +/** + * This is almost identical to `Spec`; it's duplicated to pull in the optimized + * dependencies in this file but H`{64} is replaced by H to avoid compilation + * errors. + */ +KeyGen_internal : [32]Byte -> (PublicKey, PrivateKey) +KeyGen_internal ξ = (pk, sk) where + // Step 1. + (ρ # ρ' # K) = H (ξ # IntegerToBytes`{1} `k # IntegerToBytes`{1} `ell) + + // Step 3. + A_hat = ExpandA ρ + // Step 4. + (s1, s2) = ExpandS ρ' + + // Explicitly typecast vectors in `R` to `Rq`. + s1' = castToRq s1 + s2' = castToRq s2 + + // Step 5. + t = NTTInv_Vec (A_hat ∘∘ NTT_Vec s1') + s2' + // Step 6. + (t1, t0) = Power2Round t + + // Step 8. + pk = pkEncode ρ t1 + // Step 9. + tr = H pk + // Step 10. + sk = skEncode ρ K tr s1 s2 t0 + +KeyGen_internalEquivalence : [32]Byte -> Bit +property KeyGen_internalEquivalence ξ = Spec::KeyGen_internal ξ == KeyGen_internal ξ Sign_internal = Spec::Sign_internal @@ -129,31 +162,208 @@ HintBitPack = Spec::HintBitPack HintBitUnpack = Spec::HintBitUnpack -pkEncode = Spec::pkEncode +/** + * This is unchanged from `Spec`; it's duplicated to pull in the optimized + * dependencies in this file. + */ +pkEncode : [32]Byte -> [k]R -> PublicKey +pkEncode ρ t1 = pk where + pk = ρ # join [SimpleBitPack`{2 ^^ (width (q - 1) - d) - 1} (t1@i) | i <- [0..k-1]] -pkDecode = Spec::pkDecode +pkEncodeEquivalence : [32]Byte -> [k]R -> Bit +property pkEncodeEquivalence ρ t1 = Spec::pkEncode ρ t1 == pkEncode ρ t1 -skEncode = Spec::skEncode +/** + * This is unchanged from `Spec`; it's duplicated to pull in the optimized + * dependencies in this file. + */ +pkDecode : PublicKey -> ([32]Byte, [k]R) +pkDecode pk = (ρ, t1) where + // Step 1. We split off the single `ρ` byte, then separate the remaining + // bytes into the `k` components as described. + (ρ # zBytes) = pk + z = split zBytes + // Steps 2 - 4. + t1 = [SimpleBitUnpack`{2 ^^ (width (q - 1) - d) - 1} (z@i) | i <- [0..k-1]] + +pkDecodeEquivalence : PublicKey -> Bit +property pkDecodeEquivalence pk = Spec::pkDecode pk == pkDecode pk -skDecode = Spec::skDecode +/** + * This is unchanged from `Spec`; it's duplicated to pull in the optimized + * dependencies in this file. + */ +skEncode : [32]Byte -> [32]Byte -> [64]Byte -> [ell]R -> [k]R -> [k]R + -> PrivateKey +skEncode ρ K tr s1 s2 t0 = sk9 where + // Note: `sk#` indicates the value of `sk` at Step `#`. + // Step 1. + sk1 = ρ # K # tr + // Steps 2 - 4. + sk3 = sk1 # join [BitPack`{η, η} (s1@i) | i <- [0..ell-1]] + // Steps 5 - 7. + sk6 = sk3 # join [BitPack`{η, η} (s2@i) | i <- [0..k-1]] + // Steps 8 - 10. + sk9 = sk6 # + join [BitPack`{2^^(d - 1) - 1, 2^^(d - 1)} (t0@i) | i <- [0..k-1]] + +skEncodeEquivalence : [32]Byte -> [32]Byte -> [64]Byte -> [ell]R -> [k]R -> [k]R -> Bit +property skEncodeEquivalence ρ K tr s1 s2 t0 = Spec::skEncode ρ K tr s1 s2 t0 == skEncode ρ K tr s1 s2 t0 -sigEncode = Spec::sigEncode +/** + * This is unchanged from `Spec`; it's duplicated to pull in the optimized + * dependencies in this file. + */ +skDecode : PrivateKey -> ([32]Byte, [32]Byte, [64]Byte, [ell]R, [k]R, [k]R) +skDecode sk = (ρ, K, tr, s1, s2, t0) where + // Step 1. We split off the six components, then further separate `y`, `z`, + // and `w` into their two dimensions. + (ρ # K # tr # yBytes # zBytes # wBytes) = sk + y = split`{ell} yBytes + z = split`{k} zBytes + w = split`{k} wBytes + + // Steps 2 - 4. + s1 = [BitUnpack`{η, η} (y@i) | i <- [0..ell-1]] + // Steps 5 - 7. + s2 = [BitUnpack`{η, η} (z@i) | i <- [0..k-1]] + // Steps 8 - 10. + t0 = [BitUnpack`{2^^(d - 1) - 1, 2^^(d - 1)} (w@i) | i <- [0..k-1]] + +skDecodeEquivalence : PrivateKey -> Bit +property skDecodeEquivalence sk = Spec::skDecode sk == skDecode sk -sigDecode = Spec::sigDecode +/** + * This is unchanged from `Spec`; it's duplicated to pull in the optimized + * dependencies in this file. + */ +sigEncode : [λ / 4]Byte -> [ell]R -> [k]R2 -> Signature +sigEncode c_til z h = σ where + // Note that `σ#` indicates the value of `σ` at Step `#`. + // Step 1. + σ1 = c_til + // Step 2 - 4. + σ3 = σ1 # join [BitPack`{γ1 - 1, γ1} (z@i) | i <- [0..ell-1]] + // Step 5. + σ = σ3 # HintBitPack h -w1Encode = Spec::w1Encode +/** + * This is unchanged from `Spec`; it's duplicated to pull in the optimized + * dependencies in this file. + */ +sigDecode : Signature -> ([λ / 4]Byte, [ell]R, Option ([k]R2)) +sigDecode σ = (c_til, z, h) where + // Step 1. We separate into bytes, then further split `x` into its two + // dimensions. + (c_til # xBytes # y) = σ + x = split`{ell} xBytes + + // Step 2 - 4. + z = [BitUnpack`{γ1 - 1, γ1} (x@i) | i <- [0..ell-1]] + // Step 5. + h = HintBitUnpack y -SampleInBall = Spec::SampleInBall +/** + * This is unchanged from `Spec`; it's duplicated to pull in the optimized + * dependencies in this file. + */ +w1Encode : [k]R -> [32 * k * width ((q - 1) / (2 * γ2) - 1)]Byte +w1Encode w1 = w1_til where + w1_til = join + [SimpleBitPack`{(q - 1) / (2 * γ2) - 1} (w1@i) | i <- [0..k-1]] + +w1EncodeEquivalence : [k]R -> Bit +property w1EncodeEquivalence w1 = Spec::w1Encode w1 == w1Encode w1 + +/** + * This is almost identical to `Spec`; it's duplicated to pull in the optimized + * dependencies in this file but H`{inf} is replaced by H to avoid compilation + * errors. + */ +SampleInBall : [λ / 4]Byte -> R +SampleInBall ρ = cFinal where + // Step 1. + c0 = zero + // Steps 2 - 3. + ctx_0 = H ρ + // Step 4. + ((s : [8]Byte) # ctx_1) = ctx_0 + // Step 5. + h = BytesToBits s + + // Steps 7 - 10. Uses recursion instead of a loop to sample bytes from the + // hash stream, returning the first one that's in the range `[0, i]`. + sample : [inf]Byte -> Byte -> (Byte, [inf]Byte) + sample ([j] # ctx) i = + if j > i then + sample ctx i + else (j, ctx) + + // Steps 6 - 13. Computes the value of `c` and the updated `ctx` at each + // iteration of the loop. + cAndCtx = [(c0, ctx_1)] # [(c'', ctx') where + // Steps 7 - 10. + (j, ctx') = sample ctx (fromInteger i) + // Step 11. + c' = update c i (c@j) + // Step 12. In Cryptol, we need to manually convert the exponent + // from a `Bit` to a numeric type. + hiτ = if (h @ (i + `τ - 256)) then 1 else 0 : Integer + c'' = update c' j ((-1)^^hiτ) + + | i <- [256 - τ..255] + | (c, ctx) <- cAndCtx] + + (cFinal, _) = cAndCtx ! 0 + +SampleInBallEquivalence : [λ / 4]Byte -> Bit +property SampleInBallEquivalence ρ = Spec::SampleInBall ρ == SampleInBall ρ RejNTTPoly = Spec::RejNTTPoly RejBoundedPoly = Spec::RejBoundedPoly -ExpandA = Spec::ExpandA +/** + * This is unchanged from `Spec`; it's duplicated to pull in the optimized + * dependencies in this file. + */ +ExpandA : [32]Byte -> [k][ell]Tq +ExpandA ρ = A_hat where + A_hat = [[RejNTTPoly ρ' where + ρ' = ρ # IntegerToBytes`{1} s # IntegerToBytes`{1} r + | s <- [0..ell - 1]] + | r <- [0..k - 1]] -ExpandS = Spec::ExpandS +ExpandAEquivalence : [32]Byte -> Bit +property ExpandAEquivalence ρ = Spec::ExpandA ρ == ExpandA ρ -ExpandMask = Spec::ExpandMask +/** + * This is unchanged from `Spec`; it's duplicated to pull in the optimized + * dependencies in this file. + */ +ExpandS : [64]Byte -> ([ell]R, [k]R) +ExpandS ρ = (s1, s2) where + s1 = [RejBoundedPoly (ρ # IntegerToBytes`{2} r) | r <- [0..ell-1]] + s2 = [RejBoundedPoly (ρ # IntegerToBytes`{2} (r + `ell)) | r <- [0..k-1]] + +ExpandSEquivalence : [64]Byte -> Bit +property ExpandSEquivalence ρ = Spec::ExpandS ρ == ExpandS ρ + +/** + * This is almost identical to `Spec`; it's duplicated to pull in the optimized + * dependencies in this file but H`{32 * c} is replaced by H to avoid compilation + * errors. Moreover, the type of `c` is not used so it's removed. + */ +ExpandMask : [64]Byte -> Integer -> [ell]R +ExpandMask ρ μ = y where + + y = [BitUnpack`{γ1 - 1, γ1} v where + ρ' = ρ # IntegerToBytes`{2} (μ + r) + v = H ρ' + | r <- [0..ell - 1]] + +ExpandMaskEquivalence : [64]Byte -> Integer -> Bit +property ExpandMaskEquivalence ρ μ = Spec::ExpandMask ρ μ == ExpandMask ρ μ Power2Round = Spec::Power2Round @@ -180,3 +390,6 @@ AddVectorNTT = Spec::AddVectorNTT ScalarVectorNTT = Spec::ScalarVectorNTT MatrixVectorNTT = Spec::MatrixVectorNTT + +(∘∘) : [k][ell]Tq -> [ell]Tq -> [k]Tq +(∘∘) M v = [sum [Mij * vj | Mij <- Mi | vj <- v] | Mi <- M] From fd3c350d7c16f308ffcf00db3b7b4665b90623dd Mon Sep 17 00:00:00 2001 From: Marios Georgiou Date: Fri, 31 Jan 2025 18:00:26 -0500 Subject: [PATCH 5/5] Add doc comments to all the properties to indicate whether they can prove in a reasonable amount of time or if checking is better --- .../ML_DSA/OptimizedSpecification.cry | 103 ++++++++++++++++++ 1 file changed, 103 insertions(+) diff --git a/Primitive/Asymmetric/Signature/ML_DSA/OptimizedSpecification.cry b/Primitive/Asymmetric/Signature/ML_DSA/OptimizedSpecification.cry index a812f92c..32f14fcf 100644 --- a/Primitive/Asymmetric/Signature/ML_DSA/OptimizedSpecification.cry +++ b/Primitive/Asymmetric/Signature/ML_DSA/OptimizedSpecification.cry @@ -90,6 +90,12 @@ KeyGen_internal ξ = (pk, sk) where // Step 10. sk = skEncode ρ K tr s1 s2 t0 +/** + * ```repl + * :set tests=3 + * :check KeyGen_internalEquivalence + * ``` + */ KeyGen_internalEquivalence : [32]Byte -> Bit property KeyGen_internalEquivalence ξ = Spec::KeyGen_internal ξ == KeyGen_internal ξ @@ -100,29 +106,57 @@ Verify_internal = Spec::Verify_internal IntegerToBits : {α} (fin α, α > 0) => Integer -> [α] IntegerToBits x = reverse (fromInteger x) +/** + * ```repl + * :check IntegerToBitsEquivalence`{44} + * ``` + */ IntegerToBitsEquivalence : {α} (fin α, α > 0) => Integer -> Bit property IntegerToBitsEquivalence x = Spec::IntegerToBits`{α} x == IntegerToBits`{α} x BitsToInteger y = toInteger (reverse y) +/** + * ```repl + * :check BitsToIntegerEquivalence`{44} + * :exhaust BitsToIntegerEquivalence`{10} + * ``` + */ BitsToIntegerEquivalence : {α} (fin α, α > 0) => [α] -> Bit property BitsToIntegerEquivalence x = Spec::BitsToInteger x == BitsToInteger x IntegerToBytes : {α} (fin α, α > 0) => Integer -> [α]Byte IntegerToBytes x = reverse (split (fromInteger x)) +/** + * ```repl + * :check IntegerToBytesEquivalence`{44} + * ``` + */ IntegerToBytesEquivalence : {α} (fin α, α > 0) => Integer -> Bit property IntegerToBytesEquivalence x = Spec::IntegerToBytes`{α} x == IntegerToBytes`{α} x BitsToBytes : {α} (fin α) => [α]Bit -> [α /^ 8]Byte BitsToBytes y = map reverse (split (y # zero)) +/** + * ```repl + * :prove BitsToBytesEquivalence`{320 * 8} + * :prove BitsToBytesEquivalence`{32 * 44 * 8} + * ``` + */ BitsToBytesEquivalence : {α} (fin α) => [α]Bit -> Bit property BitsToBytesEquivalence x = Spec::BitsToBytes x == BitsToBytes x BytesToBits : {α} (fin α) => [α]Byte -> [8 * α]Bit BytesToBits z = join (map reverse z) +/** + * ```repl + * :prove BytesToBitsEquivalence`{320} + * :prove BytesToBitsEquivalence`{32 * 44} + * ``` + */ BytesToBitsEquivalence : {α} (fin α) => [α]Byte -> Bit property BytesToBitsEquivalence x = Spec::BytesToBits x == BytesToBits x @@ -135,6 +169,11 @@ CoeffFromHalfByte = Spec::CoeffFromHalfByte SimpleBitPack : {b} (fin b, width b > 0) => R -> [32 * width b]Byte SimpleBitPack w = BitsToBytes (join (map IntegerToBits`{width b} w)) +/** + * ```repl + * :check SimpleBitPackEquivalence`{10} + * ``` + */ SimpleBitPackEquivalence : {b} (fin b, width b > 0) => R -> Bit property SimpleBitPackEquivalence w = Spec::SimpleBitPack`{b} w == SimpleBitPack`{b} w @@ -142,12 +181,22 @@ BitPack : {a, b} (fin a, fin b, width (a + b) > 0) => R -> [32 * width (a + b)]Byte BitPack w = BitsToBytes (join (map (\x -> IntegerToBits`{width (a + b)} (`b - x)) w)) +/** + * ```repl + * :check BitPackEquivalence`{10, 10} + * ``` + */ BitPackEquivalence : {a, b} (fin a, fin b, width (a + b) > 0) => R -> Bit property BitPackEquivalence w = Spec::BitPack`{a, b} w == BitPack`{a, b} w SimpleBitUnpack : {b} (fin b, width b > 0) => [32 * width b]Byte -> R SimpleBitUnpack v = map BitsToInteger (split (BytesToBits v)) +/** + * ```repl + * :check SimpleBitUnpackEquivalence`{10} + * ``` + */ SimpleBitUnpackEquivalence : {b} (fin b, width b > 0) => [32 * width b]Byte -> Bit property SimpleBitUnpackEquivalence v = Spec::SimpleBitUnpack`{b} v == SimpleBitUnpack`{b} v @@ -155,6 +204,11 @@ BitUnpack : {a, b} (fin a, fin b, width (a + b) > 0) => [32 * width (a + b)]Byte -> R BitUnpack v = map (\x -> `b - BitsToInteger x) (split (BytesToBits v)) +/** + * ```repl + * :check BitUnpackEquivalence`{10, 10} + * ``` + */ BitUnpackEquivalence : {a, b} (fin a, fin b, width (a + b) > 0) => [32 * width (a + b)]Byte -> Bit property BitUnpackEquivalence v = Spec::BitUnpack`{a, b} v == BitUnpack`{a, b} v @@ -170,6 +224,11 @@ pkEncode : [32]Byte -> [k]R -> PublicKey pkEncode ρ t1 = pk where pk = ρ # join [SimpleBitPack`{2 ^^ (width (q - 1) - d) - 1} (t1@i) | i <- [0..k-1]] +/** + * ```repl + * :check pkEncodeEquivalence + * ``` + */ pkEncodeEquivalence : [32]Byte -> [k]R -> Bit property pkEncodeEquivalence ρ t1 = Spec::pkEncode ρ t1 == pkEncode ρ t1 @@ -186,6 +245,11 @@ pkDecode pk = (ρ, t1) where // Steps 2 - 4. t1 = [SimpleBitUnpack`{2 ^^ (width (q - 1) - d) - 1} (z@i) | i <- [0..k-1]] +/** + * ```repl + * :check pkDecodeEquivalence + * ``` + */ pkDecodeEquivalence : PublicKey -> Bit property pkDecodeEquivalence pk = Spec::pkDecode pk == pkDecode pk @@ -207,6 +271,11 @@ skEncode ρ K tr s1 s2 t0 = sk9 where sk9 = sk6 # join [BitPack`{2^^(d - 1) - 1, 2^^(d - 1)} (t0@i) | i <- [0..k-1]] +/** + * ```repl + * :check skEncodeEquivalence + * ``` + */ skEncodeEquivalence : [32]Byte -> [32]Byte -> [64]Byte -> [ell]R -> [k]R -> [k]R -> Bit property skEncodeEquivalence ρ K tr s1 s2 t0 = Spec::skEncode ρ K tr s1 s2 t0 == skEncode ρ K tr s1 s2 t0 @@ -230,6 +299,11 @@ skDecode sk = (ρ, K, tr, s1, s2, t0) where // Steps 8 - 10. t0 = [BitUnpack`{2^^(d - 1) - 1, 2^^(d - 1)} (w@i) | i <- [0..k-1]] +/** + * ```repl + * :check skDecodeEquivalence + * ``` + */ skDecodeEquivalence : PrivateKey -> Bit property skDecodeEquivalence sk = Spec::skDecode sk == skDecode sk @@ -272,6 +346,11 @@ w1Encode w1 = w1_til where w1_til = join [SimpleBitPack`{(q - 1) / (2 * γ2) - 1} (w1@i) | i <- [0..k-1]] +/** + * ```repl + * :check w1EncodeEquivalence + * ``` + */ w1EncodeEquivalence : [k]R -> Bit property w1EncodeEquivalence w1 = Spec::w1Encode w1 == w1Encode w1 @@ -316,6 +395,12 @@ SampleInBall ρ = cFinal where (cFinal, _) = cAndCtx ! 0 +/** + * ```repl + * :set tests=3 + * :check SampleInBallEquivalence + * ``` + */ SampleInBallEquivalence : [λ / 4]Byte -> Bit property SampleInBallEquivalence ρ = Spec::SampleInBall ρ == SampleInBall ρ @@ -334,6 +419,12 @@ ExpandA ρ = A_hat where | s <- [0..ell - 1]] | r <- [0..k - 1]] +/** + * ```repl + * :set tests=3 + * :check ExpandAEquivalence + * ``` + */ ExpandAEquivalence : [32]Byte -> Bit property ExpandAEquivalence ρ = Spec::ExpandA ρ == ExpandA ρ @@ -346,6 +437,12 @@ ExpandS ρ = (s1, s2) where s1 = [RejBoundedPoly (ρ # IntegerToBytes`{2} r) | r <- [0..ell-1]] s2 = [RejBoundedPoly (ρ # IntegerToBytes`{2} (r + `ell)) | r <- [0..k-1]] +/** + * ```repl + * :set tests=5 + * :check ExpandSEquivalence + * ``` + */ ExpandSEquivalence : [64]Byte -> Bit property ExpandSEquivalence ρ = Spec::ExpandS ρ == ExpandS ρ @@ -362,6 +459,12 @@ ExpandMask ρ μ = y where v = H ρ' | r <- [0..ell - 1]] +/** + * ```repl + * :set tests=5 + * :check ExpandMaskEquivalence + * ``` + */ ExpandMaskEquivalence : [64]Byte -> Integer -> Bit property ExpandMaskEquivalence ρ μ = Spec::ExpandMask ρ μ == ExpandMask ρ μ