bend-osdev-mode-core

Releases (1):
  0.1.0.0  0x999adc34209a88c2495b3a5407a5ad25  indexed  https://jend.leeeet.dev/files.txt?path=bend-osdev-mode-core@0.1.0.0

Definitions (151, 1 to 100 shown):
  LAWS.block_octets_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/LAWS.bend&name=block_octets_round_trip)
   # A block written as Octets reads back as the same block, for every block
   law block_octets_round_trip:
     for +b: M.CmBlock
     {M.CmBlock.of_octets(M.CmBlock.to_octets(b)) == Some{b} : Maybe<&2, M.CmBlock>}
  LAWS.byte_byte (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/LAWS.bend&name=byte_byte)
   law byte_byte:
     for y: U32
     {B.byte(B.byte(y)) == B.byte(y) : U32}
  LAWS.split_cons_blocks (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/LAWS.bend&name=split_cons_blocks)
   law split_cons_blocks:
     for b: M.CmBlock
     for s: M.CmSplit
     {M.cm.split.blocks(M.cm.split.cons(b, s)) == Con{b, M.cm.split.blocks(s)} : List<&2, M.CmBlock>}
  LAWS.split_cons_tail (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/LAWS.bend&name=split_cons_tail)
   law split_cons_tail:
     for b: M.CmBlock
     for s: M.CmSplit
     {M.cm.split.tail(M.cm.split.cons(b, s)) == M.cm.split.tail(s) : List<&2, U32>}
  LAWS.split_eta (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/LAWS.bend&name=split_eta)
   law split_eta:
     for s: M.CmSplit
     {M.CmSplit{M.cm.split.blocks(s), M.cm.split.tail(s)} == s : M.CmSplit}
  LAWS.list_take_append (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/LAWS.bend&name=list_take_append)
   law list_take_append:
     for +a: List<&2, U32>
     for +b: List<&2, U32>
     {B.take(B.len(a), B.append(a, b)) == a : List<&2, U32>}
  LAWS.list_drop_append (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/LAWS.bend&name=list_drop_append)
   law list_drop_append:
     for +a: List<&2, U32>
     for +b: List<&2, U32>
     {B.drop(B.len(a), B.append(a, b)) == b : List<&2, U32>}
  LAWS.list_mask_append (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/LAWS.bend&name=list_mask_append)
   law list_mask_append:
     for +a: List<&2, U32>
     for +b: List<&2, U32>
     {B.mask(B.append(a, b)) == B.append(B.mask(a), B.mask(b)) : List<&2, U32>}
  LAWS.list_mask_take (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/LAWS.bend&name=list_mask_take)
   law list_mask_take:
     for +n: Nat
     for +xs: List<&2, U32>
     {B.mask(B.take(n, xs)) == B.take(n, B.mask(xs)) : List<&2, U32>}
  LAWS.list_len_append (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/LAWS.bend&name=list_len_append)
   law list_len_append:
     for +a: List<&2, U32>
     for +b: List<&2, U32>
     {B.len(B.append(a, b)) == Nat.add(B.len(a), B.len(b)) : Nat}
  LAWS.list_len_take (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/LAWS.bend&name=list_len_take)
   law list_len_take:
     for +n: Nat
     for +xs: List<&2, U32>
     for h1: {Nat.is_le(n, B.len(xs)) == True{} : Bool}
     {B.len(B.take(n, xs)) == n : Nat}
  LAWS.nat_lt_le (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/LAWS.bend&name=nat_lt_le)
   law nat_lt_le:
     for +a: Nat
     for +b: Nat
     for h1: {Nat.is_lt(a, b) == True{} : Bool}
     {Nat.is_le(a, b) == True{} : Bool}
  LAWS.split_bytes_onto (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/LAWS.bend&name=split_bytes_onto)
   # splitting the bytes of a block gives the block back
   law split_bytes_onto:
     for b: M.CmBlock
     for rest: List<&2, U32>
     {M.cm.split(M.cm.bytes_onto(b, rest)) == M.cm.split.cons(b, M.cm.split(rest)) : M.CmSplit}
  LAWS.mask_bytes_onto (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/LAWS.bend&name=mask_bytes_onto)
   # the bytes of a block are bytes: masking changes nothing
   law mask_bytes_onto:
     for b: M.CmBlock
     for rest: List<&2, U32>
     {B.mask(M.cm.bytes_onto(b, rest)) == M.cm.bytes_onto(b, B.mask(rest)) : List<&2, U32>}
  LAWS.join_split (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/LAWS.bend&name=join_split)
   # a masked list is its blocks and its tail joined back
   law join_split:
     for ys: List<&2, U32>
     {M.cm.join_onto(M.cm.split.blocks(M.cm.split(B.mask(ys))), M.cm.split.tail(M.cm.split(B.mask(ys)))) == B.mask(ys) : List<&2, U32>}
  LAWS.bytes_onto_block16 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/LAWS.bend&name=bytes_onto_block16)
   # the bytes of the block of any 16 values are those values, masked
   law bytes_onto_block16:
     for z0: U32
     for z1: U32
     for z2: U32
     for z3: U32
     for z4: U32
     for z5: U32
     for z6: U32
     for z7: U32
     for z8: U32
     …
  LAWS.split_tail_short (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/LAWS.bend&name=split_tail_short)
   # the tail of a split has fewer than 16 bytes
   law split_tail_short:
     for ys: List<&2, U32>
     {Nat.is_lt(B.len(M.cm.split.tail(M.cm.split(B.mask(ys)))), 16n) == True{} : Bool}
  LAWS.split_tail_masked (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/LAWS.bend&name=split_tail_masked)
   # the tail of a masked split is masked
   law split_tail_masked:
     for ys: List<&2, U32>
     {B.mask(M.cm.split.tail(M.cm.split(B.mask(ys)))) == M.cm.split.tail(M.cm.split(B.mask(ys))) : List<&2, U32>}
  LAWS.split_short (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/LAWS.bend&name=split_short)
   # fewer than 16 bytes are all tail
   law split_short:
     for ys: List<&2, U32>
     for h1: {Nat.is_lt(B.len(ys), 16n) == True{} : Bool}
     {M.cm.split(ys) == M.CmSplit{Nil{}, ys} : M.CmSplit}
  LAWS.block_of_bytes_of (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/LAWS.bend&name=block_of_bytes_of)
   # the block of a block's bytes is the block
   law block_of_bytes_of:
     for b: M.CmBlock
     {M.cm.block_of(M.cm.bytes_of(b)) == b : M.CmBlock}
  LAWS.octets_masked (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/LAWS.bend&name=octets_masked)
   # Every Octets is masked: to_list(o) = to_list(of_list(to_list(o))) = mask(to_list(o))
   law octets_masked:
     for +o: B.Octets
     {B.mask(B.Octets.to_list(o)) == B.Octets.to_list(o) : List<&2, U32>}
  LAWS.octets_len (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/LAWS.bend&name=octets_len)
   law octets_len:
     for +o: B.Octets
     for +n: Nat
     for h: {B.Octets.len(o) == n : Nat}
     {B.len(B.Octets.to_list(o)) == n : Nat}
  LAWS.blocks_len_fast (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/LAWS.bend&name=blocks_len_fast)
   law blocks_len_fast:
     for +bs: List<&2, M.CmBlock>
     {List.length(&2, M.CmBlock, bs) == M.cm.blocks.len(bs) : Nat}
  LAWS.split_fast (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/LAWS.bend&name=split_fast)
   law split_fast:
     for +xs: List<&2, U32>
     {M.cm.split(xs) == M.cm.split.fast(xs) : M.CmSplit}
  LAWS.join_onto_fast (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/LAWS.bend&name=join_onto_fast)
   law join_onto_fast:
     for +bs: List<&2, M.CmBlock>
     for +rest: List<&2, U32>
     {M.cm.join_onto(bs, rest) == M.cm.join_onto.fast(bs, rest) : List<&2, U32>}
  LAWS.bind_cong (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/LAWS.bend&name=bind_cong)
   # a bind whose continuations agree on every value agrees
   law bind_cong:
     for r: Result<&2, &2, M.CmError, B.Octets>
     for f: B.Octets -> Result<&2, &2, M.CmError, B.Octets>
     for g: B.Octets -> Result<&2, &2, M.CmError, B.Octets>
     for h: @c: B.Octets -> {f(c) == g(c) : Result<&2, &2, M.CmError, B.Octets>}
     {Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, r, f) == Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, r, g) : Result<&2, &2, M.CmError, B.Octets>}
  LAWS.dec_enc_head (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/LAWS.bend&name=dec_enc_head)
   # the first block's round trip, and the rest's
   law dec_enc_head:
     for ~K: Data
     for ~enc: K -> M.CmBlock -> M.CmBlock
     for ~dec: K -> M.CmBlock -> M.CmBlock
     for +k: K
     for +x: M.CmBlock
     for +xs: List<&2, M.CmBlock>
     for +h: {M.CmBlock.dec_enc(~K, ~enc, ~dec, k, Con{x, xs}) == Con{x, xs} : List<&2, M.CmBlock>}
     {dec(k, enc(k, x)) == x : M.CmBlock}
  LAWS.dec_enc_tail (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/LAWS.bend&name=dec_enc_tail)
   law dec_enc_tail:
     for ~K: Data
     for ~enc: K -> M.CmBlock -> M.CmBlock
     for ~dec: K -> M.CmBlock -> M.CmBlock
     for +k: K
     for +x: M.CmBlock
     for +xs: List<&2, M.CmBlock>
     for +h: {M.CmBlock.dec_enc(~K, ~enc, ~dec, k, Con{x, xs}) == Con{x, xs} : List<&2, M.CmBlock>}
     {M.CmBlock.dec_enc(~K, ~enc, ~dec, k, xs) == xs : List<&2, M.CmBlock>}
  LAWS.word_xor_xor (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/LAWS.bend&name=word_xor_xor)
   law word_xor_xor:
     for n: Nat
     for a: Word(n)
     for b: Word(n)
     {Word.xor(n, Word.xor(n, a, b), b) == a : Word(n)}
  LAWS.u32_xor_xor (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/LAWS.bend&name=u32_xor_xor)
   law u32_xor_xor:
     for a: U32
     for b: U32
     {U32.xor(U32.xor(a, b), b) == a : U32}
  LAWS.block_xor_xor (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/LAWS.bend&name=block_xor_xor)
   law block_xor_xor:
     for +a: M.CmBlock
     for +b: M.CmBlock
     {M.CmBlock.xor(M.CmBlock.xor(a, b), b) == a : M.CmBlock}
  LAWS.mask_join_onto (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/LAWS.bend&name=mask_join_onto)
   law mask_join_onto:
     for bs: List<&2, M.CmBlock>
     for +rest: List<&2, U32>
     {B.mask(M.cm.join_onto(bs, rest)) == M.cm.join_onto(bs, B.mask(rest)) : List<&2, U32>}
  LAWS.split_join_short (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/LAWS.bend&name=split_join_short)
   # blocks joined in front of a short tail split back into those blocks and tail
   law split_join_short:
     for bs: List<&2, M.CmBlock>
     for +rest: List<&2, U32>
     for h1: {M.cm.split(rest) == M.CmSplit{Nil{}, rest} : M.CmSplit}
     {M.cm.split(M.cm.join_onto(bs, rest)) == M.CmSplit{bs, rest} : M.CmSplit}
  PROOF.bits.word_bytes (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=bits.word_bytes)
   def bits.word_bytes(w: U32) -> {M.cm.word(M.cm.b0(w), M.cm.b1(w), M.cm.b2(w), M.cm.b3(w)) == w : U32}:
  PROOF.bits.byte0_word (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=bits.byte0_word)
   def bits.byte0_word(a: U32, b: U32, c: U32, d: U32) -> {M.cm.b0(M.cm.word(a, b, c, d)) == B.byte(a) : U32}:
  PROOF.bits.byte1_word (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=bits.byte1_word)
   def bits.byte1_word(a: U32, b: U32, c: U32, d: U32) -> {M.cm.b1(M.cm.word(a, b, c, d)) == B.byte(b) : U32}:
  PROOF.bits.byte2_word (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=bits.byte2_word)
   def bits.byte2_word(a: U32, b: U32, c: U32, d: U32) -> {M.cm.b2(M.cm.word(a, b, c, d)) == B.byte(c) : U32}:
  PROOF.bits.byte3_word (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=bits.byte3_word)
   def bits.byte3_word(a: U32, b: U32, c: U32, d: U32) -> {M.cm.b3(M.cm.word(a, b, c, d)) == B.byte(d) : U32}:
  PROOF.bits.byte_b0 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=bits.byte_b0)
   def bits.byte_b0(w: U32) -> {B.byte(M.cm.b0(w)) == M.cm.b0(w) : U32}:
  PROOF.bits.byte_b1 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=bits.byte_b1)
   def bits.byte_b1(w: U32) -> {B.byte(M.cm.b1(w)) == M.cm.b1(w) : U32}:
  PROOF.bits.byte_b2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=bits.byte_b2)
   def bits.byte_b2(w: U32) -> {B.byte(M.cm.b2(w)) == M.cm.b2(w) : U32}:
  PROOF.bits.byte_b3 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=bits.byte_b3)
   def bits.byte_b3(w: U32) -> {B.byte(M.cm.b3(w)) == M.cm.b3(w) : U32}:
  PROOF.bits.byte_byte (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=bits.byte_byte)
   def bits.byte_byte(y: U32) -> {B.byte(B.byte(y)) == B.byte(y) : U32}:
  PROOF.sp.cons_blocks (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=sp.cons_blocks)
   def sp.cons_blocks(b: M.CmBlock, s: M.CmSplit) -> {M.cm.split.blocks(M.cm.split.cons(b, s)) == Con{b, M.cm.split.blocks(s)} : List<&2, M.CmBlock>}:
  PROOF.sp.cons_tail (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=sp.cons_tail)
   def sp.cons_tail(b: M.CmBlock, s: M.CmSplit) -> {M.cm.split.tail(M.cm.split.cons(b, s)) == M.cm.split.tail(s) : List<&2, U32>}:
  PROOF.sp.eta (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=sp.eta)
   def sp.eta(s: M.CmSplit) -> {M.CmSplit{M.cm.split.blocks(s), M.cm.split.tail(s)} == s : M.CmSplit}:
  PROOF.bo.disc (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=bo.disc)
   def bo.disc(b: Bool) -> Type:
  PROOF.bo.empty (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=bo.empty)
   def bo.empty(h: {False{} == True{} : Bool}) -> Empty:
  PROOF.bo.absurd (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=bo.absurd)
   def bo.absurd(-A: Type, h: {False{} == True{} : Bool}) -> A:
  PROOF.li.mask_mask (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=li.mask_mask)
   def li.mask_mask(zs: List<&2, U32>) -> {B.mask(B.mask(zs)) == B.mask(zs) : List<&2, U32>}:
  PROOF.li.take_append (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=li.take_append)
   def li.take_append(+a: List<&2, U32>, +b: List<&2, U32>) -> {B.take(B.len(a), B.append(a, b)) == a : List<&2, U32>}:
  PROOF.li.drop_append (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=li.drop_append)
   def li.drop_append(+a: List<&2, U32>, +b: List<&2, U32>) -> {B.drop(B.len(a), B.append(a, b)) == b : List<&2, U32>}:
  PROOF.li.mask_append (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=li.mask_append)
   def li.mask_append(+a: List<&2, U32>, +b: List<&2, U32>) -> {B.mask(B.append(a, b)) == B.append(B.mask(a), B.mask(b)) : List<&2, U32>}:
  PROOF.li.mask_take (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=li.mask_take)
   def li.mask_take(+n: Nat, +xs: List<&2, U32>) -> {B.mask(B.take(n, xs)) == B.take(n, B.mask(xs)) : List<&2, U32>}:
  PROOF.li.len_append (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=li.len_append)
   def li.len_append(+a: List<&2, U32>, +b: List<&2, U32>) -> {B.len(B.append(a, b)) == Nat.add(B.len(a), B.len(b)) : Nat}:
  PROOF.li.len_take (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=li.len_take)
   def li.len_take(+n: Nat, +xs: List<&2, U32>) -> {Nat.is_le(n, B.len(xs)) == True{} : Bool} -> {B.len(B.take(n, xs)) == n : Nat}:
  PROOF.na.lt_le (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=na.lt_le)
   def na.lt_le(+a: Nat, +b: Nat) -> {Nat.is_lt(a, b) == True{} : Bool} -> {Nat.is_le(a, b) == True{} : Bool}:
  PROOF.sp.blk (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=sp.blk)
   # splitting the bytes of a block gives the block back
   def sp.blk(b: M.CmBlock, rest: List<&2, U32>) -> {M.cm.split(M.cm.bytes_onto(b, rest)) == M.cm.split.cons(b, M.cm.split(rest)) : M.CmSplit}:
  PROOF.sp.mask_blk (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=sp.mask_blk)
   # the bytes of a block are bytes: masking changes nothing
   def sp.mask_blk(b: M.CmBlock, rest: List<&2, U32>) -> {B.mask(M.cm.bytes_onto(b, rest)) == M.cm.bytes_onto(b, B.mask(rest)) : List<&2, U32>}:
  PROOF.sp.blk16 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=sp.blk16)
   # 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>}:
  PROOF.sp.join_split (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=sp.join_split)
   # a masked list is its blocks and its tail joined back
   def sp.join_split(ys: List<&2, U32>) -> {M.cm.join_onto(M.cm.split.blocks(M.cm.split(B.mask(ys))), M.cm.split.tail(M.cm.split(B.mask(ys)))) == B.mask(ys) : List<&2, U32>}:
  PROOF.sp.blk16g (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=sp.blk16g)
   # the bytes of the block of any 16 values are those values, masked
   def 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>}:
  PROOF.sp.tail_short (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=sp.tail_short)
   # the tail of a split has fewer than 16 bytes
   def 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}:
  PROOF.sp.tail_masked (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=sp.tail_masked)
   # the tail of a masked split is masked
   def sp.tail_masked(ys: List<&2, U32>) -> {B.mask(M.cm.split.tail(M.cm.split(B.mask(ys)))) == M.cm.split.tail(M.cm.split(B.mask(ys))) : List<&2, U32>}:
  PROOF.sp.short_split (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=sp.short_split)
   # fewer than 16 bytes are all tail
   def sp.short_split(ys: List<&2, U32>) -> {Nat.is_lt(B.len(ys), 16n) == True{} : Bool} -> {M.cm.split(ys) == M.CmSplit{Nil{}, ys} : M.CmSplit}:
  PROOF.sp.block_bytes (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=sp.block_bytes)
   # the block of a block's bytes is the block
   def sp.block_bytes(b: M.CmBlock) -> {M.cm.block_of(M.cm.bytes_of(b)) == b : M.CmBlock}:
  PROOF.oc.masked (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=oc.masked)
   # Every Octets is masked: to_list(o) = to_list(of_list(to_list(o))) = mask(to_list(o))
   def oc.masked(+o: B.Octets) -> {B.mask(B.Octets.to_list(o)) == B.Octets.to_list(o) : List<&2, U32>}:
  PROOF.oc.len (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=oc.len)
   def oc.len(+o: B.Octets, +n: Nat, h: {B.Octets.len(o) == n : Nat}) -> {B.len(B.Octets.to_list(o)) == n : Nat}:
  PROOF.tr.len_go (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=tr.len_go)
   def tr.len_go(+bs: List<&2, M.CmBlock>, +n: Nat) -> {M.cm.blocks.len.go(bs, n) == Nat.add(List.length(&2, M.CmBlock, bs), n) : Nat}:
  PROOF.tr.len_eq (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=tr.len_eq)
   def tr.len_eq(+bs: List<&2, M.CmBlock>) -> {List.length(&2, M.CmBlock, bs) == M.cm.blocks.len(bs) : Nat}:
  PROOF.tr.split_fin (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=tr.split_fin)
   def tr.split_fin(acc: List<&2, M.CmBlock>, s: M.CmSplit) -> M.CmSplit:
  PROOF.tr.split_fin_cons (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=tr.split_fin_cons)
   def tr.split_fin_cons(+b: M.CmBlock, +acc: List<&2, M.CmBlock>, +s: M.CmSplit) -> {tr.split_fin(Con{b, acc}, s) == tr.split_fin(acc, M.cm.split.cons(b, s)) : M.CmSplit}:
  PROOF.tr.split_fin_nil (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=tr.split_fin_nil)
   def tr.split_fin_nil(+s: M.CmSplit) -> {tr.split_fin(Nil{}, s) == s : M.CmSplit}:
  PROOF.tr.split_go (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=tr.split_go)
   def tr.split_go(+xs: List<&2, U32>, +acc: List<&2, M.CmBlock>) -> {M.cm.split.go(xs, acc) == tr.split_fin(acc, M.cm.split(xs)) : M.CmSplit}:
  PROOF.tr.split_eq (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=tr.split_eq)
   def tr.split_eq(+xs: List<&2, U32>) -> {M.cm.split(xs) == M.cm.split.fast(xs) : M.CmSplit}:
  PROOF.tr.join_go (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=tr.join_go)
   def tr.join_go(xs: List<&2, M.CmBlock>, rs: List<&2, M.CmBlock>, +rest: List<&2, U32>) -> {M.cm.join.go(M.cm.blocks.rev_onto(xs, rs), rest) == M.cm.join.go(rs, M.cm.join_onto(xs, rest)) : List<&2, U32>}:
  PROOF.tr.join_eq (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=tr.join_eq)
   def tr.join_eq(+bs: List<&2, M.CmBlock>, +rest: List<&2, U32>) -> {M.cm.join_onto(bs, rest) == M.cm.join_onto.fast(bs, rest) : List<&2, U32>}:
  PROOF.tr.bind_cong (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=tr.bind_cong)
   # a bind whose continuations agree on every value agrees
   def tr.bind_cong(r: Result<&2, &2, M.CmError, B.Octets>, f: B.Octets -> Result<&2, &2, M.CmError, B.Octets>, g: B.Octets -> Result<&2, &2, M.CmError, B.Octets>, h: @c: B.Octets -> {f(c) == g(c) : Result<&2, &2, M.CmError, B.Octets>}) -> {Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, r, f) == Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, r, g) : Result<&2, &2, M.CmError, B.Octets>}:
  PROOF.cmp.head (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=cmp.head)
   def cmp.head(d: M.CmBlock, xs: List<&2, M.CmBlock>) -> M.CmBlock:
  PROOF.cmp.tail (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=cmp.tail)
   def cmp.tail(xs: List<&2, M.CmBlock>) -> List<&2, M.CmBlock>:
  PROOF.li.con_hd (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=li.con_hd)
   def li.con_hd(+a: M.CmBlock, +s: List<&2, M.CmBlock>, +b: M.CmBlock, +t: List<&2, M.CmBlock>, +e: {Con{a, s} == Con{b, t} : List<&2, M.CmBlock>}) -> {a == b : M.CmBlock}:
  PROOF.li.con_tl (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=li.con_tl)
   def li.con_tl(+a: M.CmBlock, +s: List<&2, M.CmBlock>, +b: M.CmBlock, +t: List<&2, M.CmBlock>, +e: {Con{a, s} == Con{b, t} : List<&2, M.CmBlock>}) -> {s == t : List<&2, M.CmBlock>}:
  PROOF.cmp.hd (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=cmp.hd)
   # the first block's round trip, and the rest's
   def cmp.hd(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, +x: M.CmBlock, +xs: List<&2, M.CmBlock>, +h: {M.CmBlock.dec_enc(~K, ~enc, ~dec, k, Con{x, xs}) == Con{x, xs} : List<&2, M.CmBlock>}) -> {dec(k, enc(k, x)) == x : M.CmBlock}:
  PROOF.cmp.tl (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=cmp.tl)
   def cmp.tl(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, +x: M.CmBlock, +xs: List<&2, M.CmBlock>, +h: {M.CmBlock.dec_enc(~K, ~enc, ~dec, k, Con{x, xs}) == Con{x, xs} : List<&2, M.CmBlock>}) -> {M.CmBlock.dec_enc(~K, ~enc, ~dec, k, xs) == xs : List<&2, M.CmBlock>}:
  PROOF.bx.rbool (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=bx.rbool)
   def bx.rbool(a: Bool, b: Bool) -> {Bool.xor(Bool.xor(a, b), b) == a : Bool}:
  PROOF.bx.rword (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=bx.rword)
   def bx.rword(n: Nat, a: Word(n), b: Word(n)) -> {Word.xor(n, Word.xor(n, a, b), b) == a : Word(n)}:
  PROOF.bx.ru32 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=bx.ru32)
   def bx.ru32(a: U32, b: U32) -> {U32.xor(U32.xor(a, b), b) == a : U32}:
  PROOF.bx.rblock (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=bx.rblock)
   def bx.rblock(+a: M.CmBlock, +b: M.CmBlock) -> {M.CmBlock.xor(M.CmBlock.xor(a, b), b) == a : M.CmBlock}:
  PROOF.sp.mask_join_onto (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=sp.mask_join_onto)
   def sp.mask_join_onto(bs: List<&2, M.CmBlock>, +rest: List<&2, U32>) -> {B.mask(M.cm.join_onto(bs, rest)) == M.cm.join_onto(bs, B.mask(rest)) : List<&2, U32>}:
  PROOF.sp.split_join_short (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=sp.split_join_short)
   # blocks joined in front of a short tail split back into those blocks and tail
   def sp.split_join_short(bs: List<&2, M.CmBlock>, +rest: List<&2, U32>) -> {M.cm.split(rest) == M.CmSplit{Nil{}, rest} : M.CmSplit} -> {M.cm.split(M.cm.join_onto(bs, rest)) == M.CmSplit{bs, rest} : M.CmSplit}:
  PROOF.li.len_bytes (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=li.len_bytes)
   def li.len_bytes(+b: M.CmBlock, +rest: List<&2, U32>) -> {B.len(M.cm.bytes_onto(b, rest)) == Nat.add(16n, B.len(rest)) : Nat}:
  Check.toy.rot (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/check.bend&name=toy.rot)
   # A toy permutation of blocks, NOT a cipher: the words rotated, then XOR
   # with the key block. Enough to run the mode's code paths (encryption and
   # decryption differ, so mixing them up shows); the mode is tested against
   # its specification over AES in bend-osdev-aes-modes (the specifications'
   # vectors) and in ref/ (against Python's cryptography).
   def toy.rot(b: M.CmBlock) -> M.CmBlock:
  Check.toy.unrot (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/check.bend&name=toy.unrot)
   def toy.unrot(b: M.CmBlock) -> M.CmBlock:
  Check.toy.enc (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/check.bend&name=toy.enc)
   def toy.enc(k: M.CmBlock, b: M.CmBlock) -> M.CmBlock:
  Check.toy.dec (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/check.bend&name=toy.dec)
   def toy.dec(k: M.CmBlock, c: M.CmBlock) -> M.CmBlock:
  Check.key (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/check.bend&name=key)
   def key() -> M.CmBlock:
  Check.key2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/check.bend&name=key2)
   def key2() -> M.CmBlock:
  Check.hexs (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/check.bend&name=hexs)
   def hexs(bs: List<&2, M.CmBlock>) -> String:
  Check.maybe (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/check.bend&name=maybe)
   def maybe(m: Maybe<&2, M.CmBlock>) -> String:
  Check.main (https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/check.bend&name=main)
   def main() -> IO(Unit):
More: https://jend.leeeet.dev/packages/bend-osdev-mode-core.txt?definitions_offset=100