def sp.tail_short
import bend-osdev-mode-core@0.1.0.0/PROOF.bend as PROOFimport 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
283# the tail of a split has fewer than 16 bytes
284def sp.tail_short(ys: List<&2, U32>) -> {Nat.is_lt(B.len(M.cm.split.tail(M.cm.split(B.mask(ys)))), 16n) == True{} : Bool}:
285 match ys:
286 case Nil{}:
287 {==}
288 case Con{+y0, +r0}:
289 match r0:
290 case Nil{}:
291 {==}
292 case Con{+y1, +r1}:
293 match r1:
294 case Nil{}:
295 {==}
296 case Con{+y2, +r2}:
297 match r2:
298 case Nil{}:
299 {==}
300 case Con{+y3, +r3}:
301 match r3:
302 case Nil{}:
303 {==}
304 case Con{+y4, +r4}:
305 match r4:
306 case Nil{}:
307 {==}
308 case Con{+y5, +r5}:
309 match r5:
310 case Nil{}:
311 {==}
312 case Con{+y6, +r6}:
313 match r6:
314 case Nil{}:
315 {==}
316 case Con{+y7, +r7}:
317 match r7:
318 case Nil{}:
319 {==}
320 case Con{+y8, +r8}:
321 match r8:
322 case Nil{}:
323 {==}
324 case Con{+y9, +r9}:
325 match r9:
326 case Nil{}:
327 {==}
328 case Con{+y10, +r10}:
329 match r10:
330 case Nil{}:
331 {==}
332 case Con{+y11, +r11}:
333 match r11:
334 case Nil{}:
335 {==}
336 case Con{+y12, +r12}:
337 match r12:
338 case Nil{}:
339 {==}
340 case Con{+y13, +r13}:
341 match r13:
342 case Nil{}:
343 {==}
344 case Con{+y14, +r14}:
345 match r14:
346 case Nil{}:
347 {==}
348 case Con{+y15, +t}:
349 %Equal.sym(List<&2, U32>, M.cm.split.tail(M.cm.split.cons(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)), M.cm.split(B.mask(t)))), M.cm.split.tail(M.cm.split(B.mask(t))), sp.cons_tail(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)), M.cm.split(B.mask(t)))) : {Nat.is_lt(B.len(_), 16n) == True{} : Bool}
350 sp.tail_short(t)