def li.len_xor

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

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

1633def li.len_xor(xs: List<&2, U32>, ys: List<&2, U32>) -> {Nat.is_le(B.len(xs), B.len(ys)) == True{} : Bool} -> {B.len(M.cm.xor_bytes(xs, ys)) == B.len(xs) : Nat}:
1634  match xs:
1635    case Nil{}:
1636      h => {==}
1637    case Con{+a, +s}:
1638      match ys:
1639        case Nil{}:
1640          h => bo.absurd({B.len(M.cm.xor_bytes(Con{a, s}, Nil{})) == B.len(Con{a, s}) : Nat}, h)
1641        case Con{+b, +t}:
1642          h => %li.len_xor(s, t)(h) : {1n+B.len(M.cm.xor_bytes(s, t)) == 1n+_ : Nat}
1643            {==}