Runtime.NativeObservedProgram

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)))