GF16.lean
Declarations on this page (24)
- def POLY
- structure GF16
- def ZERO
- def ONE
- def new
- def add
- def sub
- def constSub
- def reduceFromByteLoop
- def reduceFromByte
- def reduceByteEntry
- def polyReduce
- def polyMulLoop
- def polyMul
- def mul
- def mul2U16
- def parallelMult
- def mul
- def constMul
- def divImplLoop
- def divImpl
- def div
- def constDivLoop
- def constDiv
SPQR V1: GF(2^16) arithmetic (src/)
Trusted in part. The theorems of Computational/ use every definition in this file except reduce., which is checked by Lean (see Computational/).
Unaccelerated software specification of $\mathrm{GF}(2^{16}) = \mathbb{F}_2[x]/(x^{16} + x^{12} + x^3 + x + 1)$ (POLY = 0x1100b, taken under TokenInit, DEV-SPQR1): GF16 (ZERO, ONE, new, add, sub, constSub, mul, constMul, divImpl, div, constDiv), byte-table reduction (reduceFromByte, REDUCE_BYTES, reduceByteEntry, polyReduce), carryless multiplication (polyMul), and paired/slice scaling (mul2U16, parallelMult). All GF16 operations are panic- and overflow-free on u16 inputs; division computes self * other^(2^16 - 2) so division by 0 returns 0.
@[expose] public sectionnamespace CryptoVerification.LibsignalSpqrV1
Field polynomial and element type (src/)
def POLY
Irreducible polynomial $x^{16} + x^{12} + x^3 + x + 1$ for $\mathrm{GF}(2^{16})$ (pub const POLY: u32 = 0x1100b, src/).
def POLY : BitVec 32 := 0x1100b#32structure GF16
Element of $\mathrm{GF}(2^{16})$ (pub struct GF16 { pub value: u16 }, src/).
structure GF16 where
value : BitVec 16
deriving DecidableEq, Repr, Inhabitednamespace GF16def ZERO
def ZERO : GF16 := ⟨0#16⟩def ONE
def ONE : GF16 := ⟨1#16⟩def new
def new (value : BitVec 16) : GF16 := ⟨value⟩
Addition and subtraction in $\mathrm{GF}(2^{16})$ (src/)
end GF16namespace reducedef reduceFromByteLoop
def reduceFromByteLoop : Nat → BitVec 8 → BitVec 32 → BitVec 32
| 0, _, out => out
| i + 1, a, out =>
let mask : BitVec 8 := 1#8 <<< i
if (mask &&& a) != 0#8 then
let shiftedPoly : BitVec 32 := POLY <<< i
let out' := out ^^^ shiftedPoly
let a' := a ^^^ ((shiftedPoly >>> 16).truncate 8)
reduceFromByteLoop i a' out'
else
reduceFromByteLoop i a outdef reduceFromByte
reduce::reduce_from_byte(mut a: u8) -> u32 (src/).
def reduceFromByte (a : BitVec 8) : BitVec 32 :=
reduceFromByteLoop 8 a 0#321 declaration not shown (lines 88–90): theorems, which Lean checks, or definitions that no headline statement uses
CryptoVerification.
def reduceByteEntry
def reduceByteEntry (idx : BitVec 8) : BitVec 16 :=
(reduceFromByte idx).truncate 16def polyReduce
reduce::poly_reduce(v: u32) -> u16 (src/): reduces a 32-bit carryless product modulo POLY = 0x1100b in two byte-table lookups.
def polyReduce (v : BitVec 32) : BitVec 16 :=
let i1 : BitVec 8 := (v >>> 24).truncate 8
let r1 : BitVec 32 := (reduceByteEntry i1).zeroExtend 32
let v1 : BitVec 32 := v ^^^ (r1 <<< 8)
let i2 : BitVec 8 := (v1 >>> 16).truncate 8
let r2 : BitVec 32 := (reduceByteEntry i2).zeroExtend 32
let v2 : BitVec 32 := v1 ^^^ r2
v2.truncate 16end reducenamespace unaccelerateddef polyMulLoop
def polyMulLoop (me : BitVec 32) (b : BitVec 16) : Nat → Nat → BitVec 32 → BitVec 32
| 0, _, acc => acc
| fuel + 1, shift, acc =>
let acc' :=
if 0#16 != (b &&& (1#16 <<< shift)) then
acc ^^^ (me <<< shift)
else
acc
polyMulLoop me b fuel (shift + 1) acc'def polyMul
unaccelerated::poly_mul(a: u16, b: u16) -> u32 (src/).
def polyMul (a b : BitVec 16) : BitVec 32 :=
polyMulLoop (a.zeroExtend 32) b 16 0 0#32def mul
unaccelerated::mul(a: u16, b: u16) -> u16 (src/).
def mul (a b : BitVec 16) : BitVec 16 :=
reduce.polyReduce (polyMul a b)end unaccelerated
Pair multiplication, field multiplication, and division (src/)
def mul2U16
mul2_u16 (src/, unaccelerated path).
def mul2U16 (a b1 b2 : BitVec 16) : BitVec 16 × BitVec 16 :=
(unaccelerated.mul a b1, unaccelerated.mul a b2)def parallelMult
parallel_mult (src/).
namespace GF16def mul
def mul (self other : GF16) : GF16 :=
⟨unaccelerated.mul self.value other.value⟩def constMul
def constMul (self other : GF16) : GF16 :=
⟨unaccelerated.mul self.value other.value⟩def divImplLoop
def divImplLoop : Nat → BitVec 16 → BitVec 16 → BitVec 16
| 0, _, out => out
| n + 1, square, out =>
let (square', out') := mul2U16 square square out
divImplLoop n square' out'def divImpl
def constDivLoop
def constDiv
def constDiv (self other : GF16) : GF16 :=
constDivLoop 15 other selfend GF1620 declarations not shown (lines 184–346): 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.
end CryptoVerification.LibsignalSpqrV1