module Runtime.TelemetryPolicy import Data.Bytes import Data.JSON import Observe.CapturePolicy import Observe.Interchange import Observe.Stream import Observe.Value import Runtime.ArenaCertificate import Runtime.TelemetryCapture import Runtime.TelemetryDrain import Runtime.TelemetryPublication import Runtime.TelemetryRecord import Std.List import Std.Natural -- This is compiled, validated data, not an unforgeable proof token. The -- policy binds each queue to a declared static source context and recipe. family TelemetryPolicyPlan : Type 0 constructor TelemetryPolicyReady field unrestricted telemetryPolicyDeclaration : (family CapturePolicy) field unrestricted telemetryPolicyOrdinarySite : (family CaptureSite) field unrestricted telemetryPolicyReservedSite : (family CaptureSite) field unrestricted telemetryPolicyDrain : (family TelemetryDrainPlan) constructor TelemetryPolicyRefused field unrestricted telemetryPolicyRefusal : Bytes end-family -- Source sites stay visible in metadata even when their profile excludes -- them. Only selected sites enter the compiled capture route inventories. family TelemetryPolicySites : Type 0 constructor TelemetryPolicySitesEnd constructor TelemetryPolicySitesNext field unrestricted telemetryPolicySiteTag : Nat field unrestricted telemetryPolicySiteDeclaration : (family CaptureSite) field unrestricted telemetryPolicySiteRecord : (family TelemetryRecordDeclaration) recursive unrestricted telemetryPolicySitesTail end-family family TelemetryRoutedPolicyPlan : Type 0 constructor TelemetryRoutedPolicyReady field unrestricted telemetryRoutedPolicyDeclaration : (family CapturePolicy) field unrestricted telemetryRoutedPolicySites : (family TelemetryPolicySites) field unrestricted telemetryRoutedPolicyDrain : (family TelemetryDispatchPlan) constructor TelemetryRoutedPolicyRefused field unrestricted telemetryRoutedPolicyReason : Bytes end-family def telemetryPolicyMember = (lambda unrestricted name : Bytes . (lambda unrestricted value : (family JSON) . (lambda unrestricted tail : (family JSON) . (constructor JSON JSONObjectMember name value tail)))) def telemetryPolicyText = (lambda unrestricted value : Bytes . (constructor JSON JSONString value)) def telemetryPolicyNatural = (lambda unrestricted value : Nat . (telemetryPolicyText (naturalDecimalBytesWithin 20 value))) def telemetryPolicyDescriptor = (lambda unrestricted policy : (family CapturePolicy) . (telemetryRecordJSON (aosDescriptorRecord b"policy" (bytes-append b"policy:" (capturePolicyIdentifier policy)) (constructor JSON JSONObject (telemetryPolicyMember b"format" (telemetryPolicyText b"AOS-CAPTURE-POLICY/1") (telemetryPolicyMember b"policy_id" (telemetryPolicyText (capturePolicyIdentifier policy)) (telemetryPolicyMember b"profile" (telemetryPolicyText (captureProfileName (capturePolicyProfile policy))) (telemetryPolicyMember b"content_opt_in" (constructor JSON JSONBoolean (capturePolicyContentEnabled policy)) (telemetryPolicyMember b"ordinary_event_budget" (telemetryPolicyNatural (capturePolicyOrdinaryCapacity policy)) (telemetryPolicyMember b"reserved_event_budget" (telemetryPolicyNatural (capturePolicyReservedCapacity policy)) (telemetryPolicyMember b"encoded_batch_byte_budget" (telemetryPolicyNatural (capturePolicyByteBudget policy)) (telemetryPolicyMember b"dimension_limit" (telemetryPolicyNatural (capturePolicyDimensionLimit policy)) (telemetryPolicyMember b"flush_after_opportunities" (telemetryPolicyNatural (capturePolicyFlushOpportunities policy)) (telemetryPolicyMember b"required" (constructor JSON JSONBoolean (capturePolicyRequired policy)) (telemetryPolicyMember b"budget_scope" (telemetryPolicyText b"per drain batch; not total process memory or lifetime event count") (telemetryPolicyMember b"flush_scope" (telemetryPolicyText b"selected plus excluded opportunities at declared safe boundaries; no wall-clock bound") (telemetryPolicyMember b"pending_behavior" (telemetryPolicyText b"return pending at a safe boundary; the run policy must drain/retry or report pause/failure") (constructor JSON JSONObjectEnd)))))))))))))))))) def telemetryPolicySiteDescriptor = (lambda unrestricted site : (family CaptureSite) . (telemetryRecordJSON (aosDescriptorRecord b"context" (bytes-append b"context:" (captureSiteIdentifier site)) (constructor JSON JSONObject (telemetryPolicyMember b"format" (telemetryPolicyText b"AOS-CAPTURE-SITE/1") (telemetryPolicyMember b"context_id" (telemetryPolicyText (captureSiteIdentifier site)) (telemetryPolicyMember b"name" (telemetryPolicyText (captureSiteName site)) (telemetryPolicyMember b"scope" (telemetryPolicyText b"static-capture-site; not an acquired runtime span") (telemetryPolicyMember b"capture_class" (telemetryPolicyText (captureClassName (captureSiteClass site))) (telemetryPolicyMember b"reserved" (constructor JSON JSONBoolean (captureSiteReserved site)) (telemetryPolicyMember b"declared_dimension_count" (telemetryPolicyNatural (captureSiteDimensions site)) (telemetryPolicyMember b"sampling_stride" (telemetryPolicyNatural (captureSiteStride site)) (telemetryPolicyMember b"sampling_coordinate" (telemetryPolicyText b"caller-supplied u64; select coordinate modulo stride equal to zero") (constructor JSON JSONObjectEnd)))))))))))))) def telemetryPolicyRecordAdmission = (lambda unrestricted policy : (family CapturePolicy) . (lambda unrestricted declaration : (family TelemetryRecordDeclaration) . (eliminate TelemetryRecordDeclaration (lambda unrestricted current : (family TelemetryRecordDeclaration) . Nat) declaration (branch TelemetryRecordDeclarationValue schema recordClass identity origin method payload . (bytes-equal identity (capturePolicyIdentifier policy)))))) def telemetryPolicyBindingDescriptorWith = (lambda unrestricted policy : (family CapturePolicy) . (lambda unrestricted site : (family CaptureSite) . (lambda unrestricted version : Bytes . (lambda unrestricted fields : (family JSON) . (telemetryRecordJSON (aosDescriptorRecord b"capture-binding" (bytes-append b"capture-binding:" (bytes-append (capturePolicyIdentifier policy) (bytes-append b":" (captureSiteIdentifier site)))) (constructor JSON JSONObject (telemetryPolicyMember b"format" (telemetryPolicyText version) (telemetryPolicyMember b"policy_id" (telemetryPolicyText (capturePolicyIdentifier policy)) (telemetryPolicyMember b"context_id" (telemetryPolicyText (captureSiteIdentifier site)) (telemetryPolicyMember b"selected_by_profile" (constructor JSON JSONBoolean (captureSiteSelected policy site)) (telemetryPolicyMember b"selection_reason" (telemetryPolicyText (aosChoose Bytes (captureSiteSelected policy site) b"profile-selected; cadence may exclude individual opportunities" b"capture-profile-excluded")) (telemetryPolicyMember b"effective_event_capacity" (telemetryPolicyNatural (aosChoose Nat (captureSiteReserved site) (capturePolicyReservedCapacity policy) (aosChoose Nat (captureSiteSelected policy site) (capturePolicyOrdinaryCapacity policy) 0))) fields))))))))))))) def telemetryPolicyBindingDescriptor = (lambda unrestricted policy : (family CapturePolicy) . (lambda unrestricted site : (family CaptureSite) . (telemetryPolicyBindingDescriptorWith policy site b"AOS-CAPTURE-BINDING/1" (constructor JSON JSONObjectEnd)))) def telemetryPolicyRoutedBindingDescriptor = (lambda unrestricted policy : (family CapturePolicy) . (lambda unrestricted tag : Nat . (lambda unrestricted site : (family CaptureSite) . (lambda unrestricted declaration : (family TelemetryRecordDeclaration) . (eliminate TelemetryRecordDeclaration (lambda unrestricted current : (family TelemetryRecordDeclaration) . Bytes) declaration (branch TelemetryRecordDeclarationValue schema recordClass policyIdentity origin method payload . (telemetryPolicyBindingDescriptorWith policy site b"AOS-CAPTURE-BINDING/2" (telemetryPolicyMember b"route_tag" (telemetryPolicyNatural tag) (telemetryPolicyMember b"schema_id" (telemetryPolicyText schema) (telemetryPolicyMember b"record_class" (telemetryPolicyText recordClass) (telemetryPolicyMember b"capacity_scope" (telemetryPolicyText b"shared queue for this role; not a separate allocation per site") (constructor JSON JSONObjectEnd)))))))))))) def telemetryPolicyDescriptors = (lambda unrestricted policy : (family CapturePolicy) . (lambda unrestricted ordinary : (family CaptureSite) . (lambda unrestricted reserved : (family CaptureSite) . (lambda unrestricted schemas : (family StdList Bytes) . (constructor StdList StdListCons Bytes (telemetryPolicyDescriptor policy) (constructor StdList StdListCons Bytes (telemetryPolicySiteDescriptor ordinary) (constructor StdList StdListCons Bytes (telemetryPolicySiteDescriptor reserved) (constructor StdList StdListCons Bytes (telemetryPolicyBindingDescriptor policy ordinary) (constructor StdList StdListCons Bytes (telemetryPolicyBindingDescriptor policy reserved) schemas))))))))) def telemetryPolicyPlan = (lambda unrestricted policy : (family CapturePolicy) . (lambda unrestricted ordinarySite : (family CaptureSite) . (lambda unrestricted reservedSite : (family CaptureSite) . (lambda unrestricted ordinary : (family TelemetryRecordDeclaration) . (lambda unrestricted reserved : (family TelemetryRecordDeclaration) . (lambda unrestricted schemas : (family StdList Bytes) . (aosChoose (family TelemetryPolicyPlan) (naturalAnd (capturePolicyAdmission policy) (naturalAnd (captureSiteAdmission policy ordinarySite) (naturalAnd (captureSiteAdmission policy reservedSite) (naturalAnd (naturalEqual (captureSiteReserved ordinarySite) 0) (naturalAnd (naturalEqual (captureSiteReserved reservedSite) 1) (naturalAnd (naturalIsZero (bytes-equal (captureSiteIdentifier ordinarySite) (captureSiteIdentifier reservedSite))) (naturalAnd (telemetryPolicyRecordAdmission policy ordinary) (telemetryPolicyRecordAdmission policy reserved)))))))) (let unrestricted drain = (telemetryDrainPlanAtContexts (captureSiteIdentifier ordinarySite) (captureSiteIdentifier reservedSite) (aosChoose Nat (captureSiteSelected policy ordinarySite) (capturePolicyOrdinaryCapacity policy) 0) (capturePolicyReservedCapacity policy) ordinary reserved (telemetryPolicyDescriptors policy ordinarySite reservedSite schemas)) in (eliminate TelemetryDrainPlan (lambda unrestricted current : (family TelemetryDrainPlan) . (family TelemetryPolicyPlan)) drain (branch TelemetryDrainReady ordinaryCapacity reservedCapacity ordinaryRecord reservedRecord descriptors bound . (aosChoose (family TelemetryPolicyPlan) (naturalLessOrEqual (publicationRecordBytes bound) (capturePolicyByteBudget policy)) (constructor TelemetryPolicyPlan TelemetryPolicyReady policy ordinarySite reservedSite drain) (constructor TelemetryPolicyPlan TelemetryPolicyRefused b"native-capture-policy-byte-budget-refused"))) (branch TelemetryDrainRefused reason . (constructor TelemetryPolicyPlan TelemetryPolicyRefused reason)))) (constructor TelemetryPolicyPlan TelemetryPolicyRefused b"native-capture-policy-declaration-refused")))))))) -- The selector's decision and saved caller iteration follow the derived drain arena. -- It is not application state and cannot overlap capture/identity storage. def telemetryPolicyDecisionAt = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (lambda unrestricted ordinary : (family TelemetryRecordPlan) . (lambda unrestricted reserved : (family TelemetryRecordPlan) . (lambda unrestricted bound : Nat . (captureAlign (telemetryDrainArenaBytes applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound)))))))) def telemetryPolicyArenaBytes = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (lambda unrestricted ordinary : (family TelemetryRecordPlan) . (lambda unrestricted reserved : (family TelemetryRecordPlan) . (lambda unrestricted bound : Nat . (naturalAdd (telemetryPolicyDecisionAt applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound) (naturalMultiply 2 captureWordBytes)))))))) def telemetryPolicyArenaCertificate = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (lambda unrestricted ordinary : (family TelemetryRecordPlan) . (lambda unrestricted reserved : (family TelemetryRecordPlan) . (lambda unrestricted bound : Nat . (naturalAnd (telemetryDrainArenaCertificate applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound) (naturalAnd (naturalLessOrEqual (telemetryPolicyArenaBytes applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound) captureExtentMaximum) (arenaCertificate (telemetryPolicyArenaBytes applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound) (constructor ArenaResidents ArenaResidentsNext (constructor ArenaResident ArenaResidentValue b"capture-policy-decision" (telemetryPolicyDecisionAt applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound) (naturalMultiply 2 captureWordBytes) captureWordBytes) (telemetryDrainResidents applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound))))))))))) def telemetryPolicySiteLookup = (lambda unrestricted wanted : Nat . (lambda unrestricted sites : (family TelemetryPolicySites) . (eliminate TelemetryPolicySites (lambda unrestricted current : (family TelemetryPolicySites) . (family TelemetryPolicySites)) sites (branch TelemetryPolicySitesEnd . (constructor TelemetryPolicySites TelemetryPolicySitesEnd)) (branch TelemetryPolicySitesNext tag site declaration following induction . (aosChoose (family TelemetryPolicySites) (naturalEqual wanted tag) (constructor TelemetryPolicySites TelemetryPolicySitesNext tag site declaration (constructor TelemetryPolicySites TelemetryPolicySitesEnd)) induction))))) def telemetryPolicyAllRoutes = (lambda unrestricted sites : (family TelemetryPolicySites) . (eliminate TelemetryPolicySites (lambda unrestricted current : (family TelemetryPolicySites) . (family TelemetryRouteDeclarations)) sites (branch TelemetryPolicySitesEnd . (constructor TelemetryRouteDeclarations TelemetryRouteDeclarationsEnd)) (branch TelemetryPolicySitesNext tag site declaration following induction . (constructor TelemetryRouteDeclarations TelemetryRouteDeclarationsNext tag (captureSiteIdentifier site) declaration induction)))) def telemetryPolicySelectedRoutes = (lambda unrestricted policy : (family CapturePolicy) . (lambda unrestricted role : Nat . (lambda unrestricted sites : (family TelemetryPolicySites) . (eliminate TelemetryPolicySites (lambda unrestricted current : (family TelemetryPolicySites) . (family TelemetryRouteDeclarations)) sites (branch TelemetryPolicySitesEnd . (constructor TelemetryRouteDeclarations TelemetryRouteDeclarationsEnd)) (branch TelemetryPolicySitesNext tag site declaration following induction . (aosChoose (family TelemetryRouteDeclarations) (naturalAnd (captureSiteSelected policy site) (naturalEqual role (captureSiteReserved site))) (constructor TelemetryRouteDeclarations TelemetryRouteDeclarationsNext tag (captureSiteIdentifier site) declaration induction) induction)))))) def telemetryPolicySitesAdmission = (lambda unrestricted policy : (family CapturePolicy) . (lambda unrestricted sites : (family TelemetryPolicySites) . (eliminate TelemetryPolicySites (lambda unrestricted current : (family TelemetryPolicySites) . Nat) sites (branch TelemetryPolicySitesEnd . 1) (branch TelemetryPolicySitesNext tag site declaration following induction . (naturalAnd induction (naturalAnd (captureSiteAdmission policy site) (telemetryPolicyRecordAdmission policy declaration))))))) def telemetryPolicySiteDescriptors = (lambda unrestricted policy : (family CapturePolicy) . (lambda unrestricted sites : (family TelemetryPolicySites) . (lambda unrestricted schemas : (family StdList Bytes) . (app (eliminate TelemetryPolicySites (lambda unrestricted current : (family TelemetryPolicySites) . (pi unrestricted tail : (family StdList Bytes) . (family StdList Bytes))) sites (branch TelemetryPolicySitesEnd . (lambda unrestricted tail : (family StdList Bytes) . tail)) (branch TelemetryPolicySitesNext tag site declaration following induction . (lambda unrestricted tail : (family StdList Bytes) . (constructor StdList StdListCons Bytes (telemetryPolicySiteDescriptor site) (constructor StdList StdListCons Bytes (telemetryPolicyRoutedBindingDescriptor policy tag site declaration) (induction tail)))))) schemas)))) def telemetryPolicyRoutedDescriptors = (lambda unrestricted policy : (family CapturePolicy) . (lambda unrestricted sites : (family TelemetryPolicySites) . (lambda unrestricted schemas : (family StdList Bytes) . (constructor StdList StdListCons Bytes (telemetryPolicyDescriptor policy) (telemetryPolicySiteDescriptors policy sites schemas))))) def telemetryRoutedPolicyPlan = (lambda unrestricted policy : (family CapturePolicy) . (lambda unrestricted sites : (family TelemetryPolicySites) . (lambda unrestricted schemas : (family StdList Bytes) . (let unrestricted ordinaryDeclarations = (telemetryPolicySelectedRoutes policy 0 sites) in (let unrestricted reservedDeclarations = (telemetryPolicySelectedRoutes policy 1 sites) in (let unrestricted descriptors = (telemetryPolicyRoutedDescriptors policy sites schemas) in (let unrestricted ordinaryCapacity = (aosChoose Nat (naturalNonzero (telemetryRouteDeclarationsCount ordinaryDeclarations)) (capturePolicyOrdinaryCapacity policy) 0) in (let unrestricted drain = (telemetryDispatchPlan ordinaryCapacity (capturePolicyReservedCapacity policy) ordinaryDeclarations reservedDeclarations descriptors) in (aosChoose (family TelemetryRoutedPolicyPlan) (naturalAnd (capturePolicyAdmission policy) (naturalAnd (telemetryPolicySitesAdmission policy sites) (naturalAnd (telemetryDrainDescriptorsAdmission descriptors) (telemetryRouteDeclarationsAdmission (telemetryPolicyAllRoutes sites) (constructor TelemetryRouteDeclarations TelemetryRouteDeclarationsEnd) descriptors)))) (eliminate TelemetryDispatchPlan (lambda unrestricted current : (family TelemetryDispatchPlan) . (family TelemetryRoutedPolicyPlan)) drain (branch TelemetryDispatchReady oc rc ordinaryRoutes reservedRoutes ordinary reserved descriptors bound . (aosChoose (family TelemetryRoutedPolicyPlan) (naturalLessOrEqual (publicationRecordBytes bound) (capturePolicyByteBudget policy)) (constructor TelemetryRoutedPolicyPlan TelemetryRoutedPolicyReady policy sites drain) (constructor TelemetryRoutedPolicyPlan TelemetryRoutedPolicyRefused b"native-routed-policy-byte-budget-refused"))) (branch TelemetryDispatchRefused reason . (constructor TelemetryRoutedPolicyPlan TelemetryRoutedPolicyRefused reason))) (constructor TelemetryRoutedPolicyPlan TelemetryRoutedPolicyRefused b"native-routed-policy-declaration-refused")))))))))) def telemetryRoutedPolicyDecisionAt = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (lambda unrestricted ordinary : (family TelemetryRecordPlan) . (lambda unrestricted reserved : (family TelemetryRecordPlan) . (lambda unrestricted bound : Nat . (captureAlign (telemetryDispatchArenaBytes applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound)))))))) def telemetryRoutedPolicyArenaBytes = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (lambda unrestricted ordinary : (family TelemetryRecordPlan) . (lambda unrestricted reserved : (family TelemetryRecordPlan) . (lambda unrestricted bound : Nat . (naturalAdd (telemetryRoutedPolicyDecisionAt applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound) (naturalMultiply 2 captureWordBytes)))))))) def telemetryRoutedPolicyArenaCertificate = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (lambda unrestricted ordinary : (family TelemetryRecordPlan) . (lambda unrestricted reserved : (family TelemetryRecordPlan) . (lambda unrestricted bound : Nat . (naturalAnd (telemetryDispatchArenaCertificate applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound) (naturalAnd (naturalLessOrEqual (telemetryRoutedPolicyArenaBytes applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound) captureExtentMaximum) (arenaCertificate (telemetryRoutedPolicyArenaBytes applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound) (constructor ArenaResidents ArenaResidentsNext (constructor ArenaResident ArenaResidentValue b"routed-policy-decision" (telemetryRoutedPolicyDecisionAt applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound) (naturalMultiply 2 captureWordBytes) captureWordBytes) (telemetryDispatchResidents applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound)))))))))))