1module Runtime.LinuxSyscall
2
3import Model.Config
4import Model.Parameter
5import Model.Word64
6import Std.Natural
7
8family LinuxFileDescriptor : Type 0
9constructor LinuxFileDescriptorValue
10field unrestricted linuxFileDescriptorWord : (family ModelWord64)
11
12end-family
13
14family LinuxSeekWhence : Type 0
15constructor LinuxSeekSet
16constructor LinuxSeekCurrent
17constructor LinuxSeekEnd
18
19end-family
20
21family LinuxSyscallRequest : Type 0
22constructor LinuxOpenAt
23field unrestricted linuxOpenDirectoryDescriptor : (family ModelWord64)
24field unrestricted linuxOpenPath : Bytes
25field unrestricted linuxOpenFlags : (family ModelWord64)
26field unrestricted linuxOpenMode : (family ModelWord64)
27constructor LinuxRead
28field unrestricted linuxReadDescriptor : (family LinuxFileDescriptor)
29field unrestricted linuxReadRequestedBytes : (family ModelWord64)
30constructor LinuxSeek
31field unrestricted linuxSeekDescriptor : (family LinuxFileDescriptor)
32field unrestricted linuxSeekOffset : (family ModelWord64)
33field unrestricted linuxSeekWhence : (family LinuxSeekWhence)
34constructor LinuxWrite
35field unrestricted linuxWriteDescriptor : (family LinuxFileDescriptor)
36field unrestricted linuxWriteBytes : Bytes
37constructor LinuxClose
38field unrestricted linuxCloseDescriptor : (family LinuxFileDescriptor)
39constructor LinuxFsync
40field unrestricted linuxFsyncDescriptor : (family LinuxFileDescriptor)
41constructor LinuxFdatasync
42field unrestricted linuxFdatasyncDescriptor : (family LinuxFileDescriptor)
43constructor LinuxUnlinkAt
44field unrestricted linuxUnlinkDirectoryDescriptor : (family ModelWord64)
45field unrestricted linuxUnlinkPath : Bytes
46field unrestricted linuxUnlinkFlags : (family ModelWord64)
47constructor LinuxRenameAt2
48field unrestricted linuxRenameSourceDirectoryDescriptor : (family ModelWord64)
49field unrestricted linuxRenameSourcePath : Bytes
50field unrestricted linuxRenameDestinationDirectoryDescriptor : (family ModelWord64)
51field unrestricted linuxRenameDestinationPath : Bytes
52field unrestricted linuxRenameFlags : (family ModelWord64)
53constructor LinuxIoctl
54field unrestricted linuxIoctlDescriptor : (family LinuxFileDescriptor)
55field unrestricted linuxIoctlRequest : (family ModelWord64)
56field unrestricted linuxIoctlPayload : Bytes
57constructor LinuxMmap
58field unrestricted linuxMmapAddress : (family ModelWord64)
59field unrestricted linuxMmapExtent : (family ModelWord64)
60field unrestricted linuxMmapProtection : (family ModelWord64)
61field unrestricted linuxMmapFlags : (family ModelWord64)
62field unrestricted linuxMmapDescriptor : (family LinuxFileDescriptor)
63field unrestricted linuxMmapOffset : (family ModelWord64)
64constructor LinuxMunmap
65field unrestricted linuxMunmapAddress : (family ModelWord64)
66field unrestricted linuxMunmapExtent : (family ModelWord64)
67
68end-family
69
70family LinuxSyscallErrorCode : Type 0
71constructor LinuxSyscallPathEmpty
72constructor LinuxSyscallPathContainsNUL
73constructor LinuxSyscallRequestedBytesOverflow
74constructor LinuxSyscallOffsetOverflow
75constructor LinuxSyscallInterrupted
76constructor LinuxSyscallKernelFailure
77constructor LinuxSyscallReadCountInvalid
78constructor LinuxSyscallWriteCountInvalid
79constructor LinuxSyscallUnexpectedEOF
80constructor LinuxSyscallSeekPositionMismatch
81constructor LinuxSyscallExtentOverflow
82constructor LinuxSyscallUnexpectedPositiveResult
83constructor LinuxSyscallIoctlPayloadInvalid
84constructor LinuxSyscallMemoryMapFailed
85constructor LinuxSyscallResponseKindMismatch
86
87end-family
88
89family LinuxSyscallResponse : Type 0
90constructor LinuxOpenSucceeded
91field unrestricted linuxOpenedDescriptor : (family LinuxFileDescriptor)
92constructor LinuxReadSucceeded
93field unrestricted linuxReadBytes : Bytes
94constructor LinuxSeekSucceeded
95field unrestricted linuxSeekPosition : (family ModelWord64)
96constructor LinuxWriteSucceeded
97field unrestricted linuxWrittenBytes : (family ModelWord64)
98constructor LinuxIoctlSucceeded
99field unrestricted linuxIoctlOutput : Bytes
100constructor LinuxMmapSucceeded
101field unrestricted linuxMappedAddress : (family ModelWord64)
102constructor LinuxUnitSucceeded
103constructor LinuxSyscallFailed
104field unrestricted linuxSyscallError : (family LinuxSyscallErrorCode)
105field unrestricted linuxSyscallErrno : (family ModelWord32)
106
107end-family
108
109family LinuxOpenProfile : Type 0
110constructor LinuxOpenCheckpointExclusive
111constructor LinuxOpenReadOnlyNoFollow
112constructor LinuxOpenDirectoryNoFollow
113constructor LinuxOpenDeviceReadWrite
114
115end-family
116
117family LinuxClockIdentifier : Type 0
118constructor LinuxClockRealtime
119constructor LinuxClockMonotonic
120constructor LinuxClockMonotonicRaw
121
122end-family
123
124family LinuxTimestamp : Type 0
125constructor LinuxTimestampValue
126field unrestricted linuxTimestampSeconds : (family ModelWord64)
127field unrestricted linuxTimestampNanoseconds : (family ModelWord32)
128
129end-family
130
131family LinuxFileStatus : Type 0
132constructor LinuxFileStatusValue
133field unrestricted linuxFileStatusDevice : (family ModelWord64)
134field unrestricted linuxFileStatusInode : (family ModelWord64)
135field unrestricted linuxFileStatusMode : (family ModelWord32)
136field unrestricted linuxFileStatusLinkCount : (family ModelWord64)
137field unrestricted linuxFileStatusUser : (family ModelWord32)
138field unrestricted linuxFileStatusGroup : (family ModelWord32)
139field unrestricted linuxFileStatusExtent : (family ModelWord64)
140field unrestricted linuxFileStatusBlockExtent : (family ModelWord64)
141field unrestricted linuxFileStatusBlocks : (family ModelWord64)
142field unrestricted linuxFileStatusModifiedAt : (family LinuxTimestamp)
143
144end-family
145
146family LinuxExtendedSyscallRequest : Type 0
147constructor LinuxFstatRequest
148field unrestricted linuxFstatDescriptor : (family LinuxFileDescriptor)
149constructor LinuxClockGettimeRequest
150field unrestricted linuxClockGettimeClock : (family LinuxClockIdentifier)
151
152end-family
153
154family LinuxExtendedSyscallResponse : Type 0
155constructor LinuxFstatSucceeded
156field unrestricted linuxFstatStatus : (family LinuxFileStatus)
157constructor LinuxClockGettimeSucceeded
158field unrestricted linuxClockGettimeTimestamp : (family LinuxTimestamp)
159constructor LinuxExtendedSyscallFailed
160field unrestricted linuxExtendedSyscallError : (family LinuxSyscallErrorCode)
161field unrestricted linuxExtendedSyscallErrno : (family ModelWord32)
162
163end-family
164
165family LinuxSyscallRequestIdentity : Type 0
166constructor LinuxSyscallRequestIdentityValue
167field unrestricted linuxSyscallRequestIdentityNatural : Nat
168
169end-family
170
171family LinuxNativeSyscallInvocation : Type 0
172constructor LinuxNativeBaseInvocation
173field unrestricted linuxNativeBaseIdentity : (family LinuxSyscallRequestIdentity)
174field unrestricted linuxNativeBaseRequest : (family LinuxSyscallRequest)
175constructor LinuxNativeExtendedInvocation
176field unrestricted linuxNativeExtendedIdentity : (family LinuxSyscallRequestIdentity)
177field unrestricted linuxNativeExtendedRequest : (family LinuxExtendedSyscallRequest)
178
179end-family
180
181family LinuxOptionalErrno : Type 0
182constructor LinuxNoErrno
183constructor LinuxSomeErrno
184field unrestricted linuxSomeErrnoValue : (family ModelWord32)
185
186end-family
187
188family LinuxCleanupTelemetry : Type 0
189constructor LinuxCleanupTelemetryValue
190field unrestricted linuxCleanupCloseAttempts : Nat
191field unrestricted linuxCleanupClosesCompleted : Nat
192field unrestricted linuxCleanupMunmapAttempts : Nat
193field unrestricted linuxCleanupMunmapsCompleted : Nat
194field unrestricted linuxCleanupUnlinkAttempts : Nat
195field unrestricted linuxCleanupUnlinksCompleted : Nat
196field unrestricted linuxCleanupSyncAttempts : Nat
197field unrestricted linuxCleanupSyncsCompleted : Nat
198field unrestricted linuxCleanupFailures : Nat
199field unrestricted linuxCleanupFirstErrno : (family LinuxOptionalErrno)
200field unrestricted linuxCleanupHostFallbacks : Nat
201
202end-family
203
204family LinuxSyscallReceiptTelemetry : Type 0
205constructor LinuxSyscallReceiptTelemetryValue
206field unrestricted linuxReceiptSyscallsIssued : Nat
207field unrestricted linuxReceiptSyscallsCompleted : Nat
208field unrestricted linuxReceiptInterruptedRetries : Nat
209field unrestricted linuxReceiptRequestedBytes : (family ModelWord64)
210field unrestricted linuxReceiptCompletedBytes : (family ModelWord64)
211field unrestricted linuxReceiptEOFObserved : Nat
212field unrestricted linuxReceiptCleanup : (family LinuxCleanupTelemetry)
213
214end-family
215
216family LinuxNativeSyscallReceipt : Type 0
217constructor LinuxNativeBaseReceipt
218field unrestricted linuxNativeBaseReceiptIdentity : (family LinuxSyscallRequestIdentity)
219field unrestricted linuxNativeBaseReceiptResponse : (family LinuxSyscallResponse)
220field unrestricted linuxNativeBaseReceiptTelemetry : (family LinuxSyscallReceiptTelemetry)
221constructor LinuxNativeExtendedReceipt
222field unrestricted linuxNativeExtendedReceiptIdentity : (family LinuxSyscallRequestIdentity)
223field unrestricted linuxNativeExtendedReceiptResponse : (family LinuxExtendedSyscallResponse)
224field unrestricted linuxNativeExtendedReceiptTelemetry : (family LinuxSyscallReceiptTelemetry)
225
226end-family
227
228family LinuxSyscallReceiptAudit : Type 0
229constructor LinuxSyscallReceiptAuditValue
230field unrestricted linuxReceiptExpectedIdentity : (family LinuxSyscallRequestIdentity)
231field unrestricted linuxReceiptActualIdentity : (family LinuxSyscallRequestIdentity)
232field unrestricted linuxReceiptAuditTelemetry : (family LinuxSyscallReceiptTelemetry)
233
234end-family
235
236family LinuxSyscallContractErrorCode : Type 0
237constructor LinuxReceiptIdentityMismatch
238constructor LinuxReceiptResponseKindMismatch
239constructor LinuxReceiptHostFallbackRejected
240constructor LinuxReceiptCleanupFailed
241constructor LinuxReceiptExactReadShort
242constructor LinuxReceiptExactWriteShort
243constructor LinuxReceiptUnexpectedEOF
244constructor LinuxReceiptExactIOPlanMismatch
245constructor LinuxReceiptTelemetryInvalid
246constructor LinuxReceiptExtendedKindMismatch
247constructor LinuxReceiptTimestampInvalid
248constructor LinuxReceiptFileStatusInvalid
249
250end-family
251
252family LinuxSyscallReceiptDecision : Type 0
253constructor LinuxSyscallReceiptAcceptedBase
254field unrestricted linuxAcceptedBaseResponse : (family LinuxSyscallResponse)
255field unrestricted linuxAcceptedBaseAudit : (family LinuxSyscallReceiptAudit)
256constructor LinuxSyscallReceiptAcceptedExtended
257field unrestricted linuxAcceptedExtendedResponse : (family LinuxExtendedSyscallResponse)
258field unrestricted linuxAcceptedExtendedAudit : (family LinuxSyscallReceiptAudit)
259constructor LinuxSyscallReceiptRetryInterrupted
260field unrestricted linuxRetryInterruptedInvocation : (family LinuxNativeSyscallInvocation)
261field unrestricted linuxRetryInterruptedAudit : (family LinuxSyscallReceiptAudit)
262constructor LinuxSyscallReceiptFailed
263field unrestricted linuxFailedSyscallError : (family LinuxSyscallErrorCode)
264field unrestricted linuxFailedSyscallErrno : (family ModelWord32)
265field unrestricted linuxFailedSyscallAudit : (family LinuxSyscallReceiptAudit)
266constructor LinuxSyscallReceiptRejected
267field unrestricted linuxRejectedContractError : (family LinuxSyscallContractErrorCode)
268field unrestricted linuxRejectedSyscallAudit : (family LinuxSyscallReceiptAudit)
269
270end-family
271
272family LinuxSuccessfulResponseKind : Type 0
273constructor LinuxSuccessfulOpenKind
274constructor LinuxSuccessfulReadKind
275constructor LinuxSuccessfulSeekKind
276constructor LinuxSuccessfulWriteKind
277constructor LinuxSuccessfulIoctlKind
278constructor LinuxSuccessfulMmapKind
279constructor LinuxSuccessfulUnitKind
280
281end-family
282
283family LinuxExactIOKind : Type 0
284constructor LinuxExactReadKind
285constructor LinuxExactWriteKind
286
287end-family
288
289family LinuxExactIOPlan : Type 0
290constructor LinuxExactIOPlanValue
291field unrestricted linuxExactIOPlanIdentity : (family LinuxSyscallRequestIdentity)
292field unrestricted linuxExactIOPlanKind : (family LinuxExactIOKind)
293field unrestricted linuxExactIOPlanDescriptor : (family LinuxFileDescriptor)
294field unrestricted linuxExactIOPlanExtent : (family ModelWord64)
295field unrestricted linuxExactIOPlanMaximumChunk : (family ModelWord64)
296
297end-family
298
299family LinuxExactIOReceipt : Type 0
300constructor LinuxExactIOReceiptValue
301field unrestricted linuxExactIOReceiptIdentity : (family LinuxSyscallRequestIdentity)
302field unrestricted linuxExactIOReceiptKind : (family LinuxExactIOKind)
303field unrestricted linuxExactIOReceiptCompleted : (family ModelWord64)
304field unrestricted linuxExactIOReceiptTelemetry : (family LinuxSyscallReceiptTelemetry)
305
306end-family
307
308family LinuxExactIOValidation : Type 0
309constructor LinuxExactIOAccepted
310field unrestricted linuxExactIOAcceptedReceipt : (family LinuxExactIOReceipt)
311constructor LinuxExactIORejected
312field unrestricted linuxExactIORejectedError : (family LinuxSyscallContractErrorCode)
313field unrestricted linuxExactIOExpectedExtent : (family ModelWord64)
314field unrestricted linuxExactIOActualExtent : (family ModelWord64)
315field unrestricted linuxExactIORejectedTelemetry : (family LinuxSyscallReceiptTelemetry)
316
317end-family
318
319def linuxAtFdcwd =
320 (constructor
321 ModelWord64
322 ModelWord64Value
323 (byte 156)
324 (byte 255)
325 (byte 255)
326 (byte 255)
327 (byte 255)
328 (byte 255)
329 (byte 255)
330 (byte 255))
331
332def linuxOpenExclusiveFlags =
333 (constructor
334 ModelWord64
335 ModelWord64Value
336 (byte 193)
337 (byte 0)
338 (byte 10)
339 (byte 0)
340 (byte 0)
341 (byte 0)
342 (byte 0)
343 (byte 0))
344
345def linuxOpenReadOnlyFlags =
346 (constructor
347 ModelWord64
348 ModelWord64Value
349 (byte 0)
350 (byte 0)
351 (byte 10)
352 (byte 0)
353 (byte 0)
354 (byte 0)
355 (byte 0)
356 (byte 0))
357
358def linuxOpenDirectoryFlags =
359 (constructor
360 ModelWord64
361 ModelWord64Value
362 (byte 0)
363 (byte 0)
364 (byte 11)
365 (byte 0)
366 (byte 0)
367 (byte 0)
368 (byte 0)
369 (byte 0))
370
371def linuxOpenReadWriteCloseOnExecFlags =
372 (constructor
373 ModelWord64
374 ModelWord64Value
375 (byte 2)
376 (byte 0)
377 (byte 8)
378 (byte 0)
379 (byte 0)
380 (byte 0)
381 (byte 0)
382 (byte 0))
383
384def linuxMemoryProtectionReadWrite =
385 (constructor
386 ModelWord64
387 ModelWord64Value
388 (byte 3)
389 (byte 0)
390 (byte 0)
391 (byte 0)
392 (byte 0)
393 (byte 0)
394 (byte 0)
395 (byte 0))
396
397def linuxMemoryMapShared =
398 (constructor
399 ModelWord64
400 ModelWord64Value
401 (byte 1)
402 (byte 0)
403 (byte 0)
404 (byte 0)
405 (byte 0)
406 (byte 0)
407 (byte 0)
408 (byte 0))
409
410def linuxOwnerReadWriteMode =
411 (constructor
412 ModelWord64
413 ModelWord64Value
414 (byte 128)
415 (byte 1)
416 (byte 0)
417 (byte 0)
418 (byte 0)
419 (byte 0)
420 (byte 0)
421 (byte 0))
422
423def linuxRenameNoReplaceFlag =
424 (constructor
425 ModelWord64
426 ModelWord64Value
427 (byte 1)
428 (byte 0)
429 (byte 0)
430 (byte 0)
431 (byte 0)
432 (byte 0)
433 (byte 0)
434 (byte 0))
435
436def linuxSyscallRead =
437 (constructor
438 ModelWord64
439 ModelWord64Value
440 (byte 0)
441 (byte 0)
442 (byte 0)
443 (byte 0)
444 (byte 0)
445 (byte 0)
446 (byte 0)
447 (byte 0))
448
449def linuxSyscallWrite =
450 (constructor
451 ModelWord64
452 ModelWord64Value
453 (byte 1)
454 (byte 0)
455 (byte 0)
456 (byte 0)
457 (byte 0)
458 (byte 0)
459 (byte 0)
460 (byte 0))
461
462def linuxSyscallClose =
463 (constructor
464 ModelWord64
465 ModelWord64Value
466 (byte 3)
467 (byte 0)
468 (byte 0)
469 (byte 0)
470 (byte 0)
471 (byte 0)
472 (byte 0)
473 (byte 0))
474
475def linuxSyscallLseek =
476 (constructor
477 ModelWord64
478 ModelWord64Value
479 (byte 8)
480 (byte 0)
481 (byte 0)
482 (byte 0)
483 (byte 0)
484 (byte 0)
485 (byte 0)
486 (byte 0))
487
488def linuxSyscallMmap =
489 (constructor
490 ModelWord64
491 ModelWord64Value
492 (byte 9)
493 (byte 0)
494 (byte 0)
495 (byte 0)
496 (byte 0)
497 (byte 0)
498 (byte 0)
499 (byte 0))
500
501def linuxSyscallMunmap =
502 (constructor
503 ModelWord64
504 ModelWord64Value
505 (byte 11)
506 (byte 0)
507 (byte 0)
508 (byte 0)
509 (byte 0)
510 (byte 0)
511 (byte 0)
512 (byte 0))
513
514def linuxSyscallIoctl =
515 (constructor
516 ModelWord64
517 ModelWord64Value
518 (byte 16)
519 (byte 0)
520 (byte 0)
521 (byte 0)
522 (byte 0)
523 (byte 0)
524 (byte 0)
525 (byte 0))
526
527def linuxSyscallFsync =
528 (constructor
529 ModelWord64
530 ModelWord64Value
531 (byte 74)
532 (byte 0)
533 (byte 0)
534 (byte 0)
535 (byte 0)
536 (byte 0)
537 (byte 0)
538 (byte 0))
539
540def linuxSyscallFdatasync =
541 (constructor
542 ModelWord64
543 ModelWord64Value
544 (byte 75)
545 (byte 0)
546 (byte 0)
547 (byte 0)
548 (byte 0)
549 (byte 0)
550 (byte 0)
551 (byte 0))
552
553def linuxSyscallOpenAt =
554 (constructor
555 ModelWord64
556 ModelWord64Value
557 (byte 1)
558 (byte 1)
559 (byte 0)
560 (byte 0)
561 (byte 0)
562 (byte 0)
563 (byte 0)
564 (byte 0))
565
566def linuxSyscallUnlinkAt =
567 (constructor
568 ModelWord64
569 ModelWord64Value
570 (byte 7)
571 (byte 1)
572 (byte 0)
573 (byte 0)
574 (byte 0)
575 (byte 0)
576 (byte 0)
577 (byte 0))
578
579def linuxSyscallRenameAt2 =
580 (constructor
581 ModelWord64
582 ModelWord64Value
583 (byte 60)
584 (byte 1)
585 (byte 0)
586 (byte 0)
587 (byte 0)
588 (byte 0)
589 (byte 0)
590 (byte 0))
591
592-- The original LinuxSyscallRequest and LinuxSyscallResponse families are the
593-- wire contract already consumed by the native executor. The identity-bound
594-- layer below deliberately wraps that contract rather than changing the arity
595-- of its constructors. fstat and clock_gettime are typed extensions because
596-- their successful receipts carry decoded kernel structures rather than an
597-- untyped byte buffer.
598def linuxZeroWord64 =
599 (constructor
600 ModelWord64
601 ModelWord64Value
602 (byte 0)
603 (byte 0)
604 (byte 0)
605 (byte 0)
606 (byte 0)
607 (byte 0)
608 (byte 0)
609 (byte 0))
610
611def linuxZeroWord32 =
612 (constructor ModelWord32 ModelWord32Value (byte 0) (byte 0) (byte 0) (byte 0))
613
614def linuxOpenReadOnlyFlag =
615 linuxZeroWord64
616
617def linuxOpenWriteOnlyFlag =
618 (constructor
619 ModelWord64
620 ModelWord64Value
621 (byte 1)
622 (byte 0)
623 (byte 0)
624 (byte 0)
625 (byte 0)
626 (byte 0)
627 (byte 0)
628 (byte 0))
629
630def linuxOpenReadWriteFlag =
631 (constructor
632 ModelWord64
633 ModelWord64Value
634 (byte 2)
635 (byte 0)
636 (byte 0)
637 (byte 0)
638 (byte 0)
639 (byte 0)
640 (byte 0)
641 (byte 0))
642
643def linuxOpenCreateFlag =
644 (constructor
645 ModelWord64
646 ModelWord64Value
647 (byte 64)
648 (byte 0)
649 (byte 0)
650 (byte 0)
651 (byte 0)
652 (byte 0)
653 (byte 0)
654 (byte 0))
655
656def linuxOpenExclusiveFlag =
657 (constructor
658 ModelWord64
659 ModelWord64Value
660 (byte 128)
661 (byte 0)
662 (byte 0)
663 (byte 0)
664 (byte 0)
665 (byte 0)
666 (byte 0)
667 (byte 0))
668
669def linuxOpenDirectoryFlag =
670 (constructor
671 ModelWord64
672 ModelWord64Value
673 (byte 0)
674 (byte 0)
675 (byte 1)
676 (byte 0)
677 (byte 0)
678 (byte 0)
679 (byte 0)
680 (byte 0))
681
682def linuxOpenNoFollowFlag =
683 (constructor
684 ModelWord64
685 ModelWord64Value
686 (byte 0)
687 (byte 0)
688 (byte 2)
689 (byte 0)
690 (byte 0)
691 (byte 0)
692 (byte 0)
693 (byte 0))
694
695def linuxOpenCloseOnExecFlag =
696 (constructor
697 ModelWord64
698 ModelWord64Value
699 (byte 0)
700 (byte 0)
701 (byte 8)
702 (byte 0)
703 (byte 0)
704 (byte 0)
705 (byte 0)
706 (byte 0))
707
708def linuxUnlinkFileFlags =
709 linuxZeroWord64
710
711def linuxErrnoInterrupted =
712 (constructor ModelWord32 ModelWord32Value (byte 4) (byte 0) (byte 0) (byte 0))
713
714def linuxExactIOChunkLimit =
715 (constructor
716 ModelWord64
717 ModelWord64Value
718 (byte 0)
719 (byte 0)
720 (byte 16)
721 (byte 0)
722 (byte 0)
723 (byte 0)
724 (byte 0)
725 (byte 0))
726
727def linuxSyscallFstat =
728 (constructor
729 ModelWord64
730 ModelWord64Value
731 (byte 5)
732 (byte 0)
733 (byte 0)
734 (byte 0)
735 (byte 0)
736 (byte 0)
737 (byte 0)
738 (byte 0))
739
740def linuxSyscallClockGettime =
741 (constructor
742 ModelWord64
743 ModelWord64Value
744 (byte 228)
745 (byte 0)
746 (byte 0)
747 (byte 0)
748 (byte 0)
749 (byte 0)
750 (byte 0)
751 (byte 0))
752
753def linuxOpenProfileFlags =
754 (lambda unrestricted profile : (family LinuxOpenProfile) .
755 (eliminate
756 LinuxOpenProfile
757 (lambda unrestricted current : (family LinuxOpenProfile) . (family ModelWord64))
758 profile
759 (branch LinuxOpenCheckpointExclusive . linuxOpenExclusiveFlags)
760 (branch LinuxOpenReadOnlyNoFollow . linuxOpenReadOnlyFlags)
761 (branch LinuxOpenDirectoryNoFollow . linuxOpenDirectoryFlags)
762 (branch LinuxOpenDeviceReadWrite . linuxOpenReadWriteCloseOnExecFlags)))
763
764def linuxOpenProfileMode =
765 (lambda unrestricted profile : (family LinuxOpenProfile) .
766 (eliminate
767 LinuxOpenProfile
768 (lambda unrestricted current : (family LinuxOpenProfile) . (family ModelWord64))
769 profile
770 (branch LinuxOpenCheckpointExclusive . linuxOwnerReadWriteMode)
771 (branch LinuxOpenReadOnlyNoFollow . linuxZeroWord64)
772 (branch LinuxOpenDirectoryNoFollow . linuxZeroWord64)
773 (branch LinuxOpenDeviceReadWrite . linuxZeroWord64)))
774
775def linuxOpenAtProfileRequest =
776 (lambda unrestricted path : Bytes .
777 (lambda unrestricted profile : (family LinuxOpenProfile) .
778 (constructor
779 LinuxSyscallRequest
780 LinuxOpenAt
781 linuxAtFdcwd
782 path
783 (linuxOpenProfileFlags profile)
784 (linuxOpenProfileMode profile))))
785
786def linuxRenameNoReplaceRequest =
787 (lambda unrestricted source : Bytes .
788 (lambda unrestricted destination : Bytes .
789 (constructor
790 LinuxSyscallRequest
791 LinuxRenameAt2
792 linuxAtFdcwd
793 source
794 linuxAtFdcwd
795 destination
796 linuxRenameNoReplaceFlag)))
797
798def linuxUnlinkFileRequest =
799 (lambda unrestricted path : Bytes .
800 (constructor LinuxSyscallRequest LinuxUnlinkAt linuxAtFdcwd path linuxUnlinkFileFlags))
801
802-- The executor must reject a timestamp whose nanosecond component is not in
803-- [0, 1000000000). File extent is likewise a decoded non-negative st_size.
804def linuxSyscallErrorCodeBytes =
805 (lambda unrestricted code : (family LinuxSyscallErrorCode) .
806 (eliminate
807 LinuxSyscallErrorCode
808 (lambda unrestricted current : (family LinuxSyscallErrorCode) . Bytes)
809 code
810 (branch LinuxSyscallPathEmpty . b"ALPHA-LINUX-001")
811 (branch LinuxSyscallPathContainsNUL . b"ALPHA-LINUX-002")
812 (branch
813 LinuxSyscallRequestedBytesOverflow
814 .
815 b"ALPHA-LINUX-003")
816 (branch LinuxSyscallOffsetOverflow . b"ALPHA-LINUX-004")
817 (branch LinuxSyscallInterrupted . b"ALPHA-LINUX-005")
818 (branch LinuxSyscallKernelFailure . b"ALPHA-LINUX-006")
819 (branch LinuxSyscallReadCountInvalid . b"ALPHA-LINUX-007")
820 (branch LinuxSyscallWriteCountInvalid . b"ALPHA-LINUX-008")
821 (branch LinuxSyscallUnexpectedEOF . b"ALPHA-LINUX-009")
822 (branch
823 LinuxSyscallSeekPositionMismatch
824 .
825 b"ALPHA-LINUX-010")
826 (branch LinuxSyscallExtentOverflow . b"ALPHA-LINUX-011")
827 (branch
828 LinuxSyscallUnexpectedPositiveResult
829 .
830 b"ALPHA-LINUX-012")
831 (branch
832 LinuxSyscallIoctlPayloadInvalid
833 .
834 b"ALPHA-LINUX-013")
835 (branch LinuxSyscallMemoryMapFailed . b"ALPHA-LINUX-014")
836 (branch
837 LinuxSyscallResponseKindMismatch
838 .
839 b"ALPHA-LINUX-015")))
840
841def linuxSyscallContractErrorCodeBytes =
842 (lambda unrestricted code : (family LinuxSyscallContractErrorCode) .
843 (eliminate
844 LinuxSyscallContractErrorCode
845 (lambda unrestricted current : (family LinuxSyscallContractErrorCode) . Bytes)
846 code
847 (branch LinuxReceiptIdentityMismatch . b"ALPHA-LINUX-101")
848 (branch
849 LinuxReceiptResponseKindMismatch
850 .
851 b"ALPHA-LINUX-102")
852 (branch
853 LinuxReceiptHostFallbackRejected
854 .
855 b"ALPHA-LINUX-103")
856 (branch LinuxReceiptCleanupFailed . b"ALPHA-LINUX-104")
857 (branch LinuxReceiptExactReadShort . b"ALPHA-LINUX-105")
858 (branch LinuxReceiptExactWriteShort . b"ALPHA-LINUX-106")
859 (branch LinuxReceiptUnexpectedEOF . b"ALPHA-LINUX-107")
860 (branch
861 LinuxReceiptExactIOPlanMismatch
862 .
863 b"ALPHA-LINUX-108")
864 (branch LinuxReceiptTelemetryInvalid . b"ALPHA-LINUX-109")
865 (branch
866 LinuxReceiptExtendedKindMismatch
867 .
868 b"ALPHA-LINUX-110")
869 (branch LinuxReceiptTimestampInvalid . b"ALPHA-LINUX-111")
870 (branch LinuxReceiptFileStatusInvalid . b"ALPHA-LINUX-112")))
871
872def linuxIdentityEqual =
873 (lambda unrestricted left : (family LinuxSyscallRequestIdentity) .
874 (lambda unrestricted right : (family LinuxSyscallRequestIdentity) .
875 (eliminate
876 LinuxSyscallRequestIdentity
877 (lambda unrestricted current : (family LinuxSyscallRequestIdentity) . Nat)
878 left
879 (branch
880 LinuxSyscallRequestIdentityValue
881 leftNatural
882 .
883 (eliminate
884 LinuxSyscallRequestIdentity
885 (lambda unrestricted current : (family LinuxSyscallRequestIdentity) . Nat)
886 right
887 (branch
888 LinuxSyscallRequestIdentityValue
889 rightNatural
890 .
891 (naturalEqual leftNatural rightNatural)))))))
892
893def linuxNativeInvocationIdentity =
894 (lambda unrestricted invocation : (family LinuxNativeSyscallInvocation) .
895 (eliminate
896 LinuxNativeSyscallInvocation
897 (lambda unrestricted current : (family LinuxNativeSyscallInvocation) .
898 (family LinuxSyscallRequestIdentity))
899 invocation
900 (branch LinuxNativeBaseInvocation identity request . identity)
901 (branch LinuxNativeExtendedInvocation identity request . identity)))
902
903def linuxNativeReceiptIdentity =
904 (lambda unrestricted receipt : (family LinuxNativeSyscallReceipt) .
905 (eliminate
906 LinuxNativeSyscallReceipt
907 (lambda unrestricted current : (family LinuxNativeSyscallReceipt) .
908 (family LinuxSyscallRequestIdentity))
909 receipt
910 (branch LinuxNativeBaseReceipt identity response telemetry . identity)
911 (branch LinuxNativeExtendedReceipt identity response telemetry . identity)))
912
913def linuxNativeReceiptTelemetry =
914 (lambda unrestricted receipt : (family LinuxNativeSyscallReceipt) .
915 (eliminate
916 LinuxNativeSyscallReceipt
917 (lambda unrestricted current : (family LinuxNativeSyscallReceipt) .
918 (family LinuxSyscallReceiptTelemetry))
919 receipt
920 (branch LinuxNativeBaseReceipt identity response telemetry . telemetry)
921 (branch LinuxNativeExtendedReceipt identity response telemetry . telemetry)))
922
923def linuxReceiptAudit =
924 (lambda unrestricted invocation : (family LinuxNativeSyscallInvocation) .
925 (lambda unrestricted receipt : (family LinuxNativeSyscallReceipt) .
926 (constructor
927 LinuxSyscallReceiptAudit
928 LinuxSyscallReceiptAuditValue
929 (linuxNativeInvocationIdentity invocation)
930 (linuxNativeReceiptIdentity receipt)
931 (linuxNativeReceiptTelemetry receipt))))
932
933def linuxCleanupFailureCount =
934 (lambda unrestricted telemetry : (family LinuxSyscallReceiptTelemetry) .
935 (eliminate
936 LinuxSyscallReceiptTelemetry
937 (lambda unrestricted current : (family LinuxSyscallReceiptTelemetry) . Nat)
938 telemetry
939 (branch
940 LinuxSyscallReceiptTelemetryValue
941 issued
942 completed
943 retries
944 requestedBytes
945 completedBytes
946 eof
947 cleanup
948 .
949 (eliminate
950 LinuxCleanupTelemetry
951 (lambda unrestricted current : (family LinuxCleanupTelemetry) . Nat)
952 cleanup
953 (branch
954 LinuxCleanupTelemetryValue
955 closeAttempts
956 closesCompleted
957 munmapAttempts
958 munmapsCompleted
959 unlinkAttempts
960 unlinksCompleted
961 syncAttempts
962 syncsCompleted
963 failures
964 firstErrno
965 hostFallbacks
966 .
967 failures)))))
968
969def linuxCleanupHostFallbackCount =
970 (lambda unrestricted telemetry : (family LinuxSyscallReceiptTelemetry) .
971 (eliminate
972 LinuxSyscallReceiptTelemetry
973 (lambda unrestricted current : (family LinuxSyscallReceiptTelemetry) . Nat)
974 telemetry
975 (branch
976 LinuxSyscallReceiptTelemetryValue
977 issued
978 completed
979 retries
980 requestedBytes
981 completedBytes
982 eof
983 cleanup
984 .
985 (eliminate
986 LinuxCleanupTelemetry
987 (lambda unrestricted current : (family LinuxCleanupTelemetry) . Nat)
988 cleanup
989 (branch
990 LinuxCleanupTelemetryValue
991 closeAttempts
992 closesCompleted
993 munmapAttempts
994 munmapsCompleted
995 unlinkAttempts
996 unlinksCompleted
997 syncAttempts
998 syncsCompleted
999 failures
1000 firstErrno
1001 hostFallbacks
1002 .
1003 hostFallbacks)))))
1004
1005def linuxFlagAnd =
1006 (lambda unrestricted left : Nat .
1007 (lambda unrestricted right : Nat .
1008 (nat-eliminate
1009 (lambda unrestricted current : Nat . Nat)
1010 zero
1011 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . right))
1012 left)))
1013
1014def linuxErrnoIsInterrupted =
1015 (lambda unrestricted errno : (family ModelWord32) .
1016 (eliminate
1017 ModelWord32
1018 (lambda unrestricted current : (family ModelWord32) . Nat)
1019 errno
1020 (branch
1021 ModelWord32Value
1022 b0
1023 b1
1024 b2
1025 b3
1026 .
1027 (linuxFlagAnd
1028 (byte-equal b0 (byte 4))
1029 (linuxFlagAnd
1030 (byte-equal b1 (byte 0))
1031 (linuxFlagAnd (byte-equal b2 (byte 0)) (byte-equal b3 (byte 0))))))))
1032
1033def linuxSuccessfulResponseKindRank =
1034 (lambda unrestricted kind : (family LinuxSuccessfulResponseKind) .
1035 (eliminate
1036 LinuxSuccessfulResponseKind
1037 (lambda unrestricted current : (family LinuxSuccessfulResponseKind) . Nat)
1038 kind
1039 (branch LinuxSuccessfulOpenKind . zero)
1040 (branch LinuxSuccessfulReadKind . (succ zero))
1041 (branch LinuxSuccessfulSeekKind . (succ (succ zero)))
1042 (branch LinuxSuccessfulWriteKind . (succ (succ (succ zero))))
1043 (branch LinuxSuccessfulIoctlKind . (succ (succ (succ (succ zero)))))
1044 (branch LinuxSuccessfulMmapKind . (succ (succ (succ (succ (succ zero))))))
1045 (branch LinuxSuccessfulUnitKind . (succ (succ (succ (succ (succ (succ zero)))))))))
1046
1047def linuxExpectedSuccessfulResponseKind =
1048 (lambda unrestricted request : (family LinuxSyscallRequest) .
1049 (eliminate
1050 LinuxSyscallRequest
1051 (lambda unrestricted current : (family LinuxSyscallRequest) .
1052 (family LinuxSuccessfulResponseKind))
1053 request
1054 (branch
1055 LinuxOpenAt
1056 directory
1057 path
1058 flags
1059 mode
1060 .
1061 (constructor LinuxSuccessfulResponseKind LinuxSuccessfulOpenKind))
1062 (branch
1063 LinuxRead
1064 descriptor
1065 requestedBytes
1066 .
1067 (constructor LinuxSuccessfulResponseKind LinuxSuccessfulReadKind))
1068 (branch
1069 LinuxSeek
1070 descriptor
1071 offset
1072 whence
1073 .
1074 (constructor LinuxSuccessfulResponseKind LinuxSuccessfulSeekKind))
1075 (branch
1076 LinuxWrite
1077 descriptor
1078 payload
1079 .
1080 (constructor LinuxSuccessfulResponseKind LinuxSuccessfulWriteKind))
1081 (branch
1082 LinuxClose
1083 descriptor
1084 .
1085 (constructor LinuxSuccessfulResponseKind LinuxSuccessfulUnitKind))
1086 (branch
1087 LinuxFsync
1088 descriptor
1089 .
1090 (constructor LinuxSuccessfulResponseKind LinuxSuccessfulUnitKind))
1091 (branch
1092 LinuxFdatasync
1093 descriptor
1094 .
1095 (constructor LinuxSuccessfulResponseKind LinuxSuccessfulUnitKind))
1096 (branch
1097 LinuxUnlinkAt
1098 directory
1099 path
1100 flags
1101 .
1102 (constructor LinuxSuccessfulResponseKind LinuxSuccessfulUnitKind))
1103 (branch
1104 LinuxRenameAt2
1105 sourceDirectory
1106 sourcePath
1107 destinationDirectory
1108 destinationPath
1109 flags
1110 .
1111 (constructor LinuxSuccessfulResponseKind LinuxSuccessfulUnitKind))
1112 (branch
1113 LinuxIoctl
1114 descriptor
1115 request
1116 payload
1117 .
1118 (constructor LinuxSuccessfulResponseKind LinuxSuccessfulIoctlKind))
1119 (branch
1120 LinuxMmap
1121 address
1122 extent
1123 protection
1124 flags
1125 descriptor
1126 offset
1127 .
1128 (constructor LinuxSuccessfulResponseKind LinuxSuccessfulMmapKind))
1129 (branch
1130 LinuxMunmap
1131 address
1132 extent
1133 .
1134 (constructor LinuxSuccessfulResponseKind LinuxSuccessfulUnitKind))))
1135
1136def linuxBaseRequestRetriesInterrupted =
1137 (lambda unrestricted request : (family LinuxSyscallRequest) .
1138 (eliminate
1139 LinuxSyscallRequest
1140 (lambda unrestricted current : (family LinuxSyscallRequest) . Nat)
1141 request
1142 (branch LinuxOpenAt directory path flags mode . (succ zero))
1143 (branch LinuxRead descriptor requestedBytes . (succ zero))
1144 (branch LinuxSeek descriptor offset whence . (succ zero))
1145 (branch LinuxWrite descriptor payload . (succ zero))
1146 -- close is never retried after EINTR: Linux may already have released fd.
1147 (branch LinuxClose descriptor . zero)
1148 (branch LinuxFsync descriptor . (succ zero))
1149 (branch LinuxFdatasync descriptor . (succ zero))
1150 -- Namespace mutation is not replayed after an indeterminate interruption.
1151 (branch LinuxUnlinkAt directory path flags . zero)
1152 (branch
1153 LinuxRenameAt2
1154 sourceDirectory
1155 sourcePath
1156 destinationDirectory
1157 destinationPath
1158 flags
1159 .
1160 zero)
1161 -- NVIDIA transport receipts carry bounded retry telemetry for ioctl.
1162 (branch LinuxIoctl descriptor ioctlRequest payload . (succ zero))
1163 (branch LinuxMmap address extent protection flags descriptor offset . zero)
1164 (branch LinuxMunmap address extent . zero)))
1165
1166def linuxExtendedRequestRetriesInterrupted =
1167 (lambda unrestricted request : (family LinuxExtendedSyscallRequest) .
1168 (eliminate
1169 LinuxExtendedSyscallRequest
1170 (lambda unrestricted current : (family LinuxExtendedSyscallRequest) . Nat)
1171 request
1172 (branch LinuxFstatRequest descriptor . (succ zero))
1173 (branch LinuxClockGettimeRequest clock . (succ zero))))
1174
1175def linuxRejectReceipt =
1176 (lambda unrestricted error : (family LinuxSyscallContractErrorCode) .
1177 (lambda unrestricted audit : (family LinuxSyscallReceiptAudit) .
1178 (constructor LinuxSyscallReceiptDecision LinuxSyscallReceiptRejected error audit)))
1179
1180def linuxAcceptBaseSuccess =
1181 (lambda unrestricted response : (family LinuxSyscallResponse) .
1182 (lambda unrestricted audit : (family LinuxSyscallReceiptAudit) .
1183 (nat-eliminate
1184 (lambda unrestricted current : Nat . (family LinuxSyscallReceiptDecision))
1185 (constructor LinuxSyscallReceiptDecision LinuxSyscallReceiptAcceptedBase response audit)
1186 (lambda unrestricted predecessor : Nat .
1187 (lambda unrestricted induction : (family LinuxSyscallReceiptDecision) .
1188 (linuxRejectReceipt
1189 (constructor LinuxSyscallContractErrorCode LinuxReceiptCleanupFailed)
1190 audit)))
1191 (linuxCleanupFailureCount
1192 (eliminate
1193 LinuxSyscallReceiptAudit
1194 (lambda unrestricted current : (family LinuxSyscallReceiptAudit) .
1195 (family LinuxSyscallReceiptTelemetry))
1196 audit
1197 (branch LinuxSyscallReceiptAuditValue expected actual telemetry . telemetry))))))
1198
1199def linuxAcceptExtendedSuccess =
1200 (lambda unrestricted response : (family LinuxExtendedSyscallResponse) .
1201 (lambda unrestricted audit : (family LinuxSyscallReceiptAudit) .
1202 (nat-eliminate
1203 (lambda unrestricted current : Nat . (family LinuxSyscallReceiptDecision))
1204 (constructor LinuxSyscallReceiptDecision LinuxSyscallReceiptAcceptedExtended response audit)
1205 (lambda unrestricted predecessor : Nat .
1206 (lambda unrestricted induction : (family LinuxSyscallReceiptDecision) .
1207 (linuxRejectReceipt
1208 (constructor LinuxSyscallContractErrorCode LinuxReceiptCleanupFailed)
1209 audit)))
1210 (linuxCleanupFailureCount
1211 (eliminate
1212 LinuxSyscallReceiptAudit
1213 (lambda unrestricted current : (family LinuxSyscallReceiptAudit) .
1214 (family LinuxSyscallReceiptTelemetry))
1215 audit
1216 (branch LinuxSyscallReceiptAuditValue expected actual telemetry . telemetry))))))
1217
1218def linuxAcceptBaseSuccessfulKind =
1219 (lambda unrestricted request : (family LinuxSyscallRequest) .
1220 (lambda unrestricted response : (family LinuxSyscallResponse) .
1221 (lambda unrestricted observed : (family LinuxSuccessfulResponseKind) .
1222 (lambda unrestricted audit : (family LinuxSyscallReceiptAudit) .
1223 (nat-eliminate
1224 (lambda unrestricted current : Nat . (family LinuxSyscallReceiptDecision))
1225 (linuxRejectReceipt
1226 (constructor LinuxSyscallContractErrorCode LinuxReceiptResponseKindMismatch)
1227 audit)
1228 (lambda unrestricted predecessor : Nat .
1229 (lambda unrestricted induction : (family LinuxSyscallReceiptDecision) .
1230 (linuxAcceptBaseSuccess response audit)))
1231 (naturalEqual
1232 (linuxSuccessfulResponseKindRank (linuxExpectedSuccessfulResponseKind request))
1233 (linuxSuccessfulResponseKindRank observed)))))))
1234
1235def linuxAcceptBaseResponse =
1236 (lambda unrestricted invocation : (family LinuxNativeSyscallInvocation) .
1237 (lambda unrestricted request : (family LinuxSyscallRequest) .
1238 (lambda unrestricted response : (family LinuxSyscallResponse) .
1239 (lambda unrestricted audit : (family LinuxSyscallReceiptAudit) .
1240 (eliminate
1241 LinuxSyscallResponse
1242 (lambda unrestricted current : (family LinuxSyscallResponse) .
1243 (family LinuxSyscallReceiptDecision))
1244 response
1245 (branch
1246 LinuxOpenSucceeded
1247 descriptor
1248 .
1249 (linuxAcceptBaseSuccessfulKind
1250 request
1251 response
1252 (constructor LinuxSuccessfulResponseKind LinuxSuccessfulOpenKind)
1253 audit))
1254 (branch
1255 LinuxReadSucceeded
1256 bytes
1257 .
1258 (linuxAcceptBaseSuccessfulKind
1259 request
1260 response
1261 (constructor LinuxSuccessfulResponseKind LinuxSuccessfulReadKind)
1262 audit))
1263 (branch
1264 LinuxSeekSucceeded
1265 position
1266 .
1267 (linuxAcceptBaseSuccessfulKind
1268 request
1269 response
1270 (constructor LinuxSuccessfulResponseKind LinuxSuccessfulSeekKind)
1271 audit))
1272 (branch
1273 LinuxWriteSucceeded
1274 written
1275 .
1276 (linuxAcceptBaseSuccessfulKind
1277 request
1278 response
1279 (constructor LinuxSuccessfulResponseKind LinuxSuccessfulWriteKind)
1280 audit))
1281 (branch
1282 LinuxIoctlSucceeded
1283 output
1284 .
1285 (linuxAcceptBaseSuccessfulKind
1286 request
1287 response
1288 (constructor LinuxSuccessfulResponseKind LinuxSuccessfulIoctlKind)
1289 audit))
1290 (branch
1291 LinuxMmapSucceeded
1292 address
1293 .
1294 (linuxAcceptBaseSuccessfulKind
1295 request
1296 response
1297 (constructor LinuxSuccessfulResponseKind LinuxSuccessfulMmapKind)
1298 audit))
1299 (branch
1300 LinuxUnitSucceeded
1301 .
1302 (linuxAcceptBaseSuccessfulKind
1303 request
1304 response
1305 (constructor LinuxSuccessfulResponseKind LinuxSuccessfulUnitKind)
1306 audit))
1307 (branch
1308 LinuxSyscallFailed
1309 error
1310 errno
1311 .
1312 (nat-eliminate
1313 (lambda unrestricted current : Nat . (family LinuxSyscallReceiptDecision))
1314 (constructor
1315 LinuxSyscallReceiptDecision
1316 LinuxSyscallReceiptFailed
1317 error
1318 errno
1319 audit)
1320 (lambda unrestricted interruptedPredecessor : Nat .
1321 (lambda unrestricted ignoredInterrupted : (family LinuxSyscallReceiptDecision) .
1322 (nat-eliminate
1323 (lambda unrestricted current : Nat . (family LinuxSyscallReceiptDecision))
1324 (constructor
1325 LinuxSyscallReceiptDecision
1326 LinuxSyscallReceiptFailed
1327 error
1328 errno
1329 audit)
1330 (lambda unrestricted retryPredecessor : Nat .
1331 (lambda unrestricted ignoredRetry : (family LinuxSyscallReceiptDecision) .
1332 (constructor
1333 LinuxSyscallReceiptDecision
1334 LinuxSyscallReceiptRetryInterrupted
1335 invocation
1336 audit)))
1337 (linuxBaseRequestRetriesInterrupted request))))
1338 (linuxErrnoIsInterrupted errno))))))))
1339
1340def linuxAcceptExtendedResponse =
1341 (lambda unrestricted invocation : (family LinuxNativeSyscallInvocation) .
1342 (lambda unrestricted request : (family LinuxExtendedSyscallRequest) .
1343 (lambda unrestricted response : (family LinuxExtendedSyscallResponse) .
1344 (lambda unrestricted audit : (family LinuxSyscallReceiptAudit) .
1345 (eliminate
1346 LinuxExtendedSyscallRequest
1347 (lambda unrestricted current : (family LinuxExtendedSyscallRequest) .
1348 (family LinuxSyscallReceiptDecision))
1349 request
1350 (branch
1351 LinuxFstatRequest
1352 descriptor
1353 .
1354 (eliminate
1355 LinuxExtendedSyscallResponse
1356 (lambda unrestricted current : (family LinuxExtendedSyscallResponse) .
1357 (family LinuxSyscallReceiptDecision))
1358 response
1359 (branch LinuxFstatSucceeded status . (linuxAcceptExtendedSuccess response audit))
1360 (branch
1361 LinuxClockGettimeSucceeded
1362 timestamp
1363 .
1364 (linuxRejectReceipt
1365 (constructor LinuxSyscallContractErrorCode LinuxReceiptExtendedKindMismatch)
1366 audit))
1367 (branch
1368 LinuxExtendedSyscallFailed
1369 error
1370 errno
1371 .
1372 (nat-eliminate
1373 (lambda unrestricted current : Nat . (family LinuxSyscallReceiptDecision))
1374 (constructor
1375 LinuxSyscallReceiptDecision
1376 LinuxSyscallReceiptFailed
1377 error
1378 errno
1379 audit)
1380 (lambda unrestricted interruptedPredecessor : Nat .
1381 (lambda unrestricted ignoredInterrupted : (family LinuxSyscallReceiptDecision) .
1382 (constructor
1383 LinuxSyscallReceiptDecision
1384 LinuxSyscallReceiptRetryInterrupted
1385 invocation
1386 audit)))
1387 (linuxErrnoIsInterrupted errno)))))
1388 (branch
1389 LinuxClockGettimeRequest
1390 clock
1391 .
1392 (eliminate
1393 LinuxExtendedSyscallResponse
1394 (lambda unrestricted current : (family LinuxExtendedSyscallResponse) .
1395 (family LinuxSyscallReceiptDecision))
1396 response
1397 (branch
1398 LinuxFstatSucceeded
1399 status
1400 .
1401 (linuxRejectReceipt
1402 (constructor LinuxSyscallContractErrorCode LinuxReceiptExtendedKindMismatch)
1403 audit))
1404 (branch
1405 LinuxClockGettimeSucceeded
1406 timestamp
1407 .
1408 (linuxAcceptExtendedSuccess response audit))
1409 (branch
1410 LinuxExtendedSyscallFailed
1411 error
1412 errno
1413 .
1414 (nat-eliminate
1415 (lambda unrestricted current : Nat . (family LinuxSyscallReceiptDecision))
1416 (constructor
1417 LinuxSyscallReceiptDecision
1418 LinuxSyscallReceiptFailed
1419 error
1420 errno
1421 audit)
1422 (lambda unrestricted interruptedPredecessor : Nat .
1423 (lambda unrestricted ignoredInterrupted : (family LinuxSyscallReceiptDecision) .
1424 (constructor
1425 LinuxSyscallReceiptDecision
1426 LinuxSyscallReceiptRetryInterrupted
1427 invocation
1428 audit)))
1429 (linuxErrnoIsInterrupted errno))))))))))
1430
1431def linuxAcceptIdentityMatchedReceipt =
1432 (lambda unrestricted invocation : (family LinuxNativeSyscallInvocation) .
1433 (lambda unrestricted receipt : (family LinuxNativeSyscallReceipt) .
1434 (eliminate
1435 LinuxNativeSyscallInvocation
1436 (lambda unrestricted current : (family LinuxNativeSyscallInvocation) .
1437 (family LinuxSyscallReceiptDecision))
1438 invocation
1439 (branch
1440 LinuxNativeBaseInvocation
1441 identity
1442 request
1443 .
1444 (eliminate
1445 LinuxNativeSyscallReceipt
1446 (lambda unrestricted current : (family LinuxNativeSyscallReceipt) .
1447 (family LinuxSyscallReceiptDecision))
1448 receipt
1449 (branch
1450 LinuxNativeBaseReceipt
1451 actual
1452 response
1453 telemetry
1454 .
1455 (linuxAcceptBaseResponse
1456 invocation
1457 request
1458 response
1459 (linuxReceiptAudit invocation receipt)))
1460 (branch
1461 LinuxNativeExtendedReceipt
1462 actual
1463 response
1464 telemetry
1465 .
1466 (linuxRejectReceipt
1467 (constructor LinuxSyscallContractErrorCode LinuxReceiptResponseKindMismatch)
1468 (linuxReceiptAudit invocation receipt)))))
1469 (branch
1470 LinuxNativeExtendedInvocation
1471 identity
1472 request
1473 .
1474 (eliminate
1475 LinuxNativeSyscallReceipt
1476 (lambda unrestricted current : (family LinuxNativeSyscallReceipt) .
1477 (family LinuxSyscallReceiptDecision))
1478 receipt
1479 (branch
1480 LinuxNativeBaseReceipt
1481 actual
1482 response
1483 telemetry
1484 .
1485 (linuxRejectReceipt
1486 (constructor LinuxSyscallContractErrorCode LinuxReceiptResponseKindMismatch)
1487 (linuxReceiptAudit invocation receipt)))
1488 (branch
1489 LinuxNativeExtendedReceipt
1490 actual
1491 response
1492 telemetry
1493 .
1494 (linuxAcceptExtendedResponse
1495 invocation
1496 request
1497 response
1498 (linuxReceiptAudit invocation receipt))))))))
1499
1500def linuxAcceptNativeSyscallReceipt =
1501 (lambda unrestricted invocation : (family LinuxNativeSyscallInvocation) .
1502 (lambda unrestricted receipt : (family LinuxNativeSyscallReceipt) .
1503 (nat-eliminate
1504 (lambda unrestricted current : Nat . (family LinuxSyscallReceiptDecision))
1505 (linuxRejectReceipt
1506 (constructor LinuxSyscallContractErrorCode LinuxReceiptIdentityMismatch)
1507 (linuxReceiptAudit invocation receipt))
1508 (lambda unrestricted identityPredecessor : Nat .
1509 (lambda unrestricted ignoredIdentity : (family LinuxSyscallReceiptDecision) .
1510 (nat-eliminate
1511 (lambda unrestricted current : Nat . (family LinuxSyscallReceiptDecision))
1512 (linuxAcceptIdentityMatchedReceipt invocation receipt)
1513 (lambda unrestricted fallbackPredecessor : Nat .
1514 (lambda unrestricted ignoredFallback : (family LinuxSyscallReceiptDecision) .
1515 (linuxRejectReceipt
1516 (constructor LinuxSyscallContractErrorCode LinuxReceiptHostFallbackRejected)
1517 (linuxReceiptAudit invocation receipt))))
1518 (linuxCleanupHostFallbackCount (linuxNativeReceiptTelemetry receipt)))))
1519 (linuxIdentityEqual
1520 (linuxNativeInvocationIdentity invocation)
1521 (linuxNativeReceiptIdentity receipt)))))
1522
1523def linuxExactIOKindRank =
1524 (lambda unrestricted kind : (family LinuxExactIOKind) .
1525 (eliminate
1526 LinuxExactIOKind
1527 (lambda unrestricted current : (family LinuxExactIOKind) . Nat)
1528 kind
1529 (branch LinuxExactReadKind . zero)
1530 (branch LinuxExactWriteKind . (succ zero))))
1531
1532def linuxRejectExactIO =
1533 (lambda unrestricted error : (family LinuxSyscallContractErrorCode) .
1534 (lambda unrestricted expected : (family ModelWord64) .
1535 (lambda unrestricted actual : (family ModelWord64) .
1536 (lambda unrestricted telemetry : (family LinuxSyscallReceiptTelemetry) .
1537 (constructor LinuxExactIOValidation LinuxExactIORejected error expected actual telemetry)))))
1538
1539def linuxExactIOShortError =
1540 (lambda unrestricted kind : (family LinuxExactIOKind) .
1541 (lambda unrestricted telemetry : (family LinuxSyscallReceiptTelemetry) .
1542 (eliminate
1543 LinuxExactIOKind
1544 (lambda unrestricted current : (family LinuxExactIOKind) .
1545 (family LinuxSyscallContractErrorCode))
1546 kind
1547 (branch
1548 LinuxExactReadKind
1549 .
1550 (eliminate
1551 LinuxSyscallReceiptTelemetry
1552 (lambda unrestricted current : (family LinuxSyscallReceiptTelemetry) .
1553 (family LinuxSyscallContractErrorCode))
1554 telemetry
1555 (branch
1556 LinuxSyscallReceiptTelemetryValue
1557 issued
1558 completed
1559 retries
1560 requestedBytes
1561 completedBytes
1562 eof
1563 cleanup
1564 .
1565 (nat-eliminate
1566 (lambda unrestricted current : Nat . (family LinuxSyscallContractErrorCode))
1567 (constructor LinuxSyscallContractErrorCode LinuxReceiptExactReadShort)
1568 (lambda unrestricted predecessor : Nat .
1569 (lambda unrestricted induction : (family LinuxSyscallContractErrorCode) .
1570 (constructor LinuxSyscallContractErrorCode LinuxReceiptUnexpectedEOF)))
1571 eof))))
1572 (branch
1573 LinuxExactWriteKind
1574 .
1575 (constructor LinuxSyscallContractErrorCode LinuxReceiptExactWriteShort)))))
1576
1577def linuxValidateExactIOReceipt =
1578 (lambda unrestricted plan : (family LinuxExactIOPlan) .
1579 (lambda unrestricted receipt : (family LinuxExactIOReceipt) .
1580 (eliminate
1581 LinuxExactIOPlan
1582 (lambda unrestricted current : (family LinuxExactIOPlan) . (family LinuxExactIOValidation))
1583 plan
1584 (branch
1585 LinuxExactIOPlanValue
1586 expectedIdentity
1587 expectedKind
1588 descriptor
1589 expected
1590 maximumChunk
1591 .
1592 (eliminate
1593 LinuxExactIOReceipt
1594 (lambda unrestricted current : (family LinuxExactIOReceipt) .
1595 (family LinuxExactIOValidation))
1596 receipt
1597 (branch
1598 LinuxExactIOReceiptValue
1599 actualIdentity
1600 actualKind
1601 actual
1602 telemetry
1603 .
1604 (nat-eliminate
1605 (lambda unrestricted current : Nat . (family LinuxExactIOValidation))
1606 (linuxRejectExactIO
1607 (constructor LinuxSyscallContractErrorCode LinuxReceiptIdentityMismatch)
1608 expected
1609 actual
1610 telemetry)
1611 (lambda unrestricted identityPredecessor : Nat .
1612 (lambda unrestricted ignoredIdentity : (family LinuxExactIOValidation) .
1613 (nat-eliminate
1614 (lambda unrestricted current : Nat . (family LinuxExactIOValidation))
1615 (linuxRejectExactIO
1616 (constructor LinuxSyscallContractErrorCode LinuxReceiptExactIOPlanMismatch)
1617 expected
1618 actual
1619 telemetry)
1620 (lambda unrestricted kindPredecessor : Nat .
1621 (lambda unrestricted ignoredKind : (family LinuxExactIOValidation) .
1622 (nat-eliminate
1623 (lambda unrestricted current : Nat . (family LinuxExactIOValidation))
1624 (linuxRejectExactIO
1625 (linuxExactIOShortError expectedKind telemetry)
1626 expected
1627 actual
1628 telemetry)
1629 (lambda unrestricted extentPredecessor : Nat .
1630 (lambda unrestricted ignoredExtent : (family LinuxExactIOValidation) .
1631 (nat-eliminate
1632 (lambda unrestricted current : Nat .
1633 (family LinuxExactIOValidation))
1634 (nat-eliminate
1635 (lambda unrestricted current : Nat .
1636 (family LinuxExactIOValidation))
1637 (constructor
1638 LinuxExactIOValidation
1639 LinuxExactIOAccepted
1640 receipt)
1641 (lambda unrestricted cleanupPredecessor : Nat .
1642 (lambda unrestricted ignoredCleanup : (family LinuxExactIOValidation) .
1643 (linuxRejectExactIO
1644 (constructor
1645 LinuxSyscallContractErrorCode
1646 LinuxReceiptCleanupFailed)
1647 expected
1648 actual
1649 telemetry)))
1650 (linuxCleanupFailureCount telemetry))
1651 (lambda unrestricted fallbackPredecessor : Nat .
1652 (lambda unrestricted ignoredFallback : (family LinuxExactIOValidation) .
1653 (linuxRejectExactIO
1654 (constructor
1655 LinuxSyscallContractErrorCode
1656 LinuxReceiptHostFallbackRejected)
1657 expected
1658 actual
1659 telemetry)))
1660 (linuxCleanupHostFallbackCount telemetry))))
1661 (modelWord64Equal expected actual))))
1662 (naturalEqual
1663 (linuxExactIOKindRank expectedKind)
1664 (linuxExactIOKindRank actualKind)))))
1665 (linuxIdentityEqual expectedIdentity actualIdentity))))))))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.