Encode one command whose record begins at body offset `offset`, given the
routine code already held, and the code held after it.
1173def nativePhysicalImageEncodeShared =
1174 (lambda unrestricted format : (family NativePhysicalImageFormat) .
1175 (lambda unrestricted offset : Nat .
1176 (lambda unrestricted held : (family StdList (family NativePhysicalImageRoutineCode)) .
1177 (lambda unrestricted operation : (family NativePhysicalOperation) .
1178 (lambda unrestricted errorIdentity : Bytes .
1179 (eliminate
1180 NativePhysicalOperation
1181 (lambda unrestricted current : (family NativePhysicalOperation) .
1182 (family NativePhysicalImageSharedEncoding))
1183 operation
1184 (branch NativePhysicalSystemCall number arguments payload result .
1185 (nativePhysicalImageSharedPlain format held operation errorIdentity))
1186 (branch NativePhysicalCopyPayloadToState destination extent payload .
1187 (nativePhysicalImageSharedPlain format held operation errorIdentity))
1188 (branch
1189 NativePhysicalMachineRoutine
1190 code
1191 arguments
1192 result
1193 .
1194 (app
1195 (lambda unrestricted at : Nat .
1196 (app
1197 (lambda unrestricted here : Nat .
1198 (nat-eliminate
1199 (lambda unrestricted current : Nat . (family NativePhysicalImageSharedEncoding))
1200 (constructor
1201 NativePhysicalImageSharedEncoding
1202 NativePhysicalImageSharedEncodingValue
1203 (nativePhysicalImageEncodeOperationForFormat format operation errorIdentity)
1204 (nat-eliminate
1205 (lambda unrestricted current : Nat .
1206 (family StdList (family NativePhysicalImageRoutineCode)))
1207 (constructor
1208 StdList
1209 StdListCons
1210 (family NativePhysicalImageRoutineCode)
1211 (constructor
1212 NativePhysicalImageRoutineCode
1213 NativePhysicalImageRoutineCodeValue
1214 code
1215 here)
1216 held)
1217 (lambda unrestricted predecessor : Nat .
1218 (lambda unrestricted ignored : (family StdList (family NativePhysicalImageRoutineCode)) .
1219 held))
1220 at))
1221 (lambda unrestricted predecessor : Nat .
1222 (lambda unrestricted ignored : (family NativePhysicalImageSharedEncoding) .
1223 (constructor
1224 NativePhysicalImageSharedEncoding
1225 NativePhysicalImageSharedEncodingValue
1226 (nativePhysicalImageEncodeOperationForFormat
1227 format
1228 (constructor
1229 NativePhysicalOperation
1230 NativePhysicalMachineRoutine
1231 (nativePhysicalImageRoutineBranch format at here)
1232 arguments
1233 result)
1234 errorIdentity)
1235 held)))
1236 (naturalAnd
1237 (naturalLess zero at)
1238 (naturalAnd
1239 (naturalIsZero (nativePhysicalImageArgumentsReadPayload arguments))
1240 (naturalLess
1241 (nativePhysicalImageRoutineBranchBytes format)
1242 (bytes-length code))))))
1243 (naturalAdd offset (nativePhysicalImageRoutineCodeOffset format arguments))))
1244 (nativePhysicalImageHeldRoutineAt code held)))
1245 (branch NativePhysicalFencePoll address expected polls .
1246 (nativePhysicalImageSharedPlain format held operation errorIdentity))
1247 (branch NativePhysicalTelemetryAppend path record .
1248 (nativePhysicalImageSharedPlain format held operation errorIdentity))
1249 (branch NativePhysicalAssertEqual left right error .
1250 (nativePhysicalImageSharedPlain format held operation errorIdentity))
1251 (branch NativePhysicalAssertOneOf observed first second error .
1252 (nativePhysicalImageSharedPlain format held operation errorIdentity))
1253 (branch NativePhysicalHaltSuccess .
1254 (nativePhysicalImageSharedPlain format held operation errorIdentity))
1255 (branch NativePhysicalRepeatBegin count .
1256 (nativePhysicalImageSharedPlain format held operation errorIdentity))
1257 (branch NativePhysicalSkipUnlessEqual left right count .
1258 (nativePhysicalImageSharedPlain format held operation errorIdentity))
1259 (branch NativePhysicalRepeatEnd .
1260 (nativePhysicalImageSharedPlain format held operation errorIdentity))
1261 (branch NativePhysicalRepeatEndWhen observed expected .
1262 (nativePhysicalImageSharedPlain format held operation errorIdentity))
1263 (branch NativePhysicalStoreWord64 destination value .
1264 (nativePhysicalImageSharedPlain format held operation errorIdentity))
1265 (branch NativePhysicalFenceWait address expected polls interval .
1266 (nativePhysicalImageSharedPlain format held operation errorIdentity))
1267 (branch NativePhysicalRepeatBeginCounted count .
1268 (nativePhysicalImageSharedPlain format held operation errorIdentity))
1269 (branch NativePhysicalAddWord64 destination left right .
1270 (nativePhysicalImageSharedPlain format held operation errorIdentity))
1271 (branch NativePhysicalFloat64 kind destination left right .
1272 (nativePhysicalImageSharedPlain format held operation errorIdentity))))))))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.