module Runtime.NativeObservedProgram import Data.Bytes import Model.Parameter import Model.Word64 import Observe.CapturePolicy import Observe.Value import Runtime.NativeObservedJournal import Runtime.NativeLaunchRecipeLoad import Runtime.NativePhysicalProgram import Runtime.NativeTelemetryPolicy import Runtime.NativeTelemetryIdentity import Runtime.TelemetryCapture import Runtime.TelemetryDrain import Runtime.TelemetryPolicy import Runtime.TelemetryRecord import Std.Natural -- A native source program with declared observation effects, lowered before -- NativePhysicalProgram serialization/target emission. Capture nodes are safe -- boundaries explicitly placed by the owning run policy, not discovered from -- payload words or injected into arbitrary instructions. Their continuation -- cannot run between pending capture, drain and retry of frozen source values. family NativeObservedSteps : Type 0 constructor NativeObservedStepsEnd constructor NativeObservedOperation field unrestricted nativeObservedOperation : (family NativePhysicalOperation) recursive unrestricted nativeObservedOperationTail -- Lift maintained host fragments without discarding their failure identities. -- The same source-scope and repeat-flow checks apply to their operations. constructor NativeObservedCommand field unrestricted nativeObservedDeclaredCommand : (family NativePhysicalCommand) recursive unrestricted nativeObservedCommandTail -- Recorder-owned resource setup is an effect, not application access to the -- private epoch bytes. Its public storage and descriptor slots stay scoped. constructor NativeObservedOpenJournal field unrestricted nativeObservedJournalPathAt : Nat field unrestricted nativeObservedJournalFileSlot : Nat field unrestricted nativeObservedJournalDirectorySlot : Nat recursive unrestricted nativeObservedJournalTail constructor NativeObservedCaptureBoundary field unrestricted nativeObservedCaptureTag : Nat field unrestricted nativeObservedCaptureValues : (family NativeTelemetrySourceValues) field unrestricted nativeObservedCaptureCoordinate : (family NativePhysicalOperand) recursive unrestricted nativeObservedCaptureTail -- Publish before application cleanup closes its sink. End also closes when -- there is no explicit finish. Finish is forbidden inside a repeat. constructor NativeObservedFinish recursive unrestricted nativeObservedFinishTail end-family family NativeObservedProgramResult : Type 0 constructor NativeObservedProgramReady field unrestricted nativeObservedProgram : (family NativePhysicalProgram) constructor NativeObservedProgramRefused field unrestricted nativeObservedProgramReason : Bytes end-family -- Current capture routines address their certified arena with signed 32-bit -- displacements. This is a realization limit, not a model/learning constraint. -- Bounded candidates make even refused u64 inputs safe to inspect. Admission -- requires the original declarations to equal those candidates; no accepted -- program silently receives a smaller application arena or fewer result slots. def nativeObservedAddressMaximum = (naturalSaturatingSubtract (naturalPowerOfTwo 31) 1) def nativeObservedCandidateBytes = (lambda unrestricted requested : Nat . (aosChoose Nat (naturalLessOrEqual requested nativeObservedAddressMaximum) requested 0)) def nativeObservedCaptureSlot = (lambda unrestricted applicationSlots : Nat . applicationSlots) def nativeObservedPublicationSlot = (lambda unrestricted applicationSlots : Nat . (succ (nativeObservedCaptureSlot applicationSlots))) def nativeObservedWorkSlot = (lambda unrestricted applicationSlots : Nat . (succ (nativeObservedPublicationSlot applicationSlots))) def nativeObservedRetrySlot = (lambda unrestricted applicationSlots : Nat . (succ (nativeObservedWorkSlot applicationSlots))) def nativeObservedPrivateSlotCount : Nat = (succ (nativeObservedRetrySlot 0)) def nativeObservedCandidateSlots = (lambda unrestricted requested : Nat . (aosChoose Nat (naturalLessOrEqual requested (naturalSaturatingSubtract (naturalDivideUnchecked nativeObservedAddressMaximum nativePhysicalWordBytes) nativeObservedPrivateSlotCount)) requested 0)) def nativeObservedOperationAllowed = (lambda unrestricted operation : (family NativePhysicalOperation) . (eliminate NativePhysicalOperation (lambda unrestricted current : (family NativePhysicalOperation) . Nat) operation (branch NativePhysicalSystemCall number arguments payload result . 1) (branch NativePhysicalCopyPayloadToState destination extent payload . 1) (branch NativePhysicalMachineRoutine code arguments result . 1) (branch NativePhysicalFencePoll address expected polls . 1) (branch NativePhysicalTelemetryAppend path record . 0) (branch NativePhysicalAssertEqual left right error . 1) (branch NativePhysicalAssertOneOf observed first second error . 1) (branch NativePhysicalHaltSuccess . 0) (branch NativePhysicalRepeatBegin count . 1) -- refused: a forward skip counts records, and observation inserts -- records around operations, so the skip would land elsewhere (branch NativePhysicalSkipUnlessEqual left right count . 0) (branch NativePhysicalRepeatEnd . 1) (branch NativePhysicalRepeatEndWhen observed expected . 1) (branch NativePhysicalStoreWord64 destination value . 1) (branch NativePhysicalFenceWait address expected polls interval . 1) (branch NativePhysicalRepeatBeginCounted count . 1) (branch NativePhysicalAddWord64 destination left right . 1) (branch NativePhysicalFloat64 numeric destination left right . 1))) def nativeObservedCaptureAdmission = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted applicationSlots : Nat . (lambda unrestricted plan : (family TelemetryRoutedPolicyPlan) . (lambda unrestricted wanted : Nat . (lambda unrestricted values : (family NativeTelemetrySourceValues) . (lambda unrestricted coordinate : (family NativePhysicalOperand) . (eliminate TelemetryRoutedPolicyPlan (lambda unrestricted current : (family TelemetryRoutedPolicyPlan) . Nat) plan (branch TelemetryRoutedPolicyReady policy sites drain . (eliminate TelemetryDispatchPlan (lambda unrestricted current : (family TelemetryDispatchPlan) . Nat) drain (branch TelemetryDispatchReady oc rc ordinaryRoutes reservedRoutes ordinary reserved descriptors bound . (eliminate TelemetryPolicySites (lambda unrestricted current : (family TelemetryPolicySites) . Nat) (telemetryPolicySiteLookup wanted sites) (branch TelemetryPolicySitesEnd . 0) (branch TelemetryPolicySitesNext tag site declaration following induction . (aosChoose Nat (captureSiteSelected policy site) (naturalAnd (naturalAnd (nativeTelemetrySourcesAdmission (telemetryRecordRouteLookup tag (aosChoose (family TelemetryRecordRoutes) (captureSiteReserved site) reservedRoutes ordinaryRoutes)) values) (nativeTelemetrySourceScopesWith (telemetryRecordRouteLookup tag (aosChoose (family TelemetryRecordRoutes) (captureSiteReserved site) reservedRoutes ordinaryRoutes)) values (nativePhysicalOperandScopeAdmission applicationBytes applicationSlots 0))) (naturalOr (naturalEqual (captureSiteStride site) 1) (nativePhysicalOperandScopeAdmission applicationBytes applicationSlots 0 coordinate))) 1)))) (branch TelemetryDispatchRefused reason . 0))) (branch TelemetryRoutedPolicyRefused reason . 0)))))))) -- Operations from a declared fragment and individually declared operations -- share scope and repeat-flow admission; preserving an error identity must not -- introduce a second, more permissive path into recorder-private storage. def nativeObservedAdmitOperation = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted applicationSlots : Nat . (lambda unrestricted operation : (family NativePhysicalOperation) . (lambda unrestricted induction : (pi unrestricted depth : Nat . (pi unrestricted closed : Nat . Nat)) . (lambda unrestricted depth : Nat . (lambda unrestricted closed : Nat . (naturalAnd (nativeObservedOperationAllowed operation) (naturalAnd (nativePhysicalOperationScopeAdmission applicationBytes applicationSlots operation) (naturalAnd (naturalOr (naturalIsZero (naturalEqual (nativePhysicalRepeatAction operation) 2)) (naturalNonzero depth)) (induction (aosChoose Nat (naturalEqual (nativePhysicalRepeatAction operation) 1) (succ depth) (aosChoose Nat (naturalEqual (nativePhysicalRepeatAction operation) 2) (naturalSaturatingSubtract depth 1) depth)) closed)))))))))) -- Check source scopes before extending storage. Finish closes observation, -- not application success: cleanup may follow, but capture cannot. Closing -- inside a repeat would invalidate later iterations and is refused statically. def nativeObservedStepsAdmission = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted applicationSlots : Nat . (lambda unrestricted plan : (family TelemetryRoutedPolicyPlan) . (lambda unrestricted steps : (family NativeObservedSteps) . (app (eliminate NativeObservedSteps (lambda unrestricted current : (family NativeObservedSteps) . (pi unrestricted depth : Nat . (pi unrestricted closed : Nat . Nat))) steps (branch NativeObservedStepsEnd . (lambda unrestricted depth : Nat . (lambda unrestricted closed : Nat . (naturalIsZero depth)))) (branch NativeObservedOperation operation following induction . (nativeObservedAdmitOperation applicationBytes applicationSlots operation induction)) (branch NativeObservedCommand command following induction . (eliminate NativePhysicalCommand (lambda unrestricted current : (family NativePhysicalCommand) . (pi unrestricted depth : Nat . (pi unrestricted closed : Nat . Nat))) command (branch NativePhysicalCommandValue operation errorIdentity . (nativeObservedAdmitOperation applicationBytes applicationSlots operation induction)))) (branch NativeObservedOpenJournal pathAt fileSlot directorySlot following induction . (lambda unrestricted depth : Nat . (lambda unrestricted closed : Nat . (naturalAnd (naturalIsZero depth) (naturalAnd (naturalIsZero closed) (naturalAnd (nativeObservedJournalAdmission applicationBytes applicationSlots pathAt fileSlot directorySlot) (induction depth closed))))))) (branch NativeObservedCaptureBoundary tag values coordinate following induction . (lambda unrestricted depth : Nat . (lambda unrestricted closed : Nat . (naturalAnd (naturalIsZero closed) (naturalAnd (nativeObservedCaptureAdmission applicationBytes applicationSlots plan tag values coordinate) (induction depth closed)))))) (branch NativeObservedFinish following induction . (lambda unrestricted depth : Nat . (lambda unrestricted closed : Nat . (naturalAnd (naturalIsZero depth) (naturalAnd (naturalIsZero closed) (induction depth 1))))))) 0 0))))) -- Each effect lowers through the maintained policy owners. End supplies a -- terminal acknowledgement only when no explicit Finish has already done so. -- Inserted nested loops preserve the application's active loop coordinates. def nativeObservedLowerSteps = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted applicationSlots : Nat . (lambda unrestricted plan : (family TelemetryRoutedPolicyPlan) . (lambda unrestricted sink : (family NativePhysicalOperand) . (lambda unrestricted directory : (family NativePhysicalOperand) . (lambda unrestricted identity : Bytes . (lambda unrestricted steps : (family NativeObservedSteps) . (app (eliminate NativeObservedSteps (lambda unrestricted current : (family NativeObservedSteps) . (pi unrestricted closed : Nat . (family NativePhysicalCommands))) steps (branch NativeObservedStepsEnd . (lambda unrestricted closed : Nat . (aosChoose (family NativePhysicalCommands) closed (constructor NativePhysicalCommands NativePhysicalCommandsEnd) (nativeTelemetryRoutedPolicyBoundaryCommands applicationBytes plan 1 sink directory (nativeObservedCaptureSlot applicationSlots) (nativeObservedPublicationSlot applicationSlots) (nativeObservedWorkSlot applicationSlots) identity (nativeLaunchRecipeAssertEqual (nativeLaunchRecipeSlotValue (nativeObservedPublicationSlot applicationSlots)) (nativeLaunchRecipeImmediate 0) (nativeTelemetryFailureIdentity b"telemetry:terminal-publication-refused") (constructor NativePhysicalCommands NativePhysicalCommandsEnd)))))) (branch NativeObservedOperation operation following induction . (lambda unrestricted closed : Nat . (nativeLaunchRecipeCommand operation identity (induction closed)))) (branch NativeObservedCommand command following induction . (lambda unrestricted closed : Nat . (constructor NativePhysicalCommands NativePhysicalCommandsNext command (induction closed)))) (branch NativeObservedOpenJournal pathAt fileSlot directorySlot following induction . (lambda unrestricted closed : Nat . (nativeObservedJournalCommands applicationBytes plan pathAt fileSlot directorySlot (nativeObservedWorkSlot applicationSlots) identity (induction closed)))) (branch NativeObservedCaptureBoundary tag values coordinate following induction . (lambda unrestricted closed : Nat . (nativeTelemetryRoutedCaptureAndContinueCommands applicationBytes plan tag values coordinate sink directory (nativeObservedCaptureSlot applicationSlots) (nativeObservedPublicationSlot applicationSlots) (nativeObservedWorkSlot applicationSlots) (nativeObservedRetrySlot applicationSlots) identity (induction closed)))) (branch NativeObservedFinish following induction . (lambda unrestricted closed : Nat . (nativeTelemetryRoutedPolicyBoundaryCommands applicationBytes plan 1 sink directory (nativeObservedCaptureSlot applicationSlots) (nativeObservedPublicationSlot applicationSlots) (nativeObservedWorkSlot applicationSlots) identity (nativeLaunchRecipeAssertEqual (nativeLaunchRecipeSlotValue (nativeObservedPublicationSlot applicationSlots)) (nativeLaunchRecipeImmediate 0) (nativeTelemetryFailureIdentity b"telemetry:terminal-publication-refused") (induction 1)))))) 0)))))))) -- Compose a maintained physical fragment with declared effects. Fragments -- retain every command identity and loop marker; admission examines each -- operation in the original application scope before recorder storage exists. def nativeObservedPrefixCommands = (lambda unrestricted commands : (family NativePhysicalCommands) . (lambda unrestricted tail : (family NativeObservedSteps) . (eliminate NativePhysicalCommands (lambda unrestricted current : (family NativePhysicalCommands) . (family NativeObservedSteps)) commands (branch NativePhysicalCommandsEnd . tail) (branch NativePhysicalCommandsNext command rest induction . (constructor NativeObservedSteps NativeObservedCommand command induction))))) def nativeObservedPrefixWith = (lambda unrestricted fragment : (pi unrestricted after : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . (nativeObservedPrefixCommands (fragment (constructor NativePhysicalCommands NativePhysicalCommandsEnd)))) def nativeObservedBuildProgramWithIdentitySource = (lambda unrestricted source : (family NativeTelemetryIdentitySource) . (lambda unrestricted requestedBytes : Nat . (lambda unrestricted requestedSlots : Nat . (lambda unrestricted plan : (family TelemetryRoutedPolicyPlan) . (lambda unrestricted sink : (family NativePhysicalOperand) . (lambda unrestricted directory : (family NativePhysicalOperand) . (lambda unrestricted identity : Bytes . (lambda unrestricted steps : (family NativeObservedSteps) . (let unrestricted applicationBytes = (nativeObservedCandidateBytes requestedBytes) in (let unrestricted applicationSlots = (nativeObservedCandidateSlots requestedSlots) in (eliminate TelemetryRoutedPolicyPlan (lambda unrestricted current : (family TelemetryRoutedPolicyPlan) . (family NativeObservedProgramResult)) plan (branch TelemetryRoutedPolicyReady policy sites drain . (eliminate TelemetryDispatchPlan (lambda unrestricted current : (family TelemetryDispatchPlan) . (family NativeObservedProgramResult)) drain (branch TelemetryDispatchReady oc rc ordinaryRoutes reservedRoutes ordinary reserved descriptors bound . (let unrestricted arena = (telemetryRoutedPolicyArenaBytes applicationBytes oc rc ordinary reserved bound) in (aosChoose (family NativeObservedProgramResult) (naturalAnd (naturalEqual requestedBytes applicationBytes) (naturalAnd (naturalEqual requestedSlots applicationSlots) (naturalAnd (naturalLessOrEqual arena nativeObservedAddressMaximum) (telemetryRoutedPolicyArenaCertificate applicationBytes oc rc ordinary reserved bound)))) (aosChoose (family NativeObservedProgramResult) (naturalAnd (nativePhysicalOperandScopeAdmission applicationBytes applicationSlots 0 sink) (naturalAnd (nativePhysicalOperandScopeAdmission applicationBytes applicationSlots 0 directory) (naturalAnd (nativeTelemetryIdentitySourceAdmission applicationBytes applicationSlots source) (nativeObservedStepsAdmission applicationBytes applicationSlots plan steps)))) (let unrestricted commands = (nativeTelemetryRoutedPolicyInitializeWithIdentity (nativeTelemetryInitializeIdentityFrom source (nativeObservedWorkSlot applicationSlots)) applicationBytes plan (nativeObservedCaptureSlot applicationSlots) identity (nativeLaunchRecipeAssertEqual (nativeLaunchRecipeSlotValue (nativeObservedCaptureSlot applicationSlots)) (nativeLaunchRecipeImmediate 0) (nativeTelemetryFailureIdentity b"telemetry:initialization-refused") (nativeObservedLowerSteps applicationBytes applicationSlots plan sink directory identity steps))) in (let unrestricted program = (constructor NativePhysicalProgram NativePhysicalProgramValue (modelWord64FromNaturalTruncated arena) (modelWord64FromNaturalTruncated (succ (nativeObservedRetrySlot applicationSlots))) commands (eliminate NativePhysicalCounts (lambda unrestricted current : (family NativePhysicalCounts) . Nat) (nativePhysicalCommandsCounts commands) (branch NativePhysicalCountsValue count syscalls copies routines polls appends assertions halts payload . count)) identity 0) in (eliminate NativePhysicalProgramValidation (lambda unrestricted current : (family NativePhysicalProgramValidation) . (family NativeObservedProgramResult)) (nativePhysicalValidateProgram program) (branch NativePhysicalProgramValidated checkedProgram validationTelemetry . (constructor NativeObservedProgramResult NativeObservedProgramReady checkedProgram)) (branch NativePhysicalProgramRejected error telemetry . (constructor NativeObservedProgramResult NativeObservedProgramRefused (bytes-append b"observed-program-lowering-refused:" (nativePhysicalErrorCodeBytes error))))))) (constructor NativeObservedProgramResult NativeObservedProgramRefused b"observed-program-source-scope-or-flow-refused")) (constructor NativeObservedProgramResult NativeObservedProgramRefused b"observed-program-native-layout-unavailable")))) (branch TelemetryDispatchRefused reason . (constructor NativeObservedProgramResult NativeObservedProgramRefused (bytes-append b"observed-program-policy-refused:" reason))))) (branch TelemetryRoutedPolicyRefused reason . (constructor NativeObservedProgramResult NativeObservedProgramRefused (bytes-append b"observed-program-policy-refused:" reason)))))))))))))) def nativeObservedBuildProgram = (nativeObservedBuildProgramWithIdentitySource (constructor NativeTelemetryIdentitySource NativeTelemetryFreshIdentity)) -- A Refused value is inspectable through nativeObservedRefusalOf. Forcing it -- into target emission supplies rejected IR, never an empty successful artifact -- or a substitute program. The target's own validator remains authoritative. def nativeObservedRequireProgram = (lambda unrestricted result : (family NativeObservedProgramResult) . (eliminate NativeObservedProgramResult (lambda unrestricted current : (family NativeObservedProgramResult) . (family NativePhysicalProgram)) result (branch NativeObservedProgramReady program . program) (branch NativeObservedProgramRefused reason . (constructor NativePhysicalProgram NativePhysicalProgramValue 0 0 (constructor NativePhysicalCommands NativePhysicalCommandsEnd) 0 (nativeTelemetryFailureIdentity (bytes-append b"observed-program:declaration-refused:" reason)) 0)))) -- Inspect the named admission failure before requesting target emission. def nativeObservedRefusalOf = (lambda unrestricted result : (family NativeObservedProgramResult) . (eliminate NativeObservedProgramResult (lambda unrestricted current : (family NativeObservedProgramResult) . Bytes) result (branch NativeObservedProgramReady program . b"") (branch NativeObservedProgramRefused reason . reason)))