PROOF.ap.cipher_inv: def of bend-osdev-aes@0.1.0.0
Import: import bend-osdev-aes@0.1.0.0/PROOF.bend as PROOF
Lines 2175-2184 of bend-osdev-aes@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&start_line=2175&end_line=2184

import Base
import bend-osdev-aes@0.1.0.0/aes.bend as X
import bend-collections@1.0.0.0/src/crypto/aes/aes.bend as A
import bend-collections@1.0.0.0/src/crypto/aes/types.bend as TT

def ap.cipher_inv(+nr: Nat, ks: List<&2, TT.State>, +s: TT.State) -> {X.aes.inv_cipher(nr, X.aes.mask_keys(ks), A.cipher(nr, X.aes.mask(s), X.aes.mask_keys(ks))) == X.aes.mask(s) : TT.State}:
  match ks:
    case Con{+k, rest}:
      %Equal.sym(TT.State, A.add_round_key(X.aes.mask(s), X.aes.mask(k)), X.aes.mask(A.add_round_key(X.aes.mask(s), X.aes.mask(k))), ap.arkl(s, k)) : {X.aes.mask(A.add_round_key(X.aes.inv_rounds(Nat.sub(nr, 1n), X.aes.mask_keys(rest), A.rounds(Nat.sub(nr, 1n), _, X.aes.mask_keys(rest))), X.aes.mask(k))) == X.aes.mask(s) : TT.State}
      %Equal.sym(TT.State, X.aes.inv_rounds(Nat.sub(nr, 1n), X.aes.mask_keys(rest), A.rounds(Nat.sub(nr, 1n), X.aes.mask(A.add_round_key(X.aes.mask(s), X.aes.mask(k))), X.aes.mask_keys(rest))), X.aes.mask(A.add_round_key(X.aes.mask(s), X.aes.mask(k))), ap.rounds_inv(Nat.sub(nr, 1n), rest, A.add_round_key(X.aes.mask(s), X.aes.mask(k)))) : {X.aes.mask(A.add_round_key(_, X.aes.mask(k))) == X.aes.mask(s) : TT.State}
      %ap.arkl(s, k) : {X.aes.mask(A.add_round_key(_, X.aes.mask(k))) == X.aes.mask(s) : TT.State}
      %Equal.sym(TT.State, A.add_round_key(A.add_round_key(X.aes.mask(s), X.aes.mask(k)), X.aes.mask(k)), X.aes.mask(s), ap.ark2(X.aes.mask(s), X.aes.mask(k))) : {X.aes.mask(_) == X.aes.mask(s) : TT.State}
      ap.mm(s)
    case Nil{}:
      ap.mm(s)

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/aes/aes.bend&name=add_round_key
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/aes/aes.bend&name=cipher
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/aes/aes.bend&name=rounds
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/aes/types.bend&name=State
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.ark2
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.arkl
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.mm
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.rounds_inv
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/aes.bend&name=aes.inv_cipher
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/aes.bend&name=aes.inv_rounds
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/aes.bend&name=aes.mask
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/aes.bend&name=aes.mask_keys