1197def nativePhysicalValidateProgram =
1198 (lambda unrestricted program : (family NativePhysicalProgram) .
1199 (eliminate
1200 NativePhysicalProgram
1201 (lambda unrestricted current : (family NativePhysicalProgram) .
1202 (family NativePhysicalProgramValidation))
1203 program
1204 (branch
1205 NativePhysicalProgramValue
1206 stateExtent
1207 resultSlots
1208 commands
1209 expected
1210 identity
1211 fallbacks
1212 .
1213 (nat-eliminate
1214 (lambda unrestricted current : Nat . (family NativePhysicalProgramValidation))
1215 (nativePhysicalReject
1216 program
1217 (constructor NativePhysicalErrorCode NativePhysicalIdentityInvalid)
1218 zero)
1219 (lambda unrestricted identityPredecessor : Nat .
1220 (lambda unrestricted ignoredIdentity : (family NativePhysicalProgramValidation) .
1221 (nat-eliminate
1222 (lambda unrestricted current : Nat . (family NativePhysicalProgramValidation))
1223 (nativePhysicalReject
1224 program
1225 (constructor NativePhysicalErrorCode NativePhysicalFallbackObserved)
1226 zero)
1227 (lambda unrestricted fallbackPredecessor : Nat .
1228 (lambda unrestricted ignoredFallback : (family NativePhysicalProgramValidation) .
1229 (nat-eliminate
1230 (lambda unrestricted current : Nat . (family NativePhysicalProgramValidation))
1231 (eliminate
1232 NativePhysicalCommandsValidation
1233 (lambda unrestricted current : (family NativePhysicalCommandsValidation) .
1234 (family NativePhysicalProgramValidation))
1235 (nat-eliminate
1236 (lambda unrestricted current : Nat .
1237 (family NativePhysicalCommandsValidation))
1238 (nativePhysicalValidateCommands commands)
1239 (lambda unrestricted predecessor : Nat .
1240 (lambda unrestricted ignoredBalance : (family NativePhysicalCommandsValidation) .
1241 (constructor
1242 NativePhysicalCommandsValidation
1243 NativePhysicalCommandsInvalid
1244 (constructor NativePhysicalErrorCode NativePhysicalRepeatUnbalanced)
1245 zero)))
1246 (nativePhysicalRepeatBalance commands))
1247 (branch
1248 NativePhysicalCommandsValid
1249 completed
1250 .
1251 (nat-eliminate
1252 (lambda unrestricted current : Nat .
1253 (family NativePhysicalProgramValidation))
1254 (nativePhysicalReject
1255 program
1256 (constructor
1257 NativePhysicalErrorCode
1258 NativePhysicalCommandCountMismatch)
1259 zero)
1260 (lambda unrestricted countPredecessor : Nat .
1261 (lambda unrestricted ignoredCount : (family NativePhysicalProgramValidation) .
1262 (nat-eliminate
1263 (lambda unrestricted valid : Nat .
1264 (family NativePhysicalProgramValidation))
1265 (nativePhysicalReject
1266 program
1267 (constructor
1268 NativePhysicalErrorCode
1269 NativePhysicalMemoryExtentInvalid)
1270 zero)
1271 (lambda unrestricted previous : Nat .
1272 (lambda unrestricted ignored : (family NativePhysicalProgramValidation) .
1273 (constructor
1274 NativePhysicalProgramValidation
1275 NativePhysicalProgramValidated
1276 program
1277 (nativePhysicalValidationTelemetryFor program zero zero b""))))
1278 (nativePhysicalMemoryAdmitted
1279 (modelWord64Natural stateExtent)
1280 (modelWord64Natural resultSlots)))))
1281 (naturalEqual completed expected)))
1282 (branch
1283 NativePhysicalCommandsInvalid
1284 error
1285 ordinal
1286 .
1287 (nativePhysicalReject program error ordinal)))
1288 (lambda unrestricted statePredecessor : Nat .
1289 (lambda unrestricted ignoredState : (family NativePhysicalProgramValidation) .
1290 (nativePhysicalReject
1291 program
1292 (constructor NativePhysicalErrorCode NativePhysicalStateExtentZero)
1293 zero)))
1294 (modelWord64IsZero stateExtent))))
1295 (naturalEqual fallbacks zero))))
1296 (naturalEqual (bytes-length identity) (byte-to-nat (byte 64)))))))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.