def ccmp.tag_le.go

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

import Base
import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M
import bend-osdev-cipher-modes@0.1.0.0/ccm.bend as CC

1742# checks that pass mean a tag of at most 16 bytes
1743def ccmp.tag_le.go(b: Bool, +m: Nat, +nl: Nat, +n: Nat, +u: Unit) -> {CC.ccm.tag_ok(m) == b : Bool} -> {CC.ccm.checks(m, nl, n) == Done{u} : Result<&2, &2, M.CmError, Unit>} -> {Nat.is_le(m, 16n) == True{} : Bool}:
1744  match b:
1745    case False{}:
1746      eb => h => rs.absurd({Nat.is_le(m, 16n) == True{} : Bool}, M.CmBadTagLength{m}, u, Equal.trans(Result<&2, &2, M.CmError, Unit>, CC.ccm.checks.tag(False{}, m, nl, n), CC.ccm.checks.tag(CC.ccm.tag_ok(m), m, nl, n), Done{u}, Equal.cong(Bool, Result<&2, &2, M.CmError, Unit>, x => CC.ccm.checks.tag(x, m, nl, n), False{}, CC.ccm.tag_ok(m), Equal.sym(Bool, CC.ccm.tag_ok(m), False{}, eb)), h))
1747    case True{}:
1748      eb => h => bo.and_l(Nat.is_le(m, 16n), Nat.is_eq(Nat.mod(m, 2n), 0n))(bo.and_r(Nat.is_le(4n, m), Bool.and(Nat.is_le(m, 16n), Nat.is_eq(Nat.mod(m, 2n), 0n)))(eb))