module Runtime.TelemetryRecord import Data.Bytes import Data.JSON import Data.JSONRender import Observe.Interchange import Observe.Value import Runtime.ArenaCertificate import Runtime.TelemetryCapture import Runtime.TelemetryIdentity import Runtime.TelemetryValue import Std.Natural -- A source-declared, fixed-shape drain recipe. Acquisition still records its -- original sequence and eight binary words. No learning convention is inferred -- from their positions. A program chooses the typed projection it actually -- captured; the shared renderer derives every destination offset. family TelemetryRecordParts : Type 0 constructor TelemetryRecordEnd constructor TelemetryRecordLiteral field unrestricted telemetryRecordLiteralBytes : Bytes recursive unrestricted telemetryRecordLiteralTail constructor TelemetryRecordDecimal field unrestricted telemetryRecordDecimalSigned : Nat field unrestricted telemetryRecordDecimalOffset : Nat recursive unrestricted telemetryRecordDecimalTail constructor TelemetryRecordHex field unrestricted telemetryRecordHexSource : Nat field unrestricted telemetryRecordHexOffset : Nat field unrestricted telemetryRecordHexWidth : Nat field unrestricted telemetryRecordHexReverse : Nat field unrestricted telemetryRecordHexNonzero : Nat recursive unrestricted telemetryRecordHexTail end-family -- Word indices refer to the captured values, excluding the sequence. Ref128 -- consumes two consecutive words. Absence is an explicit slot, not a zero. -- Lists/maps remain the existing tagged AOS structures. Their member/item -- chains are internal roles: whole-event admission rejects misuse of a chain, -- duplicate object keys, invalid constants or absence nested as a tagged value. family TelemetryCaptureValue : Type 0 constructor TelemetryConstant field unrestricted telemetryConstantValue : (family AosValue) constructor TelemetryUnsigned field unrestricted telemetryUnsignedWord : Nat constructor TelemetrySigned field unrestricted telemetrySignedWord : Nat constructor TelemetryFloat32 field unrestricted telemetryFloat32Word : Nat constructor TelemetryFloat64 field unrestricted telemetryFloat64Word : Nat constructor TelemetryReference field unrestricted telemetryReferenceKind : Bytes field unrestricted telemetryReferenceWord : Nat constructor TelemetryBytes field unrestricted telemetryBytesWord : Nat field unrestricted telemetryBytesWidth : Nat constructor TelemetryUnavailable field unrestricted telemetryUnavailableState : Bytes field unrestricted telemetryUnavailableReason : Bytes constructor TelemetryList recursive unrestricted telemetryListItems constructor TelemetryItemsEnd constructor TelemetryItemsNext recursive unrestricted telemetryItemsHead recursive unrestricted telemetryItemsTail constructor TelemetryMap recursive unrestricted telemetryMapMembers constructor TelemetryMembersEnd constructor TelemetryMembersNext field unrestricted telemetryMembersKey : Bytes recursive unrestricted telemetryMembersHead recursive unrestricted telemetryMembersTail end-family -- The public renderer accepts a declaration, not arbitrary byte parts. In -- particular, event identity/sequence patches are always derived here; a -- caller cannot supply a valid-looking envelope bound to another producer. family TelemetryRecordDeclaration : Type 0 constructor TelemetryRecordDeclarationValue field unrestricted telemetryDeclarationSchema : Bytes field unrestricted telemetryDeclarationClass : Bytes field unrestricted telemetryDeclarationPolicy : Bytes field unrestricted telemetryDeclarationOrigin : Bytes field unrestricted telemetryDeclarationMethod : Bytes field unrestricted telemetryDeclarationPayload : (family TelemetryCaptureValue) end-family -- A compiled drain plan, not a proof token. Construct it with -- (compile-time (telemetryRecordPlan declaration)); the Alpha kernel -- validates the complete closed declaration once and materializes bounded -- first-order plan data. Rejected plans cannot lower into executable code. -- As with AosLineValid, clients must use its owning validator rather than -- manufacture a Ready value. Reader admission independently validates output. family TelemetryRecordPlan : Type 0 constructor TelemetryRecordReady field unrestricted telemetryRecordPlanParts : (family TelemetryRecordParts) field unrestricted telemetryRecordPlanTemplate : Bytes constructor TelemetryRecordRefused field unrestricted telemetryRecordPlanReason : Bytes end-family def telemetryRecordLiteral = (lambda unrestricted bytes : Bytes . (constructor TelemetryRecordParts TelemetryRecordLiteral bytes (constructor TelemetryRecordParts TelemetryRecordEnd))) def telemetryRecordAppend = (lambda unrestricted left : (family TelemetryRecordParts) . (lambda unrestricted right : (family TelemetryRecordParts) . (eliminate TelemetryRecordParts (lambda unrestricted current : (family TelemetryRecordParts) . (family TelemetryRecordParts)) left (branch TelemetryRecordEnd . right) (branch TelemetryRecordLiteral bytes tail induction . (constructor TelemetryRecordParts TelemetryRecordLiteral bytes induction)) (branch TelemetryRecordDecimal signed offset tail induction . (constructor TelemetryRecordParts TelemetryRecordDecimal signed offset induction)) (branch TelemetryRecordHex source offset width reverse nonzero tail induction . (constructor TelemetryRecordParts TelemetryRecordHex source offset width reverse nonzero induction))))) def telemetryRecordWrap = (lambda unrestricted before : Bytes . (lambda unrestricted value : (family TelemetryRecordParts) . (lambda unrestricted after : Bytes . (telemetryRecordAppend (telemetryRecordLiteral before) (telemetryRecordAppend value (telemetryRecordLiteral after)))))) def telemetryRecordJSON = (lambda unrestricted value : (family JSON) . (eliminate JSONRenderResult (lambda unrestricted current : (family JSONRenderResult) . Bytes) (renderJSON value) (branch JSONRendered bytes . bytes) (branch JSONRenderFailed error . b""))) def telemetryRecordString = (lambda unrestricted value : Bytes . (telemetryRecordJSON (constructor JSON JSONString value))) -- The schema uses the same revision/class as its event declaration. Field -- meanings and expected types remain explicit source declarations; this does -- not infer learning semantics from positions in a native capture record. def telemetryRecordSchemaJSON = (lambda unrestricted declaration : (family TelemetryRecordDeclaration) . (lambda unrestricted owner : Bytes . (lambda unrestricted fields : (family JSON) . (eliminate TelemetryRecordDeclaration (lambda unrestricted current : (family TelemetryRecordDeclaration) . (family JSON)) declaration (branch TelemetryRecordDeclarationValue schema recordClass policy origin method payload . (aosDescriptorRecord b"schema" (bytes-append b"schema:" schema) (constructor JSON JSONObject (constructor JSON JSONObjectMember b"schema_id" (constructor JSON JSONString schema) (constructor JSON JSONObjectMember b"record_class" (constructor JSON JSONString recordClass) (constructor JSON JSONObjectMember b"owner" (constructor JSON JSONString owner) (constructor JSON JSONObjectMember b"fields" fields (constructor JSON JSONObjectEnd)))))))))))) def telemetryCapturedWordAt = (lambda unrestricted index : Nat . (naturalAdd captureValuesAt (naturalMultiply index captureWordBytes))) def telemetryRecordDecimalPart = (lambda unrestricted signed : Nat . (lambda unrestricted index : Nat . (constructor TelemetryRecordParts TelemetryRecordDecimal signed (telemetryCapturedWordAt index) (constructor TelemetryRecordParts TelemetryRecordEnd)))) def telemetryRecordHexPart = (lambda unrestricted source : Nat . (lambda unrestricted offset : Nat . (lambda unrestricted width : Nat . (lambda unrestricted reverse : Nat . (lambda unrestricted nonzero : Nat . (constructor TelemetryRecordParts TelemetryRecordHex source offset width reverse nonzero (constructor TelemetryRecordParts TelemetryRecordEnd))))))) def telemetryRecordValueIsEnd = (lambda unrestricted value : (family TelemetryCaptureValue) . (eliminate TelemetryCaptureValue (lambda unrestricted current : (family TelemetryCaptureValue) . Nat) value (branch TelemetryConstant constant . 0) (branch TelemetryUnsigned index . 0) (branch TelemetrySigned index . 0) (branch TelemetryFloat32 index . 0) (branch TelemetryFloat64 index . 0) (branch TelemetryReference kind index . 0) (branch TelemetryBytes index width . 0) (branch TelemetryUnavailable state reason . 0) (branch TelemetryList items induction . 0) (branch TelemetryItemsEnd . 1) (branch TelemetryItemsNext head tail headInduction tailInduction . 0) (branch TelemetryMap members induction . 0) (branch TelemetryMembersEnd . 1) (branch TelemetryMembersNext key head tail headInduction tailInduction . 0))) def telemetryRecordSeparator = (lambda unrestricted tail : (family TelemetryCaptureValue) . (aosChoose Bytes (telemetryRecordValueIsEnd tail) b"" b",")) def telemetryRecordValue = (lambda unrestricted value : (family TelemetryCaptureValue) . (eliminate TelemetryCaptureValue (lambda unrestricted current : (family TelemetryCaptureValue) . (family TelemetryRecordParts)) value (branch TelemetryConstant constant . (telemetryRecordLiteral (aosEncodeValue constant))) (branch TelemetryUnsigned index . (telemetryRecordWrap b"{\"t\":\"u64\",\"v\":" (telemetryRecordDecimalPart 0 index) b"}")) (branch TelemetrySigned index . (telemetryRecordWrap b"{\"t\":\"i64\",\"v\":" (telemetryRecordDecimalPart 1 index) b"}")) (branch TelemetryFloat32 index . (telemetryRecordWrap b"{\"t\":\"f32\",\"bits\":" (telemetryRecordHexPart 0 (telemetryCapturedWordAt index) (naturalDivideUnchecked captureWordBytes 2) 1 0) b"}")) (branch TelemetryFloat64 index . (telemetryRecordWrap b"{\"t\":\"f64\",\"bits\":" (telemetryRecordHexPart 0 (telemetryCapturedWordAt index) captureWordBytes 1 0) b"}")) (branch TelemetryReference kind index . (telemetryRecordWrap (bytes-append b"{\"t\":\"ref\",\"kind\":" (bytes-append (telemetryRecordString kind) b",\"id\":")) (telemetryRecordHexPart 0 (telemetryCapturedWordAt index) telemetryIdentityBytes 0 1) b"}")) (branch TelemetryBytes index width . (telemetryRecordWrap b"{\"t\":\"bytes\",\"hex\":" (telemetryRecordHexPart 0 (telemetryCapturedWordAt index) width 0 0) b"}")) (branch TelemetryUnavailable state reason . (telemetryRecordLiteral (bytes-append b"{\"state\":" (bytes-append (telemetryRecordString state) (bytes-append b",\"reason\":{\"code\":" (bytes-append (telemetryRecordString reason) b"}}")))))) (branch TelemetryList items induction . (telemetryRecordWrap b"{\"t\":\"list\",\"v\":[" induction b"]}")) (branch TelemetryItemsEnd . (constructor TelemetryRecordParts TelemetryRecordEnd)) (branch TelemetryItemsNext head tail headInduction tailInduction . (telemetryRecordAppend headInduction (telemetryRecordAppend (telemetryRecordLiteral (telemetryRecordSeparator tail)) tailInduction))) (branch TelemetryMap members induction . (telemetryRecordWrap b"{\"t\":\"map\",\"v\":{" induction b"}}")) (branch TelemetryMembersEnd . (constructor TelemetryRecordParts TelemetryRecordEnd)) (branch TelemetryMembersNext key head tail headInduction tailInduction . (telemetryRecordWrap (bytes-append (telemetryRecordString key) b":") (telemetryRecordAppend headInduction (telemetryRecordAppend (telemetryRecordLiteral (telemetryRecordSeparator tail)) tailInduction)) b"")))) -- The skeleton is a valid line using nonzero sentinel identities. Those are -- compile-time shape witnesses only; preflight requires real nonzero runtime -- bindings and native patches replace every identity before a record succeeds. def telemetryRecordHexWitness = (lambda unrestricted width : Nat . (telemetryHexCell (bytes-append (dataBytesRepeatByte (byte 0) (naturalSaturatingSubtract width 1)) b"\x01"))) def telemetryRecordPartBytes : (pi unrestricted parts : (family TelemetryRecordParts) . Bytes) = (lambda unrestricted parts : (family TelemetryRecordParts) . (bytes-builder-build (eliminate TelemetryRecordParts (lambda unrestricted current : (family TelemetryRecordParts) . BytesBuilder) parts (branch TelemetryRecordEnd . (bytes-builder-empty)) (branch TelemetryRecordLiteral bytes tail induction . (bytes-builder-append (bytes-builder-chunk bytes) induction)) (branch TelemetryRecordDecimal signed offset tail induction . (bytes-builder-append (bytes-builder-chunk (telemetryDecimalCell 0 0)) induction)) (branch TelemetryRecordHex source offset width reverse nonzero tail induction . (bytes-builder-append (bytes-builder-chunk (telemetryRecordHexWitness width)) induction))))) def telemetryRecordPartsAdmission = (lambda unrestricted parts : (family TelemetryRecordParts) . (eliminate TelemetryRecordParts (lambda unrestricted current : (family TelemetryRecordParts) . Nat) parts (branch TelemetryRecordEnd . 1) (branch TelemetryRecordLiteral bytes tail induction . induction) (branch TelemetryRecordDecimal signed offset tail induction . (naturalAnd induction (naturalAnd (naturalLessOrEqual signed 1) (naturalIsZero (telemetryWordCellAdmission offset captureRecordBytes telemetryDecimalCellBytes))))) (branch TelemetryRecordHex source offset width reverse nonzero tail induction . (naturalAnd induction (naturalAnd (naturalLessOrEqual source 1) (naturalAnd (naturalLessOrEqual nonzero 1) (naturalAnd (aosChoose Nat nonzero (naturalEqual width telemetryIdentityBytes) 1) (naturalIsZero (telemetryHexSliceCellAdmission width reverse offset (aosChoose Nat source telemetryIdentitySetBytes captureRecordBytes) (telemetryHexCellBytes telemetryHexSourceMaximumBytes)))))))))) -- Record shape is validated by the maintained AOS owner, not a second parser. -- Cross-record schema/sequence/capture admission is the publisher's job. def telemetryRecordBytesAdmission : (pi unrestricted bytes : Bytes . Nat) = (lambda unrestricted bytes : Bytes . (naturalAnd (naturalLessOrEqual (bytes-length bytes) 65536) (naturalAnd (naturalIsZero (aosAnyByte (lambda unrestricted b : Byte . (byte-equal b (byte 10))) bytes)) (naturalIsZero (aosLineCode bytes))))) def telemetryRecordAdmission : (pi unrestricted parts : (family TelemetryRecordParts) . Nat) = (lambda unrestricted parts : (family TelemetryRecordParts) . (naturalAnd (telemetryRecordPartsAdmission parts) (telemetryRecordBytesAdmission (telemetryRecordPartBytes parts)))) def telemetryRecordStatusBytes = captureWordBytes def telemetryRecordAt = telemetryRecordStatusBytes def telemetryRecordArenaBytes = (lambda unrestricted parts : (family TelemetryRecordParts) . (naturalAdd telemetryRecordAt (bytes-length (telemetryRecordPartBytes parts)))) def telemetryRecordArenaResidents = (lambda unrestricted base : Nat . (lambda unrestricted parts : (family TelemetryRecordParts) . (constructor ArenaResidents ArenaResidentsNext (constructor ArenaResident ArenaResidentValue b"record-status" base telemetryRecordStatusBytes captureWordBytes) (constructor ArenaResidents ArenaResidentsNext (constructor ArenaResident ArenaResidentValue b"record-json" (naturalAdd base telemetryRecordAt) (bytes-length (telemetryRecordPartBytes parts)) 1) (constructor ArenaResidents ArenaResidentsEnd))))) -- Roles: tagged value/availability slot=0, item chain=1, member chain=2, -- invalid structure=3. A valid-looking JSON tail cannot change the declared -- Alpha structure (for example, a scalar in place of an item-chain tail). def telemetryRecordValueRole = (lambda unrestricted value : (family TelemetryCaptureValue) . (eliminate TelemetryCaptureValue (lambda unrestricted current : (family TelemetryCaptureValue) . Nat) value (branch TelemetryConstant constant . 0) (branch TelemetryUnsigned index . 0) (branch TelemetrySigned index . 0) (branch TelemetryFloat32 index . 0) (branch TelemetryFloat64 index . 0) (branch TelemetryReference kind index . 0) (branch TelemetryBytes index width . 0) (branch TelemetryUnavailable state reason . 0) (branch TelemetryList items induction . (aosChoose Nat (naturalEqual induction 1) 0 3)) (branch TelemetryItemsEnd . 1) (branch TelemetryItemsNext head tail headInduction tailInduction . (aosChoose Nat (naturalAnd (naturalEqual headInduction 0) (naturalEqual tailInduction 1)) 1 3)) (branch TelemetryMap members induction . (aosChoose Nat (naturalEqual induction 2) 0 3)) (branch TelemetryMembersEnd . 2) (branch TelemetryMembersNext key head tail headInduction tailInduction . (aosChoose Nat (naturalAnd (naturalEqual headInduction 0) (naturalEqual tailInduction 2)) 2 3)))) def telemetryRecordContextBytes = (lambda unrestricted context : Bytes . (aosChoose Bytes (naturalIsZero (bytes-length context)) b"{\"state\":\"not_recorded\",\"reason\":{\"code\":\"native-capture-context-not-acquired\"}}" (bytes-append b"{\"state\":\"present\",\"value\":{\"id\":" (bytes-append (telemetryRecordString context) b"}}")))) -- Time remains unacquired. An explicit source context is distinct from an -- inferred runtime span or a clock correlation. def telemetryEventRecordAtContext = (lambda unrestricted context : Bytes . (lambda unrestricted schema : Bytes . (lambda unrestricted recordClass : Bytes . (lambda unrestricted policy : Bytes . (lambda unrestricted origin : Bytes . (lambda unrestricted method : Bytes . (lambda unrestricted payload : (family TelemetryCaptureValue) . (aosChoose (family TelemetryRecordParts) (naturalEqual (telemetryRecordValueRole payload) 2) (telemetryRecordAppend (telemetryRecordLiteral b"{\"format\":\"AOS-JSON/1\",\"type\":\"event\",\"aos_version\":\"1.0\",\"event_id\":{\"attempt_id\":") (telemetryRecordAppend (telemetryRecordHexPart 1 (telemetryIdentityOffset telemetryAttemptIdentityIndex) telemetryIdentityBytes 0 1) (telemetryRecordAppend (telemetryRecordLiteral b",\"producer_id\":") (telemetryRecordAppend (telemetryRecordHexPart 1 (telemetryIdentityOffset telemetryProducerIdentityIndex) telemetryIdentityBytes 0 1) (telemetryRecordAppend (telemetryRecordLiteral b",\"producer_epoch\":") (telemetryRecordAppend (telemetryRecordHexPart 1 (telemetryIdentityOffset telemetryProducerEpochIndex) telemetryIdentityBytes 0 1) (telemetryRecordAppend (telemetryRecordLiteral b",\"sequence\":") (constructor TelemetryRecordParts TelemetryRecordDecimal 0 captureSequenceAt (telemetryRecordAppend (telemetryRecordLiteral b"},\"schema_id\":") (telemetryRecordAppend (telemetryRecordLiteral (telemetryRecordString schema)) (telemetryRecordAppend (telemetryRecordLiteral b",\"record_class\":") (telemetryRecordAppend (telemetryRecordLiteral (telemetryRecordString recordClass)) (telemetryRecordAppend (telemetryRecordLiteral b",\"policy_id\":") (telemetryRecordAppend (telemetryRecordLiteral (telemetryRecordString policy)) (telemetryRecordAppend (telemetryRecordLiteral b",\"origin\":{\"kind\":") (telemetryRecordAppend (telemetryRecordLiteral (telemetryRecordString origin)) (telemetryRecordAppend (telemetryRecordLiteral b",\"method\":") (telemetryRecordAppend (telemetryRecordLiteral (telemetryRecordString method)) (telemetryRecordAppend (telemetryRecordLiteral (bytes-append b"},\"time\":{\"state\":\"not_recorded\",\"reason\":{\"code\":\"native-capture-clock-not-acquired\"}},\"context\":" (bytes-append (telemetryRecordContextBytes context) b",\"payload\":{"))) (telemetryRecordAppend (telemetryRecordValue payload) (telemetryRecordAppend (telemetryRecordLiteral b"},\"extensions\":[],\"required_extensions\":[]}") (constructor TelemetryRecordParts TelemetryRecordEnd)))))))))))))))))))))) (constructor TelemetryRecordParts TelemetryRecordEnd))))))))) def telemetryEventRecord = (telemetryEventRecordAtContext b"") def telemetryRecordDeclarationPartsAtContext : (pi unrestricted context : Bytes . (pi unrestricted declaration : (family TelemetryRecordDeclaration) . (family TelemetryRecordParts))) = (lambda unrestricted context : Bytes . (lambda unrestricted declaration : (family TelemetryRecordDeclaration) . (eliminate TelemetryRecordDeclaration (lambda unrestricted current : (family TelemetryRecordDeclaration) . (family TelemetryRecordParts)) declaration (branch TelemetryRecordDeclarationValue schema recordClass policy origin method payload . (telemetryEventRecordAtContext context schema recordClass policy origin method payload))))) def telemetryRecordDeclarationParts = (telemetryRecordDeclarationPartsAtContext b"") def telemetryRecordPlanAtContext = (lambda unrestricted context : Bytes . (lambda unrestricted declaration : (family TelemetryRecordDeclaration) . (let unrestricted parts = (telemetryRecordDeclarationPartsAtContext context declaration) in (aosChoose (family TelemetryRecordPlan) (telemetryRecordAdmission parts) (constructor TelemetryRecordPlan TelemetryRecordReady parts (telemetryRecordPartBytes parts)) (constructor TelemetryRecordPlan TelemetryRecordRefused b"native-record-declaration-refused"))))) def telemetryRecordPlan = (telemetryRecordPlanAtContext b"") def telemetryRecordWordRequired = (lambda unrestricted parts : (family TelemetryRecordParts) . (lambda unrestricted index : Nat . (let unrestricted start = (telemetryCapturedWordAt index) in (let unrestricted end = (naturalAdd start captureWordBytes) in (eliminate TelemetryRecordParts (lambda unrestricted current : (family TelemetryRecordParts) . Nat) parts (branch TelemetryRecordEnd . 0) (branch TelemetryRecordLiteral bytes tail induction . induction) (branch TelemetryRecordDecimal signed offset tail induction . (naturalOr induction (naturalAnd (naturalLess index captureValueWords) (naturalAnd (naturalLess start (naturalAdd offset captureWordBytes)) (naturalLess offset end))))) (branch TelemetryRecordHex source offset width reverse nonzero tail induction . (naturalOr induction (naturalAnd (naturalEqual source 0) (naturalAnd (naturalLess index captureValueWords) (naturalAnd (naturalLess start (naturalAdd offset width)) (naturalLess offset end)))))))))))