module Data.SHA256ScheduleExpand import Data.SHA256 import Data.SHA256Core import Data.SHA256Schedule import Model.Config import Model.Word32 import Model.Word32Logic import Std.Natural family SHA256ScheduleDependenciesResult : Type 0 constructor SHA256ScheduleDependenciesSucceeded field unrestricted sha256ScheduleWordMinus2 : (family ModelWord32) field unrestricted sha256ScheduleWordMinus7 : (family ModelWord32) field unrestricted sha256ScheduleWordMinus15 : (family ModelWord32) field unrestricted sha256ScheduleWordMinus16 : (family ModelWord32) constructor SHA256ScheduleDependenciesFailed field unrestricted sha256ScheduleDependenciesError : (family SHA256ErrorCode) field unrestricted sha256ScheduleDependenciesFailureIndex : Nat end-family family SHA256ScheduleExpansionState : Type 0 constructor SHA256ScheduleExpansionStateValue field unrestricted sha256ExpansionSchedule : (family SHA256Schedule) field unrestricted sha256ExpansionNextIndex : Nat field unrestricted sha256ExpansionGeneratedWords : Nat field unrestricted sha256ExpansionLookupCount : Nat field unrestricted sha256ExpansionSigmaCount : Nat field unrestricted sha256ExpansionRotateCount : Nat field unrestricted sha256ExpansionShiftCount : Nat field unrestricted sha256ExpansionAddCount : Nat end-family family SHA256ScheduleExpansionStepResult : Type 0 constructor SHA256ScheduleExpansionStepSucceeded field unrestricted sha256ExpansionStepState : (family SHA256ScheduleExpansionState) constructor SHA256ScheduleExpansionStepFailed field unrestricted sha256ExpansionStepError : (family SHA256ErrorCode) field unrestricted sha256ExpansionStepFailureIndex : Nat end-family family SHA256ScheduleExpansionTelemetry : Type 0 constructor SHA256ScheduleExpansionTelemetryValue field unrestricted sha256ExpansionTelemetryGeneratedWords : Nat field unrestricted sha256ExpansionTelemetryLookupCount : Nat field unrestricted sha256ExpansionTelemetrySigmaCount : Nat field unrestricted sha256ExpansionTelemetryRotateCount : Nat field unrestricted sha256ExpansionTelemetryShiftCount : Nat field unrestricted sha256ExpansionTelemetryAddCount : Nat end-family family SHA256ScheduleExpansionResult : Type 0 constructor SHA256ScheduleExpansionSucceeded field unrestricted sha256ExpandedSchedule : (family SHA256Schedule) field unrestricted sha256ExpansionTelemetry : (family SHA256ScheduleExpansionTelemetry) constructor SHA256ScheduleExpansionFailed field unrestricted sha256ExpansionError : (family SHA256ErrorCode) field unrestricted sha256ExpansionFailureIndex : Nat end-family def sha256NaturalTwo = (byte-to-nat (byte 2)) def sha256NaturalSeven = (byte-to-nat (byte 7)) def sha256NaturalFifteen = (byte-to-nat (byte 15)) def sha256NaturalFortyEight = (byte-to-nat (byte 48)) def sha256LookupScheduleDependencies = (lambda unrestricted schedule : (family SHA256Schedule) . (lambda unrestricted index : Nat . (eliminate SHA256ScheduleLookupResult (lambda unrestricted current : (family SHA256ScheduleLookupResult) . (family SHA256ScheduleDependenciesResult)) (sha256ScheduleLookup schedule (naturalSaturatingSubtract index sha256NaturalTwo)) (branch SHA256ScheduleLookupSucceeded wordMinus2 . (eliminate SHA256ScheduleLookupResult (lambda unrestricted current : (family SHA256ScheduleLookupResult) . (family SHA256ScheduleDependenciesResult)) (sha256ScheduleLookup schedule (naturalSaturatingSubtract index sha256NaturalSeven)) (branch SHA256ScheduleLookupSucceeded wordMinus7 . (eliminate SHA256ScheduleLookupResult (lambda unrestricted current : (family SHA256ScheduleLookupResult) . (family SHA256ScheduleDependenciesResult)) (sha256ScheduleLookup schedule (naturalSaturatingSubtract index sha256NaturalFifteen)) (branch SHA256ScheduleLookupSucceeded wordMinus15 . (eliminate SHA256ScheduleLookupResult (lambda unrestricted current : (family SHA256ScheduleLookupResult) . (family SHA256ScheduleDependenciesResult)) (sha256ScheduleLookup schedule (naturalSaturatingSubtract index sha256NaturalSixteen)) (branch SHA256ScheduleLookupSucceeded wordMinus16 . (constructor SHA256ScheduleDependenciesResult SHA256ScheduleDependenciesSucceeded wordMinus2 wordMinus7 wordMinus15 wordMinus16)) (branch SHA256ScheduleLookupFailed error failedIndex . (constructor SHA256ScheduleDependenciesResult SHA256ScheduleDependenciesFailed error failedIndex)))) (branch SHA256ScheduleLookupFailed error failedIndex . (constructor SHA256ScheduleDependenciesResult SHA256ScheduleDependenciesFailed error failedIndex)))) (branch SHA256ScheduleLookupFailed error failedIndex . (constructor SHA256ScheduleDependenciesResult SHA256ScheduleDependenciesFailed error failedIndex)))) (branch SHA256ScheduleLookupFailed error failedIndex . (constructor SHA256ScheduleDependenciesResult SHA256ScheduleDependenciesFailed error failedIndex))))) def sha256ExpandScheduleStep = (lambda unrestricted state : (family SHA256ScheduleExpansionState) . (eliminate SHA256ScheduleExpansionState (lambda unrestricted current : (family SHA256ScheduleExpansionState) . (family SHA256ScheduleExpansionStepResult)) state (branch SHA256ScheduleExpansionStateValue schedule nextIndex generated lookups sigmas rotates shifts adds . (eliminate SHA256ScheduleDependenciesResult (lambda unrestricted current : (family SHA256ScheduleDependenciesResult) . (family SHA256ScheduleExpansionStepResult)) (sha256LookupScheduleDependencies schedule nextIndex) (branch SHA256ScheduleDependenciesSucceeded wordMinus2 wordMinus7 wordMinus15 wordMinus16 . (app (lambda unrestricted generatedWord : (family ModelWord32) . (constructor SHA256ScheduleExpansionStepResult SHA256ScheduleExpansionStepSucceeded (constructor SHA256ScheduleExpansionState SHA256ScheduleExpansionStateValue (sha256ScheduleAppend schedule generatedWord) (succ nextIndex) (succ generated) (naturalAdd lookups sha256NaturalFour) (naturalAdd sigmas sha256NaturalTwo) (naturalAdd rotates sha256NaturalFour) (naturalAdd shifts sha256NaturalTwo) (naturalAdd adds (byte-to-nat (byte 3)))))) (modelWord32AddFour (sha256SmallSigma1 wordMinus2) wordMinus7 (sha256SmallSigma0 wordMinus15) wordMinus16))) (branch SHA256ScheduleDependenciesFailed error failedIndex . (constructor SHA256ScheduleExpansionStepResult SHA256ScheduleExpansionStepFailed error failedIndex)))))) -- Run `fuel` expansion steps, FIRST-ORDER. -- -- The previous definition folded with a FUNCTION accumulator -- (`pi state . Result`) and recursed by applying the induction hypothesis to the -- next state. Because the VM normalizes a fold's function part before the -- concrete state is supplied, it symbolically unrolled all 48 iterations of a -- large step body (four schedule lookups + sigma arithmetic each) into one giant -- term and only then evaluated it -- ~O(fuel^2 * body) work that kept expansion -- slow even after the lookup itself was made linear. -- -- This version folds with a first-order accumulator: the step-result VALUE -- (`Succeeded state | Failed`). Each iteration runs exactly one `expandStep` on -- the concrete accumulated state (or threads a failure through), so the whole -- expansion is O(fuel) over concrete values with no symbolic term building. The -- computed words -- and therefore the digest -- are unchanged. def sha256ExpandScheduleWithFuel = (lambda unrestricted fuel : Nat . (lambda unrestricted initialState : (family SHA256ScheduleExpansionState) . (eliminate SHA256ScheduleExpansionStepResult (lambda unrestricted current : (family SHA256ScheduleExpansionStepResult) . (family SHA256ScheduleExpansionResult)) (nat-eliminate (lambda unrestricted current : Nat . (family SHA256ScheduleExpansionStepResult)) (constructor SHA256ScheduleExpansionStepResult SHA256ScheduleExpansionStepSucceeded initialState) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SHA256ScheduleExpansionStepResult) . (eliminate SHA256ScheduleExpansionStepResult (lambda unrestricted current : (family SHA256ScheduleExpansionStepResult) . (family SHA256ScheduleExpansionStepResult)) induction (branch SHA256ScheduleExpansionStepSucceeded state . (sha256ExpandScheduleStep state)) (branch SHA256ScheduleExpansionStepFailed error failedIndex . induction)))) fuel) (branch SHA256ScheduleExpansionStepSucceeded state . (eliminate SHA256ScheduleExpansionState (lambda unrestricted current : (family SHA256ScheduleExpansionState) . (family SHA256ScheduleExpansionResult)) state (branch SHA256ScheduleExpansionStateValue schedule nextIndex generated lookups sigmas rotates shifts adds . (constructor SHA256ScheduleExpansionResult SHA256ScheduleExpansionSucceeded schedule (constructor SHA256ScheduleExpansionTelemetry SHA256ScheduleExpansionTelemetryValue generated lookups sigmas rotates shifts adds))))) (branch SHA256ScheduleExpansionStepFailed error failedIndex . (constructor SHA256ScheduleExpansionResult SHA256ScheduleExpansionFailed error failedIndex))))) def sha256ValidateExpandedSchedule = (lambda unrestricted result : (family SHA256ScheduleExpansionResult) . (eliminate SHA256ScheduleExpansionResult (lambda unrestricted current : (family SHA256ScheduleExpansionResult) . (family SHA256ScheduleExpansionResult)) result (branch SHA256ScheduleExpansionSucceeded schedule telemetry . (nat-eliminate (lambda unrestricted validLength : Nat . (family SHA256ScheduleExpansionResult)) (constructor SHA256ScheduleExpansionResult SHA256ScheduleExpansionFailed (constructor SHA256ErrorCode SHA256ScheduleLengthInvalid) (sha256ScheduleLength schedule)) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SHA256ScheduleExpansionResult) . (constructor SHA256ScheduleExpansionResult SHA256ScheduleExpansionSucceeded schedule telemetry))) (naturalEqual (sha256ScheduleLength schedule) sha256NaturalSixtyFour))) (branch SHA256ScheduleExpansionFailed error failedIndex . (constructor SHA256ScheduleExpansionResult SHA256ScheduleExpansionFailed error failedIndex)))) def sha256ExpandSchedule = (lambda unrestricted initialSchedule : (family SHA256Schedule) . (nat-eliminate (lambda unrestricted validInitialLength : Nat . (family SHA256ScheduleExpansionResult)) (constructor SHA256ScheduleExpansionResult SHA256ScheduleExpansionFailed (constructor SHA256ErrorCode SHA256ScheduleLengthInvalid) (sha256ScheduleLength initialSchedule)) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SHA256ScheduleExpansionResult) . (sha256ValidateExpandedSchedule (sha256ExpandScheduleWithFuel sha256NaturalFortyEight (constructor SHA256ScheduleExpansionState SHA256ScheduleExpansionStateValue initialSchedule sha256NaturalSixteen zero zero zero zero zero zero))))) (naturalEqual (sha256ScheduleLength initialSchedule) sha256NaturalSixteen)))