PROOF.ap.rounds_out: def of bend-osdev-aes@0.1.0.0
Import: import bend-osdev-aes@0.1.0.0/PROOF.bend as PROOF
Lines 2141-2151 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=2141&end_line=2151

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.rounds_out(n: Nat, ks: List<&2, TT.State>, +z: TT.State) -> {A.rounds(n, X.aes.mask(z), X.aes.mask_keys(ks)) == X.aes.mask(A.rounds(n, X.aes.mask(z), X.aes.mask_keys(ks))) : TT.State}:
  match n ks:
    case 0n Con{+k, rest}:
      ap.last_out(z, k)
    case 1n+p Con{+k, rest}:
      %Equal.sym(TT.State, A.round(X.aes.mask(z), X.aes.mask(k)), X.aes.mask(A.round(X.aes.mask(z), X.aes.mask(k))), ap.round_out(z, k)) : {A.rounds(p, _, X.aes.mask_keys(rest)) == X.aes.mask(A.rounds(p, _, X.aes.mask_keys(rest))) : TT.State}
      ap.rounds_out(p, rest, A.round(X.aes.mask(z), X.aes.mask(k)))
    case 0n Nil{}:
      Equal.sym(TT.State, X.aes.mask(X.aes.mask(z)), X.aes.mask(z), ap.mm(z))
    case 1n+p Nil{}:
      Equal.sym(TT.State, X.aes.mask(X.aes.mask(z)), X.aes.mask(z), ap.mm(z))

Uses (11):
  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=bend-collections@1.0.0.0/src/crypto/aes/aes.bend&name=round
  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.last_out
  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.round_out
  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