module Runtime.TelemetryPolicyRoutine import Observe.Value import Runtime.TelemetryCapture import Runtime.TelemetryPublication import Std.Natural -- Shared leaf algorithms for selection, unsigned source arithmetic, flush -- cadence and continuation. Emitters own the calling convention and preserve -- their host interpreter's persistent registers. Word operations wrap at 64 -- bits; loads/stores are little-endian. Add supplies Below iff unsigned carry -- occurred. Compare supplies unsigned order. Divide takes Result with zero -- Argument2 as the unsigned dividend, returns quotient in Result and remainder -- in Argument2, and requires a positive divisor. Multiply supplies the wrapped -- low product in Result and may clobber Argument2; no high-product claim. -- SetWord retains all 64 bits, unlike an ISA's smaller immediate fields. family TelemetryPolicyCondition : Type 0 constructor TelemetryPolicyZero constructor TelemetryPolicyNotZero constructor TelemetryPolicyBelow constructor TelemetryPolicyAbove end-family family TelemetryPolicyBackend : Type 0 parameter erased A : Type 0 parameter erased R : Type 0 constructor TelemetryPolicyBackendValue field unrestricted backendPolicySet : (pi unrestricted a0 : R . (pi unrestricted a1 : Nat . (pi unrestricted a2 : A . A))) field unrestricted backendPolicySetWord : (pi unrestricted a0 : R . (pi unrestricted a1 : Nat . (pi unrestricted a2 : A . A))) field unrestricted backendPolicyMove : (pi unrestricted a0 : R . (pi unrestricted a1 : R . (pi unrestricted a2 : A . A))) field unrestricted backendPolicyStore : (pi unrestricted a0 : R . (pi unrestricted a1 : Nat . (pi unrestricted a2 : R . (pi unrestricted a3 : A . A)))) field unrestricted backendPolicyLoad : (pi unrestricted a0 : R . (pi unrestricted a1 : R . (pi unrestricted a2 : Nat . (pi unrestricted a3 : A . A)))) field unrestricted backendPolicyCompareImmediate : (pi unrestricted a0 : R . (pi unrestricted a1 : Nat . (pi unrestricted a2 : A . A))) field unrestricted backendPolicyCompare : (pi unrestricted a0 : R . (pi unrestricted a1 : R . (pi unrestricted a2 : A . A))) field unrestricted backendPolicySubtract : (pi unrestricted a0 : R . (pi unrestricted a1 : R . (pi unrestricted a2 : A . A))) field unrestricted backendPolicyAdd : (pi unrestricted a0 : R . (pi unrestricted a1 : R . (pi unrestricted a2 : A . A))) field unrestricted backendPolicyDivide : (pi unrestricted a0 : R . (pi unrestricted a1 : A . A)) field unrestricted backendPolicyMultiply : (pi unrestricted a0 : R . (pi unrestricted a1 : A . A)) field unrestricted backendPolicyJumpIf : (pi unrestricted a0 : (family TelemetryPolicyCondition) . (pi unrestricted a1 : Bytes . (pi unrestricted a2 : A . A))) field unrestricted backendPolicyJump : (pi unrestricted a0 : Bytes . (pi unrestricted a1 : A . A)) field unrestricted backendPolicyLabel : (pi unrestricted a0 : Bytes . (pi unrestricted a1 : A . A)) field unrestricted backendPolicyReturn : (pi unrestricted a0 : A . A) field unrestricted backendPolicyEnd : A field unrestricted backendPolicyResult : R field unrestricted backendPolicyArgument0 : R field unrestricted backendPolicyArgument1 : R field unrestricted backendPolicyArgument2 : R field unrestricted backendPolicyArgument3 : R field unrestricted backendPolicyArgument4 : R field unrestricted backendPolicyArgument5 : R field unrestricted backendPolicyScratch0 : R field unrestricted backendPolicyScratch1 : R end-family def telemetryPolicySiteAssemblyFor = (lambda erased A : Type 0 . (lambda erased R : Type 0 . (lambda unrestricted backend : (family TelemetryPolicyBackend A R) . (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (lambda unrestricted required : Nat . (lambda unrestricted enabled : Nat . (lambda unrestricted stride : Nat . (lambda unrestricted bound : Nat . (eliminate TelemetryPolicyBackend (lambda unrestricted current : (family TelemetryPolicyBackend A R) . A) backend (branch TelemetryPolicyBackendValue policySet policySetWord policyMove policyStore policyLoad policyCompareImmediate policyCompare policySubtract policyAdd policyDivide policyMultiply policyJumpIf policyJump policyLabel policyReturn policyEnd policyResult policyArgument0 policyArgument1 policyArgument2 policyArgument3 policyArgument4 policyArgument5 policyScratch0 policyScratch1 . (policySet policyResult 4 (policyStore policyArgument3 0 policyResult (policyCompareImmediate policyArgument4 (publicationArenaBytesForBody bound) (policyJumpIf (constructor TelemetryPolicyCondition TelemetryPolicyNotZero) b"site-refused" (policyLoad policyResult policyArgument0 captureOrdinaryCapacityAt (policyCompareImmediate policyResult ordinaryCapacity (policyJumpIf (constructor TelemetryPolicyCondition TelemetryPolicyNotZero) b"site-refused" (policyLoad policyResult policyArgument0 captureReservedCapacityAt (policyCompareImmediate policyResult reservedCapacity (policyJumpIf (constructor TelemetryPolicyCondition TelemetryPolicyNotZero) b"site-refused" (policyLoad policyResult policyArgument0 captureRequiredAt (policyCompareImmediate policyResult required (policyJumpIf (constructor TelemetryPolicyCondition TelemetryPolicyNotZero) b"site-refused" (policyLoad policyResult policyArgument1 publicationFinishedAt (policyCompareImmediate policyResult 0 (policyJumpIf (constructor TelemetryPolicyCondition TelemetryPolicyNotZero) b"site-refused" (aosChoose A enabled (aosChoose A (naturalEqual stride 1) (policySet policyResult 1 (policyStore policyArgument3 0 policyResult (policySet policyResult 1 (policyReturn (policyLabel b"site-excluded" (policySet policyResult 0 (policyStore policyArgument3 0 policyResult (policySet policyResult 1 (policyReturn (policyLabel b"site-refused" (policySet policyResult 0 (policyReturn policyEnd)))))))))))) (policyMove policyResult policyArgument2 (policySet policyArgument2 0 (policySetWord policyArgument4 stride (policyDivide policyArgument4 (policyCompareImmediate policyArgument2 0 (policyJumpIf (constructor TelemetryPolicyCondition TelemetryPolicyNotZero) b"site-excluded" (policySet policyResult 1 (policyStore policyArgument3 0 policyResult (policySet policyResult 1 (policyReturn (policyLabel b"site-excluded" (policySet policyResult 0 (policyStore policyArgument3 0 policyResult (policySet policyResult 1 (policyReturn (policyLabel b"site-refused" (policySet policyResult 0 (policyReturn policyEnd))))))))))))))))))) (policyJump b"site-excluded" (policySet policyResult 1 (policyStore policyArgument3 0 policyResult (policySet policyResult 1 (policyReturn (policyLabel b"site-excluded" (policySet policyResult 0 (policyStore policyArgument3 0 policyResult (policySet policyResult 1 (policyReturn (policyLabel b"site-refused" (policySet policyResult 0 (policyReturn policyEnd))))))))))))))))))))))))))))))))))))))))) def telemetryPolicyFlushAssemblyFor = (lambda erased A : Type 0 . (lambda erased R : Type 0 . (lambda unrestricted backend : (family TelemetryPolicyBackend A R) . (lambda unrestricted threshold : Nat . (lambda unrestricted bound : Nat . (eliminate TelemetryPolicyBackend (lambda unrestricted current : (family TelemetryPolicyBackend A R) . A) backend (branch TelemetryPolicyBackendValue policySet policySetWord policyMove policyStore policyLoad policyCompareImmediate policyCompare policySubtract policyAdd policyDivide policyMultiply policyJumpIf policyJump policyLabel policyReturn policyEnd policyResult policyArgument0 policyArgument1 policyArgument2 policyArgument3 policyArgument4 policyArgument5 policyScratch0 policyScratch1 . (policySet policyResult 7 (policyStore policyArgument4 0 policyResult (policyCompareImmediate policyArgument5 (publicationArenaBytesForBody bound) (policyJumpIf (constructor TelemetryPolicyCondition TelemetryPolicyNotZero) b"policy-flush-invalid" (policyCompareImmediate policyArgument3 1 (policyJumpIf (constructor TelemetryPolicyCondition TelemetryPolicyAbove) b"policy-flush-invalid" (policyCompareImmediate policyArgument2 4 (policyJumpIf (constructor TelemetryPolicyCondition TelemetryPolicyAbove) b"policy-flush-invalid" (policyJumpIf (constructor TelemetryPolicyCondition TelemetryPolicyZero) b"policy-flush-invalid" (policyLoad policyResult policyArgument1 publicationFinishedAt (policyCompareImmediate policyResult 1 (policyJumpIf (constructor TelemetryPolicyCondition TelemetryPolicyAbove) b"policy-flush-invalid" (policyJumpIf (constructor TelemetryPolicyCondition TelemetryPolicyZero) b"policy-flush-closed" (policyLoad policyResult policyArgument1 publicationPoisonedAt (policyCompareImmediate policyResult 1 (policyJumpIf (constructor TelemetryPolicyCondition TelemetryPolicyAbove) b"policy-flush-invalid" (policyJumpIf (constructor TelemetryPolicyCondition TelemetryPolicyZero) b"policy-flush-poisoned" (policyCompareImmediate policyArgument2 3 (policyJumpIf (constructor TelemetryPolicyCondition TelemetryPolicyNotZero) b"policy-flush-terminal" (policyCompareImmediate policyArgument3 1 (policyJumpIf (constructor TelemetryPolicyCondition TelemetryPolicyZero) b"policy-flush-invalid" (policyJump b"policy-flush-requested" (policyLabel b"policy-flush-terminal" (policyCompareImmediate policyArgument3 1 (policyJumpIf (constructor TelemetryPolicyCondition TelemetryPolicyZero) b"policy-flush-requested" (policySetWord policyArgument5 threshold (policyLoad policyResult policyArgument0 captureNextSequenceAt (policyLoad policyScratch0 policyArgument1 publicationPublishedNextAt (policyCompare policyResult policyScratch0 (policyJumpIf (constructor TelemetryPolicyCondition TelemetryPolicyBelow) b"policy-flush-invalid" (policySubtract policyResult policyScratch0 (policyCompare policyResult policyArgument5 (policyJumpIf (constructor TelemetryPolicyCondition TelemetryPolicyAbove) b"policy-flush-requested" (policyJumpIf (constructor TelemetryPolicyCondition TelemetryPolicyZero) b"policy-flush-requested" (policyLoad policyScratch1 policyArgument0 captureExcludedAt (policyLoad policyScratch0 policyArgument1 publicationPublishedExcludedAt (policyCompare policyScratch1 policyScratch0 (policyJumpIf (constructor TelemetryPolicyCondition TelemetryPolicyBelow) b"policy-flush-invalid" (policySubtract policyScratch1 policyScratch0 (policyCompare policyScratch1 policyArgument5 (policyJumpIf (constructor TelemetryPolicyCondition TelemetryPolicyAbove) b"policy-flush-requested" (policyJumpIf (constructor TelemetryPolicyCondition TelemetryPolicyZero) b"policy-flush-requested" (policyAdd policyResult policyScratch1 (policyJumpIf (constructor TelemetryPolicyCondition TelemetryPolicyBelow) b"policy-flush-requested" (policyCompare policyResult policyArgument5 (policyJumpIf (constructor TelemetryPolicyCondition TelemetryPolicyAbove) b"policy-flush-requested" (policyJumpIf (constructor TelemetryPolicyCondition TelemetryPolicyZero) b"policy-flush-requested" (policySet policyResult 0 (policyReturn (policyLabel b"policy-flush-requested" (policySet policyResult 1 (policyReturn (policyLabel b"policy-flush-invalid" (policySet policyResult 4 (policyStore policyArgument4 0 policyResult (policySet policyResult 0 (policyReturn (policyLabel b"policy-flush-closed" (policySet policyResult 5 (policyStore policyArgument4 0 policyResult (policySet policyResult 0 (policyReturn (policyLabel b"policy-flush-poisoned" (policySet policyResult 6 (policyStore policyArgument4 0 policyResult (policySet policyResult 0 (policyReturn policyEnd)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) def telemetryPolicyAffineAssemblyFor = (lambda erased A : Type 0 . (lambda erased R : Type 0 . (lambda unrestricted backend : (family TelemetryPolicyBackend A R) . (eliminate TelemetryPolicyBackend (lambda unrestricted current : (family TelemetryPolicyBackend A R) . A) backend (branch TelemetryPolicyBackendValue policySet policySetWord policyMove policyStore policyLoad policyCompareImmediate policyCompare policySubtract policyAdd policyDivide policyMultiply policyJumpIf policyJump policyLabel policyReturn policyEnd policyResult policyArgument0 policyArgument1 policyArgument2 policyArgument3 policyArgument4 policyArgument5 policyScratch0 policyScratch1 . (policyMove policyResult policyArgument0 (policyMove policyArgument4 policyArgument2 (policyMultiply policyArgument4 (policyAdd policyResult policyArgument1 (policyStore policyArgument3 0 policyResult (policySet policyResult 0 (policyReturn policyEnd)))))))))))) def telemetryPolicyPendingAssemblyFor = (lambda erased A : Type 0 . (lambda erased R : Type 0 . (lambda unrestricted backend : (family TelemetryPolicyBackend A R) . (eliminate TelemetryPolicyBackend (lambda unrestricted current : (family TelemetryPolicyBackend A R) . A) backend (branch TelemetryPolicyBackendValue policySet policySetWord policyMove policyStore policyLoad policyCompareImmediate policyCompare policySubtract policyAdd policyDivide policyMultiply policyJumpIf policyJump policyLabel policyReturn policyEnd policyResult policyArgument0 policyArgument1 policyArgument2 policyArgument3 policyArgument4 policyArgument5 policyScratch0 policyScratch1 . (policyCompareImmediate policyArgument0 3 (policyJumpIf (constructor TelemetryPolicyCondition TelemetryPolicyNotZero) b"capture-not-pending" (policySet policyResult 1 (policyReturn (policyLabel b"capture-not-pending" (policySet policyResult 0 (policyReturn policyEnd)))))))))))) def telemetryPolicyContinuationAssemblyFor = (lambda erased A : Type 0 . (lambda erased R : Type 0 . (lambda unrestricted backend : (family TelemetryPolicyBackend A R) . (lambda unrestricted required : Nat . (eliminate TelemetryPolicyBackend (lambda unrestricted current : (family TelemetryPolicyBackend A R) . A) backend (branch TelemetryPolicyBackendValue policySet policySetWord policyMove policyStore policyLoad policyCompareImmediate policyCompare policySubtract policyAdd policyDivide policyMultiply policyJumpIf policyJump policyLabel policyReturn policyEnd policyResult policyArgument0 policyArgument1 policyArgument2 policyArgument3 policyArgument4 policyArgument5 policyScratch0 policyScratch1 . (policyCompareImmediate policyArgument0 1 (policyJumpIf (constructor TelemetryPolicyCondition TelemetryPolicyBelow) b"capture-continuation-allowed" (policyJumpIf (constructor TelemetryPolicyCondition TelemetryPolicyZero) b"capture-continuation-allowed" (aosChoose A (naturalEqual required 0) (policyCompareImmediate policyArgument0 2 (policyJumpIf (constructor TelemetryPolicyCondition TelemetryPolicyZero) b"capture-continuation-allowed" (policySet policyResult 0 (policyReturn (policyLabel b"capture-continuation-allowed" (policySet policyResult 1 (policyReturn policyEnd))))))) (policySet policyResult 0 (policyReturn (policyLabel b"capture-continuation-allowed" (policySet policyResult 1 (policyReturn policyEnd)))))))))))))))