module Compiler.NormalizationBudget import Model.Config import Model.Word32 import Std.Word import Std.Natural import Compiler.NaturalMagnitude import Compiler.IntegerLiteral import Data.Bytes -- Fixed-width work accounting. An exhausted charge preserves the last valid -- state; it never wraps, partially charges, or supplies an admissible residual. family NormalizationBudget : Type 0 constructor NormalizationBudgetValue field unrestricted normalizationWorkLimit : (family ModelWord32) field unrestricted normalizationWorkRemaining : (family ModelWord32) field unrestricted normalizationWorkUsed : (family ModelWord32) end-family family NormalizationCostResult : Type 0 constructor NormalizationCostWord field unrestricted normalizationCost : (family ModelWord32) constructor NormalizationCostTooLarge constructor NormalizationCostInvalid end-family family NormalizationChargeResult : Type 0 constructor NormalizationCharged field unrestricted normalizationUpdatedBudget : (family NormalizationBudget) constructor NormalizationChargeExhausted field unrestricted normalizationUnchangedBudget : (family NormalizationBudget) field unrestricted normalizationRejectedCharge : (family ModelWord32) constructor NormalizationChargeInvalid end-family -- Internal payload traversal state. Stopped blocks skip their remaining work. family NormalizationPayloadState : Type 0 constructor NormalizationPayloadActive field unrestricted normalizationPayloadRemaining : Bytes field unrestricted normalizationPayloadBudget : (family NormalizationBudget) constructor NormalizationPayloadStopped field unrestricted normalizationPayloadResult : (family NormalizationChargeResult) end-family -- Bounded admission for unary metadata operations. The cursor grows only as -- far as the available budget; the requested natural is never eliminated. family NormalizationNaturalState : Type 0 constructor NormalizationNaturalActive field unrestricted normalizationNaturalCursor : Nat field unrestricted normalizationNaturalBudget : (family NormalizationBudget) constructor NormalizationNaturalStopped field unrestricted normalizationNaturalResult : (family NormalizationChargeResult) end-family -- Magnitudes are decimal digits in little-endian order. Conversion visits at -- most ten admitted digits, never the represented natural value. def normalizationCostDecimalText = (lambda unrestricted digits : Bytes . (bytes-eliminate (lambda unrestricted current : Bytes . Bytes) b"" (lambda unrestricted head : Byte . (lambda unrestricted tail : Bytes . (lambda unrestricted induction : Bytes . (bytes-append induction (bytes (nat-to-byte (Std.Natural/naturalAdd (byte-to-nat head) (byte-to-nat (byte 48))))))))) digits)) def finishNormalizationCostWord = (lambda unrestricted result : (family IntegerLiteralResult) . (eliminate IntegerLiteralResult (lambda unrestricted current : (family IntegerLiteralResult) . (family NormalizationCostResult)) result (branch IntegerLiteralWord width sign bytesLE . (eliminate DataBytesWord32ExactDecodeResult (lambda unrestricted current : (family DataBytesWord32ExactDecodeResult) . (family NormalizationCostResult)) (Std.Word/stdU32DecodeLEExact bytesLE) (branch DataBytesWord32ExactlyDecoded word telemetry . (constructor NormalizationCostResult NormalizationCostWord word)) (branch DataBytesWord32ExactDecodeFailed error telemetry . (constructor NormalizationCostResult NormalizationCostInvalid)))) (branch IntegerLiteralFailed failure . (eliminate IntegerLiteralFailure (lambda unrestricted current : (family IntegerLiteralFailure) . (family NormalizationCostResult)) failure (branch IntegerLiteralMissingDigits . (constructor NormalizationCostResult NormalizationCostInvalid)) (branch IntegerLiteralBadDigit . (constructor NormalizationCostResult NormalizationCostInvalid)) (branch IntegerLiteralBadSeparator . (constructor NormalizationCostResult NormalizationCostInvalid)) (branch IntegerLiteralOutOfRange . (constructor NormalizationCostResult NormalizationCostTooLarge)))))) def normalizationCostFromMagnitude = (lambda unrestricted digits : Bytes . (eliminate NaturalMagnitudeResult (lambda unrestricted current : (family NaturalMagnitudeResult) . (family NormalizationCostResult)) (Compiler.NaturalMagnitude/magnitudeDecodeCanonical digits) (branch NaturalMagnitudeAccepted canonical . (app (nat-eliminate (lambda unrestricted tooLong : Nat . (pi unrestricted force : Nat . (family NormalizationCostResult))) (lambda unrestricted force : Nat . (app (nat-eliminate (lambda unrestricted empty : Nat . (pi unrestricted force : Nat . (family NormalizationCostResult))) (lambda unrestricted force : Nat . (finishNormalizationCostWord (Compiler.IntegerLiteral/integerLiteralParse (constructor IntegerLiteralRadix IntegerLiteralDecimal) (constructor IntegerLiteralKind IntegerLiteralUnsigned) (constructor IntegerLiteralSign IntegerLiteralPositive) (constructor IntegerLiteralWidth IntegerLiteralWidth32) (normalizationCostDecimalText canonical)))) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (pi unrestricted force : Nat . (family NormalizationCostResult)) . (lambda unrestricted force : Nat . (constructor NormalizationCostResult NormalizationCostWord Model.Word32/modelWord32Zero)))) (bytes-equal canonical b"")) zero)) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (pi unrestricted force : Nat . (family NormalizationCostResult)) . (lambda unrestricted force : Nat . (constructor NormalizationCostResult NormalizationCostTooLarge)))) (nat-less-than (byte-to-nat (byte 10)) (bytes-length canonical))) zero)) (branch NaturalMagnitudeRejected failure . (constructor NormalizationCostResult NormalizationCostInvalid)))) def normalizationBudget = (lambda unrestricted limit : (family ModelWord32) . (constructor NormalizationBudget NormalizationBudgetValue limit limit Model.Word32/modelWord32Zero)) -- Both operands are at most limit. Their sum cannot wrap to limit: that -- would require limit + 2^32 <= 2*limit, impossible for a U32 limit. def normalizationBudgetValid = (lambda unrestricted budget : (family NormalizationBudget) . (eliminate NormalizationBudget (lambda unrestricted current : (family NormalizationBudget) . Nat) budget (branch NormalizationBudgetValue limit remaining used . (Std.Natural/naturalAnd (Std.Natural/naturalIsZero (Std.Word/stdU32LessThan limit remaining)) (Std.Natural/naturalAnd (Std.Natural/naturalIsZero (Std.Word/stdU32LessThan limit used)) (bytes-equal (Std.Word/stdU32EncodeLE limit) (Std.Word/stdU32EncodeLE (Std.Word/stdU32AddWrapping remaining used)))))))) def chargeValidNormalizationBudget = (lambda unrestricted amount : (family ModelWord32) . (lambda unrestricted budget : (family NormalizationBudget) . (eliminate NormalizationBudget (lambda unrestricted current : (family NormalizationBudget) . (family NormalizationChargeResult)) budget (branch NormalizationBudgetValue limit remaining used . (app (nat-eliminate (lambda unrestricted insufficient : Nat . (pi unrestricted force : Nat . (family NormalizationChargeResult))) (lambda unrestricted force : Nat . (constructor NormalizationChargeResult NormalizationCharged (constructor NormalizationBudget NormalizationBudgetValue limit (Std.Word/stdU32SubtractWrapping remaining amount) (Std.Word/stdU32AddWrapping used amount)))) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (pi unrestricted force : Nat . (family NormalizationChargeResult)) . (lambda unrestricted force : Nat . (constructor NormalizationChargeResult NormalizationChargeExhausted budget amount)))) (Std.Word/stdU32LessThan remaining amount)) zero))))) def chargeNormalizationBudgetGeneral = (lambda unrestricted amount : (family ModelWord32) . (lambda unrestricted budget : (family NormalizationBudget) . (app (nat-eliminate (lambda unrestricted valid : Nat . (pi unrestricted force : Nat . (family NormalizationChargeResult))) (lambda unrestricted force : Nat . (constructor NormalizationChargeResult NormalizationChargeInvalid)) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (pi unrestricted force : Nat . (family NormalizationChargeResult)) . (lambda unrestricted force : Nat . (chargeValidNormalizationBudget amount budget)))) (normalizationBudgetValid budget)) zero))) def normalizationWordOne = (constructor ModelWord32 ModelWord32Value (byte 1) (byte 0) (byte 0) (byte 0)) def normalizationBytePredecessor = (lambda unrestricted value : Byte . (nat-to-byte (nat-eliminate (lambda unrestricted current : Nat . Nat) (byte-to-nat (byte 255)) (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Nat . predecessor)) (byte-to-nat value)))) def normalizationWordChoose = (lambda unrestricted condition : Nat . (lambda unrestricted selected : (pi unrestricted force : Nat . (family ModelWord32)) . (lambda unrestricted fallback : (pi unrestricted force : Nat . (family ModelWord32)) . (app (nat-eliminate (lambda unrestricted current : Nat . (pi unrestricted force : Nat . (family ModelWord32))) fallback (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (pi unrestricted force : Nat . (family ModelWord32)) . selected)) condition) zero)))) -- Called only after proving remaining > 0. Borrow visits at most four bytes; -- it never runs bitwise XOR to subtract a single unit. def normalizationWordPredecessor = (lambda unrestricted word : (family ModelWord32) . (eliminate ModelWord32 (lambda unrestricted current : (family ModelWord32) . (family ModelWord32)) word (branch ModelWord32Value b0 b1 b2 b3 . (normalizationWordChoose (byte-equal b0 (byte 0)) (lambda unrestricted force : Nat . (normalizationWordChoose (byte-equal b1 (byte 0)) (lambda unrestricted force : Nat . (normalizationWordChoose (byte-equal b2 (byte 0)) (lambda unrestricted force : Nat . (constructor ModelWord32 ModelWord32Value (byte 255) (byte 255) (byte 255) (normalizationBytePredecessor b3))) (lambda unrestricted force : Nat . (constructor ModelWord32 ModelWord32Value (byte 255) (byte 255) (normalizationBytePredecessor b2) b3)))) (lambda unrestricted force : Nat . (constructor ModelWord32 ModelWord32Value (byte 255) (normalizationBytePredecessor b1) b2 b3)))) (lambda unrestricted force : Nat . (constructor ModelWord32 ModelWord32Value (normalizationBytePredecessor b0) b1 b2 b3)))))) def chargeNormalizationBudgetOneValid = (lambda unrestricted budget : (family NormalizationBudget) . (eliminate NormalizationBudget (lambda unrestricted current : (family NormalizationBudget) . (family NormalizationChargeResult)) budget (branch NormalizationBudgetValue limit remaining used . (app (nat-eliminate (lambda unrestricted empty : Nat . (pi unrestricted force : Nat . (family NormalizationChargeResult))) (lambda unrestricted force : Nat . (constructor NormalizationChargeResult NormalizationCharged (constructor NormalizationBudget NormalizationBudgetValue limit (normalizationWordPredecessor remaining) (Std.Word/stdU32AddWrapping used normalizationWordOne)))) (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (pi unrestricted force : Nat . (family NormalizationChargeResult)) . (lambda unrestricted force : Nat . (constructor NormalizationChargeResult NormalizationChargeExhausted budget normalizationWordOne)))) (Std.Word/stdU32IsZero remaining)) zero)))) def chargeNormalizationBudgetOne = (lambda unrestricted budget : (family NormalizationBudget) . (app (nat-eliminate (lambda unrestricted valid : Nat . (pi unrestricted force : Nat . (family NormalizationChargeResult))) (lambda unrestricted force : Nat . (constructor NormalizationChargeResult NormalizationChargeInvalid)) (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (pi unrestricted force : Nat . (family NormalizationChargeResult)) . (lambda unrestricted force : Nat . (chargeNormalizationBudgetOneValid budget)))) (normalizationBudgetValid budget)) zero)) def chargeNormalizationBudget = (lambda unrestricted amount : (family ModelWord32) . (lambda unrestricted budget : (family NormalizationBudget) . (app (nat-eliminate (lambda unrestricted one : Nat . (pi unrestricted force : Nat . (family NormalizationChargeResult))) (lambda unrestricted force : Nat . (chargeNormalizationBudgetGeneral amount budget)) (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (pi unrestricted force : Nat . (family NormalizationChargeResult)) . (lambda unrestricted force : Nat . (chargeNormalizationBudgetOne budget)))) (bytes-equal (Std.Word/stdU32EncodeLE amount) (bytes 1 0 0 0))) zero))) -- Charge one byte at a time without folding over the entire payload. def stepNormalizationPayload = (lambda unrestricted state : (family NormalizationPayloadState) . (eliminate NormalizationPayloadState (lambda unrestricted current : (family NormalizationPayloadState) . (family NormalizationPayloadState)) state (branch NormalizationPayloadActive payload budget . (app (nat-eliminate (lambda unrestricted nonempty : Nat . (pi unrestricted force : Nat . (family NormalizationPayloadState))) (lambda unrestricted force : Nat . (constructor NormalizationPayloadState NormalizationPayloadStopped (constructor NormalizationChargeResult NormalizationCharged budget))) (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (pi unrestricted force : Nat . (family NormalizationPayloadState)) . (lambda unrestricted force : Nat . (eliminate NormalizationChargeResult (lambda unrestricted result : (family NormalizationChargeResult) . (family NormalizationPayloadState)) (chargeNormalizationBudgetOne budget) (branch NormalizationCharged next . (constructor NormalizationPayloadState NormalizationPayloadActive (bytes-tail payload) next)) (branch NormalizationChargeExhausted unchanged amount . (constructor NormalizationPayloadState NormalizationPayloadStopped (constructor NormalizationChargeResult NormalizationChargeExhausted unchanged amount))) (branch NormalizationChargeInvalid . (constructor NormalizationPayloadState NormalizationPayloadStopped (constructor NormalizationChargeResult NormalizationChargeInvalid))))))) (nat-less-than zero (bytes-length payload))) zero)) (branch NormalizationPayloadStopped result . state))) def repeatNormalizationPayloadSmall = (lambda unrestricted count : Nat . (lambda unrestricted step : (pi unrestricted state : (family NormalizationPayloadState) . (family NormalizationPayloadState)) . (lambda unrestricted state : (family NormalizationPayloadState) . (eliminate NormalizationPayloadState (lambda unrestricted current : (family NormalizationPayloadState) . (family NormalizationPayloadState)) state (branch NormalizationPayloadActive payload budget . (nat-eliminate (lambda unrestricted index : Nat . (family NormalizationPayloadState)) state (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family NormalizationPayloadState) . (step induction))) count)) (branch NormalizationPayloadStopped result . state))))) -- Exactly four little-endian budget bytes build base-256 iteration blocks. -- Each block checks Stopped before entering; no unary budget conversion occurs. def iterateNormalizationPayload = (lambda unrestricted digits : Bytes . (lambda unrestricted step : (pi unrestricted state : (family NormalizationPayloadState) . (family NormalizationPayloadState)) . (lambda unrestricted seed : (family NormalizationPayloadState) . (app (bytes-eliminate (lambda unrestricted remaining : Bytes . (pi unrestricted step : (pi unrestricted state : (family NormalizationPayloadState) . (family NormalizationPayloadState)) . (pi unrestricted seed : (family NormalizationPayloadState) . (family NormalizationPayloadState)))) (lambda unrestricted step : (pi unrestricted state : (family NormalizationPayloadState) . (family NormalizationPayloadState)) . (lambda unrestricted seed : (family NormalizationPayloadState) . seed)) (lambda unrestricted head : Byte . (lambda unrestricted tail : Bytes . (lambda unrestricted continue : (pi unrestricted step : (pi unrestricted state : (family NormalizationPayloadState) . (family NormalizationPayloadState)) . (pi unrestricted seed : (family NormalizationPayloadState) . (family NormalizationPayloadState))) . (lambda unrestricted step : (pi unrestricted state : (family NormalizationPayloadState) . (family NormalizationPayloadState)) . (lambda unrestricted seed : (family NormalizationPayloadState) . (continue (lambda unrestricted state : (family NormalizationPayloadState) . (repeatNormalizationPayloadSmall (succ (byte-to-nat (byte 255))) step state)) (repeatNormalizationPayloadSmall (byte-to-nat head) step seed))))))) digits) step seed)))) def finishNormalizationPayload = (lambda unrestricted state : (family NormalizationPayloadState) . (eliminate NormalizationPayloadState (lambda unrestricted current : (family NormalizationPayloadState) . (family NormalizationChargeResult)) state (branch NormalizationPayloadActive payload budget . (app (nat-eliminate (lambda unrestricted nonempty : Nat . (pi unrestricted force : Nat . (family NormalizationChargeResult))) (lambda unrestricted force : Nat . (constructor NormalizationChargeResult NormalizationCharged budget)) (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (pi unrestricted force : Nat . (family NormalizationChargeResult)) . (lambda unrestricted force : Nat . (constructor NormalizationChargeResult NormalizationChargeExhausted budget normalizationWordOne)))) (nat-less-than zero (bytes-length payload))) zero)) (branch NormalizationPayloadStopped result . result))) -- A sequence of checked unit charges; exhaustion retains the last valid budget. -- This bounds traversed payload by the remaining budget, including U32_MAX. def chargeNormalizationBytes = (lambda unrestricted payload : Bytes . (lambda unrestricted budget : (family NormalizationBudget) . (app (nat-eliminate (lambda unrestricted valid : Nat . (pi unrestricted force : Nat . (family NormalizationChargeResult))) (lambda unrestricted force : Nat . (constructor NormalizationChargeResult NormalizationChargeInvalid)) (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (pi unrestricted force : Nat . (family NormalizationChargeResult)) . (lambda unrestricted force : Nat . (eliminate NormalizationBudget (lambda unrestricted current : (family NormalizationBudget) . (family NormalizationChargeResult)) budget (branch NormalizationBudgetValue limit remaining used . (finishNormalizationPayload (iterateNormalizationPayload (Std.Word/stdU32EncodeLE remaining) stepNormalizationPayload (constructor NormalizationPayloadState NormalizationPayloadActive payload budget)))))))) (normalizationBudgetValid budget)) zero))) def stepNormalizationNatural = (lambda unrestricted target : Nat . (lambda unrestricted state : (family NormalizationNaturalState) . (eliminate NormalizationNaturalState (lambda unrestricted current : (family NormalizationNaturalState) . (family NormalizationNaturalState)) state (branch NormalizationNaturalActive cursor budget . (app (nat-eliminate (lambda unrestricted nonempty : Nat . (pi unrestricted force : Nat . (family NormalizationNaturalState))) (lambda unrestricted force : Nat . (constructor NormalizationNaturalState NormalizationNaturalStopped (constructor NormalizationChargeResult NormalizationCharged budget))) (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (pi unrestricted force : Nat . (family NormalizationNaturalState)) . (lambda unrestricted force : Nat . (eliminate NormalizationChargeResult (lambda unrestricted result : (family NormalizationChargeResult) . (family NormalizationNaturalState)) (chargeNormalizationBudgetOne budget) (branch NormalizationCharged next . (constructor NormalizationNaturalState NormalizationNaturalActive (succ cursor) next)) (branch NormalizationChargeExhausted unchanged amount . (constructor NormalizationNaturalState NormalizationNaturalStopped (constructor NormalizationChargeResult NormalizationChargeExhausted unchanged amount))) (branch NormalizationChargeInvalid . (constructor NormalizationNaturalState NormalizationNaturalStopped (constructor NormalizationChargeResult NormalizationChargeInvalid))))))) (nat-less-than cursor target)) zero)) (branch NormalizationNaturalStopped result . state)))) def repeatNormalizationNaturalSmall = (lambda unrestricted count : Nat . (lambda unrestricted step : (pi unrestricted state : (family NormalizationNaturalState) . (family NormalizationNaturalState)) . (lambda unrestricted state : (family NormalizationNaturalState) . (eliminate NormalizationNaturalState (lambda unrestricted current : (family NormalizationNaturalState) . (family NormalizationNaturalState)) state (branch NormalizationNaturalActive cursor budget . (nat-eliminate (lambda unrestricted index : Nat . (family NormalizationNaturalState)) state (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family NormalizationNaturalState) . (step induction))) count)) (branch NormalizationNaturalStopped result . state))))) -- Exactly four little-endian budget bytes build base-256 iteration blocks. -- Each block checks Stopped before entering; no unary budget conversion occurs. def iterateNormalizationNatural = (lambda unrestricted digits : Bytes . (lambda unrestricted step : (pi unrestricted state : (family NormalizationNaturalState) . (family NormalizationNaturalState)) . (lambda unrestricted seed : (family NormalizationNaturalState) . (app (bytes-eliminate (lambda unrestricted remaining : Bytes . (pi unrestricted step : (pi unrestricted state : (family NormalizationNaturalState) . (family NormalizationNaturalState)) . (pi unrestricted seed : (family NormalizationNaturalState) . (family NormalizationNaturalState)))) (lambda unrestricted step : (pi unrestricted state : (family NormalizationNaturalState) . (family NormalizationNaturalState)) . (lambda unrestricted seed : (family NormalizationNaturalState) . seed)) (lambda unrestricted head : Byte . (lambda unrestricted tail : Bytes . (lambda unrestricted continue : (pi unrestricted step : (pi unrestricted state : (family NormalizationNaturalState) . (family NormalizationNaturalState)) . (pi unrestricted seed : (family NormalizationNaturalState) . (family NormalizationNaturalState))) . (lambda unrestricted step : (pi unrestricted state : (family NormalizationNaturalState) . (family NormalizationNaturalState)) . (lambda unrestricted seed : (family NormalizationNaturalState) . (continue (lambda unrestricted state : (family NormalizationNaturalState) . (repeatNormalizationNaturalSmall (succ (byte-to-nat (byte 255))) step state)) (repeatNormalizationNaturalSmall (byte-to-nat head) step seed))))))) digits) step seed)))) def finishNormalizationNatural = (lambda unrestricted target : Nat . (lambda unrestricted state : (family NormalizationNaturalState) . (eliminate NormalizationNaturalState (lambda unrestricted current : (family NormalizationNaturalState) . (family NormalizationChargeResult)) state (branch NormalizationNaturalActive cursor budget . (app (nat-eliminate (lambda unrestricted nonempty : Nat . (pi unrestricted force : Nat . (family NormalizationChargeResult))) (lambda unrestricted force : Nat . (constructor NormalizationChargeResult NormalizationCharged budget)) (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (pi unrestricted force : Nat . (family NormalizationChargeResult)) . (lambda unrestricted force : Nat . (constructor NormalizationChargeResult NormalizationChargeExhausted budget normalizationWordOne)))) (nat-less-than cursor target)) zero)) (branch NormalizationNaturalStopped result . result)))) -- A sequence of checked unit charges; exhaustion retains the last valid budget. -- This bounds the natural cursor by the remaining budget, including U32_MAX. def chargeNormalizationNatural = (lambda unrestricted target : Nat . (lambda unrestricted budget : (family NormalizationBudget) . (app (nat-eliminate (lambda unrestricted valid : Nat . (pi unrestricted force : Nat . (family NormalizationChargeResult))) (lambda unrestricted force : Nat . (constructor NormalizationChargeResult NormalizationChargeInvalid)) (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (pi unrestricted force : Nat . (family NormalizationChargeResult)) . (lambda unrestricted force : Nat . (eliminate NormalizationBudget (lambda unrestricted current : (family NormalizationBudget) . (family NormalizationChargeResult)) budget (branch NormalizationBudgetValue limit remaining used . (finishNormalizationNatural target (iterateNormalizationNatural (Std.Word/stdU32EncodeLE remaining) (stepNormalizationNatural target) (constructor NormalizationNaturalState NormalizationNaturalActive zero budget)))))))) (normalizationBudgetValid budget)) zero)))