PROOF.sp.blk16: def of bend-osdev-mode-core@0.1.0.0
Import: import bend-osdev-mode-core@0.1.0.0/PROOF.bend as PROOF
Lines 200-204 of bend-osdev-mode-core@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&start_line=200&end_line=204

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

# the block of 16 bytes, as bytes again
def sp.blk16(y0: U32, y1: U32, y2: U32, y3: U32, y4: U32, y5: U32, y6: U32, y7: U32, y8: U32, y9: U32, y10: U32, y11: U32, y12: U32, y13: U32, y14: U32, y15: U32, rest: List<&2, U32>) -> {M.cm.bytes_onto(M.cm.block16(B.byte(y0), B.byte(y1), B.byte(y2), B.byte(y3), B.byte(y4), B.byte(y5), B.byte(y6), B.byte(y7), B.byte(y8), B.byte(y9), B.byte(y10), B.byte(y11), B.byte(y12), B.byte(y13), B.byte(y14), B.byte(y15)), rest) == Con{B.byte(y0), Con{B.byte(y1), Con{B.byte(y2), Con{B.byte(y3), Con{B.byte(y4), Con{B.byte(y5), Con{B.byte(y6), Con{B.byte(y7), Con{B.byte(y8), Con{B.byte(y9), Con{B.byte(y10), Con{B.byte(y11), Con{B.byte(y12), Con{B.byte(y13), Con{B.byte(y14), Con{B.byte(y15), rest}}}}}}}}}}}}}}}} : List<&2, U32>}:
  match y0 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15:
    case U32{WCon{y00, WCon{y01, WCon{y02, WCon{y03, WCon{y04, WCon{y05, WCon{y06, WCon{y07, WCon{y08, WCon{y09, WCon{y010, WCon{y011, WCon{y012, WCon{y013, WCon{y014, WCon{y015, WCon{y016, WCon{y017, WCon{y018, WCon{y019, WCon{y020, WCon{y021, WCon{y022, WCon{y023, WCon{y024, WCon{y025, WCon{y026, WCon{y027, WCon{y028, WCon{y029, WCon{y030, WCon{y031, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{y10, WCon{y11, WCon{y12, WCon{y13, WCon{y14, WCon{y15, WCon{y16, WCon{y17, WCon{y18, WCon{y19, WCon{y110, WCon{y111, WCon{y112, WCon{y113, WCon{y114, WCon{y115, WCon{y116, WCon{y117, WCon{y118, WCon{y119, WCon{y120, WCon{y121, WCon{y122, WCon{y123, WCon{y124, WCon{y125, WCon{y126, WCon{y127, WCon{y128, WCon{y129, WCon{y130, WCon{y131, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{y20, WCon{y21, WCon{y22, WCon{y23, WCon{y24, WCon{y25, WCon{y26, WCon{y27, WCon{y28, WCon{y29, WCon{y210, WCon{y211, WCon{y212, WCon{y213, WCon{y214, WCon{y215, WCon{y216, WCon{y217, WCon{y218, WCon{y219, WCon{y220, WCon{y221, WCon{y222, WCon{y223, WCon{y224, WCon{y225, WCon{y226, WCon{y227, WCon{y228, WCon{y229, WCon{y230, WCon{y231, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{y30, WCon{y31, WCon{y32, WCon{y33, WCon{y34, WCon{y35, WCon{y36, WCon{y37, WCon{y38, WCon{y39, WCon{y310, WCon{y311, WCon{y312, WCon{y313, WCon{y314, WCon{y315, WCon{y316, WCon{y317, WCon{y318, WCon{y319, WCon{y320, WCon{y321, WCon{y322, WCon{y323, WCon{y324, WCon{y325, WCon{y326, WCon{y327, WCon{y328, WCon{y329, WCon{y330, WCon{y331, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{y40, WCon{y41, WCon{y42, WCon{y43, WCon{y44, WCon{y45, WCon{y46, WCon{y47, WCon{y48, WCon{y49, WCon{y410, WCon{y411, WCon{y412, WCon{y413, WCon{y414, WCon{y415, WCon{y416, WCon{y417, WCon{y418, WCon{y419, WCon{y420, WCon{y421, WCon{y422, WCon{y423, WCon{y424, WCon{y425, WCon{y426, WCon{y427, WCon{y428, WCon{y429, WCon{y430, WCon{y431, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{y50, WCon{y51, WCon{y52, WCon{y53, WCon{y54, WCon{y55, WCon{y56, WCon{y57, WCon{y58, WCon{y59, WCon{y510, WCon{y511, WCon{y512, WCon{y513, WCon{y514, WCon{y515, WCon{y516, WCon{y517, WCon{y518, WCon{y519, WCon{y520, WCon{y521, WCon{y522, WCon{y523, WCon{y524, WCon{y525, WCon{y526, WCon{y527, WCon{y528, WCon{y529, WCon{y530, WCon{y531, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{y60, WCon{y61, WCon{y62, WCon{y63, WCon{y64, WCon{y65, WCon{y66, WCon{y67, WCon{y68, WCon{y69, WCon{y610, WCon{y611, WCon{y612, WCon{y613, WCon{y614, WCon{y615, WCon{y616, WCon{y617, WCon{y618, WCon{y619, WCon{y620, WCon{y621, WCon{y622, WCon{y623, WCon{y624, WCon{y625, WCon{y626, WCon{y627, WCon{y628, WCon{y629, WCon{y630, WCon{y631, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{y70, WCon{y71, WCon{y72, WCon{y73, WCon{y74, WCon{y75, WCon{y76, WCon{y77, WCon{y78, WCon{y79, WCon{y710, WCon{y711, WCon{y712, WCon{y713, WCon{y714, WCon{y715, WCon{y716, WCon{y717, WCon{y718, WCon{y719, WCon{y720, WCon{y721, WCon{y722, WCon{y723, WCon{y724, WCon{y725, WCon{y726, WCon{y727, WCon{y728, WCon{y729, WCon{y730, WCon{y731, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{y80, WCon{y81, WCon{y82, WCon{y83, WCon{y84, WCon{y85, WCon{y86, WCon{y87, WCon{y88, WCon{y89, WCon{y810, WCon{y811, WCon{y812, WCon{y813, WCon{y814, WCon{y815, WCon{y816, WCon{y817, WCon{y818, WCon{y819, WCon{y820, WCon{y821, WCon{y822, WCon{y823, WCon{y824, WCon{y825, WCon{y826, WCon{y827, WCon{y828, WCon{y829, WCon{y830, WCon{y831, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{y90, WCon{y91, WCon{y92, WCon{y93, WCon{y94, WCon{y95, WCon{y96, WCon{y97, WCon{y98, WCon{y99, WCon{y910, WCon{y911, WCon{y912, WCon{y913, WCon{y914, WCon{y915, WCon{y916, WCon{y917, WCon{y918, WCon{y919, WCon{y920, WCon{y921, WCon{y922, WCon{y923, WCon{y924, WCon{y925, WCon{y926, WCon{y927, WCon{y928, WCon{y929, WCon{y930, WCon{y931, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{y100, WCon{y101, WCon{y102, WCon{y103, WCon{y104, WCon{y105, WCon{y106, WCon{y107, WCon{y108, WCon{y109, WCon{y1010, WCon{y1011, WCon{y1012, WCon{y1013, WCon{y1014, WCon{y1015, WCon{y1016, WCon{y1017, WCon{y1018, WCon{y1019, WCon{y1020, WCon{y1021, WCon{y1022, WCon{y1023, WCon{y1024, WCon{y1025, WCon{y1026, WCon{y1027, WCon{y1028, WCon{y1029, WCon{y1030, WCon{y1031, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{y110, WCon{y111, WCon{y112, WCon{y113, WCon{y114, WCon{y115, WCon{y116, WCon{y117, WCon{y118, WCon{y119, WCon{y1110, WCon{y1111, WCon{y1112, WCon{y1113, WCon{y1114, WCon{y1115, WCon{y1116, WCon{y1117, WCon{y1118, WCon{y1119, WCon{y1120, WCon{y1121, WCon{y1122, WCon{y1123, WCon{y1124, WCon{y1125, WCon{y1126, WCon{y1127, WCon{y1128, WCon{y1129, WCon{y1130, WCon{y1131, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{y120, WCon{y121, WCon{y122, WCon{y123, WCon{y124, WCon{y125, WCon{y126, WCon{y127, WCon{y128, WCon{y129, WCon{y1210, WCon{y1211, WCon{y1212, WCon{y1213, WCon{y1214, WCon{y1215, WCon{y1216, WCon{y1217, WCon{y1218, WCon{y1219, WCon{y1220, WCon{y1221, WCon{y1222, WCon{y1223, WCon{y1224, WCon{y1225, WCon{y1226, WCon{y1227, WCon{y1228, WCon{y1229, WCon{y1230, WCon{y1231, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{y130, WCon{y131, WCon{y132, WCon{y133, WCon{y134, WCon{y135, WCon{y136, WCon{y137, WCon{y138, WCon{y139, WCon{y1310, WCon{y1311, WCon{y1312, WCon{y1313, WCon{y1314, WCon{y1315, WCon{y1316, WCon{y1317, WCon{y1318, WCon{y1319, WCon{y1320, WCon{y1321, WCon{y1322, WCon{y1323, WCon{y1324, WCon{y1325, WCon{y1326, WCon{y1327, WCon{y1328, WCon{y1329, WCon{y1330, WCon{y1331, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{y140, WCon{y141, WCon{y142, WCon{y143, WCon{y144, WCon{y145, WCon{y146, WCon{y147, WCon{y148, WCon{y149, WCon{y1410, WCon{y1411, WCon{y1412, WCon{y1413, WCon{y1414, WCon{y1415, WCon{y1416, WCon{y1417, WCon{y1418, WCon{y1419, WCon{y1420, WCon{y1421, WCon{y1422, WCon{y1423, WCon{y1424, WCon{y1425, WCon{y1426, WCon{y1427, WCon{y1428, WCon{y1429, WCon{y1430, WCon{y1431, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{y150, WCon{y151, WCon{y152, WCon{y153, WCon{y154, WCon{y155, WCon{y156, WCon{y157, WCon{y158, WCon{y159, WCon{y1510, WCon{y1511, WCon{y1512, WCon{y1513, WCon{y1514, WCon{y1515, WCon{y1516, WCon{y1517, WCon{y1518, WCon{y1519, WCon{y1520, WCon{y1521, WCon{y1522, WCon{y1523, WCon{y1524, WCon{y1525, WCon{y1526, WCon{y1527, WCon{y1528, WCon{y1529, WCon{y1530, WCon{y1531, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
      {==}

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Nil
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=byte
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/mode_core.bend&name=cm.block16
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/mode_core.bend&name=cm.bytes_onto