def xtsp.len16

bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:1502

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M

1502# the bytes the stealing passes through: tl, then the stolen tail of b
1503def xtsp.len16(+tl: List<&2, U32>, +b: M.CmBlock, h: {Nat.is_lt(B.len(tl), 16n) == True{} : Bool}) -> {Nat.is_eq(B.len(B.append(tl, B.drop(B.len(tl), M.cm.bytes_of(b)))), 16n) == True{} : Bool}:
1504  %Equal.sym(Nat, B.len(B.append(tl, B.drop(B.len(tl), M.cm.bytes_of(b)))), Nat.add(B.len(tl), B.len(B.drop(B.len(tl), M.cm.bytes_of(b)))), li.len_append(tl, B.drop(B.len(tl), M.cm.bytes_of(b)))) : {Nat.is_eq(_, 16n) == True{} : Bool}
1505  %Equal.sym(Nat, B.len(B.drop(B.len(tl), M.cm.bytes_of(b))), Nat.sub(16n, B.len(tl)), li.len_drop(B.len(tl), M.cm.bytes_of(b))) : {Nat.is_eq(Nat.add(B.len(tl), _), 16n) == True{} : Bool}
1506  %Equal.sym(Nat, Nat.add(B.len(tl), Nat.sub(16n, B.len(tl))), 16n, na.add_sub(B.len(tl), 16n)(na.lt_le(B.len(tl), 16n)(h))) : {Nat.is_eq(_, 16n) == True{} : Bool}
1507  {==}