1329def nativePhysicalValidateProgram =
1330 (lambda unrestricted program : (family NativePhysicalProgram) .
1331 (eliminate
1332 NativePhysicalProgram
1333 (lambda unrestricted current : (family NativePhysicalProgram) .
1334 (family NativePhysicalProgramValidation))
1335 program
1336 (branch
1337 NativePhysicalProgramValue
1338 stateExtent
1339 resultSlots
1340 commands
1341 expected
1342 identity
1343 fallbacks
1344 .
1345 (nat-eliminate
1346 (lambda unrestricted current : Nat . (family NativePhysicalProgramValidation))
1347 (nativePhysicalReject
1348 program
1349 (constructor NativePhysicalErrorCode NativePhysicalIdentityInvalid)
1350 zero)
1351 (lambda unrestricted identityPredecessor : Nat .
1352 (lambda unrestricted ignoredIdentity : (family NativePhysicalProgramValidation) .
1353 (nat-eliminate
1354 (lambda unrestricted current : Nat . (family NativePhysicalProgramValidation))
1355 (nativePhysicalReject
1356 program
1357 (constructor NativePhysicalErrorCode NativePhysicalFallbackObserved)
1358 zero)
1359 (lambda unrestricted fallbackPredecessor : Nat .
1360 (lambda unrestricted ignoredFallback : (family NativePhysicalProgramValidation) .
1361 (nat-eliminate
1362 (lambda unrestricted current : Nat . (family NativePhysicalProgramValidation))
1363 (eliminate
1364 NativePhysicalCommandsValidation
1365 (lambda unrestricted current : (family NativePhysicalCommandsValidation) .
1366 (family NativePhysicalProgramValidation))
1367 (nat-eliminate
1368 (lambda unrestricted current : Nat .
1369 (family NativePhysicalCommandsValidation))
1370 (nativePhysicalValidateCommands commands)
1371 (lambda unrestricted predecessor : Nat .
1372 (lambda unrestricted ignoredBalance : (family NativePhysicalCommandsValidation) .
1373 (constructor
1374 NativePhysicalCommandsValidation
1375 NativePhysicalCommandsInvalid
1376 (constructor NativePhysicalErrorCode NativePhysicalRepeatUnbalanced)
1377 zero)))
1378 (nativePhysicalRepeatBalance commands))
1379 (branch
1380 NativePhysicalCommandsValid
1381 completed
1382 .
1383 (nat-eliminate
1384 (lambda unrestricted current : Nat .
1385 (family NativePhysicalProgramValidation))
1386 (nativePhysicalReject
1387 program
1388 (constructor
1389 NativePhysicalErrorCode
1390 NativePhysicalCommandCountMismatch)
1391 zero)
1392 (lambda unrestricted countPredecessor : Nat .
1393 (lambda unrestricted ignoredCount : (family NativePhysicalProgramValidation) .
1394 (nat-eliminate
1395 (lambda unrestricted valid : Nat .
1396 (family NativePhysicalProgramValidation))
1397 (nativePhysicalReject
1398 program
1399 (constructor
1400 NativePhysicalErrorCode
1401 NativePhysicalMemoryExtentInvalid)
1402 zero)
1403 (lambda unrestricted previous : Nat .
1404 (lambda unrestricted ignored : (family NativePhysicalProgramValidation) .
1405 (constructor
1406 NativePhysicalProgramValidation
1407 NativePhysicalProgramValidated
1408 program
1409 (nativePhysicalValidationTelemetryFor program zero zero b""))))
1410 (nativePhysicalMemoryAdmitted
1411 (modelWord64Natural stateExtent)
1412 (modelWord64Natural resultSlots)
1413 (nativePhysicalRepeatMaximumDepth commands)))))
1414 (naturalEqual completed expected)))
1415 (branch
1416 NativePhysicalCommandsInvalid
1417 error
1418 ordinal
1419 .
1420 (nativePhysicalReject program error ordinal)))
1421 (lambda unrestricted statePredecessor : Nat .
1422 (lambda unrestricted ignoredState : (family NativePhysicalProgramValidation) .
1423 (nativePhysicalReject
1424 program
1425 (constructor NativePhysicalErrorCode NativePhysicalStateExtentZero)
1426 zero)))
1427 (modelWord64IsZero stateExtent))))
1428 (naturalEqual fallbacks zero))))
1429 (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.