module Observe.CapturePolicy import Data.Bytes import Observe.Value import Std.Natural -- Profiles select source-declared quantities; they do not infer meaning from -- names or values. Content capture needs a separate opt-in even in diagnostics. family CaptureProfile : Type 0 constructor CaptureLifecycleProfile constructor CaptureProgressProfile constructor CapturePerformanceProfile constructor CaptureDiagnosticProfile end-family family CaptureClass : Type 0 constructor CaptureLifecycleClass constructor CaptureHealthClass constructor CaptureProgressClass constructor CapturePerformanceClass constructor CaptureDiagnosticClass constructor CaptureContentClass end-family -- Budgets apply to an encoded drain batch, not to the lifetime of a run or -- total process memory. Flush bounds count selected plus excluded opportunities -- between declared safe boundaries; they are not acquired wall-clock bounds. family CapturePolicy : Type 0 constructor CapturePolicyValue field unrestricted capturePolicyVersionField : Nat field unrestricted capturePolicyIdentityField : Bytes field unrestricted capturePolicyProfileField : (family CaptureProfile) field unrestricted capturePolicyContentField : Nat field unrestricted capturePolicyOrdinaryField : Nat field unrestricted capturePolicyReservedField : Nat field unrestricted capturePolicyBytesField : Nat field unrestricted capturePolicyDimensionsField : Nat field unrestricted capturePolicyFlushField : Nat field unrestricted capturePolicyRequiredField : Nat end-family family CaptureSite : Type 0 constructor CaptureSiteValue field unrestricted captureSiteIdentityField : Bytes field unrestricted captureSiteNameField : Bytes field unrestricted captureSiteKindField : (family CaptureClass) field unrestricted captureSiteReservedField : Nat field unrestricted captureSiteDimensionsField : Nat field unrestricted captureSiteStrideField : Nat end-family def captureProfileLevel = (lambda unrestricted profile : (family CaptureProfile) . (eliminate CaptureProfile (lambda unrestricted current : (family CaptureProfile) . Nat) profile (branch CaptureLifecycleProfile . 0) (branch CaptureProgressProfile . 1) (branch CapturePerformanceProfile . 2) (branch CaptureDiagnosticProfile . 3))) def captureProfileName = (lambda unrestricted profile : (family CaptureProfile) . (eliminate CaptureProfile (lambda unrestricted current : (family CaptureProfile) . Bytes) profile (branch CaptureLifecycleProfile . b"lifecycle") (branch CaptureProgressProfile . b"progress") (branch CapturePerformanceProfile . b"performance") (branch CaptureDiagnosticProfile . b"diagnostic"))) def captureClassLevel = (lambda unrestricted kind : (family CaptureClass) . (eliminate CaptureClass (lambda unrestricted current : (family CaptureClass) . Nat) kind (branch CaptureLifecycleClass . 0) (branch CaptureHealthClass . 0) (branch CaptureProgressClass . 1) (branch CapturePerformanceClass . 2) (branch CaptureDiagnosticClass . 3) (branch CaptureContentClass . 4))) def captureClassName = (lambda unrestricted kind : (family CaptureClass) . (eliminate CaptureClass (lambda unrestricted current : (family CaptureClass) . Bytes) kind (branch CaptureLifecycleClass . b"lifecycle") (branch CaptureHealthClass . b"health") (branch CaptureProgressClass . b"progress") (branch CapturePerformanceClass . b"performance") (branch CaptureDiagnosticClass . b"diagnostic") (branch CaptureContentClass . b"content"))) def capturePolicyIdentifier = (lambda unrestricted value : (family CapturePolicy) . (eliminate CapturePolicy (lambda unrestricted current : (family CapturePolicy) . Bytes) value (branch CapturePolicyValue version identity profile content ordinary reserved bytes dimensions flush required . identity))) def capturePolicyProfile = (lambda unrestricted value : (family CapturePolicy) . (eliminate CapturePolicy (lambda unrestricted current : (family CapturePolicy) . (family CaptureProfile)) value (branch CapturePolicyValue version identity profile content ordinary reserved bytes dimensions flush required . profile))) def capturePolicyContentEnabled = (lambda unrestricted value : (family CapturePolicy) . (eliminate CapturePolicy (lambda unrestricted current : (family CapturePolicy) . Nat) value (branch CapturePolicyValue version identity profile content ordinary reserved bytes dimensions flush required . content))) def capturePolicyOrdinaryCapacity = (lambda unrestricted value : (family CapturePolicy) . (eliminate CapturePolicy (lambda unrestricted current : (family CapturePolicy) . Nat) value (branch CapturePolicyValue version identity profile content ordinary reserved bytes dimensions flush required . ordinary))) def capturePolicyReservedCapacity = (lambda unrestricted value : (family CapturePolicy) . (eliminate CapturePolicy (lambda unrestricted current : (family CapturePolicy) . Nat) value (branch CapturePolicyValue version identity profile content ordinary reserved bytes dimensions flush required . reserved))) def capturePolicyByteBudget = (lambda unrestricted value : (family CapturePolicy) . (eliminate CapturePolicy (lambda unrestricted current : (family CapturePolicy) . Nat) value (branch CapturePolicyValue version identity profile content ordinary reserved bytes dimensions flush required . bytes))) def capturePolicyDimensionLimit = (lambda unrestricted value : (family CapturePolicy) . (eliminate CapturePolicy (lambda unrestricted current : (family CapturePolicy) . Nat) value (branch CapturePolicyValue version identity profile content ordinary reserved bytes dimensions flush required . dimensions))) def capturePolicyFlushOpportunities = (lambda unrestricted value : (family CapturePolicy) . (eliminate CapturePolicy (lambda unrestricted current : (family CapturePolicy) . Nat) value (branch CapturePolicyValue version identity profile content ordinary reserved bytes dimensions flush required . flush))) def capturePolicyRequired = (lambda unrestricted value : (family CapturePolicy) . (eliminate CapturePolicy (lambda unrestricted current : (family CapturePolicy) . Nat) value (branch CapturePolicyValue version identity profile content ordinary reserved bytes dimensions flush required . required))) def captureSiteIdentifier = (lambda unrestricted value : (family CaptureSite) . (eliminate CaptureSite (lambda unrestricted current : (family CaptureSite) . Bytes) value (branch CaptureSiteValue identity name kind reserved dimensions stride . identity))) def captureSiteName = (lambda unrestricted value : (family CaptureSite) . (eliminate CaptureSite (lambda unrestricted current : (family CaptureSite) . Bytes) value (branch CaptureSiteValue identity name kind reserved dimensions stride . name))) def captureSiteClass = (lambda unrestricted value : (family CaptureSite) . (eliminate CaptureSite (lambda unrestricted current : (family CaptureSite) . (family CaptureClass)) value (branch CaptureSiteValue identity name kind reserved dimensions stride . kind))) def captureSiteReserved = (lambda unrestricted value : (family CaptureSite) . (eliminate CaptureSite (lambda unrestricted current : (family CaptureSite) . Nat) value (branch CaptureSiteValue identity name kind reserved dimensions stride . reserved))) def captureSiteDimensions = (lambda unrestricted value : (family CaptureSite) . (eliminate CaptureSite (lambda unrestricted current : (family CaptureSite) . Nat) value (branch CaptureSiteValue identity name kind reserved dimensions stride . dimensions))) def captureSiteStride = (lambda unrestricted value : (family CaptureSite) . (eliminate CaptureSite (lambda unrestricted current : (family CaptureSite) . Nat) value (branch CaptureSiteValue identity name kind reserved dimensions stride . stride))) def capturePolicyAdmission = (lambda unrestricted policy : (family CapturePolicy) . (eliminate CapturePolicy (lambda unrestricted current : (family CapturePolicy) . Nat) policy (branch CapturePolicyValue version identity profile content ordinary reserved bytes dimensions flush required . (naturalAnd (naturalEqual version 1) (naturalAnd (aosIsIdentity identity) (naturalAnd (naturalLessOrEqual content 1) (naturalAnd (naturalLessOrEqual required 1) (naturalAnd (naturalLessOrEqual 2 reserved) (naturalAnd (naturalLessOrEqual (naturalAdd ordinary reserved) 1024) (naturalAnd (naturalNonzero bytes) (naturalAnd (naturalLessOrEqual bytes 18446744073709551615) (naturalAnd (naturalLessOrEqual dimensions 18446744073709551615) (naturalAnd (naturalNonzero flush) (naturalAnd (naturalLessOrEqual flush 18446744073709551615) (aosChoose Nat content (naturalEqual (captureProfileLevel profile) 3) 1))))))))))))))) def captureSiteAdmission = (lambda unrestricted policy : (family CapturePolicy) . (lambda unrestricted site : (family CaptureSite) . (eliminate CaptureSite (lambda unrestricted current : (family CaptureSite) . Nat) site (branch CaptureSiteValue identity name kind reserved dimensions stride . (naturalAnd (capturePolicyAdmission policy) (naturalAnd (aosIsIdentity identity) (naturalAnd (naturalNonzero (bytes-length name)) (naturalAnd (naturalLessOrEqual (bytes-length name) 256) (naturalAnd (naturalLessOrEqual reserved 1) (naturalAnd (naturalLessOrEqual dimensions (capturePolicyDimensionLimit policy)) (naturalAnd (naturalNonzero stride) (naturalAnd (naturalLessOrEqual stride 18446744073709551615) (naturalAnd (aosChoose Nat (bytes-equal (captureClassName kind) b"health") reserved 1) (aosChoose Nat reserved (naturalAnd (naturalEqual (captureClassLevel kind) 0) (naturalEqual stride 1)) 1)))))))))))))) def captureSiteSelected = (lambda unrestricted policy : (family CapturePolicy) . (lambda unrestricted site : (family CaptureSite) . (naturalAnd (captureSiteAdmission policy site) (aosChoose Nat (naturalEqual (captureClassLevel (captureSiteClass site)) 4) (capturePolicyContentEnabled policy) (naturalLessOrEqual (captureClassLevel (captureSiteClass site)) (captureProfileLevel (capturePolicyProfile policy))))))) -- A pending capture is not complete and cannot justify workload continuation. -- The runtime returns it at a safe boundary; the owning run policy must drain -- and retry or report its declared pause/failure, never turn it into success. def captureCanContinue = (lambda unrestricted required : Nat . (lambda unrestricted decision : Nat . (naturalAnd (naturalLessOrEqual required 1) (naturalOr (naturalLessOrEqual decision 1) (naturalAnd (naturalEqual required 0) (naturalEqual decision 2))))))