File size: 1,862 Bytes
ebed3db | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 | -- seb_lattice.ads
-- SEB Lattice Circuit — Ahmad Ali Parr, SnapKitty Collective 2026
-- SPARK 2014, Pure, No heap, No external deps
--
-- Compile: gnatmake -O2 -gnat2012 seb_lattice_test.adb seb_lattice.adb
-- GNATprove: gnatprove -P seb_lattice.gpr --level=4
package SEB_Lattice
with SPARK_Mode => On,
Pure
is
-- Primitive types
type Byte is mod 256
with Size => 8;
type Index32 is range 0 .. 31;
type Index64 is range 0 .. 63;
type Poly is array (Index32) of Byte;
type Payload is array (Index64) of Byte;
-- 96-byte record
type Record96 is record
Data : Payload;
Commitment : Poly;
end record
with Size => 768; -- 96 bytes = 768 bits
pragma Compile_Time_Error
(Record96'Size /= 768, "Record96 must be exactly 96 bytes");
-- Genesis: all-zero commitment
Genesis_Tip : constant Poly := (others => 0);
-- Fixed public constants (frozen at genesis)
K0 : constant Poly := (0 => 1, others => 0); -- x^0 = 1
K1 : constant Poly := (1 => 1, others => 0); -- x^1
K2 : constant Poly := (2 => 1, others => 0); -- x^2
-- GF(256) multiply: AES irreducible x^8+x^4+x^3+x+1 (0x11B)
function GF256_Mul (X, Y : Byte) return Byte
with Pure_Function,
Global => null;
-- Cyclic convolution in GF(256)[x]/(x^32+1)
function Cyclic_Convolve (A, B : Poly) return Poly
with Pure_Function,
Global => null;
-- Circuit: next = K0⊗prev XOR K1⊗b XOR K2⊗c
-- Since K0=1: next = prev XOR K1⊗b XOR K2⊗c
function Lattice_Commit (Prev : Poly; Data : Payload) return Poly
with Pure_Function,
Global => null;
-- Constant-time equality
function CT_EQ (A, B : Poly) return Boolean
with Pure_Function,
Global => null,
Post => CT_EQ'Result = (A = B);
end SEB_Lattice;
|