Poly.lean
Declarations on this page (92)
- inductive PolyPanic
- def toSpqrPanic
- inductive PolynomialError
- inductive EncodingError
- def CHUNK_SIZE
- def NUM_POLYS
- def USIZE_MAX
- structure Chunk
- def u16ToBeBytes
- def u16FromBeBytes
- structure Pt
- def serialize
- def deserialize
- def cmp
- structure SortedSetPt
- def new
- def withCapacity
- def len
- def asSlice
- def binarySearchAux
- def binarySearch
- def replace
- def push
- structure Poly
- def zero
- def multXdiffAssignTrailingLoop
- def multXdiffAssignTrailing
-
def lagrange
Interpolate Prepare Loop - def lagrangeInterpolatePrepare
- def lagrangeDenominator
- def lagrangeCompleteDivLoop
- def lagrangeInterpolateComplete
- def lagrangeAccumulateCoeffs
- def lagrangeInterpolateLoop
- def lagrangeInterpolate
- def lagrangeInterpolatePt
- def addAssignCoeffs
- def addAssign
- def multAssign
- def computeAtPowersLoop
- def computeAt
- def lagrangeSum
- structure PolyConst
- def mult
- def multXdiff
- def lagrangeInterpolatePtLoop
- def lagrangeInterpolatePt
- def toPoly
- def constPolysToPolys
-
def lagrange
Polys For Complete Points - def COMPLETE_POINTS_POLYS_1
- def COMPLETE_POINTS_POLYS_3
- def COMPLETE_POINTS_POLYS_5
- def COMPLETE_POINTS_POLYS_30
- def COMPLETE_POINTS_POLYS_34
- def COMPLETE_POINTS_POLYS_36
- def checkCompletePoints
- def fromCompletePoints
- def serialize
- def bytesToGF16List
- def deserialize
- structure Point
- inductive EncoderState
- structure ProtoPolynomialEncoder
- structure PolyEncoder
- def intoPb
- def decodePbPoints
- def decodePbPolys
- def fromPb
- def enumeratePts
- def pointsToPolysLoop
- def pointAt
- def distributeMsgChunks
- def encodeBytesBase
- def encodeBytes
- def chunkAtLoop
- def chunkAt
- def nextChunk
- structure ProtoPolynomialDecoder
- structure PolyDecoder
- def necessaryPoints
- def newWithPolyCount
- def new
- def intoPb
- def pushChunksExact4
- def decodeDecoderPbPts
- def fromPb
- def addChunkLoop
- def addChunk
- def collectPointsVecs
- def decodedMessageLoop
- def decodedMessage
SPQR V1: polynomial erasure coding (src/, src/)
Trusted in part. The theorems of Computational/ use only part of this file (see Computational/): the rest (the OptionEncoder / OptionDecoder functions, the run*Guard self-tests, isOkEq / isErrEq / isOkErrEq, PolyConst. and Pt.) is checked by Lean.
Models SPQR's 32-byte chunk erasure code (Chunk) over $\mathrm{GF}(2^{16})$ with explicit panic (PolyPanic) and error (PolynomialError, EncodingError) values:
-
Pt(cmp,eqcomparingxonly) andSortedSetPt(len,replace,push, where pushing an existingxoverwrites the storedPt); -
Poly(zero,lagrangeInterpolate,fromCompletePoints,computeAt) and fixed-lengthPolyConst(PolyConst.) for precomputed complete-point Lagrange bases;wf -
PolyEncoder(encodeBytes,chunkAt,nextChunk,intoPb,fromPbviaProtoPolynomialEncoder) andPolyDecoder(new,addChunk,decodedMessage,intoPb,fromPbviaProtoPolynomialDecoder); -
kernel-checked guard theorems (
pt_serialize_and_ord_guard, …,option_).encoder_ decoder_ guard
@[expose] public sectionnamespace CryptoVerification.LibsignalSpqrV1Panic and Error types
inductive PolyPanic
Rust panic sites in src/ and src/, represented as values.
inductive PolyPanic where
| boundsCheck
| sliceIndexFail
| unwrapFailed
| expectFailed
| addOverflow
| subOverflow
| mulOverflow
| explicitPanic
deriving DecidableEq, Repr, Inhabitednamespace PolyPanicdef toSpqrPanic
def toSpqrPanic : PolyPanic → SpqrPanic
| .boundsCheck => .site "src/encoding/polynomial.rs: slice/vec index bounds_check"
| .sliceIndexFail => .site "src/encoding/polynomial.rs:120,241: slice range slice_index_fail"
| .unwrapFailed => .site "src/encoding.rs:64,84,94 / src/encoding/polynomial.rs:44–45,51: unwrap_failed"
| .expectFailed => .site "src/encoding/polynomial.rs:675,969: expect_failed"
| .addOverflow => .site "src/encoding/polynomial.rs:137,154: usize add_overflow"
| .subOverflow => .site "src/encoding/polynomial.rs:184,221,224,431: usize sub_overflow"
| .mulOverflow => .site "src/encoding/polynomial.rs:946: usize mul_overflow"
| .explicitPanic => .site "src/encoding/polynomial.rs:432: overflow in const mult_xdiff"end PolyPanicinductive PolynomialError
PolynomialError (src/).
inductive PolynomialError where
| messageLengthEven
| messageLengthTooLong
| serializationInvalid
deriving DecidableEq, Repr, Inhabitedinductive EncodingError
EncodingError (src/).
inductive EncodingError where
| polynomialError (e : PolynomialError)
| chunkIndexDecodingError
| chunkDataDecodingError
deriving DecidableEq, Repr, Inhabited
Constants and Chunk (src/, src/)
def CHUNK_SIZE
def CHUNK_SIZE : Nat := 32def NUM_POLYS
Number of $\mathrm{GF}(2^{16})$ polynomials or point sets per message (CHUNK_SIZE / 2 = 16).
def NUM_POLYS : Nat := CHUNK_SIZE / 2def USIZE_MAX
def USIZE_MAX : Nat := (1 <<< 64) - 1structure Chunk
32-byte erasure-coded chunk (src/) with 16-bit chunk index.
structure Chunk where
index : BitVec 16
data : List.Vector (BitVec 8) 32
deriving DecidableEq
Big-endian u16 byte conversion helpers
def u16ToBeBytes
def u16ToBeBytes (v : BitVec 16) : List (BitVec 8) :=
[(v >>> 8).setWidth 8, v.setWidth 8]def u16FromBeBytes
def u16FromBeBytes (b0 b1 : BitVec 8) : BitVec 16 :=
(b0.zeroExtend 16 <<< 8) ||| b1.zeroExtend 16
Pt (src/)
structure Pt
namespace Ptdef serialize
def serialize (self : Pt) : List (BitVec 8) :=
u16ToBeBytes self.x.value ++ u16ToBeBytes self.y.valuedef deserialize
Pt::deserialize (src/); panics with .unwrapFailed unless s..
def deserialize (s : List (BitVec 8)) : Except PolyPanic Pt :=
match s with
| [b0, b1, b2, b3] =>
.ok { x := GF16.new (u16FromBeBytes b0 b1), y := GF16.new (u16FromBeBytes b2 b3) }
| _ => .error .unwrapFaileddef cmp
1 declaration not shown (lines 140–142): theorems, which Lean checks, or definitions that no headline statement uses
CryptoVerification.
end Pt
sorted_vec::SortedSet<Pt> (sorted-vec-0.8.11/)
structure SortedSetPt
structure SortedSetPt where
vec : List Pt
deriving DecidableEq, Repr, Inhabitednamespace SortedSetPtdef new
def new : SortedSetPt :=
{ vec := [] }def withCapacity
def withCapacity (_capacity : Nat) : SortedSetPt :=
{ vec := [] }def len
def len (self : SortedSetPt) : Nat :=
self.vec.lengthdef asSlice
def asSlice (self : SortedSetPt) : List Pt :=
self.vecdef binarySearchAux
def binarySearchAux (target : Pt) : Nat → List Pt → Except Nat Nat
| idx, [] => .error idx
| idx, pt :: rest =>
match Pt.cmp pt target with
| .lt => binarySearchAux target (idx + 1) rest
| .eq => .ok idx
| .gt => .error idxdef binarySearch
slice::binary_search on SortedSet<Pt> by Pt., returning .ok idx on an x-match or .error insertIdx at the insertion position.
def binarySearch (self : SortedSetPt) (target : Pt) : Except Nat Nat :=
binarySearchAux target 0 self.vecdef replace
SortedSet::replace (sorted-vec-0.8.11/): overwrites an existing point with matching x and returns some old, or inserts in x-order and returns none.
def replace (self : SortedSetPt) (element : Pt) : SortedSetPt × Nat × Option Pt :=
match self.binarySearch element with
| .ok existingIndex =>
let old := self.vec[existingIndex]?
({ vec := self.vec.set existingIndex element }, existingIndex, old)
| .error insertIndex =>
let vec' := self.vec.take insertIndex ++ (element :: self.vec.drop insertIndex)
({ vec := vec' }, insertIndex, none)def push
SortedSet::push (sorted-vec-0.8.11/): appends at the back when element., replaces last when element., and delegates to replace when element..
def push (self : SortedSetPt) (element : Pt) : SortedSetPt × Nat × Option Pt :=
match self.vec.getLast? with
| some last =>
match Pt.cmp element last with
| .gt =>
let newVec := self.vec ++ [element]
({ vec := newVec }, newVec.length - 1, none)
| .eq =>
let newVec := self.vec.dropLast ++ [element]
({ vec := newVec }, newVec.length - 1, some last)
| .lt =>
self.replace element
| none =>
({ vec := [element] }, 0, none)end SortedSetPt
Poly (src/)
structure Poly
Polynomial over $\mathrm{GF}(2^{16})$ with coefficients in ascending degree order (coefficients[k] is the coefficient of $x^k$).
structure Poly where
coefficients : List GF16
deriving DecidableEq, Repr, Inhabitednamespace Polydef zero
def zero (_capacity : Nat := 0) : Poly :=
{ coefficients := [] }def multXdiffAssignTrailingLoop
def multXdiffAssignTrailingLoop (difference : GF16) : Nat → Nat → List GF16 → Except PolyPanic (List GF16)
| _, 0, coeffs => .ok coeffs
| i, rem + 1, coeffs =>
if i == 0 then
.error .subOverflow
else
match coeffs[i]?, coeffs[i - 1]? with
| some ci, some ciPrev =>
let delta := GF16.mul ci difference
let coeffs' := coeffs.set (i - 1) (GF16.sub ciPrev delta)
multXdiffAssignTrailingLoop difference (i + 1) rem coeffs'
| _, _ => .error .boundsCheckdef multXdiffAssignTrailing
Poly::mult_xdiff_assign_trailing (src/): multiplies self[start..] by $(x - \mathrm{difference})$, propagating carry into self[start - 1] (.subOverflow if start == 0 and self. is non-empty).
def multXdiffAssignTrailing (self : Poly) (start : Nat) (difference : GF16) : Except PolyPanic Poly := do
let l := self.coefficients.length
if start >= l then
return self
else
let coeffs' ← multXdiffAssignTrailingLoop difference start (l - start) self.coefficients
return { coefficients := coeffs' }
def lagrange
def lagrangeInterpolatePrepareLoop (pts : List Pt) (offset : Nat) : Nat → Nat → Poly → Except PolyPanic Poly
| _, 0, p => .ok p
| i, rem + 1, p => do
let some pi := pts[i]? | .error .boundsCheck
if i > offset then
.error .subOverflow
else
let p' ← p.multXdiffAssignTrailing (offset - i) pi.x
lagrangeInterpolatePrepareLoop pts offset (i + 1) rem p'def lagrangeInterpolatePrepare
Poly::lagrange_src/): computes $\prod_i (x - \mathrm{pts}[i].x)$ of degree pts..
def lagrangeInterpolatePrepare (pts : List Pt) : Except PolyPanic Poly := do
let offset := pts.length
if offset + 1 > USIZE_MAX then
.error .addOverflow
else
let p0 : Poly := { coefficients := List.replicate offset GF16.ZERO ++ [GF16.ONE] }
lagrangeInterpolatePrepareLoop pts offset 0 offset p0def lagrangeDenominator
def lagrangeCompleteDivLoop
def lagrangeCompleteDivLoop (pix scale : GF16) (len : Nat) : Nat → Nat → List GF16 → Except PolyPanic (List GF16)
| _, 0, coeffs => .ok coeffs
| j, rem + 1, coeffs =>
if j > len then
.error .subOverflow
else
let idx := len - j
if idx == 0 then
.error .subOverflow
else
match coeffs[idx]?, coeffs[idx - 1]? with
| some cIdx, some cPrev =>
let negativeDelta := GF16.mul cIdx pix
let coeffs1 := coeffs.set idx (GF16.mul cIdx scale)
let coeffs2 := coeffs1.set (idx - 1) (GF16.add cPrev negativeDelta)
lagrangeCompleteDivLoop pix scale len (j + 1) rem coeffs2
| _, _ => .error .boundsCheckdef lagrangeInterpolateComplete
Poly::lagrange_src/): divides $(x - \mathrm{pts}[i].x)$ out of self into upper coefficients [1..] and scales by $\mathrm{pts}[i].y / \prod_{p_j.x \ne \mathrm{pts}[i].x} (\mathrm{pts}[i].x - p_j.x)$.
def lagrangeInterpolateComplete (self : Poly) (pts : List Pt) (i : Nat) : Except PolyPanic Poly := do
let some pi := pts[i]? | .error .boundsCheck
let denominator := lagrangeDenominator pi.x pts
let scale := GF16.div pi.y denominator
let len := self.coefficients.length
if len <= 1 then
return self
else
let coeffs' ← lagrangeCompleteDivLoop pi.x scale len 1 (len - 1) self.coefficients
return { coefficients := coeffs' }def lagrangeAccumulateCoeffs
def lagrangeAccumulateCoeffs : Nat → Nat → List GF16 → List GF16 → Except PolyPanic (List GF16)
| _, 0, outCoeffs, _ => .ok outCoeffs
| j, rem + 1, outCoeffs, workingCoeffs =>
if j + 1 > USIZE_MAX then
.error .addOverflow
else
match outCoeffs[j]?, workingCoeffs[j + 1]? with
| some o, some w =>
lagrangeAccumulateCoeffs (j + 1) rem (outCoeffs.set j (GF16.add o w)) workingCoeffs
| _, _ => .error .boundsCheckdef lagrangeInterpolateLoop
def lagrangeInterpolateLoop (template : Poly) (pts : List Pt) :
Nat → Nat → List GF16 → Except PolyPanic (List GF16)
| _, 0, outCoeffs => .ok outCoeffs
| i, rem + 1, outCoeffs => do
let working ← template.lagrangeInterpolateComplete pts i
let outCoeffs' ← lagrangeAccumulateCoeffs 0 outCoeffs.length outCoeffs working.coefficients
lagrangeInterpolateLoop template pts (i + 1) rem outCoeffs'def lagrangeInterpolate
Poly::lagrange_interpolate (src/): returns the Lagrange interpolating polynomial of degree < pts..
def lagrangeInterpolate (pts : List Pt) : Except PolyPanic Poly := do
if pts.isEmpty then
return Poly.zero pts.length
else
let template ← Poly.lagrangeInterpolatePrepare pts
let working0 ← template.lagrangeInterpolateComplete pts 0
match working0.coefficients with
| [] => .error .sliceIndexFail
| _ :: rest0 =>
let outCoeffs ← lagrangeInterpolateLoop template pts 1 (pts.length - 1) rest0
return { coefficients := outCoeffs }def lagrangeInterpolatePt
Poly::lagrange_interpolate_pt (src/): Lagrange basis polynomial for pts[i].
def lagrangeInterpolatePt (pts : List Pt) (i : Nat) : Except PolyPanic Poly := do
let result ← Poly.lagrangeInterpolatePrepare pts
let result ← result.lagrangeInterpolateComplete pts i
match result.coefficients with
| [] => .error .sliceIndexFail
| _ :: rest => return { coefficients := rest }def addAssignCoeffs
def addAssignCoeffs : List GF16 → List GF16 → List GF16
| selfCoeffs, [] => selfCoeffs
| [], otherCoeffs => otherCoeffs
| c :: cs, o :: os => GF16.add c o :: addAssignCoeffs cs osdef addAssign
def addAssign (self other : Poly) : Poly :=
{ coefficients := addAssignCoeffs self.coefficients other.coefficients }def multAssign
def multAssign (self : Poly) (m : GF16) : Poly :=
{ coefficients := parallelMult m self.coefficients }def computeAtPowersLoop
def computeAtPowersLoop : Nat → Nat → List GF16 → Except PolyPanic (List GF16)
| _, 0, xs => .ok xs
| i, rem + 1, xs =>
match xs[i / 2]?, xs[(i / 2) + (i % 2)]? with
| some a, some b =>
computeAtPowersLoop (i + 1) rem (xs ++ [GF16.mul a b])
| _, _ => .error .boundsCheckdef computeAt
def computeAt (self : Poly) (x : GF16) : Except PolyPanic GF16 := do
let len := self.coefficients.length
let xs0 : List GF16 := [GF16.ONE, x]
let xs ← if len <= 2 then .ok xs0 else computeAtPowersLoop 2 (len - 2) xs0
let pairs := self.coefficients.zip xs
return pairs.foldl (fun out (a, b) => GF16.add out (GF16.mul a b)) GF16.ZEROdef lagrangeSum
Poly::lagrange_sum (src/): $\sum_i \mathrm{polys}[i] \cdot \mathrm{pts}[i].y$.
end Poly
PolyConst<N> and precomputed complete-point Lagrange bases (src/)
structure PolyConst
Fixed-length polynomial of n coefficients (PolyConst<N>, src/).
structure PolyConst (n : Nat) where
coefficients : List GF16
deriving DecidableEq, Repr, Inhabitednamespace PolyConst1 declaration not shown (lines 393–394): theorems, which Lean checks, or definitions that no headline statement uses
CryptoVerification.
def mult
def mult {n : Nat} (self : PolyConst n) (m : GF16) : PolyConst n :=
{ coefficients := self.coefficients.map (fun c => GF16.constMul c m) }def multXdiff
PolyConst::<N>::mult_xdiff (src/): multiplies self by $(x - \mathrm{difference})$ within n coefficients; panics on n == 0 (.subOverflow) or non-zero top coefficient (.explicitPanic).
def multXdiff {n : Nat} (self : PolyConst n) (difference : GF16) : Except PolyPanic (PolyConst n) := do
if n == 0 then
.error .subOverflow
else
let some top := self.coefficients[n - 1]? | .error .boundsCheck
if top != GF16.ZERO then
.error .explicitPanic
else
let xp : List GF16 := GF16.ZERO :: self.coefficients.take (n - 1)
let dp : List GF16 := self.coefficients.map (fun c => GF16.constMul c difference)
let out : List GF16 := (xp.zip dp).map (fun (a, b) => GF16.constSub a b)
return { coefficients := out }def lagrangeInterpolatePtLoop
def lagrangeInterpolatePtLoop (n : Nat) (pts : List Pt) (pix : GF16) :
Nat → Nat → PolyConst n → GF16 → Except PolyPanic (PolyConst n × GF16)
| _, 0, p, denominator => .ok (p, denominator)
| j, rem + 1, p, denominator => do
let some pj := pts[j]? | .error .boundsCheck
if pix == pj.x then
lagrangeInterpolatePtLoop n pts pix (j + 1) rem p denominator
else
let p' ← p.multXdiff pj.x
let denominator' := GF16.constMul denominator (GF16.constSub pix pj.x)
lagrangeInterpolatePtLoop n pts pix (j + 1) rem p' denominator'def lagrangeInterpolatePt
PolyConst::<N>::lagrange_interpolate_pt (src/).
def lagrangeInterpolatePt (n : Nat) (pts : List Pt) (i : Nat) : Except PolyPanic (PolyConst n) := do
let some pi := pts[i]? | .error .boundsCheck
if n == 0 then
.error .boundsCheck
else
let p0 : PolyConst n := { coefficients := GF16.ONE :: List.replicate (n - 1) GF16.ZERO }
let (p, denominator) ← lagrangeInterpolatePtLoop n pts pi.x 0 n p0 GF16.ONE
return p.mult (GF16.constDiv pi.y denominator)def toPoly
def toPoly {n : Nat} (self : PolyConst n) : Poly :=
{ coefficients := self.coefficients }end PolyConstdef constPolysToPolys
def constPolysToPolys {n : Nat} (cps : List (PolyConst n)) : List Poly :=
cps.map PolyConst.toPoly
def lagrange
Precomputes the n Lagrange basis polynomials for $x = 0, \dots, n - 1$ (src/).
def COMPLETE_POINTS_POLYS_1
def COMPLETE_POINTS_POLYS_1 : Except PolyPanic (List (PolyConst 1)) :=
lagrangePolysForCompletePoints 1def COMPLETE_POINTS_POLYS_3
def COMPLETE_POINTS_POLYS_3 : Except PolyPanic (List (PolyConst 3)) :=
lagrangePolysForCompletePoints 3def COMPLETE_POINTS_POLYS_5
def COMPLETE_POINTS_POLYS_5 : Except PolyPanic (List (PolyConst 5)) :=
lagrangePolysForCompletePoints 5def COMPLETE_POINTS_POLYS_30
def COMPLETE_POINTS_POLYS_30 : Except PolyPanic (List (PolyConst 30)) :=
lagrangePolysForCompletePoints 30def COMPLETE_POINTS_POLYS_34
def COMPLETE_POINTS_POLYS_34 : Except PolyPanic (List (PolyConst 34)) :=
lagrangePolysForCompletePoints 34def COMPLETE_POINTS_POLYS_36
def COMPLETE_POINTS_POLYS_36 : Except PolyPanic (List (PolyConst 36)) :=
lagrangePolysForCompletePoints 36namespace Polydef checkCompletePoints
def checkCompletePoints : Nat → List Pt → Bool
| _, [] => true
| i, pt :: rest =>
if pt.x != GF16.new (BitVec.ofNat 16 i) then
false
else
checkCompletePoints (i + 1) restdef fromCompletePoints
Poly::from_complete_points (src/): interpolates pts when pts[i].x == i, using COMPLETE_POINTS_POLYS_{1,3,5,30,34,36} for matching lengths and Poly. otherwise.
def fromCompletePoints (pts : List Pt) : Except PolyPanic (Except Unit Poly) := do
if !checkCompletePoints 0 pts then
return .error ()
else
let n := pts.length
let polys : List Poly ←
if n == 0 then
pure []
else if n == 1 then do
let cps ← COMPLETE_POINTS_POLYS_1
pure (constPolysToPolys cps)
else if n == 3 then do
let cps ← COMPLETE_POINTS_POLYS_3
pure (constPolysToPolys cps)
else if n == 5 then do
let cps ← COMPLETE_POINTS_POLYS_5
pure (constPolysToPolys cps)
else if n == 30 then do
let cps ← COMPLETE_POINTS_POLYS_30
pure (constPolysToPolys cps)
else if n == 34 then do
let cps ← COMPLETE_POINTS_POLYS_34
pure (constPolysToPolys cps)
else if n == 36 then do
let cps ← COMPLETE_POINTS_POLYS_36
pure (constPolysToPolys cps)
else do
let ones : List Pt := pts.map (fun pt => { x := pt.x, y := GF16.ONE })
(List.range n).mapM (fun i => Poly.lagrangeInterpolatePt ones i)
return .ok (Poly.lagrangeSum pts polys)def serialize
def serialize (self : Poly) : List (BitVec 8) :=
self.coefficients.flatMap (fun c => u16ToBeBytes c.value)def bytesToGF16List
def bytesToGF16List : List (BitVec 8) → Except PolyPanic (List GF16)
| [] => .ok []
| [ _ ] => .error .boundsCheck
| b0 :: b1 :: rest => do
let tail ← bytesToGF16List rest
return GF16.new (u16FromBeBytes b0 b1) :: taildef deserialize
Poly::deserialize (src/): rejects empty or odd-length inputs with .serializationInvalid, otherwise decodes big-endian GF16 coefficients.
def deserialize (serialized : List (BitVec 8)) : Except PolyPanic (Except PolynomialError Poly) := do
if serialized.isEmpty || serialized.length % 2 == 1 then
return .error .serializationInvalid
else
let coefficients ← bytesToGF16List serialized
return .ok { coefficients }end Poly
Point, EncoderState, ProtoPolynomialEncoder, and PolyEncoder (src/)
structure Point
Buffered GF16 points for one of the 16 encoder polynomials (src/).
structure Point where
value : List GF16
deriving DecidableEq, Repr, Inhabitedinductive EncoderState
structure ProtoPolynomialEncoder
pqrpb::PolynomialEncoder (src/).
structure ProtoPolynomialEncoder where
idx : BitVec 32
pts : List (List (BitVec 8))
polys : List (List (BitVec 8))
deriving DecidableEq, Repr, Inhabitedstructure PolyEncoder
Erasure-code encoder (src/): next chunk index idx and EncoderState.
structure PolyEncoder where
idx : BitVec 32
s : EncoderState
deriving DecidableEq, Repr, Inhabitednamespace PolyEncoderdef intoPb
PolyEncoder::into_pb (src/).
def intoPb (self : PolyEncoder) : ProtoPolynomialEncoder :=
match self.s with
| .points points =>
{ idx := self.idx
pts := points.map (fun pt => pt.value.flatMap (fun g => u16ToBeBytes g.value))
polys := [] }
| .polys polys =>
{ idx := self.idx
pts := []
polys := polys.map Poly.serialize }def decodePbPoints
def decodePbPoints : List (List (BitVec 8)) → Except PolyPanic (Except PolynomialError (List Point))
| [] => .ok (.ok [])
| pts :: rest => do
if pts.length % 2 != 0 then
return .error .serializationInvalid
else
let v ← Poly.bytesToGF16List pts
let tailRes ← decodePbPoints rest
match tailRes with
| .error e => return .error e
| .ok tail => return .ok ({ value := v } :: tail)def decodePbPolys
def decodePbPolys : List (List (BitVec 8)) → Except PolyPanic (Except PolynomialError (List Poly))
| [] => .ok (.ok [])
| polyBytes :: rest => do
let pRes ← Poly.deserialize polyBytes
match pRes with
| .error e => return .error e
| .ok p =>
let tailRes ← decodePbPolys rest
match tailRes with
| .error e => return .error e
| .ok tail => return .ok (p :: tail)def fromPb
PolyEncoder::from_pb (src/): decodes an encoder from its protobuf form; requires exactly one of pts or polys to have NUM_POLYS (16) entries.
def fromPb (pb : ProtoPolynomialEncoder) : Except PolyPanic (Except PolynomialError PolyEncoder) := do
if !pb.pts.isEmpty then
if !pb.polys.isEmpty then
return .error .serializationInvalid
else if pb.pts.length != NUM_POLYS then
return .error .serializationInvalid
else
let ptsRes ← decodePbPoints pb.pts
match ptsRes with
| .error e => return .error e
| .ok out => return .ok { idx := pb.idx, s := .points out }
else if pb.polys.length == NUM_POLYS then
let polysRes ← decodePbPolys pb.polys
match polysRes with
| .error e => return .error e
| .ok out => return .ok { idx := pb.idx, s := .polys out }
else
return .error .serializationInvaliddef enumeratePts
def pointsToPolysLoop
def pointsToPolysLoop (pts : List Point) : Nat → Nat → List Poly → Except PolyPanic (List Poly)
| _, 0, acc => .ok acc
| i, rem + 1, acc => do
let some ptList := pts[i]? | .error .boundsCheck
let ptVec : List Pt := enumeratePts 0 ptList.value
let res ← Poly.fromCompletePoints ptVec
match res with
| .error () => .error .expectFailed
| .ok p => pointsToPolysLoop pts (i + 1) rem (acc ++ [p])def pointAt
PolyEncoder::point_at (src/): reads pts[poly].value[idx] directly when in .points and in bounds; otherwise interpolates all 16 polynomials into .polys and evaluates polys[poly] at idx.
def pointAt (self : PolyEncoder) (poly : Nat) (idx : Nat) : Except PolyPanic (PolyEncoder × GF16) := do
let self ←
match self.s with
| .points pts => do
let some pt := pts[poly]? | .error .boundsCheck
match pt.value[idx]? with
| some val => return (self, val)
| none =>
let polys ← pointsToPolysLoop pts 0 NUM_POLYS []
pure { self with s := .polys polys }
| .polys _ => pure self
match self.s with
| .polys polys =>
let some p := polys[poly]? | .error .boundsCheck
let val ← p.computeAt (GF16.new (BitVec.ofNat 16 idx))
return (self, val)
| .points _ =>
.error .explicitPanicdef distributeMsgChunks
def distributeMsgChunks : Nat → List (BitVec 8) → List Point → Except PolyPanic (List Point)
| _, [], pts => .ok pts
| _, [ _ ], _ => .error .boundsCheck
| i, c0 :: c1 :: rest, pts => do
let poly := i % pts.length
let some pt := pts[poly]? | .error .boundsCheck
let gf := GF16.new ((c0.zeroExtend 16 <<< 8) + c1.zeroExtend 16)
let pts' := pts.set poly { value := pt.value ++ [gf] }
distributeMsgChunks (i + 1) rest pts'def encodeBytesBase
PolyEncoder::encode_bytes_base (src/): rejects odd-length or overlong (> 2^16 * 16 bytes) messages and distributes big-endian GF16 pairs across 16 Point buffers.
def encodeBytesBase (msg : List (BitVec 8)) : Except PolyPanic (Except EncodingError PolyEncoder) := do
if msg.length % 2 != 0 then
return .error (.polynomialError .messageLengthEven)
else if msg.length > (1 <<< 16) * NUM_POLYS then
return .error (.polynomialError .messageLengthTooLong)
else
let initPts : List Point := List.replicate NUM_POLYS { value := [] }
let pts ← distributeMsgChunks 0 msg initPts
return .ok { idx := 0#32, s := .points pts }def encodeBytes
<PolyEncoder as Encoder>::encode_bytes (src/).
def encodeBytes (msg : List (BitVec 8)) : Except PolyPanic (Except EncodingError PolyEncoder) :=
encodeBytesBase msgdef chunkAtLoop
def chunkAtLoop (idx : BitVec 16) :
(i : Nat) → (rem : Nat) → PolyEncoder →
Except PolyPanic (PolyEncoder × List.Vector (BitVec 8) (2 * rem))
| _, 0, self => .ok (self, List.Vector.nil)
| i, rem + 1, self => do
let totalIdx := idx.toNat * 16 + i
let poly := totalIdx % 16
let polyIdx := totalIdx / 16
let (self', p) ← self.pointAt poly polyIdx
let (self'', tail) ← chunkAtLoop idx (i + 1) rem self'
let b0 : BitVec 8 := (p.value >>> 8).setWidth 8
let b1 : BitVec 8 := p.value.setWidth 8
return (self'', b0 ::ᵥ b1 ::ᵥ tail)def chunkAt
PolyEncoder::chunk_at (src/): emits the 32-byte chunk at 16-bit idx (one GF16 value per polynomial).
def chunkAt (self : PolyEncoder) (idx : BitVec 16) : Except PolyPanic (PolyEncoder × Chunk) := do
let (self', data) ← chunkAtLoop idx 0 16 self
return (self', { index := idx, data := data })def nextChunk
<PolyEncoder as Encoder>::next_chunk (src/): emits chunkAt (self.self. wrapping modulo $2^{32}$.
def nextChunk (self : PolyEncoder) : Except PolyPanic (PolyEncoder × Chunk) := do
let (self', out) ← self.chunkAt (self.idx.setWidth 16)
return ({ self' with idx := self'.idx + 1#32 }, out)end PolyEncoder
ProtoPolynomialDecoder and PolyDecoder (src/)
structure ProtoPolynomialDecoder
pqrpb::PolynomialDecoder (src/).
structure ProtoPolynomialDecoder where
ptsNeeded : BitVec 32
polys : BitVec 32
pts : List (List (BitVec 8))
isComplete : Bool
deriving DecidableEq, Repr, Inhabitedstructure PolyDecoder
Erasure-code decoder (src/): target 2-byte point count ptsNeeded, 16 SortedSetPt sets pts, and isComplete flag.
structure PolyDecoder where
ptsNeeded : Nat
pts : List SortedSetPt
isComplete : Bool
deriving DecidableEq, Repr, Inhabitednamespace PolyDecoderdef necessaryPoints
PolyDecoder::necessary_points (src/).
def necessaryPoints (self : PolyDecoder) (poly : Nat) : Nat :=
let pointsPerPoly := self.ptsNeeded / 16
let pointsRemaining := self.ptsNeeded % 16
if poly < pointsRemaining then
pointsPerPoly + 1
else
pointsPerPolydef newWithPolyCount
PolyDecoder::new_with_poly_count (src/); rejects odd lenBytes with .messageLengthEven.
def newWithPolyCount (lenBytes : Nat) (_polys : Nat) :
Except PolyPanic (Except EncodingError PolyDecoder) := do
if lenBytes % 2 != 0 then
return .error (.polynomialError .messageLengthEven)
else
return .ok
{ ptsNeeded := lenBytes / 2
pts := List.replicate 16 SortedSetPt.new
isComplete := false }def new
<PolyDecoder as Decoder>::new (src/).
def new (lenBytes : Nat) : Except PolyPanic (Except EncodingError PolyDecoder) :=
newWithPolyCount lenBytes 16def intoPb
PolyDecoder::into_pb (src/).
def intoPb (self : PolyDecoder) : ProtoPolynomialDecoder :=
{ ptsNeeded := BitVec.ofNat 32 self.ptsNeeded
polys := 16#32
isComplete := self.isComplete
pts := self.pts.map (fun s => s.vec.flatMap Pt.serialize) }def pushChunksExact4
def pushChunksExact4 : List (BitVec 8) → SortedSetPt → Except PolyPanic SortedSetPt
| [], v => .ok v
| b0 :: b1 :: b2 :: b3 :: rest, v => do
let pt ← Pt.deserialize [b0, b1, b2, b3]
let (v', _, _) := v.push pt
pushChunksExact4 rest v'
| _, _ => .error .unwrapFaileddef decodeDecoderPbPts
def decodeDecoderPbPts : List (List (BitVec 8)) →
Except PolyPanic (Except PolynomialError (List SortedSetPt))
| [] => .ok (.ok [])
| pts :: rest => do
if pts.length % 4 != 0 then
return .error .serializationInvalid
else
let v ← pushChunksExact4 pts (SortedSetPt.withCapacity (pts.length / 4))
let tailRes ← decodeDecoderPbPts rest
match tailRes with
| .error e => return .error e
| .ok tail => return .ok (v :: tail)def fromPb
PolyDecoder::from_pb (src/): requires 16 point sets whose byte lengths are multiples of 4.
def fromPb (pb : ProtoPolynomialDecoder) : Except PolyPanic (Except PolynomialError PolyDecoder) := do
if pb.pts.length != 16 then
return .error .serializationInvalid
else
let ptsRes ← decodeDecoderPbPts pb.pts
match ptsRes with
| .error e => return .error e
| .ok outPts =>
return .ok
{ ptsNeeded := pb.ptsNeeded.toNat
isComplete := pb.isComplete
pts := outPts }def addChunkLoop
def addChunkLoop (chunk : Chunk) :
Nat → Nat → PolyDecoder → Except PolyPanic PolyDecoder
| _, 0, self => .ok self
| i, rem + 1, self => do
let totalIdx := chunk.index.toNat * 16 + i
let poly := totalIdx % 16
let polyIdx := totalIdx / 16
let x := GF16.new (BitVec.ofNat 16 polyIdx)
let y1 := chunk.data.get ⟨(i * 2) % 32, Nat.mod_lt _ (chunk:Chunki:ℕrem:ℕself:PolyDecodertotalIdx:ℕ := chunk.index.toNat * 16 + ipoly:ℕ := totalIdx % 16polyIdx:ℕ := totalIdx / 16x:GF16 := GF16.new (BitVec.ofNat 16 polyIdx)⊢ 0 < 32 All goals completed! 🐙)⟩
let y2 := chunk.data.get ⟨(i * 2 + 1) % 32, Nat.mod_lt _ (chunk:Chunki:ℕrem:ℕself:PolyDecodertotalIdx:ℕ := chunk.index.toNat * 16 + ipoly:ℕ := totalIdx % 16polyIdx:ℕ := totalIdx / 16x:GF16 := GF16.new (BitVec.ofNat 16 polyIdx)y1:BitVec 8 := chunk.data.get ⟨i * 2 % 32, ⋯⟩⊢ 0 < 32 All goals completed! 🐙)⟩
let y := GF16.new ((y1.zeroExtend 16 <<< 8) + y2.zeroExtend 16)
let some polyPts := self.pts[poly]? | .error .boundsCheck
let nec := self.necessaryPoints i
let self' :=
if polyIdx < nec || polyPts.len < nec then
let (polyPts', _, _) := polyPts.push { x := x, y := y }
{ self with pts := self.pts.set poly polyPts' }
else
self
addChunkLoop chunk (i + 1) rem self'def addChunk
<PolyDecoder as Decoder>::add_chunk (src/).
def addChunk (self : PolyDecoder) (chunk : Chunk) : Except PolyPanic PolyDecoder :=
addChunkLoop chunk 0 16 selfdef collectPointsVecs
def collectPointsVecs (self : PolyDecoder) :
Nat → Nat → Bool → List (List Pt) → Except PolyPanic (Bool × List (List Pt))
| _, 0, retNone, pointsVecs => .ok (retNone, pointsVecs)
| i, rem + 1, retNone, pointsVecs => do
let some pts := self.pts[i]? | .error .boundsCheck
let nec := self.necessaryPoints i
if pts.len < nec then
collectPointsVecs self (i + 1) rem true pointsVecs
else
collectPointsVecs self (i + 1) rem retNone (pointsVecs ++ [pts.asSlice.take nec])def decodedMessageLoop
def decodedMessageLoop (self : PolyDecoder) (pointsVecs : List (List Pt)) :
Nat → Nat → List (Option Poly) → List (BitVec 8) →
Except PolyPanic (List (Option Poly) × List (BitVec 8))
| _, 0, polys, out => .ok (polys, out)
| i, rem + 1, polys, out => do
let poly := i % 16
let polyIdx := i / 16
let pt : Pt := { x := GF16.new (BitVec.ofNat 16 polyIdx), y := GF16.ZERO }
let some polyPts := self.pts[poly]? | .error .boundsCheck
let (polys', y) ←
match polyPts.binarySearch pt with
| .ok idx =>
let some foundPt := polyPts.vec[idx]? | .error .boundsCheck
pure (polys, foundPt.y)
| .error _ =>
let some optPoly := polys[poly]? | .error .boundsCheck
let polys1 ←
match optPoly with
| some _ => pure polys
| none =>
let some ptsSlice := pointsVecs[poly]? | .error .boundsCheck
let interp ← Poly.lagrangeInterpolate ptsSlice
pure (polys.set poly (some interp))
let some (some p) := polys1[poly]? | .error .expectFailed
let yVal ← p.computeAt pt.x
pure (polys1, yVal)
let out' := out ++ u16ToBeBytes y.value
decodedMessageLoop self pointsVecs (i + 1) rem polys' out'def decodedMessage
<PolyDecoder as Decoder>::decoded_message (src/): returns none if isComplete is set or any polynomial lacks necessaryPoints points, otherwise reconstructs the message via direct lookup or Lagrange interpolation.
def decodedMessage (self : PolyDecoder) : Except PolyPanic (Option (List (BitVec 8))) := do
if self.isComplete then
return none
else
let (retNone, pointsVecs) ← collectPointsVecs self 0 self.pts.length false []
if retNone then
return none
else if self.ptsNeeded * 2 > USIZE_MAX then
.error .mulOverflow
else
let initPolys : List (Option Poly) := List.replicate 16 none
let (_, out) ← decodedMessageLoop self pointsVecs 0 self.ptsNeeded initPolys []
return some outend PolyDecoder22 declarations not shown (lines 887–1083): theorems, which Lean checks, or definitions that no headline statement uses
CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification.
end CryptoVerification.LibsignalSpqrV1