module Runtime.TelemetryValueRoutine import Observe.Value import Runtime.TelemetryCapture import Runtime.TelemetryValue import Std.Natural -- One bounded decimal/hex algorithm, instantiated with host instruction -- emitters. Word operations wrap at 64 bits; byte loads zero-extend and byte -- stores truncate. Compare is unsigned. AddImmediate sign-extends its 32-bit -- operand, including the decrement; shifts are logical. Divide consumes Result -- with zero RemainderOrExtent, yields quotient/remainder in those roles and -- requires a positive divisor (the decimal algorithm uses ten). All extent -- refusal branches precede source loads or destination writes. Pointer validity -- and disjoint buffers remain caller arena obligations, not an entropy or -- durability claim. Emitters preserve their interpreter's persistent state. -- Direct decimal uses Input as a word and RemainderOrExtent as destination -- capacity. Hex/word/slice use Input as a pointer, RemainderOrExtent as source -- capacity and Counter as destination capacity. Adapters check both ranges -- before replacing those roles with the direct decimal ABI. Hex branch names -- include byte and nibble position so specialization cannot duplicate labels. -- There is no IO, allocation, clock acquisition or acquisition-state mutation. family TelemetryValueCondition : Type 0 constructor TelemetryValueZero constructor TelemetryValueNotZero constructor TelemetryValueBelow constructor TelemetryValueAbove end-family family TelemetryValueRoutineKind : Type 0 constructor TelemetryValueDecimalRoutine field unrestricted valueDecimalRoutineSigned : Nat constructor TelemetryValueHexRoutine field unrestricted valueHexRoutineWidth : Nat field unrestricted valueHexRoutineReverse : Nat constructor TelemetryValueWordRoutine field unrestricted valueWordRoutineSigned : Nat field unrestricted valueWordRoutineOffset : Nat constructor TelemetryValueSliceRoutine field unrestricted valueSliceRoutineWidth : Nat field unrestricted valueSliceRoutineReverse : Nat field unrestricted valueSliceRoutineOffset : Nat end-family family TelemetryValueBackend : Type 0 parameter erased A : Type 0 parameter erased R : Type 0 constructor TelemetryValueBackendValue field unrestricted backendValueLoad64 : (pi unrestricted a0 : R . (pi unrestricted a1 : R . (pi unrestricted a2 : Nat . (pi unrestricted a3 : A . A)))) field unrestricted backendValueLoad8 : (pi unrestricted a0 : R . (pi unrestricted a1 : R . (pi unrestricted a2 : Nat . (pi unrestricted a3 : A . A)))) field unrestricted backendValueStore8 : (pi unrestricted a0 : R . (pi unrestricted a1 : Nat . (pi unrestricted a2 : R . (pi unrestricted a3 : A . A)))) field unrestricted backendValueMove : (pi unrestricted a0 : R . (pi unrestricted a1 : R . (pi unrestricted a2 : A . A))) field unrestricted backendValueSet : (pi unrestricted a0 : R . (pi unrestricted a1 : Nat . (pi unrestricted a2 : A . A))) field unrestricted backendValueCompareImmediate : (pi unrestricted a0 : R . (pi unrestricted a1 : Nat . (pi unrestricted a2 : A . A))) field unrestricted backendValueCompare : (pi unrestricted a0 : R . (pi unrestricted a1 : R . (pi unrestricted a2 : A . A))) field unrestricted backendValueAdd : (pi unrestricted a0 : R . (pi unrestricted a1 : R . (pi unrestricted a2 : A . A))) field unrestricted backendValueAddImmediate : (pi unrestricted a0 : R . (pi unrestricted a1 : Nat . (pi unrestricted a2 : A . A))) field unrestricted backendValueSubtract : (pi unrestricted a0 : R . (pi unrestricted a1 : R . (pi unrestricted a2 : A . A))) field unrestricted backendValueShiftRight : (pi unrestricted a0 : R . (pi unrestricted a1 : Nat . (pi unrestricted a2 : A . A))) field unrestricted backendValueAndImmediate : (pi unrestricted a0 : R . (pi unrestricted a1 : Nat . (pi unrestricted a2 : A . A))) field unrestricted backendValueDivide : (pi unrestricted a0 : R . (pi unrestricted a1 : A . A)) field unrestricted backendValueJumpIf : (pi unrestricted a0 : (family TelemetryValueCondition) . (pi unrestricted a1 : Bytes . (pi unrestricted a2 : A . A))) field unrestricted backendValueJump : (pi unrestricted a0 : Bytes . (pi unrestricted a1 : A . A)) field unrestricted backendValueLabel : (pi unrestricted a0 : Bytes . (pi unrestricted a1 : A . A)) field unrestricted backendValueReturn : (pi unrestricted a0 : A . A) field unrestricted backendValueEnd : A field unrestricted backendValueResult : R field unrestricted backendValueInput : R field unrestricted backendValueDestination : R field unrestricted backendValueRemainderOrExtent : R field unrestricted backendValueCounter : R field unrestricted backendValueDivisor : R field unrestricted backendValueSourceCursor : R field unrestricted backendValueDestinationCursor : R field unrestricted backendValueNegative : R end-family def telemetryValueAssemblyFor = (lambda erased A : Type 0 . (lambda erased R : Type 0 . (lambda unrestricted backend : (family TelemetryValueBackend A R) . (lambda unrestricted kind : (family TelemetryValueRoutineKind) . (eliminate TelemetryValueBackend (lambda unrestricted current : (family TelemetryValueBackend A R) . A) backend (branch TelemetryValueBackendValue valueLoad64 valueLoad8 valueStore8 valueMove valueSet valueCompareImmediate valueCompare valueAdd valueAddImmediate valueSubtract valueShiftRight valueAndImmediate valueDivide valueJumpIf valueJump valueLabel valueReturn valueEnd valueResult valueInput valueDestination valueRemainderOrExtent valueCounter valueDivisor valueSourceCursor valueDestinationCursor valueNegative . (let unrestricted cellDecimalFinish = (valueLabel b"cell-space" (valueCompare valueDestinationCursor valueSourceCursor (valueJumpIf (constructor TelemetryValueCondition TelemetryValueZero) b"cell-complete" (valueSet valueResult 32 (valueStore8 valueDestinationCursor 0 valueResult (valueAddImmediate valueDestinationCursor 1 (valueJump b"cell-space" (valueLabel b"cell-complete" (valueSet valueResult 34 (valueStore8 valueDestination 0 valueResult (valueSet valueResult 0 (valueReturn (valueLabel b"cell-refused" (valueSet valueResult 4 (valueReturn valueEnd))))))))))))))) in (let unrestricted cellDecimalCopy = (valueMove valueSourceCursor valueDestination (valueAdd valueSourceCursor valueCounter (valueAddImmediate valueSourceCursor 1 (valueMove valueDestinationCursor valueDestination (valueAddImmediate valueDestinationCursor 1 (valueCompareImmediate valueNegative 0 (valueJumpIf (constructor TelemetryValueCondition TelemetryValueZero) b"cell-positive" (valueSet valueResult 45 (valueStore8 valueDestinationCursor 0 valueResult (valueAddImmediate valueDestinationCursor 1 (valueLabel b"cell-positive" (valueSet valueDivisor telemetryDecimalDigits (valueSubtract valueDivisor valueCounter (valueLabel b"cell-copy" (valueLoad8 valueResult valueSourceCursor 0 (valueStore8 valueDestinationCursor 0 valueResult (valueAddImmediate valueSourceCursor 1 (valueAddImmediate valueDestinationCursor 1 (valueAddImmediate valueDivisor 0xffffffff (valueCompareImmediate valueDivisor 0 (valueJumpIf (constructor TelemetryValueCondition TelemetryValueNotZero) b"cell-copy" (valueSet valueResult 34 (valueStore8 valueDestinationCursor 0 valueResult (valueAddImmediate valueDestinationCursor 1 (valueMove valueSourceCursor valueDestination (valueAddImmediate valueSourceCursor telemetryDecimalCellBytes cellDecimalFinish)))))))))))))))))))))))))) in (let unrestricted cellDecimalDigits = (valueSet valueCounter telemetryDecimalDigits (valueSet valueDivisor 10 (valueLabel b"cell-digit" (valueSet valueRemainderOrExtent 0 (valueDivide valueDivisor (valueAddImmediate valueRemainderOrExtent 48 (valueMove valueSourceCursor valueDestination (valueAdd valueSourceCursor valueCounter (valueStore8 valueSourceCursor 0 valueRemainderOrExtent (valueAddImmediate valueCounter 0xffffffff (valueCompareImmediate valueResult 0 (valueJumpIf (constructor TelemetryValueCondition TelemetryValueNotZero) b"cell-digit" cellDecimalCopy)))))))))))) in (let unrestricted cellDecimalAssembly = (lambda unrestricted signed : Nat . (valueCompareImmediate valueRemainderOrExtent telemetryDecimalCellBytes (valueJumpIf (constructor TelemetryValueCondition TelemetryValueBelow) b"cell-refused" (valueMove valueResult valueInput (valueSet valueNegative 0 (aosChoose A signed (valueMove valueNegative valueInput (valueShiftRight valueNegative 63 (valueCompareImmediate valueNegative 0 (valueJumpIf (constructor TelemetryValueCondition TelemetryValueZero) b"cell-magnitude" (valueSet valueResult 0 (valueSubtract valueResult valueInput (valueLabel b"cell-magnitude" cellDecimalDigits))))))) cellDecimalDigits)))))) in (let unrestricted cellHexNibble = (lambda unrestricted name : Bytes . (lambda unrestricted offset : Nat . (lambda unrestricted tail : A . (valueCompareImmediate valueResult 9 (valueJumpIf (constructor TelemetryValueCondition TelemetryValueAbove) (bytes-append name b"-letter") (valueAddImmediate valueResult 48 (valueJump (bytes-append name b"-store") (valueLabel (bytes-append name b"-letter") (valueAddImmediate valueResult 87 (valueLabel (bytes-append name b"-store") (valueStore8 valueDestination offset valueResult tail))))))))))) in (let unrestricted cellHexByte = (lambda unrestricted source : Nat . (lambda unrestricted index : Nat . (lambda unrestricted tail : A . (let unrestricted destination = (naturalAdd 1 (naturalMultiply 2 index)) in (let unrestricted name = (naturalDecimalBytesWithin 20 index) in (valueLoad8 valueResult valueInput source (valueShiftRight valueResult 4 (cellHexNibble (bytes-append name b"-high") destination (valueLoad8 valueResult valueInput source (valueAndImmediate valueResult 15 (cellHexNibble (bytes-append name b"-low") (succ destination) tail))))))))))) in (let unrestricted cellHexAssembly = (lambda unrestricted width : Nat . (lambda unrestricted reverse : Nat . (valueCompareImmediate valueRemainderOrExtent width (valueJumpIf (constructor TelemetryValueCondition TelemetryValueBelow) b"cell-hex-refused" (valueCompareImmediate valueCounter (telemetryHexCellBytes width) (valueJumpIf (constructor TelemetryValueCondition TelemetryValueBelow) b"cell-hex-refused" (nat-eliminate (lambda unrestricted current : Nat . A) (valueSet valueResult 34 (valueStore8 valueDestination 0 valueResult (valueStore8 valueDestination (naturalAdd 1 (naturalMultiply 2 width)) valueResult (valueSet valueResult 0 (valueReturn (valueLabel b"cell-hex-refused" (valueSet valueResult 4 (valueReturn valueEnd)))))))) (lambda unrestricted index : Nat . (lambda unrestricted induction : A . (cellHexByte (aosChoose Nat reverse (naturalSaturatingSubtract width (succ index)) index) index induction))) width))))))) in (eliminate TelemetryValueRoutineKind (lambda unrestricted current : (family TelemetryValueRoutineKind) . A) kind (branch TelemetryValueDecimalRoutine signed . (cellDecimalAssembly signed)) (branch TelemetryValueHexRoutine width reverse . (cellHexAssembly width reverse)) (branch TelemetryValueWordRoutine signed offset . (valueCompareImmediate valueRemainderOrExtent (naturalAdd offset captureWordBytes) (valueJumpIf (constructor TelemetryValueCondition TelemetryValueBelow) b"cell-refused" (valueCompareImmediate valueCounter telemetryDecimalCellBytes (valueJumpIf (constructor TelemetryValueCondition TelemetryValueBelow) b"cell-refused" (valueLoad64 valueInput valueInput offset (valueMove valueRemainderOrExtent valueCounter (cellDecimalAssembly signed)))))))) (branch TelemetryValueSliceRoutine width reverse offset . (valueCompareImmediate valueRemainderOrExtent (naturalAdd offset width) (valueJumpIf (constructor TelemetryValueCondition TelemetryValueBelow) b"cell-hex-refused" (valueCompareImmediate valueCounter (telemetryHexCellBytes width) (valueJumpIf (constructor TelemetryValueCondition TelemetryValueBelow) b"cell-hex-refused" (valueAddImmediate valueInput offset (cellHexAssembly width reverse)))))))))))))))))))))