Runtime.TextArtifactRequest

1module Runtime.TextArtifactRequest
2
3import Data.Bytes
4import Model.Word64
5import Std.Natural
6
7-- One request record drives both operations of every R6 text artifact.  The
8-- native host consumes exactly one path argument naming this record; no
9-- working-directory convention or positional train-only ABI is involved.
10family TextArtifactOperation : Type 0
11constructor TextArtifactTrain
12constructor TextArtifactPredict
13
14end-family
15
16family TextArtifactRequest : Type 0
17constructor TextArtifactRequestValue
18field unrestricted textArtifactOperation : (family TextArtifactOperation)
19field unrestricted textArtifactInputPath : Bytes
20field unrestricted textArtifactCheckpointInputPath : Bytes
21field unrestricted textArtifactCheckpointOutputPath : Bytes
22field unrestricted textArtifactPredictionsOutputPath : Bytes
23field unrestricted textArtifactResultOutputPath : Bytes
24field unrestricted textArtifactCheckpointTemporaryPath : Bytes
25field unrestricted textArtifactCheckpointDirectoryPath : Bytes
26
27end-family
28
29def textArtifactRequestMagic : Bytes =
30  b"ALPHATX1"
31
32-- Version 2 adds the checkpoint's temporary path and its directory: the
33-- host writes the checkpoint to the temporary, then renames it over the
34-- output path and syncs the directory (Checkpoint.Envelope's publication).
35def textArtifactRequestVersion : Nat =
36  2
37
38-- The operation is deliberately represented by a harmless Linux syscall
39-- number.  After the shared prediction prefix, getpid returns and training
40-- continues; exit_group(0) terminates a predict request before the optimizer.
41-- This keeps one static ELF and one native command stream without introducing
42-- a second host interpreter or CPU-learning branch.
43def textArtifactTrainOperationWord : Nat =
44  39
45
46def textArtifactPredictOperationWord : Nat =
47  231
48
49def textArtifactPathExtent : Nat =
50  256
51
52def textArtifactPathMaximumLength : Nat =
53  255
54
55def textArtifactRequestPaths : Nat =
56  7
57
58-- magic[8] + version:u64 + operation:u64 + seven NUL-padded paths[256].
59def textArtifactRequestEncodedLength : Nat =
60  (naturalAdd 24 (naturalMultiply textArtifactRequestPaths textArtifactPathExtent))
61
62def textArtifactZeroBytes =
63  (lambda unrestricted count : Nat .
64    (dataBytesRepeatByte (byte 0) count))
65
66def textArtifactOperationWord =
67  (lambda unrestricted operation : (family TextArtifactOperation) .
68    (eliminate
69      TextArtifactOperation
70      (lambda unrestricted current : (family TextArtifactOperation) . Nat)
71      operation
72      (branch TextArtifactTrain . textArtifactTrainOperationWord)
73      (branch TextArtifactPredict . textArtifactPredictOperationWord)))
74
75def textArtifactPathValid =
76  (lambda unrestricted path : Bytes .
77    (naturalAnd
78      (naturalNonzero (bytes-length path))
79      (naturalLessOrEqual (bytes-length path) textArtifactPathMaximumLength)))
80
81def textArtifactEncodePath =
82  (lambda unrestricted path : Bytes .
83    (bytes-append
84      path
85      (textArtifactZeroBytes
86        (naturalSaturatingSubtract textArtifactPathExtent (bytes-length path)))))
87
88def textArtifactRequestFieldsValid =
89  (lambda unrestricted request : (family TextArtifactRequest) .
90    (eliminate
91      TextArtifactRequest
92      (lambda unrestricted current : (family TextArtifactRequest) . Nat)
93      request
94      (branch
95        TextArtifactRequestValue
96        operation
97        input
98        checkpointInput
99        checkpointOutput
100        predictionsOutput
101        resultOutput
102        checkpointTemporary
103        checkpointDirectory
104        .
105        (naturalAnd
106          (textArtifactPathValid input)
107          (naturalAnd
108            (textArtifactPathValid checkpointInput)
109            (naturalAnd
110              (textArtifactPathValid checkpointOutput)
111              (naturalAnd
112                (textArtifactPathValid predictionsOutput)
113                (naturalAnd
114                  (textArtifactPathValid resultOutput)
115                  (naturalAnd
116                    (textArtifactPathValid checkpointTemporary)
117                    (textArtifactPathValid checkpointDirectory))))))))))
118
119def textArtifactRequestEncodeUnchecked =
120  (lambda unrestricted request : (family TextArtifactRequest) .
121    (eliminate
122      TextArtifactRequest
123      (lambda unrestricted current : (family TextArtifactRequest) . Bytes)
124      request
125      (branch
126        TextArtifactRequestValue
127        operation
128        input
129        checkpointInput
130        checkpointOutput
131        predictionsOutput
132        resultOutput
133        checkpointTemporary
134        checkpointDirectory
135        .
136        (bytes-append
137          textArtifactRequestMagic
138          (bytes-append
139            (dataBytesWord64LE (modelWord64FromNaturalTruncated textArtifactRequestVersion))
140            (bytes-append
141              (dataBytesWord64LE
142                (modelWord64FromNaturalTruncated (textArtifactOperationWord operation)))
143              (bytes-append
144                (textArtifactEncodePath input)
145                (bytes-append
146                  (textArtifactEncodePath checkpointInput)
147                  (bytes-append
148                    (textArtifactEncodePath checkpointOutput)
149                    (bytes-append
150                      (textArtifactEncodePath predictionsOutput)
151                      (bytes-append
152                        (textArtifactEncodePath resultOutput)
153                        (bytes-append
154                          (textArtifactEncodePath checkpointTemporary)
155                          (textArtifactEncodePath checkpointDirectory)))))))))))))
156
157-- Invalid requests have no wire representation.  This makes the encoder
158-- fail-closed while keeping construction and static evaluation lightweight.
159def textArtifactRequestEncode =
160  (lambda unrestricted request : (family TextArtifactRequest) .
161    (nat-eliminate
162      (lambda unrestricted current : Nat . Bytes)
163      b""
164      (lambda unrestricted predecessor : Nat .
165        (lambda unrestricted induction : Bytes .
166          (textArtifactRequestEncodeUnchecked request)))
167      (textArtifactRequestFieldsValid request)))
168
169def textArtifactEncodedFieldTerminated =
170  (lambda unrestricted offset : Nat .
171    (lambda unrestricted raw : Bytes .
172      (naturalAnd
173        (naturalNonzero
174          (byte-to-nat (dataBytesByteAtValidated raw offset)))
175        (naturalIsZero
176          (byte-to-nat
177            (dataBytesByteAtValidated
178              raw
179              (naturalAdd offset textArtifactPathMaximumLength)))))))
180
181-- Native hosts perform these same checks before opening any supplied path.
182-- Path fields must begin non-NUL and terminate inside their fixed extent.
183def textArtifactRequestBytesValid =
184  (lambda unrestricted raw : Bytes .
185    (naturalAnd
186      (naturalEqual (bytes-length raw) textArtifactRequestEncodedLength)
187      (naturalAnd
188        (bytes-equal (dataBytesTakeValidated 8 raw) textArtifactRequestMagic)
189        (naturalAnd
190          (bytes-equal
191            (dataBytesTakeValidated 8 (dataBytesDropValidated 8 raw))
192            (dataBytesWord64LE
193              (modelWord64FromNaturalTruncated textArtifactRequestVersion)))
194          (naturalAnd
195            (naturalOr
196              (bytes-equal
197                (dataBytesTakeValidated 8 (dataBytesDropValidated 16 raw))
198                (dataBytesWord64LE
199                  (modelWord64FromNaturalTruncated textArtifactTrainOperationWord)))
200              (bytes-equal
201                (dataBytesTakeValidated 8 (dataBytesDropValidated 16 raw))
202                (dataBytesWord64LE
203                  (modelWord64FromNaturalTruncated textArtifactPredictOperationWord))))
204            (naturalAnd
205              (textArtifactEncodedFieldTerminated 24 raw)
206              (naturalAnd
207                (textArtifactEncodedFieldTerminated 280 raw)
208                (naturalAnd
209                  (textArtifactEncodedFieldTerminated 536 raw)
210                  (naturalAnd
211                    (textArtifactEncodedFieldTerminated 792 raw)
212                    (naturalAnd
213                      (textArtifactEncodedFieldTerminated 1048 raw)
214                      (naturalAnd
215                        (textArtifactEncodedFieldTerminated 1304 raw)
216                        (textArtifactEncodedFieldTerminated 1560 raw))))))))))))