module Data.SHA256Digest import Data.Bytes import Data.SHA256 import Data.SHA256Compress import Data.SHA256Padding import Data.SHA256Schedule import Model.Parameter import Model.Word64 import Std.Foundation import Std.Natural family SHA256DigestTelemetry : Type 0 constructor SHA256DigestTelemetryValue field unrestricted sha256DigestTelemetryInputBytes : Nat field unrestricted sha256DigestTelemetryPaddedBytes : Nat field unrestricted sha256DigestTelemetryBlocks : Nat field unrestricted sha256DigestTelemetryDecodedWords : Nat field unrestricted sha256DigestTelemetryExpandedWords : Nat field unrestricted sha256DigestTelemetryRounds : Nat field unrestricted sha256DigestTelemetryLookups : Nat field unrestricted sha256DigestTelemetrySigmas : Nat field unrestricted sha256DigestTelemetryRotates : Nat field unrestricted sha256DigestTelemetryShifts : Nat field unrestricted sha256DigestTelemetryBooleans : Nat field unrestricted sha256DigestTelemetryAdds : Nat end-family family SHA256DigestBlockRunResult : Type 0 constructor SHA256DigestBlocksSucceeded field unrestricted sha256DigestBlockState : (family SHA256State) field unrestricted sha256DigestBlockTelemetry : (family SHA256DigestTelemetry) constructor SHA256DigestBlocksFailed field unrestricted sha256DigestBlockError : (family SHA256ErrorCode) field unrestricted sha256DigestBlockFailureOrdinal : Nat field unrestricted sha256DigestBlockFailureInternalIndex : Nat field unrestricted sha256DigestBlockTelemetryBeforeFailure : (family SHA256DigestTelemetry) end-family family SHA256DigestGroupResult : Type 0 constructor SHA256DigestGroupSucceeded field unrestricted sha256DigestGroupState : (family SHA256State) field unrestricted sha256DigestGroupRemaining : Bytes field unrestricted sha256DigestGroupTelemetry : (family SHA256DigestTelemetry) constructor SHA256DigestGroupFailed field unrestricted sha256DigestGroupError : (family SHA256ErrorCode) field unrestricted sha256DigestGroupFailureOrdinal : Nat field unrestricted sha256DigestGroupFailureInternalIndex : Nat field unrestricted sha256DigestGroupTelemetryBeforeFailure : (family SHA256DigestTelemetry) end-family family SHA256DigestExecutionResult : Type 0 constructor SHA256DigestExecutionSucceeded field unrestricted sha256DigestExecutionDigest : (family SHA256Digest) field unrestricted sha256DigestExecutionTelemetry : (family SHA256DigestTelemetry) constructor SHA256DigestExecutionFailed field unrestricted sha256DigestExecutionError : (family SHA256ErrorCode) field unrestricted sha256DigestExecutionFailureOrdinal : Nat field unrestricted sha256DigestExecutionTelemetryBeforeFailure : (family SHA256DigestTelemetry) end-family family SHA256HexResult : Type 0 constructor SHA256HexSucceeded field unrestricted sha256HexBytes : Bytes field unrestricted sha256HexTelemetry : (family SHA256DigestTelemetry) constructor SHA256HexFailed field unrestricted sha256HexError : (family SHA256ErrorCode) field unrestricted sha256HexFailureOrdinal : Nat field unrestricted sha256HexTelemetryBeforeFailure : (family SHA256DigestTelemetry) end-family family SHA256NaturalWord64Result : Type 0 constructor SHA256NaturalWord64Succeeded field unrestricted sha256NaturalWord64Value : (family ModelWord64) constructor SHA256NaturalWord64Failed field unrestricted sha256NaturalWord64Error : (family SHA256ErrorCode) end-family family SHA256UpdateTelemetry : Type 0 constructor SHA256UpdateTelemetryValue field unrestricted sha256UpdateInputBytes : Nat field unrestricted sha256UpdateTotalBytesBefore : (family ModelWord64) field unrestricted sha256UpdatePendingBytesBefore : Nat field unrestricted sha256UpdateCombinedBytes : Nat field unrestricted sha256UpdateCompressedBytes : Nat field unrestricted sha256UpdateCompressedBlocks : Nat field unrestricted sha256UpdatePendingBytesAfter : Nat field unrestricted sha256UpdateTotalBytesAfter : (family ModelWord64) field unrestricted sha256UpdateCompressionTelemetry : (family SHA256DigestTelemetry) end-family family SHA256ContextUpdateResult : Type 0 constructor SHA256ContextUpdateSucceeded field unrestricted sha256UpdatedContext : (family SHA256Context) field unrestricted sha256UpdateTelemetry : (family SHA256UpdateTelemetry) constructor SHA256ContextUpdateFailed field unrestricted sha256UpdateError : (family SHA256ErrorCode) field unrestricted sha256UpdateFailureOrdinal : Nat field unrestricted sha256UpdateFailureInternalIndex : Nat field unrestricted sha256UpdateTelemetryBeforeFailure : (family SHA256DigestTelemetry) end-family family SHA256FinalizeTelemetry : Type 0 constructor SHA256FinalizeTelemetryValue field unrestricted sha256FinalizeTotalBytes : (family ModelWord64) field unrestricted sha256FinalizePendingBytes : Nat field unrestricted sha256FinalizeBitLength : (family ModelWord64) field unrestricted sha256FinalizeZeroBytes : Nat field unrestricted sha256FinalizeCompressedBytes : Nat field unrestricted sha256FinalizeCompressedBlocks : Nat field unrestricted sha256FinalizeDigestBytes : Nat field unrestricted sha256FinalizeCompressionTelemetry : (family SHA256DigestTelemetry) end-family family SHA256ContextFinalizeResult : Type 0 constructor SHA256ContextFinalizeSucceeded field unrestricted sha256FinalizedDigest : (family SHA256Digest) field unrestricted sha256FinalizeTelemetry : (family SHA256FinalizeTelemetry) constructor SHA256ContextFinalizeFailed field unrestricted sha256FinalizeError : (family SHA256ErrorCode) field unrestricted sha256FinalizeFailureOrdinal : Nat field unrestricted sha256FinalizeFailureInternalIndex : Nat field unrestricted sha256FinalizeTelemetryBeforeFailure : (family SHA256DigestTelemetry) end-family family SHA256DigestIdentity : Type 0 constructor SHA256DigestIdentityValue field unrestricted sha256DigestIdentityBinary : (family SHA256Digest) end-family family SHA256DigestIdentityResult : Type 0 constructor SHA256DigestIdentitySucceeded field unrestricted sha256ValidatedDigestIdentity : (family SHA256DigestIdentity) constructor SHA256DigestIdentityFailed field unrestricted sha256DigestIdentityError : (family SHA256ErrorCode) end-family -- A first-order split of a byte string into a taken prefix and the rest, used to -- slice fixed-size blocks without a function-valued fold or bytes-eliminate. family SHA256BytesSplit : Type 0 constructor SHA256BytesSplitValue field unrestricted sha256BytesSplitTaken : Bytes field unrestricted sha256BytesSplitRest : Bytes end-family -- Field projection for `sha256DigestTelemetryAdds`, generated from the declaration: the family -- has one constructor, so this is the unique total projection. def sha256DigestTelemetryAdds = (lambda unrestricted value : (family SHA256DigestTelemetry) . (eliminate SHA256DigestTelemetry (lambda unrestricted current : (family SHA256DigestTelemetry) . Nat) value (branch SHA256DigestTelemetryValue sha256DigestTelemetryInputBytes sha256DigestTelemetryPaddedBytes sha256DigestTelemetryBlocks sha256DigestTelemetryDecodedWords sha256DigestTelemetryExpandedWords sha256DigestTelemetryRounds sha256DigestTelemetryLookups sha256DigestTelemetrySigmas sha256DigestTelemetryRotates sha256DigestTelemetryShifts sha256DigestTelemetryBooleans sha256DigestTelemetryAdds . sha256DigestTelemetryAdds))) -- Field projection for `sha256DigestTelemetryBooleans`, generated from the declaration: the family -- has one constructor, so this is the unique total projection. def sha256DigestTelemetryBooleans = (lambda unrestricted value : (family SHA256DigestTelemetry) . (eliminate SHA256DigestTelemetry (lambda unrestricted current : (family SHA256DigestTelemetry) . Nat) value (branch SHA256DigestTelemetryValue sha256DigestTelemetryInputBytes sha256DigestTelemetryPaddedBytes sha256DigestTelemetryBlocks sha256DigestTelemetryDecodedWords sha256DigestTelemetryExpandedWords sha256DigestTelemetryRounds sha256DigestTelemetryLookups sha256DigestTelemetrySigmas sha256DigestTelemetryRotates sha256DigestTelemetryShifts sha256DigestTelemetryBooleans sha256DigestTelemetryAdds . sha256DigestTelemetryBooleans))) -- Field projection for `sha256DigestTelemetryDecodedWords`, generated from the declaration: the family -- has one constructor, so this is the unique total projection. def sha256DigestTelemetryDecodedWords = (lambda unrestricted value : (family SHA256DigestTelemetry) . (eliminate SHA256DigestTelemetry (lambda unrestricted current : (family SHA256DigestTelemetry) . Nat) value (branch SHA256DigestTelemetryValue sha256DigestTelemetryInputBytes sha256DigestTelemetryPaddedBytes sha256DigestTelemetryBlocks sha256DigestTelemetryDecodedWords sha256DigestTelemetryExpandedWords sha256DigestTelemetryRounds sha256DigestTelemetryLookups sha256DigestTelemetrySigmas sha256DigestTelemetryRotates sha256DigestTelemetryShifts sha256DigestTelemetryBooleans sha256DigestTelemetryAdds . sha256DigestTelemetryDecodedWords))) -- Field projection for `sha256DigestTelemetryExpandedWords`, generated from the declaration: the family -- has one constructor, so this is the unique total projection. def sha256DigestTelemetryExpandedWords = (lambda unrestricted value : (family SHA256DigestTelemetry) . (eliminate SHA256DigestTelemetry (lambda unrestricted current : (family SHA256DigestTelemetry) . Nat) value (branch SHA256DigestTelemetryValue sha256DigestTelemetryInputBytes sha256DigestTelemetryPaddedBytes sha256DigestTelemetryBlocks sha256DigestTelemetryDecodedWords sha256DigestTelemetryExpandedWords sha256DigestTelemetryRounds sha256DigestTelemetryLookups sha256DigestTelemetrySigmas sha256DigestTelemetryRotates sha256DigestTelemetryShifts sha256DigestTelemetryBooleans sha256DigestTelemetryAdds . sha256DigestTelemetryExpandedWords))) -- Field projection for `sha256DigestTelemetryInputBytes`, generated from the declaration: the family -- has one constructor, so this is the unique total projection. def sha256DigestTelemetryInputBytes = (lambda unrestricted value : (family SHA256DigestTelemetry) . (eliminate SHA256DigestTelemetry (lambda unrestricted current : (family SHA256DigestTelemetry) . Nat) value (branch SHA256DigestTelemetryValue sha256DigestTelemetryInputBytes sha256DigestTelemetryPaddedBytes sha256DigestTelemetryBlocks sha256DigestTelemetryDecodedWords sha256DigestTelemetryExpandedWords sha256DigestTelemetryRounds sha256DigestTelemetryLookups sha256DigestTelemetrySigmas sha256DigestTelemetryRotates sha256DigestTelemetryShifts sha256DigestTelemetryBooleans sha256DigestTelemetryAdds . sha256DigestTelemetryInputBytes))) -- Field projection for `sha256DigestTelemetryLookups`, generated from the declaration: the family -- has one constructor, so this is the unique total projection. def sha256DigestTelemetryLookups = (lambda unrestricted value : (family SHA256DigestTelemetry) . (eliminate SHA256DigestTelemetry (lambda unrestricted current : (family SHA256DigestTelemetry) . Nat) value (branch SHA256DigestTelemetryValue sha256DigestTelemetryInputBytes sha256DigestTelemetryPaddedBytes sha256DigestTelemetryBlocks sha256DigestTelemetryDecodedWords sha256DigestTelemetryExpandedWords sha256DigestTelemetryRounds sha256DigestTelemetryLookups sha256DigestTelemetrySigmas sha256DigestTelemetryRotates sha256DigestTelemetryShifts sha256DigestTelemetryBooleans sha256DigestTelemetryAdds . sha256DigestTelemetryLookups))) -- Field projection for `sha256DigestTelemetryPaddedBytes`, generated from the declaration: the family -- has one constructor, so this is the unique total projection. def sha256DigestTelemetryPaddedBytes = (lambda unrestricted value : (family SHA256DigestTelemetry) . (eliminate SHA256DigestTelemetry (lambda unrestricted current : (family SHA256DigestTelemetry) . Nat) value (branch SHA256DigestTelemetryValue sha256DigestTelemetryInputBytes sha256DigestTelemetryPaddedBytes sha256DigestTelemetryBlocks sha256DigestTelemetryDecodedWords sha256DigestTelemetryExpandedWords sha256DigestTelemetryRounds sha256DigestTelemetryLookups sha256DigestTelemetrySigmas sha256DigestTelemetryRotates sha256DigestTelemetryShifts sha256DigestTelemetryBooleans sha256DigestTelemetryAdds . sha256DigestTelemetryPaddedBytes))) -- Field projection for `sha256DigestTelemetryRotates`, generated from the declaration: the family -- has one constructor, so this is the unique total projection. def sha256DigestTelemetryRotates = (lambda unrestricted value : (family SHA256DigestTelemetry) . (eliminate SHA256DigestTelemetry (lambda unrestricted current : (family SHA256DigestTelemetry) . Nat) value (branch SHA256DigestTelemetryValue sha256DigestTelemetryInputBytes sha256DigestTelemetryPaddedBytes sha256DigestTelemetryBlocks sha256DigestTelemetryDecodedWords sha256DigestTelemetryExpandedWords sha256DigestTelemetryRounds sha256DigestTelemetryLookups sha256DigestTelemetrySigmas sha256DigestTelemetryRotates sha256DigestTelemetryShifts sha256DigestTelemetryBooleans sha256DigestTelemetryAdds . sha256DigestTelemetryRotates))) -- Field projection for `sha256DigestTelemetryRounds`, generated from the declaration: the family -- has one constructor, so this is the unique total projection. def sha256DigestTelemetryRounds = (lambda unrestricted value : (family SHA256DigestTelemetry) . (eliminate SHA256DigestTelemetry (lambda unrestricted current : (family SHA256DigestTelemetry) . Nat) value (branch SHA256DigestTelemetryValue sha256DigestTelemetryInputBytes sha256DigestTelemetryPaddedBytes sha256DigestTelemetryBlocks sha256DigestTelemetryDecodedWords sha256DigestTelemetryExpandedWords sha256DigestTelemetryRounds sha256DigestTelemetryLookups sha256DigestTelemetrySigmas sha256DigestTelemetryRotates sha256DigestTelemetryShifts sha256DigestTelemetryBooleans sha256DigestTelemetryAdds . sha256DigestTelemetryRounds))) -- Field projection for `sha256DigestTelemetryShifts`, generated from the declaration: the family -- has one constructor, so this is the unique total projection. def sha256DigestTelemetryShifts = (lambda unrestricted value : (family SHA256DigestTelemetry) . (eliminate SHA256DigestTelemetry (lambda unrestricted current : (family SHA256DigestTelemetry) . Nat) value (branch SHA256DigestTelemetryValue sha256DigestTelemetryInputBytes sha256DigestTelemetryPaddedBytes sha256DigestTelemetryBlocks sha256DigestTelemetryDecodedWords sha256DigestTelemetryExpandedWords sha256DigestTelemetryRounds sha256DigestTelemetryLookups sha256DigestTelemetrySigmas sha256DigestTelemetryRotates sha256DigestTelemetryShifts sha256DigestTelemetryBooleans sha256DigestTelemetryAdds . sha256DigestTelemetryShifts))) -- Field projection for `sha256DigestTelemetrySigmas`, generated from the declaration: the family -- has one constructor, so this is the unique total projection. def sha256DigestTelemetrySigmas = (lambda unrestricted value : (family SHA256DigestTelemetry) . (eliminate SHA256DigestTelemetry (lambda unrestricted current : (family SHA256DigestTelemetry) . Nat) value (branch SHA256DigestTelemetryValue sha256DigestTelemetryInputBytes sha256DigestTelemetryPaddedBytes sha256DigestTelemetryBlocks sha256DigestTelemetryDecodedWords sha256DigestTelemetryExpandedWords sha256DigestTelemetryRounds sha256DigestTelemetryLookups sha256DigestTelemetrySigmas sha256DigestTelemetryRotates sha256DigestTelemetryShifts sha256DigestTelemetryBooleans sha256DigestTelemetryAdds . sha256DigestTelemetrySigmas))) -- Field projection (fields do not create definitions). def sha256DigestTelemetryBlocks = (lambda unrestricted value : (family SHA256DigestTelemetry) . (eliminate SHA256DigestTelemetry (lambda unrestricted current : (family SHA256DigestTelemetry) . Nat) value (branch SHA256DigestTelemetryValue sha256DigestTelemetryInputBytes sha256DigestTelemetryPaddedBytes sha256DigestTelemetryBlocksField sha256DigestTelemetryDecodedWords sha256DigestTelemetryExpandedWords sha256DigestTelemetryRounds sha256DigestTelemetryLookups sha256DigestTelemetrySigmas sha256DigestTelemetryRotates sha256DigestTelemetryShifts sha256DigestTelemetryBooleans sha256DigestTelemetryAdds . sha256DigestTelemetryBlocksField))) def sha256DigestTelemetryInitial = (lambda unrestricted inputBytes : Nat . (lambda unrestricted paddedBytes : Nat . (constructor SHA256DigestTelemetry SHA256DigestTelemetryValue inputBytes paddedBytes zero zero zero zero zero zero zero zero zero zero))) -- The per-block counts come FIRST: `naturalAdd` folds over its first argument, -- so adding the running total the other way round made every block cost the -- total so far (quadratic; D17 measurement: 27 min for 240 KB). def sha256DigestTelemetryAddCompression = (lambda unrestricted telemetry : (family SHA256DigestTelemetry) . (lambda unrestricted compression : (family SHA256CompressionTelemetry) . (eliminate SHA256DigestTelemetry (lambda unrestricted current : (family SHA256DigestTelemetry) . (family SHA256DigestTelemetry)) telemetry (branch SHA256DigestTelemetryValue inputBytes paddedBytes blocks decoded expanded rounds lookups sigmas rotates shifts booleans adds . (eliminate SHA256CompressionTelemetry (lambda unrestricted current : (family SHA256CompressionTelemetry) . (family SHA256DigestTelemetry)) compression (branch SHA256CompressionTelemetryValue nextDecoded nextExpanded nextRounds nextLookups nextSigmas nextRotates nextShifts nextBooleans nextAdds . (constructor SHA256DigestTelemetry SHA256DigestTelemetryValue inputBytes paddedBytes (succ blocks) (naturalAdd nextDecoded decoded) (naturalAdd nextExpanded expanded) (naturalAdd nextRounds rounds) (naturalAdd nextLookups lookups) (naturalAdd nextSigmas sigmas) (naturalAdd nextRotates rotates) (naturalAdd nextShifts shifts) (naturalAdd nextBooleans booleans) (naturalAdd nextAdds adds)))))))) def sha256DigestTelemetryCombine = (lambda unrestricted inputBytes : Nat . (lambda unrestricted paddedBytes : Nat . (lambda unrestricted left : (family SHA256DigestTelemetry) . (lambda unrestricted right : (family SHA256DigestTelemetry) . (eliminate SHA256DigestTelemetry (lambda unrestricted current : (family SHA256DigestTelemetry) . (family SHA256DigestTelemetry)) left (branch SHA256DigestTelemetryValue leftInput leftPadded leftBlocks leftDecoded leftExpanded leftRounds leftLookups leftSigmas leftRotates leftShifts leftBooleans leftAdds . (eliminate SHA256DigestTelemetry (lambda unrestricted current : (family SHA256DigestTelemetry) . (family SHA256DigestTelemetry)) right (branch SHA256DigestTelemetryValue rightInput rightPadded rightBlocks rightDecoded rightExpanded rightRounds rightLookups rightSigmas rightRotates rightShifts rightBooleans rightAdds . (constructor SHA256DigestTelemetry SHA256DigestTelemetryValue inputBytes paddedBytes (naturalAdd leftBlocks rightBlocks) (naturalAdd leftDecoded rightDecoded) (naturalAdd leftExpanded rightExpanded) (naturalAdd leftRounds rightRounds) (naturalAdd leftLookups rightLookups) (naturalAdd leftSigmas rightSigmas) (naturalAdd leftRotates rightRotates) (naturalAdd leftShifts rightShifts) (naturalAdd leftBooleans rightBooleans) (naturalAdd leftAdds rightAdds)))))))))) def sha256DigestTelemetryBlockCount = (lambda unrestricted telemetry : (family SHA256DigestTelemetry) . (eliminate SHA256DigestTelemetry (lambda unrestricted current : (family SHA256DigestTelemetry) . Nat) telemetry (branch SHA256DigestTelemetryValue input padded blocks decoded expanded rounds lookups sigmas rotates shifts booleans adds . blocks))) def sha256DigestTelemetryPaddedCount = (lambda unrestricted telemetry : (family SHA256DigestTelemetry) . (eliminate SHA256DigestTelemetry (lambda unrestricted current : (family SHA256DigestTelemetry) . Nat) telemetry (branch SHA256DigestTelemetryValue input padded blocks decoded expanded rounds lookups sigmas rotates shifts booleans adds . padded))) -- First-order prefix take. -- -- The previous definition folded a FUNCTION accumulator (`pi input . Bytes`) and, -- worse, used `bytes-eliminate` inside the step. The VM's bytes recursor EAGERLY -- evaluates the tail's recursive result before the branch (which ignores it) -- runs, so composing it under the fuel fold re-walked every suffix at every -- level -- an exponential that made even `take 64` of a 64-byte LITERAL cost -- minutes and gigabytes, which then fed a non-literal block into decode/expand -- and blew those up in turn. This version folds a FIRST-ORDER value accumulator -- (taken prefix + remaining bytes) built only from the O(1) native primitives -- bytes-head / bytes-tail / bytes-cons / bytes-append, so a take over a literal -- stays a literal and costs O(fuel^2) bounded work. For the 64-aligned blocks the -- digest driver slices, the bytes produced are identical, so the digest is -- preserved exactly. def sha256DigestTakeWithFuel = (lambda unrestricted fuel : Nat . (lambda unrestricted input : Bytes . (eliminate SHA256BytesSplit (lambda unrestricted current : (family SHA256BytesSplit) . Bytes) (nat-eliminate (lambda unrestricted current : Nat . (family SHA256BytesSplit)) (constructor SHA256BytesSplit SHA256BytesSplitValue b"" input) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SHA256BytesSplit) . (eliminate SHA256BytesSplit (lambda unrestricted current : (family SHA256BytesSplit) . (family SHA256BytesSplit)) induction (branch SHA256BytesSplitValue taken rest . (constructor SHA256BytesSplit SHA256BytesSplitValue (bytes-append taken (bytes-cons (bytes-head rest) b"")) (bytes-tail rest)))))) fuel) (branch SHA256BytesSplitValue taken rest . taken)))) -- First-order drop: peel `fuel` bytes with the native O(1) bytes-tail instead of -- the higher-order `bytes-eliminate` fold (same exponential as take above). On a -- literal the result stays a literal. def sha256DigestDropWithFuel = (lambda unrestricted fuel : Nat . (lambda unrestricted input : Bytes . (nat-eliminate (lambda unrestricted current : Nat . Bytes) input (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Bytes . (bytes-tail induction))) fuel))) -- D18: the block loop runs as an outer fold over GROUPS of blocks with an -- inner fold over one group, so the garbage of a group is reclaimed when the -- group ends instead of the whole message's garbage staying resident (the -- flat loop held 8.7 GB for a 240 KB message). def sha256DigestBlocksPerGroup : Nat = 32 -- Compress `count` blocks off the front of `input`, returning the state and -- what is left (no length check: the caller sizes the groups). def sha256DigestRunBlockGroup = (lambda unrestricted count : Nat . (nat-eliminate (lambda unrestricted current : Nat . (pi unrestricted state : (family SHA256State) . (pi unrestricted input : Bytes . (pi unrestricted telemetry : (family SHA256DigestTelemetry) . (family SHA256DigestGroupResult))))) (lambda unrestricted state : (family SHA256State) . (lambda unrestricted input : Bytes . (lambda unrestricted telemetry : (family SHA256DigestTelemetry) . (constructor SHA256DigestGroupResult SHA256DigestGroupSucceeded state input telemetry)))) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (pi unrestricted state : (family SHA256State) . (pi unrestricted input : Bytes . (pi unrestricted telemetry : (family SHA256DigestTelemetry) . (family SHA256DigestGroupResult)))) . (lambda unrestricted state : (family SHA256State) . (lambda unrestricted input : Bytes . (lambda unrestricted telemetry : (family SHA256DigestTelemetry) . (eliminate SHA256CompressionResult (lambda unrestricted current : (family SHA256CompressionResult) . (family SHA256DigestGroupResult)) (sha256CompressBlock state (sha256DigestTakeWithFuel sha256NaturalSixtyFour input)) (branch SHA256CompressionSucceeded nextState compressionTelemetry . (induction nextState (sha256DigestDropWithFuel sha256NaturalSixtyFour input) (sha256DigestTelemetryAddCompression telemetry compressionTelemetry))) (branch SHA256CompressionFailed error failedIndex . (constructor SHA256DigestGroupResult SHA256DigestGroupFailed error (sha256DigestTelemetryBlockCount telemetry) failedIndex telemetry)))))))) count)) -- `groups` full groups, then the remainder group of `rest` blocks. def sha256DigestRunBlockGroups = (lambda unrestricted groups : Nat . (lambda unrestricted rest : Nat . (nat-eliminate (lambda unrestricted current : Nat . (pi unrestricted state : (family SHA256State) . (pi unrestricted input : Bytes . (pi unrestricted telemetry : (family SHA256DigestTelemetry) . (family SHA256DigestGroupResult))))) (sha256DigestRunBlockGroup rest) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (pi unrestricted state : (family SHA256State) . (pi unrestricted input : Bytes . (pi unrestricted telemetry : (family SHA256DigestTelemetry) . (family SHA256DigestGroupResult)))) . (lambda unrestricted state : (family SHA256State) . (lambda unrestricted input : Bytes . (lambda unrestricted telemetry : (family SHA256DigestTelemetry) . (eliminate SHA256DigestGroupResult (lambda unrestricted current : (family SHA256DigestGroupResult) . (family SHA256DigestGroupResult)) (sha256DigestRunBlockGroup sha256DigestBlocksPerGroup state input telemetry) (branch SHA256DigestGroupSucceeded nextState remaining nextTelemetry . (induction nextState remaining nextTelemetry)) (branch SHA256DigestGroupFailed error ordinal internalIndex before . (constructor SHA256DigestGroupResult SHA256DigestGroupFailed error ordinal internalIndex before)))))))) groups))) -- The public shape is unchanged: exactly `blockCount` blocks must consume the -- whole input, or the run fails with SHA256BlockLengthInvalid. def sha256DigestRunBlocks = (lambda unrestricted blockCount : Nat . (lambda unrestricted state : (family SHA256State) . (lambda unrestricted input : Bytes . (lambda unrestricted telemetry : (family SHA256DigestTelemetry) . (eliminate SHA256DigestGroupResult (lambda unrestricted current : (family SHA256DigestGroupResult) . (family SHA256DigestBlockRunResult)) (sha256DigestRunBlockGroups (naturalDivideUnchecked blockCount sha256DigestBlocksPerGroup) (naturalModuloUnchecked blockCount sha256DigestBlocksPerGroup) state input telemetry) (branch SHA256DigestGroupSucceeded finalState remaining finalTelemetry . (nat-eliminate (lambda unrestricted empty : Nat . (family SHA256DigestBlockRunResult)) (constructor SHA256DigestBlockRunResult SHA256DigestBlocksFailed (constructor SHA256ErrorCode SHA256BlockLengthInvalid) (sha256DigestTelemetryBlockCount finalTelemetry) zero finalTelemetry) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SHA256DigestBlockRunResult) . (constructor SHA256DigestBlockRunResult SHA256DigestBlocksSucceeded finalState finalTelemetry))) (naturalIsZero (bytes-length remaining)))) (branch SHA256DigestGroupFailed error ordinal internalIndex before . (constructor SHA256DigestBlockRunResult SHA256DigestBlocksFailed error ordinal internalIndex before))))))) def sha256DigestStateBytes = (lambda unrestricted state : (family SHA256State) . (eliminate SHA256State (lambda unrestricted current : (family SHA256State) . Bytes) state (branch SHA256StateValue w0 w1 w2 w3 w4 w5 w6 w7 . (bytes-builder-build (bytes-builder-append (bytes-builder-chunk (dataBytesWord32BE w0)) (bytes-builder-append (bytes-builder-chunk (dataBytesWord32BE w1)) (bytes-builder-append (bytes-builder-chunk (dataBytesWord32BE w2)) (bytes-builder-append (bytes-builder-chunk (dataBytesWord32BE w3)) (bytes-builder-append (bytes-builder-chunk (dataBytesWord32BE w4)) (bytes-builder-append (bytes-builder-chunk (dataBytesWord32BE w5)) (bytes-builder-append (bytes-builder-chunk (dataBytesWord32BE w6)) (bytes-builder-chunk (dataBytesWord32BE w7))))))))))))) def sha256NaturalToWord64 = (lambda unrestricted value : Nat . (eliminate SHA256LengthEncodingResult (lambda unrestricted current : (family SHA256LengthEncodingResult) . (family SHA256NaturalWord64Result)) (sha256EncodeBitLength value) (branch SHA256LengthEncodingSucceeded encoded encodedValue . (eliminate DataBytesWord64DecodeResult (lambda unrestricted current : (family DataBytesWord64DecodeResult) . (family SHA256NaturalWord64Result)) (dataBytesReadWord64BE encoded) (branch DataBytesWord64Decoded word remaining . (nat-eliminate (lambda unrestricted empty : Nat . (family SHA256NaturalWord64Result)) (constructor SHA256NaturalWord64Result SHA256NaturalWord64Failed (constructor SHA256ErrorCode SHA256LengthEncodingInvalid)) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SHA256NaturalWord64Result) . (constructor SHA256NaturalWord64Result SHA256NaturalWord64Succeeded word))) (naturalIsZero (bytes-length remaining)))) (branch DataBytesWord64DecodeFailed decodeError . (constructor SHA256NaturalWord64Result SHA256NaturalWord64Failed (constructor SHA256ErrorCode SHA256LengthEncodingInvalid))))) (branch SHA256LengthEncodingFailed error remaining . (constructor SHA256NaturalWord64Result SHA256NaturalWord64Failed error)))) -- Part of `sha256Update`, lifted out to keep it inside the §28.3 size and -- nesting limits; the parameters are the locals it still needs. def sha256UpdatePart1 = (lambda unrestricted state : (family SHA256State) . (lambda unrestricted totalBytes : (family ModelWord64) . (lambda unrestricted inputBytes : Nat . (lambda unrestricted nextTotalBytes : (family ModelWord64) . (lambda unrestricted pendingBefore : Nat . (lambda unrestricted combined : Bytes . (lambda unrestricted combinedBytes : Nat . (lambda unrestricted compressedBytes : Nat . (lambda unrestricted compressedBlocks : Nat . (app (lambda unrestricted compressed : Bytes . (app (lambda unrestricted nextPending : Bytes . (app (lambda unrestricted operations : (family SHA256DigestTelemetry) . (eliminate SHA256DigestBlockRunResult (lambda unrestricted current : (family SHA256DigestBlockRunResult) . (family SHA256ContextUpdateResult)) (sha256DigestRunBlocks compressedBlocks state compressed operations) (branch SHA256DigestBlocksSucceeded nextState nextOperations . (app (lambda unrestricted nextContext : (family SHA256Context) . (eliminate SHA256ContextValidationResult (lambda unrestricted current : (family SHA256ContextValidationResult) . (family SHA256ContextUpdateResult)) (sha256ValidateContext nextContext) (branch SHA256ContextValidated checkedContext checkedTelemetry . (constructor SHA256ContextUpdateResult SHA256ContextUpdateSucceeded checkedContext (constructor SHA256UpdateTelemetry SHA256UpdateTelemetryValue inputBytes totalBytes pendingBefore combinedBytes compressedBytes compressedBlocks (bytes-length nextPending) nextTotalBytes nextOperations))) (branch SHA256ContextValidationFailed nextError nextValidation . (constructor SHA256ContextUpdateResult SHA256ContextUpdateFailed nextError compressedBlocks zero nextOperations)))) (constructor SHA256Context SHA256ContextValue nextState nextTotalBytes nextPending))) (branch SHA256DigestBlocksFailed blockError blockOrdinal internalIndex partialTelemetry . (constructor SHA256ContextUpdateResult SHA256ContextUpdateFailed blockError blockOrdinal internalIndex partialTelemetry)))) (sha256DigestTelemetryInitial inputBytes compressedBytes))) (sha256DigestDropWithFuel compressedBytes combined))) (sha256DigestTakeWithFuel compressedBytes combined))))))))))) -- Part of `sha256Update`, lifted out to keep it inside the §28.3 size and -- nesting limits; the parameters are the locals it still needs. def sha256UpdatePart2 = (lambda unrestricted input : Bytes . (lambda unrestricted state : (family SHA256State) . (lambda unrestricted totalBytes : (family ModelWord64) . (lambda unrestricted pending : Bytes . (lambda unrestricted inputBytes : Nat . (lambda unrestricted nextTotalBytes : (family ModelWord64) . (lambda unrestricted pendingBefore : Nat . (app (lambda unrestricted combined : Bytes . (app (lambda unrestricted combinedBytes : Nat . (app (lambda unrestricted compressedBytes : Nat . (sha256UpdatePart1 state totalBytes inputBytes nextTotalBytes pendingBefore combined combinedBytes compressedBytes (naturalDivideUnchecked compressedBytes sha256NaturalSixtyFour))) (naturalSaturatingSubtract combinedBytes (naturalModuloUnchecked combinedBytes sha256NaturalSixtyFour)))) (bytes-length combined))) (bytes-append pending input))))))))) def sha256Update = (lambda unrestricted context : (family SHA256Context) . (lambda unrestricted input : Bytes . (eliminate SHA256ContextValidationResult (lambda unrestricted current : (family SHA256ContextValidationResult) . (family SHA256ContextUpdateResult)) (sha256ValidateContext context) (branch SHA256ContextValidated validated validationTelemetry . (eliminate SHA256Context (lambda unrestricted current : (family SHA256Context) . (family SHA256ContextUpdateResult)) validated (branch SHA256ContextValue state totalBytes pending . (app (lambda unrestricted inputBytes : Nat . (eliminate SHA256NaturalWord64Result (lambda unrestricted current : (family SHA256NaturalWord64Result) . (family SHA256ContextUpdateResult)) (sha256NaturalToWord64 inputBytes) (branch SHA256NaturalWord64Succeeded inputWord64 . (eliminate ModelWord64CheckedResult (lambda unrestricted current : (family ModelWord64CheckedResult) . (family SHA256ContextUpdateResult)) (modelWord64AddChecked totalBytes inputWord64) (branch ModelWord64CheckedSucceeded nextTotalBytes . (nat-eliminate (lambda unrestricted withinLimit : Nat . (family SHA256ContextUpdateResult)) (constructor SHA256ContextUpdateResult SHA256ContextUpdateFailed (constructor SHA256ErrorCode SHA256InputLengthOverflow) zero zero (sha256DigestTelemetryInitial inputBytes zero)) (lambda unrestricted limitPredecessor : Nat . (lambda unrestricted limitInduction : (family SHA256ContextUpdateResult) . (sha256UpdatePart2 input state totalBytes pending inputBytes nextTotalBytes (bytes-length pending)))) (sha256Word64WithinInputLimit nextTotalBytes))) (branch ModelWord64CheckedFailed arithmeticError . (constructor SHA256ContextUpdateResult SHA256ContextUpdateFailed (constructor SHA256ErrorCode SHA256InputLengthOverflow) zero zero (sha256DigestTelemetryInitial inputBytes zero))))) (branch SHA256NaturalWord64Failed error . (constructor SHA256ContextUpdateResult SHA256ContextUpdateFailed error zero zero (sha256DigestTelemetryInitial inputBytes zero))))) (bytes-length input))))) (branch SHA256ContextValidationFailed error validationTelemetry . (constructor SHA256ContextUpdateResult SHA256ContextUpdateFailed error zero zero (sha256DigestTelemetryInitial (bytes-length input) zero)))))) def sha256Finalize = (lambda unrestricted context : (family SHA256Context) . (eliminate SHA256Context (lambda unrestricted current : (family SHA256Context) . (family SHA256ContextFinalizeResult)) context (branch SHA256ContextValue state totalBytes pending . (eliminate SHA256ContextPaddingResult (lambda unrestricted current : (family SHA256ContextPaddingResult) . (family SHA256ContextFinalizeResult)) (sha256PadContext context) (branch SHA256ContextPaddingSucceeded suffix paddingTelemetry . (eliminate SHA256ContextPaddingTelemetry (lambda unrestricted current : (family SHA256ContextPaddingTelemetry) . (family SHA256ContextFinalizeResult)) paddingTelemetry (branch SHA256ContextPaddingTelemetryValue checkedTotal pendingBytes bitLength zeroBytes finalBytes blockCount . (app (lambda unrestricted operations : (family SHA256DigestTelemetry) . (eliminate SHA256DigestBlockRunResult (lambda unrestricted current : (family SHA256DigestBlockRunResult) . (family SHA256ContextFinalizeResult)) (sha256DigestRunBlocks blockCount state suffix operations) (branch SHA256DigestBlocksSucceeded finalState finalOperations . (app (lambda unrestricted digestBytes : Bytes . (eliminate SHA256Result (lambda unrestricted current : (family SHA256Result) . (family SHA256ContextFinalizeResult)) (sha256DigestFromBytes digestBytes) (branch SHA256Succeeded digest . (constructor SHA256ContextFinalizeResult SHA256ContextFinalizeSucceeded digest (constructor SHA256FinalizeTelemetry SHA256FinalizeTelemetryValue checkedTotal pendingBytes bitLength zeroBytes finalBytes blockCount (bytes-length digestBytes) finalOperations))) (branch SHA256Failed error . (constructor SHA256ContextFinalizeResult SHA256ContextFinalizeFailed error blockCount zero finalOperations)))) (sha256DigestStateBytes finalState))) (branch SHA256DigestBlocksFailed blockError blockOrdinal internalIndex partialTelemetry . (constructor SHA256ContextFinalizeResult SHA256ContextFinalizeFailed blockError blockOrdinal internalIndex partialTelemetry)))) (sha256DigestTelemetryInitial pendingBytes finalBytes))))) (branch SHA256ContextPaddingFailed error stage validationTelemetry . (constructor SHA256ContextFinalizeResult SHA256ContextFinalizeFailed error stage zero (sha256DigestTelemetryInitial (bytes-length pending) zero))))))) def sha256DigestExecute = (lambda unrestricted input : Bytes . (eliminate SHA256ContextUpdateResult (lambda unrestricted current : (family SHA256ContextUpdateResult) . (family SHA256DigestExecutionResult)) (sha256Update sha256InitialContext input) (branch SHA256ContextUpdateSucceeded context updateTelemetry . (eliminate SHA256UpdateTelemetry (lambda unrestricted current : (family SHA256UpdateTelemetry) . (family SHA256DigestExecutionResult)) updateTelemetry (branch SHA256UpdateTelemetryValue inputBytes totalBefore pendingBefore combinedBytes compressedBytes compressedBlocks pendingAfter totalAfter updateOperations . (eliminate SHA256ContextFinalizeResult (lambda unrestricted current : (family SHA256ContextFinalizeResult) . (family SHA256DigestExecutionResult)) (sha256Finalize context) (branch SHA256ContextFinalizeSucceeded digest finalizeTelemetry . (eliminate SHA256FinalizeTelemetry (lambda unrestricted current : (family SHA256FinalizeTelemetry) . (family SHA256DigestExecutionResult)) finalizeTelemetry (branch SHA256FinalizeTelemetryValue finalTotal finalPending bitLength zeroBytes finalBytes finalBlocks digestBytes finalOperations . (constructor SHA256DigestExecutionResult SHA256DigestExecutionSucceeded digest (sha256DigestTelemetryCombine inputBytes (naturalAdd compressedBytes finalBytes) updateOperations finalOperations))))) (branch SHA256ContextFinalizeFailed error ordinal internalIndex finalOperations . (constructor SHA256DigestExecutionResult SHA256DigestExecutionFailed error ordinal (sha256DigestTelemetryCombine inputBytes (naturalAdd compressedBytes (sha256DigestTelemetryPaddedCount finalOperations)) updateOperations finalOperations))))))) (branch SHA256ContextUpdateFailed error ordinal internalIndex telemetry . (constructor SHA256DigestExecutionResult SHA256DigestExecutionFailed error ordinal telemetry)))) -- Canonical SHA-256 identity text is exactly 64 lowercase ASCII hex bytes. -- Uppercase is deliberately rejected so one digest has one display spelling. def sha256DigestHexByteInRange = (lambda unrestricted value : Byte . (lambda unrestricted lower : Byte . (lambda unrestricted upper : Byte . (naturalAnd (naturalLessOrEqual (byte-to-nat lower) (byte-to-nat value)) (nat-less-than (byte-to-nat value) (byte-to-nat upper)))))) -- Returns 0..15 for lowercase hexadecimal and 16 for every invalid byte. def sha256DigestLowerHexNibble = (lambda unrestricted value : Byte . (nat-eliminate (lambda unrestricted decimal : Nat . Nat) (nat-eliminate (lambda unrestricted lower : Nat . Nat) (byte-to-nat (byte 16)) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . (naturalSaturatingSubtract (byte-to-nat value) (byte-to-nat (byte 87))))) (sha256DigestHexByteInRange value (byte 97) (byte 103))) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . (naturalSaturatingSubtract (byte-to-nat value) (byte-to-nat (byte 48))))) (sha256DigestHexByteInRange value (byte 48) (byte 58)))) -- Decode exactly `pairs` pairs. The public caller first proves a 64-byte -- source length, so the two heads in every one of the 32 steps are in range. def sha256DigestDecodeHexPairs = (lambda unrestricted pairs : Nat . (nat-eliminate (lambda unrestricted current : Nat . (pi unrestricted input : Bytes . (family StdResult (family SHA256ErrorCode) Bytes))) (lambda unrestricted input : Bytes . (constructor StdResult StdSuccess (family SHA256ErrorCode) Bytes b"")) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (pi unrestricted input : Bytes . (family StdResult (family SHA256ErrorCode) Bytes)) . (lambda unrestricted input : Bytes . (app (lambda unrestricted high : Nat . (app (lambda unrestricted low : Nat . (nat-eliminate (lambda unrestricted invalid : Nat . (family StdResult (family SHA256ErrorCode) Bytes)) (eliminate StdResult (lambda unrestricted current : (family StdResult (family SHA256ErrorCode) Bytes) . (family StdResult (family SHA256ErrorCode) Bytes)) (induction (bytes-tail (bytes-tail input))) (branch StdFailure error . (constructor StdResult StdFailure (family SHA256ErrorCode) Bytes error)) (branch StdSuccess decodedTail . (constructor StdResult StdSuccess (family SHA256ErrorCode) Bytes (bytes-cons (nat-to-byte (naturalAdd (naturalMultiply high 16) low)) decodedTail)))) (lambda unrestricted invalidPredecessor : Nat . (lambda unrestricted invalidInduction : (family StdResult (family SHA256ErrorCode) Bytes) . (constructor StdResult StdFailure (family SHA256ErrorCode) Bytes (constructor SHA256ErrorCode SHA256DigestHexInvalid)))) (naturalOr (naturalIsZero (nat-less-than high 16)) (naturalIsZero (nat-less-than low 16))))) (sha256DigestLowerHexNibble (bytes-head (bytes-tail input))))) (sha256DigestLowerHexNibble (bytes-head input)))))) pairs)) def sha256DigestFromHex : (pi unrestricted input : Bytes . (family SHA256Result)) = (lambda unrestricted input : Bytes . (nat-eliminate (lambda unrestricted validLength : Nat . (family SHA256Result)) (constructor SHA256Result SHA256Failed (constructor SHA256ErrorCode SHA256DigestLengthInvalid)) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SHA256Result) . (eliminate StdResult (lambda unrestricted current : (family StdResult (family SHA256ErrorCode) Bytes) . (family SHA256Result)) (sha256DigestDecodeHexPairs (byte-to-nat (byte 32)) input) (branch StdFailure error . (constructor SHA256Result SHA256Failed error)) (branch StdSuccess decoded . (sha256DigestFromBytes decoded))))) (naturalEqual (bytes-length input) (byte-to-nat (byte 64))))) def sha256DigestToHex = (lambda unrestricted digest : (family SHA256Digest) . (dataBytesRenderHex (sha256DigestToBytes digest))) def sha256DigestIdentity = (lambda unrestricted digest : (family SHA256Digest) . (constructor SHA256DigestIdentityResult SHA256DigestIdentitySucceeded (constructor SHA256DigestIdentity SHA256DigestIdentityValue digest))) -- A checked identity owns only the 32-byte digest. Canonical lowercase -- hexadecimal is derived, so no constructor can pair valid binary bytes with -- unrelated display text. def sha256DigestIdentityBinary = (lambda unrestricted identity : (family SHA256DigestIdentity) . (eliminate SHA256DigestIdentity (lambda unrestricted current : (family SHA256DigestIdentity) . (family SHA256Digest)) identity (branch SHA256DigestIdentityValue binary . binary))) def sha256DigestIdentityHex = (lambda unrestricted identity : (family SHA256DigestIdentity) . (sha256DigestToHex (sha256DigestIdentityBinary identity))) def sha256DigestIdentityEqual = (lambda unrestricted left : (family SHA256DigestIdentity) . (lambda unrestricted right : (family SHA256DigestIdentity) . (sha256DigestEqual (sha256DigestIdentityBinary left) (sha256DigestIdentityBinary right)))) -- Text is admitted exactly once: parsing rejects non-canonical spellings, -- then sha256DigestIdentity re-renders the checked binary value. The result -- therefore cannot contain a 64-byte string that merely looks digest-like. def sha256DigestIdentityFromHex = (lambda unrestricted input : Bytes . (eliminate SHA256Result (lambda unrestricted current : (family SHA256Result) . (family SHA256DigestIdentityResult)) (sha256DigestFromHex input) (branch SHA256Succeeded digest . (sha256DigestIdentity digest)) (branch SHA256Failed error . (constructor SHA256DigestIdentityResult SHA256DigestIdentityFailed error)))) def sha256Bytes = (lambda unrestricted input : Bytes . (eliminate SHA256DigestExecutionResult (lambda unrestricted current : (family SHA256DigestExecutionResult) . (family SHA256Result)) (sha256DigestExecute input) (branch SHA256DigestExecutionSucceeded digest telemetry . (constructor SHA256Result SHA256Succeeded digest)) (branch SHA256DigestExecutionFailed error ordinal telemetry . (constructor SHA256Result SHA256Failed error)))) def sha256Hex = (lambda unrestricted input : Bytes . (eliminate SHA256DigestExecutionResult (lambda unrestricted current : (family SHA256DigestExecutionResult) . (family SHA256HexResult)) (sha256DigestExecute input) (branch SHA256DigestExecutionSucceeded digest telemetry . (eliminate SHA256DigestIdentityResult (lambda unrestricted current : (family SHA256DigestIdentityResult) . (family SHA256HexResult)) (sha256DigestIdentity digest) (branch SHA256DigestIdentitySucceeded identity . (eliminate SHA256DigestIdentity (lambda unrestricted current : (family SHA256DigestIdentity) . (family SHA256HexResult)) identity (branch SHA256DigestIdentityValue binary . (constructor SHA256HexResult SHA256HexSucceeded (sha256DigestToHex binary) telemetry)))) (branch SHA256DigestIdentityFailed error . (constructor SHA256HexResult SHA256HexFailed error (sha256DigestTelemetryBlockCount telemetry) telemetry)))) (branch SHA256DigestExecutionFailed error ordinal telemetry . (constructor SHA256HexResult SHA256HexFailed error ordinal telemetry)))) def sha256HexBytesOrEmpty = (lambda unrestricted result : (family SHA256HexResult) . (eliminate SHA256HexResult (lambda unrestricted current : (family SHA256HexResult) . Bytes) result (branch SHA256HexSucceeded hexBytes telemetry . hexBytes) (branch SHA256HexFailed error ordinal telemetry . b""))) -- Bytes -> Bytes raw digest: the 32 digest bytes of the input, or empty -- bytes on the failure path. Downstream 32-length gates keep empty -- fail-closed (the raw counterpart of sha256Digest below). def sha256RawDigestOrEmpty = (lambda unrestricted material : Bytes . (eliminate SHA256Result (lambda unrestricted current : (family SHA256Result) . Bytes) (sha256Bytes material) (branch SHA256Succeeded digest . (eliminate SHA256Digest (lambda unrestricted current : (family SHA256Digest) . Bytes) digest (branch SHA256DigestValue raw proof . raw))) (branch SHA256Failed error . b""))) -- Bytes -> Bytes convenience digest: the 64-hex identity of the input, -- or empty bytes on the (length-guarded) failure path. Downstream -- 64-length/equality gates keep empty fail-closed. def sha256Digest = (lambda unrestricted material : Bytes . (sha256HexBytesOrEmpty (sha256Hex material)))