1276def attentionHeadLayoutSM86Image =
1277 (lambda unrestricted kind : (family AttentionHeadLayoutSM86Kind) .
1278 (app
1279 (lambda unrestricted program : (family SM86Program) .
1280 (app
1281 (lambda unrestricted actual : Nat .
1282 (nat-eliminate
1283 (lambda unrestricted countValid : Nat . (family AttentionHeadLayoutSM86ImageResult))
1284 (constructor
1285 AttentionHeadLayoutSM86ImageResult
1286 AttentionHeadLayoutSM86ImageFailed
1287 (constructor
1288 AttentionHeadLayoutSM86FailureCode
1289 AttentionHeadLayoutInstructionCountMismatch)
1290 actual
1291 (attentionHeadLayoutSM86FailureCodeBytes
1292 (constructor
1293 AttentionHeadLayoutSM86FailureCode
1294 AttentionHeadLayoutInstructionCountMismatch))
1295 (attentionHeadLayoutSM86TelemetryFor kind actual zero zero zero))
1296 (lambda unrestricted countPredecessor : Nat .
1297 (lambda unrestricted countInduction : (family AttentionHeadLayoutSM86ImageResult) .
1298 (eliminate
1299 SM86ProgramEncodingResult
1300 (lambda unrestricted current : (family SM86ProgramEncodingResult) .
1301 (family AttentionHeadLayoutSM86ImageResult))
1302 (sm86EncodeProgram program)
1303 (branch
1304 SM86ProgramEncodingSucceeded
1305 image
1306 encodingTelemetry
1307 .
1308 (eliminate
1309 SM86ProgramEncodingTelemetry
1310 (lambda unrestricted current : (family SM86ProgramEncodingTelemetry) .
1311 (family AttentionHeadLayoutSM86ImageResult))
1312 encodingTelemetry
1313 (branch
1314 SM86ProgramEncodingTelemetryValue
1315 instructions
1316 bytes
1317 fields
1318 bits
1319 highest
1320 .
1321 (app
1322 (lambda unrestricted identity : Bytes .
1323 (nat-eliminate
1324 (lambda unrestricted valid : Nat .
1325 (family AttentionHeadLayoutSM86ImageResult))
1326 (constructor
1327 AttentionHeadLayoutSM86ImageResult
1328 AttentionHeadLayoutSM86ImageFailed
1329 (constructor
1330 AttentionHeadLayoutSM86FailureCode
1331 AttentionHeadLayoutIdentityInvalid)
1332 zero
1333 (attentionHeadLayoutSM86FailureCodeBytes
1334 (constructor
1335 AttentionHeadLayoutSM86FailureCode
1336 AttentionHeadLayoutIdentityInvalid))
1337 (attentionHeadLayoutSM86TelemetryFor
1338 kind
1339 instructions
1340 bytes
1341 fields
1342 bits))
1343 (lambda unrestricted validPredecessor : Nat .
1344 (lambda unrestricted validInduction : (family AttentionHeadLayoutSM86ImageResult) .
1345 (constructor
1346 AttentionHeadLayoutSM86ImageResult
1347 AttentionHeadLayoutSM86ImageReady
1348 kind
1349 image
1350 identity
1351 (attentionHeadLayoutSM86TelemetryFor
1352 kind
1353 instructions
1354 bytes
1355 fields
1356 bits))))
1357 (naturalEqual (bytes-length identity) attentionHeadLayoutSM86N64)))
1358 (sha256HexBytesOrEmpty (sha256Hex image))))))
1359 (branch
1360 SM86ProgramEncodingFailed
1361 index
1362 failure
1363 encodingTelemetry
1364 .
1365 (constructor
1366 AttentionHeadLayoutSM86ImageResult
1367 AttentionHeadLayoutSM86ImageFailed
1368 (constructor
1369 AttentionHeadLayoutSM86FailureCode
1370 AttentionHeadLayoutEncodingFailed)
1371 index
1372 (sm86InstructionEncodingStableCode failure)
1373 (attentionHeadLayoutSM86TelemetryFor kind actual zero zero zero))))))
1374 (naturalEqual actual (attentionHeadLayoutSM86ExpectedInstructions kind))))
1375 (sm86ProgramCount program)))
1376 (attentionHeadLayoutSM86Program kind)))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.