module Runtime.TelemetrySeal import Std.Foundation import Std.List import Std.Natural -- One SHA-256/ALPHATEL algorithm, specialized to a host instruction emitter. -- The emitter owns register assignment, instruction selection and branch -- flags. Loads/stores are little-endian and permit unaligned access; 8/32-bit -- loads zero-extend. Word operations wrap at 64 bits, shifts are logical, and -- 8/32-bit stores truncate. AddImm sign-extends its 32-bit operand and sets -- zero status; CmpImm supplies unsigned comparison status. Label and move -- operations preserve that status. These obligations are tested on each host. -- -- Registers are logical roles inherited from the original implementation: -- RDI/RSI/RDX/RCX/R8/R9 carry the six arguments; the remaining names denote -- scratch values. The emitter chooses physical registers and preserves its -- calling convention. The fixed work-area slots are part of this algorithm, -- not per-system addresses. Callers supply writable, nonoverlapping bounded -- buffers, a positive block count and body length, and valid SHA padding. family TelemetrySealCondition : Type 0 constructor TelemetrySealBelow constructor TelemetrySealNotZero end-family family TelemetrySealBackend : Type 0 parameter erased sealBackendAssembly : Type 0 parameter erased sealBackendRegister : Type 0 constructor TelemetrySealBackendValue field unrestricted backendSealLoad32 : (pi unrestricted a0 : sealBackendRegister . (pi unrestricted a1 : sealBackendRegister . (pi unrestricted a2 : Nat . (pi unrestricted a3 : sealBackendAssembly . sealBackendAssembly)))) field unrestricted backendSealLoad64 : (pi unrestricted a0 : sealBackendRegister . (pi unrestricted a1 : sealBackendRegister . (pi unrestricted a2 : Nat . (pi unrestricted a3 : sealBackendAssembly . sealBackendAssembly)))) field unrestricted backendSealLoad8 : (pi unrestricted a0 : sealBackendRegister . (pi unrestricted a1 : sealBackendRegister . (pi unrestricted a2 : Nat . (pi unrestricted a3 : sealBackendAssembly . sealBackendAssembly)))) field unrestricted backendSealStore32 : (pi unrestricted a0 : sealBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : sealBackendRegister . (pi unrestricted a3 : sealBackendAssembly . sealBackendAssembly)))) field unrestricted backendSealStore64 : (pi unrestricted a0 : sealBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : sealBackendRegister . (pi unrestricted a3 : sealBackendAssembly . sealBackendAssembly)))) field unrestricted backendSealStore8 : (pi unrestricted a0 : sealBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : sealBackendRegister . (pi unrestricted a3 : sealBackendAssembly . sealBackendAssembly)))) field unrestricted backendSealMov : (pi unrestricted a0 : sealBackendRegister . (pi unrestricted a1 : sealBackendRegister . (pi unrestricted a2 : sealBackendAssembly . sealBackendAssembly))) field unrestricted backendSealAdd : (pi unrestricted a0 : sealBackendRegister . (pi unrestricted a1 : sealBackendRegister . (pi unrestricted a2 : sealBackendAssembly . sealBackendAssembly))) field unrestricted backendSealAnd : (pi unrestricted a0 : sealBackendRegister . (pi unrestricted a1 : sealBackendRegister . (pi unrestricted a2 : sealBackendAssembly . sealBackendAssembly))) field unrestricted backendSealOr : (pi unrestricted a0 : sealBackendRegister . (pi unrestricted a1 : sealBackendRegister . (pi unrestricted a2 : sealBackendAssembly . sealBackendAssembly))) field unrestricted backendSealXor : (pi unrestricted a0 : sealBackendRegister . (pi unrestricted a1 : sealBackendRegister . (pi unrestricted a2 : sealBackendAssembly . sealBackendAssembly))) field unrestricted backendSealShl : (pi unrestricted a0 : sealBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : sealBackendAssembly . sealBackendAssembly))) field unrestricted backendSealShr : (pi unrestricted a0 : sealBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : sealBackendAssembly . sealBackendAssembly))) field unrestricted backendSealMovImm : (pi unrestricted a0 : sealBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : sealBackendAssembly . sealBackendAssembly))) field unrestricted backendSealAddImm : (pi unrestricted a0 : sealBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : sealBackendAssembly . sealBackendAssembly))) field unrestricted backendSealAndImm : (pi unrestricted a0 : sealBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : sealBackendAssembly . sealBackendAssembly))) field unrestricted backendSealCmpImm : (pi unrestricted a0 : sealBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : sealBackendAssembly . sealBackendAssembly))) field unrestricted backendSealMulImm : (pi unrestricted a0 : sealBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : sealBackendAssembly . sealBackendAssembly))) field unrestricted backendSealLabel : (pi unrestricted a0 : Bytes . (pi unrestricted a1 : sealBackendAssembly . sealBackendAssembly)) field unrestricted backendSealJumpIf : (pi unrestricted a0 : (family TelemetrySealCondition) . (pi unrestricted a1 : Bytes . (pi unrestricted a2 : sealBackendAssembly . sealBackendAssembly))) field unrestricted backendSealReturn : (pi unrestricted a0 : sealBackendAssembly . sealBackendAssembly) field unrestricted backendSealEnd : sealBackendAssembly field unrestricted backendSealRAX : sealBackendRegister field unrestricted backendSealRBX : sealBackendRegister field unrestricted backendSealRCX : sealBackendRegister field unrestricted backendSealRDX : sealBackendRegister field unrestricted backendSealRSI : sealBackendRegister field unrestricted backendSealRDI : sealBackendRegister field unrestricted backendSealRBP : sealBackendRegister field unrestricted backendSealR8 : sealBackendRegister field unrestricted backendSealR9 : sealBackendRegister field unrestricted backendSealR10 : sealBackendRegister field unrestricted backendSealR11 : sealBackendRegister field unrestricted backendSealR12 : sealBackendRegister field unrestricted backendSealR13 : sealBackendRegister field unrestricted backendSealR14 : sealBackendRegister field unrestricted backendSealR15 : sealBackendRegister end-family def sealMonotonicAt : Nat = 13 def sealWorkBytes : Nat = 640 def sealW = (lambda unrestricted t : Nat . (naturalMultiply 4 t)) def sealK = (lambda unrestricted t : Nat . (naturalAdd 256 (naturalMultiply 4 t))) def sealVar = (lambda unrestricted slot : Nat . (naturalAdd 512 (naturalMultiply 4 slot))) def sealH = (lambda unrestricted i : Nat . (naturalAdd 544 (naturalMultiply 4 i))) def sealSaved = (lambda unrestricted i : Nat . (naturalAdd 576 (naturalMultiply 8 i))) def sealRoundConstants : (family StdList Nat) = (constructor StdList StdListCons Nat 0x428a2f98 (constructor StdList StdListCons Nat 0x71374491 (constructor StdList StdListCons Nat 0xb5c0fbcf (constructor StdList StdListCons Nat 0xe9b5dba5 (constructor StdList StdListCons Nat 0x3956c25b (constructor StdList StdListCons Nat 0x59f111f1 (constructor StdList StdListCons Nat 0x923f82a4 (constructor StdList StdListCons Nat 0xab1c5ed5 (constructor StdList StdListCons Nat 0xd807aa98 (constructor StdList StdListCons Nat 0x12835b01 (constructor StdList StdListCons Nat 0x243185be (constructor StdList StdListCons Nat 0x550c7dc3 (constructor StdList StdListCons Nat 0x72be5d74 (constructor StdList StdListCons Nat 0x80deb1fe (constructor StdList StdListCons Nat 0x9bdc06a7 (constructor StdList StdListCons Nat 0xc19bf174 (constructor StdList StdListCons Nat 0xe49b69c1 (constructor StdList StdListCons Nat 0xefbe4786 (constructor StdList StdListCons Nat 0x0fc19dc6 (constructor StdList StdListCons Nat 0x240ca1cc (constructor StdList StdListCons Nat 0x2de92c6f (constructor StdList StdListCons Nat 0x4a7484aa (constructor StdList StdListCons Nat 0x5cb0a9dc (constructor StdList StdListCons Nat 0x76f988da (constructor StdList StdListCons Nat 0x983e5152 (constructor StdList StdListCons Nat 0xa831c66d (constructor StdList StdListCons Nat 0xb00327c8 (constructor StdList StdListCons Nat 0xbf597fc7 (constructor StdList StdListCons Nat 0xc6e00bf3 (constructor StdList StdListCons Nat 0xd5a79147 (constructor StdList StdListCons Nat 0x06ca6351 (constructor StdList StdListCons Nat 0x14292967 (constructor StdList StdListCons Nat 0x27b70a85 (constructor StdList StdListCons Nat 0x2e1b2138 (constructor StdList StdListCons Nat 0x4d2c6dfc (constructor StdList StdListCons Nat 0x53380d13 (constructor StdList StdListCons Nat 0x650a7354 (constructor StdList StdListCons Nat 0x766a0abb (constructor StdList StdListCons Nat 0x81c2c92e (constructor StdList StdListCons Nat 0x92722c85 (constructor StdList StdListCons Nat 0xa2bfe8a1 (constructor StdList StdListCons Nat 0xa81a664b (constructor StdList StdListCons Nat 0xc24b8b70 (constructor StdList StdListCons Nat 0xc76c51a3 (constructor StdList StdListCons Nat 0xd192e819 (constructor StdList StdListCons Nat 0xd6990624 (constructor StdList StdListCons Nat 0xf40e3585 (constructor StdList StdListCons Nat 0x106aa070 (constructor StdList StdListCons Nat 0x19a4c116 (constructor StdList StdListCons Nat 0x1e376c08 (constructor StdList StdListCons Nat 0x2748774c (constructor StdList StdListCons Nat 0x34b0bcb5 (constructor StdList StdListCons Nat 0x391c0cb3 (constructor StdList StdListCons Nat 0x4ed8aa4a (constructor StdList StdListCons Nat 0x5b9cca4f (constructor StdList StdListCons Nat 0x682e6ff3 (constructor StdList StdListCons Nat 0x748f82ee (constructor StdList StdListCons Nat 0x78a5636f (constructor StdList StdListCons Nat 0x84c87814 (constructor StdList StdListCons Nat 0x8cc70208 (constructor StdList StdListCons Nat 0x90befffa (constructor StdList StdListCons Nat 0xa4506ceb (constructor StdList StdListCons Nat 0xbef9a3f7 (constructor StdList StdListCons Nat 0xc67178f2 (constructor StdList StdListEmpty Nat))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) def sealInitialHash : (family StdList Nat) = (constructor StdList StdListCons Nat 0x6a09e667 (constructor StdList StdListCons Nat 0xbb67ae85 (constructor StdList StdListCons Nat 0x3c6ef372 (constructor StdList StdListCons Nat 0xa54ff53a (constructor StdList StdListCons Nat 0x510e527f (constructor StdList StdListCons Nat 0x9b05688c (constructor StdList StdListCons Nat 0x1f83d9ab (constructor StdList StdListCons Nat 0x5be0cd19 (constructor StdList StdListEmpty Nat))))))))) def sealAt = (lambda unrestricted values : (family StdList Nat) . (lambda unrestricted p : Nat . (eliminate StdOption (lambda unrestricted current : (family StdOption Nat) . Nat) (stdListIndex Nat values p) (branch StdNone . 0) (branch StdSome value . value)))) def sealSlot = (lambda unrestricted v : Nat . (lambda unrestricted t : Nat . (sealVar (naturalModuloUnchecked (naturalSaturatingSubtract (naturalAdd v 64) t) 8)))) def telemetrySealAssemblyFor = (lambda erased A : Type 0 . (lambda erased R : Type 0 . (lambda unrestricted backend : (family TelemetrySealBackend A R) . (eliminate TelemetrySealBackend (lambda unrestricted current : (family TelemetrySealBackend A R) . A) backend (branch TelemetrySealBackendValue sealLoad32 sealLoad64 sealLoad8 sealStore32 sealStore64 sealStore8 sealMov sealAdd sealAnd sealOr sealXor sealShl sealShr sealMovImm sealAddImm sealAndImm sealCmpImm sealMulImm sealLabel sealJumpIf sealReturn sealEnd sealRAX sealRBX sealRCX sealRDX sealRSI sealRDI sealRBP sealR8 sealR9 sealR10 sealR11 sealR12 sealR13 sealR14 sealR15 . (let unrestricted sealFor = (lambda unrestricted count : Nat . (lambda unrestricted body : (pi unrestricted index : Nat . (pi unrestricted rest : A . A)) . (lambda unrestricted tail : A . (nat-eliminate (lambda unrestricted current : Nat . A) tail (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : A . (body (naturalSaturatingSubtract (naturalSaturatingSubtract count 1) predecessor) induction))) count)))) in (let unrestricted sealRotate = (lambda unrestricted d : R . (lambda unrestricted s : R . (lambda unrestricted n : Nat . (lambda unrestricted rest : A . (sealMov d s (sealShl d 32 (sealOr d s (sealShr d n rest)))))))) in (let unrestricted sealSigma = (lambda unrestricted d : R . (lambda unrestricted t : R . (lambda unrestricted s : R . (lambda unrestricted x : Nat . (lambda unrestricted y : Nat . (lambda unrestricted z : Nat . (lambda unrestricted shift : Nat . (lambda unrestricted rest : A . (sealRotate d s x (sealRotate t s y (sealXor d t (nat-eliminate (lambda unrestricted current : Nat . A) (sealRotate t s z (sealXor d t rest)) (lambda unrestricted p : Nat . (lambda unrestricted i : A . (sealMov t s (sealShr t z (sealXor d t rest))))) shift)))))))))))) in (let unrestricted sealConstant = (lambda unrestricted at : Nat . (lambda unrestricted value : Nat . (lambda unrestricted rest : A . (sealMovImm sealRAX value (sealStore32 sealR9 at sealRAX rest))))) in (let unrestricted sealMessageWord = (lambda unrestricted i : Nat . (lambda unrestricted rest : A . (sealLoad8 sealRAX sealRDI (naturalMultiply 4 i) (sealShl sealRAX 8 (sealLoad8 sealRBX sealRDI (naturalAdd 1 (naturalMultiply 4 i)) (sealOr sealRAX sealRBX (sealShl sealRAX 8 (sealLoad8 sealRBX sealRDI (naturalAdd 2 (naturalMultiply 4 i)) (sealOr sealRAX sealRBX (sealShl sealRAX 8 (sealLoad8 sealRBX sealRDI (naturalAdd 3 (naturalMultiply 4 i)) (sealOr sealRAX sealRBX (sealStore32 sealR9 (sealW i) sealRAX rest))))))))))))) in (let unrestricted sealScheduleWord = (lambda unrestricted k : Nat . (lambda unrestricted rest : A . (let unrestricted t = (naturalAdd 16 k) in (sealLoad32 sealRAX sealR9 (sealW (naturalSaturatingSubtract t 15)) (sealSigma sealRBX sealR10 sealRAX 7 18 3 1 (sealLoad32 sealRAX sealR9 (sealW (naturalSaturatingSubtract t 2)) (sealSigma sealR11 sealR10 sealRAX 17 19 10 1 (sealAdd sealRBX sealR11 (sealLoad32 sealR10 sealR9 (sealW (naturalSaturatingSubtract t 16)) (sealAdd sealRBX sealR10 (sealLoad32 sealR10 sealR9 (sealW (naturalSaturatingSubtract t 7)) (sealAdd sealRBX sealR10 (sealStore32 sealR9 (sealW t) sealRBX rest))))))))))))) in (let unrestricted sealRound = (lambda unrestricted t : Nat . (lambda unrestricted rest : A . -- t1 = h + S1(e) + ch(e, f, g) + K[t] + W[t], in rbx (sealLoad32 sealRAX sealR9 (sealSlot 4 t) (sealSigma sealRBX sealR10 sealRAX 6 11 25 0 (sealLoad32 sealR11 sealR9 (sealSlot 5 t) (sealMov sealR10 sealRAX (sealAnd sealR10 sealR11 (sealLoad32 sealR12 sealR9 (sealSlot 6 t) (sealMov sealR11 sealRAX (sealAnd sealR11 sealR12 (sealXor sealR11 sealR12 (sealXor sealR10 sealR11 (sealAdd sealRBX sealR10 (sealLoad32 sealR10 sealR9 (sealSlot 7 t) (sealAdd sealRBX sealR10 (sealLoad32 sealR10 sealR9 (sealK t) (sealAdd sealRBX sealR10 (sealLoad32 sealR10 sealR9 (sealW t) (sealAdd sealRBX sealR10 -- t2 = S0(a) + maj(a, b, c), in r10 (sealLoad32 sealRAX sealR9 (sealSlot 0 t) (sealSigma sealR10 sealR11 sealRAX 2 13 22 0 (sealLoad32 sealR11 sealR9 (sealSlot 1 t) (sealLoad32 sealR12 sealR9 (sealSlot 2 t) (sealMov sealR13 sealRAX (sealAnd sealR13 sealR11 (sealMov sealR14 sealRAX (sealAnd sealR14 sealR12 (sealXor sealR13 sealR14 (sealAnd sealR11 sealR12 (sealXor sealR13 sealR11 (sealAdd sealR10 sealR13 -- d + t1 is the next e (d's slot), t1 + t2 the next a (h's slot) (sealLoad32 sealR11 sealR9 (sealSlot 3 t) (sealAdd sealR11 sealRBX (sealStore32 sealR9 (sealSlot 3 t) sealR11 (sealAdd sealRBX sealR10 (sealStore32 sealR9 (sealSlot 7 t) sealRBX rest)))))))))))))))))))))))))))))))))))) in (let unrestricted sealLoadVariable = (lambda unrestricted i : Nat . (lambda unrestricted rest : A . (sealLoad32 sealRAX sealR9 (sealH i) (sealStore32 sealR9 (sealVar i) sealRAX rest)))) in (let unrestricted sealAccumulate = (lambda unrestricted i : Nat . (lambda unrestricted rest : A . (sealLoad32 sealRAX sealR9 (sealH i) (sealLoad32 sealRBX sealR9 (sealVar i) (sealAdd sealRAX sealRBX (sealStore32 sealR9 (sealH i) sealRAX rest)))))) in (let unrestricted sealHexDigit = (lambda unrestricted q : Nat . (lambda unrestricted rest : A . (let unrestricted skip = (bytes-cons (nat-to-byte q) b"seal-hex-digit") in (sealLoad32 sealRAX sealR9 (sealH (naturalDivideUnchecked q 8)) (sealShr sealRAX (naturalMultiply 4 (naturalSaturatingSubtract 7 (naturalModuloUnchecked q 8))) (sealAndImm sealRAX 15 (sealCmpImm sealRAX 10 (sealJumpIf (constructor TelemetrySealCondition TelemetrySealBelow) skip (sealAddImm sealRAX 39 (sealLabel skip (sealAddImm sealRAX 48 (sealStore8 sealRDX q sealRAX rest)))))))))))) in (let unrestricted sealSaveRegisters = (lambda unrestricted rest : A . (sealStore64 sealR9 (sealSaved 0) sealRBX (sealStore64 sealR9 (sealSaved 1) sealR12 (sealStore64 sealR9 (sealSaved 2) sealR13 (sealStore64 sealR9 (sealSaved 3) sealR14 (sealStore64 sealR9 (sealSaved 4) sealR15 rest)))))) in (let unrestricted sealRestoreRegisters = (lambda unrestricted rest : A . (sealLoad64 sealRBX sealR9 (sealSaved 0) (sealLoad64 sealR12 sealR9 (sealSaved 1) (sealLoad64 sealR13 sealR9 (sealSaved 2) (sealLoad64 sealR14 sealR9 (sealSaved 3) (sealLoad64 sealR15 sealR9 (sealSaved 4) rest)))))) in (sealSaveRegisters -- the clock reading into the body: seconds * 1e9 + nanoseconds (sealLoad64 sealRAX sealR8 0 (sealMulImm sealRAX 1000000000 (sealLoad64 sealRBX sealR8 8 (sealAdd sealRAX sealRBX (sealStore64 sealRDI sealMonotonicAt sealRAX -- the constants, the initial hash; r15 keeps the body's start (sealFor 64 (lambda unrestricted t : Nat . (sealConstant (sealK t) (sealAt sealRoundConstants t))) (sealFor 8 (lambda unrestricted i : Nat . (sealConstant (sealH i) (sealAt sealInitialHash i))) (sealMov sealR15 sealRDI (sealLabel b"seal-block" (sealFor 16 sealMessageWord (sealFor 48 sealScheduleWord (sealFor 8 sealLoadVariable (sealFor 64 sealRound (sealFor 8 sealAccumulate (sealAddImm sealRDI 64 (sealAddImm sealRSI 0xFFFFFFFF (sealJumpIf (constructor TelemetrySealCondition TelemetrySealNotZero) b"seal-block" -- the body into the record after "ALPHATEL", rdx left after it (sealAddImm sealRDX 8 (sealLabel b"seal-copy" (sealLoad8 sealRAX sealR15 0 (sealStore8 sealRDX 0 sealRAX (sealAddImm sealR15 1 (sealAddImm sealRDX 1 (sealAddImm sealRCX 0xFFFFFFFF (sealJumpIf (constructor TelemetrySealCondition TelemetrySealNotZero) b"seal-copy" -- the digest's 64 hex digits (sealFor 64 sealHexDigit (sealRestoreRegisters (sealReturn sealEnd))))))))))))))))))))))))))))))))))))))))))))))