1module Runtime.NativeObservedProgram
2
3import Data.Bytes
4import Model.Parameter
5import Model.Word64
6import Observe.CapturePolicy
7import Observe.Value
8import Runtime.NativeObservedJournal
9import Runtime.NativeLaunchRecipeLoad
10import Runtime.NativePhysicalProgram
11import Runtime.NativeTelemetryPolicy
12import Runtime.NativeTelemetryIdentity
13import Runtime.TelemetryCapture
14import Runtime.TelemetryDrain
15import Runtime.TelemetryPolicy
16import Runtime.TelemetryRecord
17import Std.Natural
18
19-- A native source program with declared observation effects, lowered before
20-- NativePhysicalProgram serialization/target emission. Capture nodes are safe
21-- boundaries explicitly placed by the owning run policy, not discovered from
22-- payload words or injected into arbitrary instructions. Their continuation
23-- cannot run between pending capture, drain and retry of frozen source values.
24family NativeObservedSteps : Type 0
25constructor NativeObservedStepsEnd
26constructor NativeObservedOperation
27field unrestricted nativeObservedOperation : (family NativePhysicalOperation)
28recursive unrestricted nativeObservedOperationTail
29-- Lift maintained host fragments without discarding their failure identities.
30-- The same source-scope and repeat-flow checks apply to their operations.
31constructor NativeObservedCommand
32field unrestricted nativeObservedDeclaredCommand : (family NativePhysicalCommand)
33recursive unrestricted nativeObservedCommandTail
34-- Recorder-owned resource setup is an effect, not application access to the
35-- private epoch bytes. Its public storage and descriptor slots stay scoped.
36constructor NativeObservedOpenJournal
37field unrestricted nativeObservedJournalPathAt : Nat
38field unrestricted nativeObservedJournalFileSlot : Nat
39field unrestricted nativeObservedJournalDirectorySlot : Nat
40recursive unrestricted nativeObservedJournalTail
41constructor NativeObservedCaptureBoundary
42field unrestricted nativeObservedCaptureTag : Nat
43field unrestricted nativeObservedCaptureValues : (family NativeTelemetrySourceValues)
44field unrestricted nativeObservedCaptureCoordinate : (family NativePhysicalOperand)
45recursive unrestricted nativeObservedCaptureTail
46-- Publish before application cleanup closes its sink. End also closes when
47-- there is no explicit finish. Finish is forbidden inside a repeat.
48constructor NativeObservedFinish
49recursive unrestricted nativeObservedFinishTail
50
51end-family
52
53family NativeObservedProgramResult : Type 0
54constructor NativeObservedProgramReady
55field unrestricted nativeObservedProgram : (family NativePhysicalProgram)
56constructor NativeObservedProgramRefused
57field unrestricted nativeObservedProgramReason : Bytes
58
59end-family
60
61-- Current capture routines address their certified arena with signed 32-bit
62-- displacements. This is a realization limit, not a model/learning constraint.
63-- Bounded candidates make even refused u64 inputs safe to inspect. Admission
64-- requires the original declarations to equal those candidates; no accepted
65-- program silently receives a smaller application arena or fewer result slots.
66def nativeObservedAddressMaximum =
67 (naturalSaturatingSubtract (naturalPowerOfTwo 31) 1)
68
69def nativeObservedCandidateBytes =
70 (lambda unrestricted requested : Nat .
71 (aosChoose Nat (naturalLessOrEqual requested nativeObservedAddressMaximum) requested 0))
72
73def nativeObservedCaptureSlot =
74 (lambda unrestricted applicationSlots : Nat . applicationSlots)
75
76def nativeObservedPublicationSlot =
77 (lambda unrestricted applicationSlots : Nat . (succ (nativeObservedCaptureSlot applicationSlots)))
78
79def nativeObservedWorkSlot =
80 (lambda unrestricted applicationSlots : Nat .
81 (succ (nativeObservedPublicationSlot applicationSlots)))
82
83def nativeObservedRetrySlot =
84 (lambda unrestricted applicationSlots : Nat . (succ (nativeObservedWorkSlot applicationSlots)))
85
86def nativeObservedPrivateSlotCount : Nat =
87 (succ (nativeObservedRetrySlot 0))
88
89def nativeObservedCandidateSlots =
90 (lambda unrestricted requested : Nat .
91 (aosChoose
92 Nat
93 (naturalLessOrEqual
94 requested
95 (naturalSaturatingSubtract
96 (naturalDivideUnchecked nativeObservedAddressMaximum nativePhysicalWordBytes)
97 nativeObservedPrivateSlotCount))
98 requested
99 0))
100
101def nativeObservedOperationAllowed =
102 (lambda unrestricted operation : (family NativePhysicalOperation) .
103 (eliminate
104 NativePhysicalOperation
105 (lambda unrestricted current : (family NativePhysicalOperation) . Nat)
106 operation
107 (branch NativePhysicalSystemCall number arguments payload result . 1)
108 (branch NativePhysicalCopyPayloadToState destination extent payload . 1)
109 (branch NativePhysicalMachineRoutine code arguments result . 1)
110 (branch NativePhysicalFencePoll address expected polls . 1)
111 (branch NativePhysicalTelemetryAppend path record . 0)
112 (branch NativePhysicalAssertEqual left right error . 1)
113 (branch NativePhysicalAssertOneOf observed first second error . 1)
114 (branch NativePhysicalHaltSuccess . 0)
115 (branch NativePhysicalRepeatBegin count . 1)
116 -- refused: a forward skip counts records, and observation inserts
117 -- records around operations, so the skip would land elsewhere
118 (branch NativePhysicalSkipUnlessEqual left right count . 0)
119 (branch NativePhysicalRepeatEnd . 1)
120 (branch NativePhysicalRepeatEndWhen observed expected . 1)
121 (branch NativePhysicalStoreWord64 destination value . 1)
122 (branch NativePhysicalFenceWait address expected polls interval . 1)
123 (branch NativePhysicalRepeatBeginCounted count . 1)
124 (branch NativePhysicalAddWord64 destination left right . 1)
125 (branch NativePhysicalFloat64 numeric destination left right . 1)))
126
127def nativeObservedCaptureAdmission =
128 (lambda unrestricted applicationBytes : Nat .
129 (lambda unrestricted applicationSlots : Nat .
130 (lambda unrestricted plan : (family TelemetryRoutedPolicyPlan) .
131 (lambda unrestricted wanted : Nat .
132 (lambda unrestricted values : (family NativeTelemetrySourceValues) .
133 (lambda unrestricted coordinate : (family NativePhysicalOperand) .
134 (eliminate
135 TelemetryRoutedPolicyPlan
136 (lambda unrestricted current : (family TelemetryRoutedPolicyPlan) . Nat)
137 plan
138 (branch
139 TelemetryRoutedPolicyReady
140 policy
141 sites
142 drain
143 .
144 (eliminate
145 TelemetryDispatchPlan
146 (lambda unrestricted current : (family TelemetryDispatchPlan) . Nat)
147 drain
148 (branch
149 TelemetryDispatchReady
150 oc
151 rc
152 ordinaryRoutes
153 reservedRoutes
154 ordinary
155 reserved
156 descriptors
157 bound
158 .
159 (eliminate
160 TelemetryPolicySites
161 (lambda unrestricted current : (family TelemetryPolicySites) . Nat)
162 (telemetryPolicySiteLookup wanted sites)
163 (branch TelemetryPolicySitesEnd . 0)
164 (branch
165 TelemetryPolicySitesNext
166 tag
167 site
168 declaration
169 following
170 induction
171 .
172 (aosChoose
173 Nat
174 (captureSiteSelected policy site)
175 (naturalAnd
176 (naturalAnd
177 (nativeTelemetrySourcesAdmission
178 (telemetryRecordRouteLookup
179 tag
180 (aosChoose
181 (family TelemetryRecordRoutes)
182 (captureSiteReserved site)
183 reservedRoutes
184 ordinaryRoutes))
185 values)
186 (nativeTelemetrySourceScopesWith
187 (telemetryRecordRouteLookup
188 tag
189 (aosChoose
190 (family TelemetryRecordRoutes)
191 (captureSiteReserved site)
192 reservedRoutes
193 ordinaryRoutes))
194 values
195 (nativePhysicalOperandScopeAdmission
196 applicationBytes
197 applicationSlots
198 0)))
199 (naturalOr
200 (naturalEqual (captureSiteStride site) 1)
201 (nativePhysicalOperandScopeAdmission
202 applicationBytes
203 applicationSlots
204 0
205 coordinate)))
206 1))))
207 (branch TelemetryDispatchRefused reason . 0)))
208 (branch TelemetryRoutedPolicyRefused reason . 0))))))))
209
210-- Operations from a declared fragment and individually declared operations
211-- share scope and repeat-flow admission; preserving an error identity must not
212-- introduce a second, more permissive path into recorder-private storage.
213def nativeObservedAdmitOperation =
214 (lambda unrestricted applicationBytes : Nat .
215 (lambda unrestricted applicationSlots : Nat .
216 (lambda unrestricted operation : (family NativePhysicalOperation) .
217 (lambda unrestricted induction : (pi unrestricted depth : Nat . (pi unrestricted closed : Nat . Nat)) .
218 (lambda unrestricted depth : Nat .
219 (lambda unrestricted closed : Nat .
220 (naturalAnd
221 (nativeObservedOperationAllowed operation)
222 (naturalAnd
223 (nativePhysicalOperationScopeAdmission
224 applicationBytes
225 applicationSlots
226 operation)
227 (naturalAnd
228 (naturalOr
229 (naturalIsZero (naturalEqual (nativePhysicalRepeatAction operation) 2))
230 (naturalNonzero depth))
231 (induction
232 (aosChoose
233 Nat
234 (naturalEqual (nativePhysicalRepeatAction operation) 1)
235 (succ depth)
236 (aosChoose
237 Nat
238 (naturalEqual (nativePhysicalRepeatAction operation) 2)
239 (naturalSaturatingSubtract depth 1)
240 depth))
241 closed))))))))))
242
243-- Check source scopes before extending storage. Finish closes observation,
244-- not application success: cleanup may follow, but capture cannot. Closing
245-- inside a repeat would invalidate later iterations and is refused statically.
246def nativeObservedStepsAdmission =
247 (lambda unrestricted applicationBytes : Nat .
248 (lambda unrestricted applicationSlots : Nat .
249 (lambda unrestricted plan : (family TelemetryRoutedPolicyPlan) .
250 (lambda unrestricted steps : (family NativeObservedSteps) .
251 (app
252 (eliminate
253 NativeObservedSteps
254 (lambda unrestricted current : (family NativeObservedSteps) .
255 (pi unrestricted depth : Nat . (pi unrestricted closed : Nat . Nat)))
256 steps
257 (branch
258 NativeObservedStepsEnd
259 .
260 (lambda unrestricted depth : Nat .
261 (lambda unrestricted closed : Nat . (naturalIsZero depth))))
262 (branch
263 NativeObservedOperation
264 operation
265 following
266 induction
267 .
268 (nativeObservedAdmitOperation applicationBytes applicationSlots operation induction))
269 (branch
270 NativeObservedCommand
271 command
272 following
273 induction
274 .
275 (eliminate
276 NativePhysicalCommand
277 (lambda unrestricted current : (family NativePhysicalCommand) .
278 (pi unrestricted depth : Nat . (pi unrestricted closed : Nat . Nat)))
279 command
280 (branch
281 NativePhysicalCommandValue
282 operation
283 errorIdentity
284 .
285 (nativeObservedAdmitOperation
286 applicationBytes
287 applicationSlots
288 operation
289 induction))))
290 (branch
291 NativeObservedOpenJournal
292 pathAt
293 fileSlot
294 directorySlot
295 following
296 induction
297 .
298 (lambda unrestricted depth : Nat .
299 (lambda unrestricted closed : Nat .
300 (naturalAnd
301 (naturalIsZero depth)
302 (naturalAnd
303 (naturalIsZero closed)
304 (naturalAnd
305 (nativeObservedJournalAdmission
306 applicationBytes
307 applicationSlots
308 pathAt
309 fileSlot
310 directorySlot)
311 (induction depth closed)))))))
312 (branch
313 NativeObservedCaptureBoundary
314 tag
315 values
316 coordinate
317 following
318 induction
319 .
320 (lambda unrestricted depth : Nat .
321 (lambda unrestricted closed : Nat .
322 (naturalAnd
323 (naturalIsZero closed)
324 (naturalAnd
325 (nativeObservedCaptureAdmission
326 applicationBytes
327 applicationSlots
328 plan
329 tag
330 values
331 coordinate)
332 (induction depth closed))))))
333 (branch
334 NativeObservedFinish
335 following
336 induction
337 .
338 (lambda unrestricted depth : Nat .
339 (lambda unrestricted closed : Nat .
340 (naturalAnd
341 (naturalIsZero depth)
342 (naturalAnd (naturalIsZero closed) (induction depth 1)))))))
343 0
344 0)))))
345
346-- Each effect lowers through the maintained policy owners. End supplies a
347-- terminal acknowledgement only when no explicit Finish has already done so.
348-- Inserted nested loops preserve the application's active loop coordinates.
349def nativeObservedLowerSteps =
350 (lambda unrestricted applicationBytes : Nat .
351 (lambda unrestricted applicationSlots : Nat .
352 (lambda unrestricted plan : (family TelemetryRoutedPolicyPlan) .
353 (lambda unrestricted sink : (family NativePhysicalOperand) .
354 (lambda unrestricted directory : (family NativePhysicalOperand) .
355 (lambda unrestricted identity : Bytes .
356 (lambda unrestricted steps : (family NativeObservedSteps) .
357 (app
358 (eliminate
359 NativeObservedSteps
360 (lambda unrestricted current : (family NativeObservedSteps) .
361 (pi unrestricted closed : Nat . (family NativePhysicalCommands)))
362 steps
363 (branch
364 NativeObservedStepsEnd
365 .
366 (lambda unrestricted closed : Nat .
367 (aosChoose
368 (family NativePhysicalCommands)
369 closed
370 (constructor NativePhysicalCommands NativePhysicalCommandsEnd)
371 (nativeTelemetryRoutedPolicyBoundaryCommands
372 applicationBytes
373 plan
374 1
375 sink
376 directory
377 (nativeObservedCaptureSlot applicationSlots)
378 (nativeObservedPublicationSlot applicationSlots)
379 (nativeObservedWorkSlot applicationSlots)
380 identity
381 (nativeLaunchRecipeAssertEqual
382 (nativeLaunchRecipeSlotValue
383 (nativeObservedPublicationSlot applicationSlots))
384 (nativeLaunchRecipeImmediate 0)
385 (nativeTelemetryFailureIdentity
386 b"telemetry:terminal-publication-refused")
387 (constructor NativePhysicalCommands NativePhysicalCommandsEnd))))))
388 (branch
389 NativeObservedOperation
390 operation
391 following
392 induction
393 .
394 (lambda unrestricted closed : Nat .
395 (nativeLaunchRecipeCommand operation identity (induction closed))))
396 (branch
397 NativeObservedCommand
398 command
399 following
400 induction
401 .
402 (lambda unrestricted closed : Nat .
403 (constructor
404 NativePhysicalCommands
405 NativePhysicalCommandsNext
406 command
407 (induction closed))))
408 (branch
409 NativeObservedOpenJournal
410 pathAt
411 fileSlot
412 directorySlot
413 following
414 induction
415 .
416 (lambda unrestricted closed : Nat .
417 (nativeObservedJournalCommands
418 applicationBytes
419 plan
420 pathAt
421 fileSlot
422 directorySlot
423 (nativeObservedWorkSlot applicationSlots)
424 identity
425 (induction closed))))
426 (branch
427 NativeObservedCaptureBoundary
428 tag
429 values
430 coordinate
431 following
432 induction
433 .
434 (lambda unrestricted closed : Nat .
435 (nativeTelemetryRoutedCaptureAndContinueCommands
436 applicationBytes
437 plan
438 tag
439 values
440 coordinate
441 sink
442 directory
443 (nativeObservedCaptureSlot applicationSlots)
444 (nativeObservedPublicationSlot applicationSlots)
445 (nativeObservedWorkSlot applicationSlots)
446 (nativeObservedRetrySlot applicationSlots)
447 identity
448 (induction closed))))
449 (branch
450 NativeObservedFinish
451 following
452 induction
453 .
454 (lambda unrestricted closed : Nat .
455 (nativeTelemetryRoutedPolicyBoundaryCommands
456 applicationBytes
457 plan
458 1
459 sink
460 directory
461 (nativeObservedCaptureSlot applicationSlots)
462 (nativeObservedPublicationSlot applicationSlots)
463 (nativeObservedWorkSlot applicationSlots)
464 identity
465 (nativeLaunchRecipeAssertEqual
466 (nativeLaunchRecipeSlotValue
467 (nativeObservedPublicationSlot applicationSlots))
468 (nativeLaunchRecipeImmediate 0)
469 (nativeTelemetryFailureIdentity
470 b"telemetry:terminal-publication-refused")
471 (induction 1))))))
472 0))))))))
473
474-- Compose a maintained physical fragment with declared effects. Fragments
475-- retain every command identity and loop marker; admission examines each
476-- operation in the original application scope before recorder storage exists.
477def nativeObservedPrefixCommands =
478 (lambda unrestricted commands : (family NativePhysicalCommands) .
479 (lambda unrestricted tail : (family NativeObservedSteps) .
480 (eliminate
481 NativePhysicalCommands
482 (lambda unrestricted current : (family NativePhysicalCommands) .
483 (family NativeObservedSteps))
484 commands
485 (branch NativePhysicalCommandsEnd . tail)
486 (branch
487 NativePhysicalCommandsNext
488 command
489 rest
490 induction
491 .
492 (constructor NativeObservedSteps NativeObservedCommand command induction)))))
493
494def nativeObservedPrefixWith =
495 (lambda unrestricted fragment : (pi unrestricted after : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
496 (nativeObservedPrefixCommands
497 (fragment (constructor NativePhysicalCommands NativePhysicalCommandsEnd))))
498
499def nativeObservedBuildProgramWithIdentitySource =
500 (lambda unrestricted source : (family NativeTelemetryIdentitySource) .
501 (lambda unrestricted requestedBytes : Nat .
502 (lambda unrestricted requestedSlots : Nat .
503 (lambda unrestricted plan : (family TelemetryRoutedPolicyPlan) .
504 (lambda unrestricted sink : (family NativePhysicalOperand) .
505 (lambda unrestricted directory : (family NativePhysicalOperand) .
506 (lambda unrestricted identity : Bytes .
507 (lambda unrestricted steps : (family NativeObservedSteps) .
508 (let unrestricted applicationBytes =
509 (nativeObservedCandidateBytes requestedBytes)
510 in
511 (let unrestricted applicationSlots =
512 (nativeObservedCandidateSlots requestedSlots)
513 in
514 (eliminate
515 TelemetryRoutedPolicyPlan
516 (lambda unrestricted current : (family TelemetryRoutedPolicyPlan) .
517 (family NativeObservedProgramResult))
518 plan
519 (branch
520 TelemetryRoutedPolicyReady
521 policy
522 sites
523 drain
524 .
525 (eliminate
526 TelemetryDispatchPlan
527 (lambda unrestricted current : (family TelemetryDispatchPlan) .
528 (family NativeObservedProgramResult))
529 drain
530 (branch
531 TelemetryDispatchReady
532 oc
533 rc
534 ordinaryRoutes
535 reservedRoutes
536 ordinary
537 reserved
538 descriptors
539 bound
540 .
541 (let unrestricted arena =
542 (telemetryRoutedPolicyArenaBytes
543 applicationBytes
544 oc
545 rc
546 ordinary
547 reserved
548 bound)
549 in
550 (aosChoose
551 (family NativeObservedProgramResult)
552 (naturalAnd
553 (naturalEqual requestedBytes applicationBytes)
554 (naturalAnd
555 (naturalEqual requestedSlots applicationSlots)
556 (naturalAnd
557 (naturalLessOrEqual arena nativeObservedAddressMaximum)
558 (telemetryRoutedPolicyArenaCertificate
559 applicationBytes
560 oc
561 rc
562 ordinary
563 reserved
564 bound))))
565 (aosChoose
566 (family NativeObservedProgramResult)
567 (naturalAnd
568 (nativePhysicalOperandScopeAdmission
569 applicationBytes
570 applicationSlots
571 0
572 sink)
573 (naturalAnd
574 (nativePhysicalOperandScopeAdmission
575 applicationBytes
576 applicationSlots
577 0
578 directory)
579 (naturalAnd
580 (nativeTelemetryIdentitySourceAdmission applicationBytes applicationSlots source)
581 (nativeObservedStepsAdmission
582 applicationBytes
583 applicationSlots
584 plan
585 steps))))
586 (let unrestricted commands =
587 (nativeTelemetryRoutedPolicyInitializeWithIdentity
588 (nativeTelemetryInitializeIdentityFrom source (nativeObservedWorkSlot applicationSlots))
589 applicationBytes
590 plan
591 (nativeObservedCaptureSlot applicationSlots)
592 identity
593 (nativeLaunchRecipeAssertEqual
594 (nativeLaunchRecipeSlotValue
595 (nativeObservedCaptureSlot applicationSlots))
596 (nativeLaunchRecipeImmediate 0)
597 (nativeTelemetryFailureIdentity
598 b"telemetry:initialization-refused")
599 (nativeObservedLowerSteps
600 applicationBytes
601 applicationSlots
602 plan
603 sink
604 directory
605 identity
606 steps)))
607 in
608 (let unrestricted program =
609 (constructor
610 NativePhysicalProgram
611 NativePhysicalProgramValue
612 (modelWord64FromNaturalTruncated arena)
613 (modelWord64FromNaturalTruncated
614 (succ (nativeObservedRetrySlot applicationSlots)))
615 commands
616 (eliminate
617 NativePhysicalCounts
618 (lambda unrestricted current : (family NativePhysicalCounts) .
619 Nat)
620 (nativePhysicalCommandsCounts commands)
621 (branch
622 NativePhysicalCountsValue
623 count
624 syscalls
625 copies
626 routines
627 polls
628 appends
629 assertions
630 halts
631 payload
632 .
633 count))
634 identity
635 0)
636 in
637 (eliminate
638 NativePhysicalProgramValidation
639 (lambda unrestricted current : (family NativePhysicalProgramValidation) .
640 (family NativeObservedProgramResult))
641 (nativePhysicalValidateProgram program)
642 (branch
643 NativePhysicalProgramValidated
644 checkedProgram
645 validationTelemetry
646 .
647 (constructor
648 NativeObservedProgramResult
649 NativeObservedProgramReady
650 checkedProgram))
651 (branch
652 NativePhysicalProgramRejected
653 error
654 telemetry
655 .
656 (constructor
657 NativeObservedProgramResult
658 NativeObservedProgramRefused
659 (bytes-append
660 b"observed-program-lowering-refused:"
661 (nativePhysicalErrorCodeBytes error)))))))
662 (constructor
663 NativeObservedProgramResult
664 NativeObservedProgramRefused
665 b"observed-program-source-scope-or-flow-refused"))
666 (constructor
667 NativeObservedProgramResult
668 NativeObservedProgramRefused
669 b"observed-program-native-layout-unavailable"))))
670 (branch
671 TelemetryDispatchRefused
672 reason
673 .
674 (constructor
675 NativeObservedProgramResult
676 NativeObservedProgramRefused
677 (bytes-append b"observed-program-policy-refused:" reason)))))
678 (branch
679 TelemetryRoutedPolicyRefused
680 reason
681 .
682 (constructor
683 NativeObservedProgramResult
684 NativeObservedProgramRefused
685 (bytes-append b"observed-program-policy-refused:" reason))))))))))))))
686
687def nativeObservedBuildProgram =
688 (nativeObservedBuildProgramWithIdentitySource (constructor NativeTelemetryIdentitySource NativeTelemetryFreshIdentity))
689
690-- A Refused value is inspectable through nativeObservedRefusalOf. Forcing it
691-- into target emission supplies rejected IR, never an empty successful artifact
692-- or a substitute program. The target's own validator remains authoritative.
693def nativeObservedRequireProgram =
694 (lambda unrestricted result : (family NativeObservedProgramResult) .
695 (eliminate
696 NativeObservedProgramResult
697 (lambda unrestricted current : (family NativeObservedProgramResult) .
698 (family NativePhysicalProgram))
699 result
700 (branch NativeObservedProgramReady program . program)
701 (branch
702 NativeObservedProgramRefused
703 reason
704 .
705 (constructor
706 NativePhysicalProgram
707 NativePhysicalProgramValue
708 0
709 0
710 (constructor NativePhysicalCommands NativePhysicalCommandsEnd)
711 0
712 (nativeTelemetryFailureIdentity
713 (bytes-append b"observed-program:declaration-refused:" reason))
714 0))))
715
716-- Inspect the named admission failure before requesting target emission.
717def nativeObservedRefusalOf =
718 (lambda unrestricted result : (family NativeObservedProgramResult) .
719 (eliminate
720 NativeObservedProgramResult
721 (lambda unrestricted current : (family NativeObservedProgramResult) . Bytes)
722 result
723 (branch NativeObservedProgramReady program . b"")
724 (branch NativeObservedProgramRefused reason . reason)))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.