def sp.blk16g
bend-osdev-mode-core@0.1.0.0 · PROOF.bend:277
import bend-osdev-mode-core@0.1.0.0/PROOF.bend as PROOF
import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B
import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M
277
278def sp.blk16g(z0: U32, z1: U32, z2: U32, z3: U32, z4: U32, z5: U32, z6: U32, z7: U32, z8: U32, z9: U32, z10: U32, z11: U32, z12: U32, z13: U32, z14: U32, z15: U32, rest: List<&2, U32>) -> {M.cm.bytes_onto(M.cm.block16(z0, z1, z2, z3, z4, z5, z6, z7, z8, z9, z10, z11, z12, z13, z14, z15), rest) == Con{B.byte(z0), Con{B.byte(z1), Con{B.byte(z2), Con{B.byte(z3), Con{B.byte(z4), Con{B.byte(z5), Con{B.byte(z6), Con{B.byte(z7), Con{B.byte(z8), Con{B.byte(z9), Con{B.byte(z10), Con{B.byte(z11), Con{B.byte(z12), Con{B.byte(z13), Con{B.byte(z14), Con{B.byte(z15), rest}}}}}}}}}}}}}}}} : List<&2, U32>}:
279 match z0 z1 z2 z3 z4 z5 z6 z7 z8 z9 z10 z11 z12 z13 z14 z15:
280 case U32{WCon{z00, WCon{z01, WCon{z02, WCon{z03, WCon{z04, WCon{z05, WCon{z06, WCon{z07, WCon{z08, WCon{z09, WCon{z010, WCon{z011, WCon{z012, WCon{z013, WCon{z014, WCon{z015, WCon{z016, WCon{z017, WCon{z018, WCon{z019, WCon{z020, WCon{z021, WCon{z022, WCon{z023, WCon{z024, WCon{z025, WCon{z026, WCon{z027, WCon{z028, WCon{z029, WCon{z030, WCon{z031, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{z10, WCon{z11, WCon{z12, WCon{z13, WCon{z14, WCon{z15, WCon{z16, WCon{z17, WCon{z18, WCon{z19, WCon{z110, WCon{z111, WCon{z112, WCon{z113, WCon{z114, WCon{z115, WCon{z116, WCon{z117, WCon{z118, WCon{z119, WCon{z120, WCon{z121, WCon{z122, WCon{z123, WCon{z124, WCon{z125, WCon{z126, WCon{z127, WCon{z128, WCon{z129, WCon{z130, WCon{z131, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{z20, WCon{z21, WCon{z22, WCon{z23, WCon{z24, WCon{z25, WCon{z26, WCon{z27, WCon{z28, WCon{z29, WCon{z210, WCon{z211, WCon{z212, WCon{z213, WCon{z214, WCon{z215, WCon{z216, WCon{z217, WCon{z218, WCon{z219, WCon{z220, WCon{z221, WCon{z222, WCon{z223, WCon{z224, WCon{z225, WCon{z226, WCon{z227, WCon{z228, WCon{z229, WCon{z230, WCon{z231, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{z30, WCon{z31, WCon{z32, WCon{z33, WCon{z34, WCon{z35, WCon{z36, WCon{z37, WCon{z38, WCon{z39, WCon{z310, WCon{z311, WCon{z312, WCon{z313, WCon{z314, WCon{z315, WCon{z316, WCon{z317, WCon{z318, WCon{z319, WCon{z320, WCon{z321, WCon{z322, WCon{z323, WCon{z324, WCon{z325, WCon{z326, WCon{z327, WCon{z328, WCon{z329, WCon{z330, WCon{z331, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{z40, WCon{z41, WCon{z42, WCon{z43, WCon{z44, WCon{z45, WCon{z46, WCon{z47, WCon{z48, WCon{z49, WCon{z410, WCon{z411, WCon{z412, WCon{z413, WCon{z414, WCon{z415, WCon{z416, WCon{z417, WCon{z418, WCon{z419, WCon{z420, WCon{z421, WCon{z422, WCon{z423, WCon{z424, WCon{z425, WCon{z426, WCon{z427, WCon{z428, WCon{z429, WCon{z430, WCon{z431, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{z50, WCon{z51, WCon{z52, WCon{z53, WCon{z54, WCon{z55, WCon{z56, WCon{z57, WCon{z58, WCon{z59, WCon{z510, WCon{z511, WCon{z512, WCon{z513, WCon{z514, WCon{z515, WCon{z516, WCon{z517, WCon{z518, WCon{z519, WCon{z520, WCon{z521, WCon{z522, WCon{z523, WCon{z524, WCon{z525, WCon{z526, WCon{z527, WCon{z528, WCon{z529, WCon{z530, WCon{z531, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{z60, WCon{z61, WCon{z62, WCon{z63, WCon{z64, WCon{z65, WCon{z66, WCon{z67, WCon{z68, WCon{z69, WCon{z610, WCon{z611, WCon{z612, WCon{z613, WCon{z614, WCon{z615, WCon{z616, WCon{z617, WCon{z618, WCon{z619, WCon{z620, WCon{z621, WCon{z622, WCon{z623, WCon{z624, WCon{z625, WCon{z626, WCon{z627, WCon{z628, WCon{z629, WCon{z630, WCon{z631, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{z70, WCon{z71, WCon{z72, WCon{z73, WCon{z74, WCon{z75, WCon{z76, WCon{z77, WCon{z78, WCon{z79, WCon{z710, WCon{z711, WCon{z712, WCon{z713, WCon{z714, WCon{z715, WCon{z716, WCon{z717, WCon{z718, WCon{z719, WCon{z720, WCon{z721, WCon{z722, WCon{z723, WCon{z724, WCon{z725, WCon{z726, WCon{z727, WCon{z728, WCon{z729, WCon{z730, WCon{z731, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{z80, WCon{z81, WCon{z82, WCon{z83, WCon{z84, WCon{z85, WCon{z86, WCon{z87, WCon{z88, WCon{z89, WCon{z810, WCon{z811, WCon{z812, WCon{z813, WCon{z814, WCon{z815, WCon{z816, WCon{z817, WCon{z818, WCon{z819, WCon{z820, WCon{z821, WCon{z822, WCon{z823, WCon{z824, WCon{z825, WCon{z826, WCon{z827, WCon{z828, WCon{z829, WCon{z830, WCon{z831, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{z90, WCon{z91, WCon{z92, WCon{z93, WCon{z94, WCon{z95, WCon{z96, WCon{z97, WCon{z98, WCon{z99, WCon{z910, WCon{z911, WCon{z912, WCon{z913, WCon{z914, WCon{z915, WCon{z916, WCon{z917, WCon{z918, WCon{z919, WCon{z920, WCon{z921, WCon{z922, WCon{z923, WCon{z924, WCon{z925, WCon{z926, WCon{z927, WCon{z928, WCon{z929, WCon{z930, WCon{z931, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{z100, WCon{z101, WCon{z102, WCon{z103, WCon{z104, WCon{z105, WCon{z106, WCon{z107, WCon{z108, WCon{z109, WCon{z1010, WCon{z1011, WCon{z1012, WCon{z1013, WCon{z1014, WCon{z1015, WCon{z1016, WCon{z1017, WCon{z1018, WCon{z1019, WCon{z1020, WCon{z1021, WCon{z1022, WCon{z1023, WCon{z1024, WCon{z1025, WCon{z1026, WCon{z1027, WCon{z1028, WCon{z1029, WCon{z1030, WCon{z1031, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{z110, WCon{z111, WCon{z112, WCon{z113, WCon{z114, WCon{z115, WCon{z116, WCon{z117, WCon{z118, WCon{z119, WCon{z1110, WCon{z1111, WCon{z1112, WCon{z1113, WCon{z1114, WCon{z1115, WCon{z1116, WCon{z1117, WCon{z1118, WCon{z1119, WCon{z1120, WCon{z1121, WCon{z1122, WCon{z1123, WCon{z1124, WCon{z1125, WCon{z1126, WCon{z1127, WCon{z1128, WCon{z1129, WCon{z1130, WCon{z1131, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{z120, WCon{z121, WCon{z122, WCon{z123, WCon{z124, WCon{z125, WCon{z126, WCon{z127, WCon{z128, WCon{z129, WCon{z1210, WCon{z1211, WCon{z1212, WCon{z1213, WCon{z1214, WCon{z1215, WCon{z1216, WCon{z1217, WCon{z1218, WCon{z1219, WCon{z1220, WCon{z1221, WCon{z1222, WCon{z1223, WCon{z1224, WCon{z1225, WCon{z1226, WCon{z1227, WCon{z1228, WCon{z1229, WCon{z1230, WCon{z1231, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{z130, WCon{z131, WCon{z132, WCon{z133, WCon{z134, WCon{z135, WCon{z136, WCon{z137, WCon{z138, WCon{z139, WCon{z1310, WCon{z1311, WCon{z1312, WCon{z1313, WCon{z1314, WCon{z1315, WCon{z1316, WCon{z1317, WCon{z1318, WCon{z1319, WCon{z1320, WCon{z1321, WCon{z1322, WCon{z1323, WCon{z1324, WCon{z1325, WCon{z1326, WCon{z1327, WCon{z1328, WCon{z1329, WCon{z1330, WCon{z1331, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{z140, WCon{z141, WCon{z142, WCon{z143, WCon{z144, WCon{z145, WCon{z146, WCon{z147, WCon{z148, WCon{z149, WCon{z1410, WCon{z1411, WCon{z1412, WCon{z1413, WCon{z1414, WCon{z1415, WCon{z1416, WCon{z1417, WCon{z1418, WCon{z1419, WCon{z1420, WCon{z1421, WCon{z1422, WCon{z1423, WCon{z1424, WCon{z1425, WCon{z1426, WCon{z1427, WCon{z1428, WCon{z1429, WCon{z1430, WCon{z1431, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{z150, WCon{z151, WCon{z152, WCon{z153, WCon{z154, WCon{z155, WCon{z156, WCon{z157, WCon{z158, WCon{z159, WCon{z1510, WCon{z1511, WCon{z1512, WCon{z1513, WCon{z1514, WCon{z1515, WCon{z1516, WCon{z1517, WCon{z1518, WCon{z1519, WCon{z1520, WCon{z1521, WCon{z1522, WCon{z1523, WCon{z1524, WCon{z1525, WCon{z1526, WCon{z1527, WCon{z1528, WCon{z1529, WCon{z1530, WCon{z1531, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
281 {==}