module Data.SHA256 import Model.Config import Model.Parameter import Std.Byte import Std.Foundation import Std.Natural family SHA256State : Type 0 constructor SHA256StateValue field unrestricted sha256StateWord0 : (family ModelWord32) field unrestricted sha256StateWord1 : (family ModelWord32) field unrestricted sha256StateWord2 : (family ModelWord32) field unrestricted sha256StateWord3 : (family ModelWord32) field unrestricted sha256StateWord4 : (family ModelWord32) field unrestricted sha256StateWord5 : (family ModelWord32) field unrestricted sha256StateWord6 : (family ModelWord32) field unrestricted sha256StateWord7 : (family ModelWord32) end-family family SHA256Schedule : Type 0 constructor SHA256ScheduleEnd constructor SHA256ScheduleNext field unrestricted sha256ScheduleWord : (family ModelWord32) recursive unrestricted sha256ScheduleTail end-family family SHA256Context : Type 0 constructor SHA256ContextValue field unrestricted sha256ContextState : (family SHA256State) field unrestricted sha256ContextTotalBytes : (family ModelWord64) field unrestricted sha256ContextPendingBytes : Bytes end-family family SHA256DigestLengthValidity : Type 0 constructor SHA256DigestLengthValid constructor SHA256DigestLengthInvalid end-family family SHA256Digest : Type 0 constructor SHA256DigestValue field unrestricted sha256DigestBytes : Bytes field erased sha256DigestLengthProof : (equal (family SHA256DigestLengthValidity) (nat-eliminate (lambda unrestricted equalLength : Nat . (family SHA256DigestLengthValidity)) (constructor SHA256DigestLengthValidity SHA256DigestLengthInvalid) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SHA256DigestLengthValidity) . (constructor SHA256DigestLengthValidity SHA256DigestLengthValid))) (naturalEqual (bytes-length sha256DigestBytes) (byte-to-nat (byte 32)))) (constructor SHA256DigestLengthValidity SHA256DigestLengthValid)) end-family family SHA256CompressionInput : Type 0 constructor SHA256CompressionInputValue field unrestricted sha256CompressionState : (family SHA256State) field unrestricted sha256CompressionBlock : Bytes end-family family SHA256RoundInput : Type 0 constructor SHA256RoundInputValue field unrestricted sha256RoundIndex : (family ModelWord32) field unrestricted sha256RoundConstant : (family ModelWord32) field unrestricted sha256RoundScheduleWord : (family ModelWord32) field unrestricted sha256RoundA : (family ModelWord32) field unrestricted sha256RoundB : (family ModelWord32) field unrestricted sha256RoundC : (family ModelWord32) field unrestricted sha256RoundD : (family ModelWord32) field unrestricted sha256RoundE : (family ModelWord32) field unrestricted sha256RoundF : (family ModelWord32) field unrestricted sha256RoundG : (family ModelWord32) field unrestricted sha256RoundH : (family ModelWord32) end-family family SHA256ErrorCode : Type 0 constructor SHA256InputLengthOverflow constructor SHA256PendingBlockTooLarge constructor SHA256ContextLengthMismatch constructor SHA256BlockLengthInvalid constructor SHA256ScheduleLengthInvalid constructor SHA256RoundCountInvalid constructor SHA256DigestLengthInvalid constructor SHA256LengthEncodingInvalid constructor SHA256PaddingLengthInvalid constructor SHA256FileOpenFailed constructor SHA256FileReadFailed constructor SHA256FileCloseFailed constructor SHA256DigestHexInvalid end-family family SHA256Result : Type 0 constructor SHA256Succeeded field unrestricted sha256ResultDigest : (family SHA256Digest) constructor SHA256Failed field unrestricted sha256ResultError : (family SHA256ErrorCode) end-family def sha256ErrorCodeBytes = (lambda unrestricted code : (family SHA256ErrorCode) . (eliminate SHA256ErrorCode (lambda unrestricted current : (family SHA256ErrorCode) . Bytes) code (branch SHA256InputLengthOverflow . b"ALPHA-SHA256-001") (branch SHA256PendingBlockTooLarge . b"ALPHA-SHA256-002") (branch SHA256ContextLengthMismatch . b"ALPHA-SHA256-003") (branch SHA256BlockLengthInvalid . b"ALPHA-SHA256-004") (branch SHA256ScheduleLengthInvalid . b"ALPHA-SHA256-005") (branch SHA256RoundCountInvalid . b"ALPHA-SHA256-006") (branch SHA256DigestLengthInvalid . b"ALPHA-SHA256-007") (branch SHA256LengthEncodingInvalid . b"ALPHA-SHA256-008") (branch SHA256PaddingLengthInvalid . b"ALPHA-SHA256-009") (branch SHA256FileOpenFailed . b"ALPHA-SHA256-010") (branch SHA256FileReadFailed . b"ALPHA-SHA256-011") (branch SHA256FileCloseFailed . b"ALPHA-SHA256-012") (branch SHA256DigestHexInvalid . b"ALPHA-SHA256-013"))) -- The only public Bytes -> SHA256Digest boundary. The equality witness is -- erased, but the ordinary kernel still checks that construction is possible -- only when the byte sequence is exactly 32 bytes long. def sha256DigestFromBytes : (pi unrestricted input : Bytes . (family SHA256Result)) = (lambda unrestricted input : Bytes . (app (eliminate SHA256DigestLengthValidity (lambda unrestricted decision : (family SHA256DigestLengthValidity) . (pi erased witness : (equal (family SHA256DigestLengthValidity) (nat-eliminate (lambda unrestricted equalLength : Nat . (family SHA256DigestLengthValidity)) (constructor SHA256DigestLengthValidity SHA256DigestLengthInvalid) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SHA256DigestLengthValidity) . (constructor SHA256DigestLengthValidity SHA256DigestLengthValid))) (naturalEqual (bytes-length input) (byte-to-nat (byte 32)))) decision) . (family SHA256Result))) (nat-eliminate (lambda unrestricted equalLength : Nat . (family SHA256DigestLengthValidity)) (constructor SHA256DigestLengthValidity SHA256DigestLengthInvalid) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SHA256DigestLengthValidity) . (constructor SHA256DigestLengthValidity SHA256DigestLengthValid))) (naturalEqual (bytes-length input) (byte-to-nat (byte 32)))) (branch SHA256DigestLengthValid . (lambda erased witness : (equal (family SHA256DigestLengthValidity) (nat-eliminate (lambda unrestricted equalLength : Nat . (family SHA256DigestLengthValidity)) (constructor SHA256DigestLengthValidity SHA256DigestLengthInvalid) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SHA256DigestLengthValidity) . (constructor SHA256DigestLengthValidity SHA256DigestLengthValid))) (naturalEqual (bytes-length input) (byte-to-nat (byte 32)))) (constructor SHA256DigestLengthValidity SHA256DigestLengthValid)) . (constructor SHA256Result SHA256Succeeded (constructor SHA256Digest SHA256DigestValue input witness)))) (branch SHA256DigestLengthInvalid . (lambda erased witness : (equal (family SHA256DigestLengthValidity) (nat-eliminate (lambda unrestricted equalLength : Nat . (family SHA256DigestLengthValidity)) (constructor SHA256DigestLengthValidity SHA256DigestLengthInvalid) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SHA256DigestLengthValidity) . (constructor SHA256DigestLengthValidity SHA256DigestLengthValid))) (naturalEqual (bytes-length input) (byte-to-nat (byte 32)))) (constructor SHA256DigestLengthValidity SHA256DigestLengthInvalid)) . (constructor SHA256Result SHA256Failed (constructor SHA256ErrorCode SHA256DigestLengthInvalid))))) (refl (family SHA256DigestLengthValidity) (nat-eliminate (lambda unrestricted equalLength : Nat . (family SHA256DigestLengthValidity)) (constructor SHA256DigestLengthValidity SHA256DigestLengthInvalid) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SHA256DigestLengthValidity) . (constructor SHA256DigestLengthValidity SHA256DigestLengthValid))) (naturalEqual (bytes-length input) (byte-to-nat (byte 32))))))) def sha256DigestToBytes = (lambda unrestricted digest : (family SHA256Digest) . (eliminate SHA256Digest (lambda unrestricted current : (family SHA256Digest) . Bytes) digest (branch SHA256DigestValue bytes proof . bytes))) def sha256DigestEqual = (lambda unrestricted left : (family SHA256Digest) . (lambda unrestricted right : (family SHA256Digest) . (bytes-equal (sha256DigestToBytes left) (sha256DigestToBytes right)))) def sha256InitialState = (constructor SHA256State SHA256StateValue (constructor ModelWord32 ModelWord32Value (byte 103) (byte 230) (byte 9) (byte 106)) (constructor ModelWord32 ModelWord32Value (byte 133) (byte 174) (byte 103) (byte 187)) (constructor ModelWord32 ModelWord32Value (byte 114) (byte 243) (byte 110) (byte 60)) (constructor ModelWord32 ModelWord32Value (byte 58) (byte 245) (byte 79) (byte 165)) (constructor ModelWord32 ModelWord32Value (byte 127) (byte 82) (byte 14) (byte 81)) (constructor ModelWord32 ModelWord32Value (byte 140) (byte 104) (byte 5) (byte 155)) (constructor ModelWord32 ModelWord32Value (byte 171) (byte 217) (byte 131) (byte 31)) (constructor ModelWord32 ModelWord32Value (byte 25) (byte 205) (byte 224) (byte 91))) def sha256InitialContext = (constructor SHA256Context SHA256ContextValue sha256InitialState (constructor ModelWord64 ModelWord64Value (byte 0) (byte 0) (byte 0) (byte 0) (byte 0) (byte 0) (byte 0) (byte 0)) b"") def sha256MaximumInputBytes = (constructor ModelWord64 ModelWord64Value (byte 255) (byte 255) (byte 255) (byte 255) (byte 255) (byte 255) (byte 255) (byte 31)) def sha256Word64Eight = (constructor ModelWord64 ModelWord64Value (byte 8) (byte 0) (byte 0) (byte 0) (byte 0) (byte 0) (byte 0) (byte 0)) def sha256BlockBytes = (constructor ModelWord32 ModelWord32Value (byte 64) (byte 0) (byte 0) (byte 0)) def sha256ScheduleWords = (constructor ModelWord32 ModelWord32Value (byte 64) (byte 0) (byte 0) (byte 0)) def sha256DigestBytes = (constructor ModelWord32 ModelWord32Value (byte 32) (byte 0) (byte 0) (byte 0))