-- 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;