AESTraceProof.expand_step: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_TraceProof.bend as AESTraceProof
Lines 13-27 of qasim-bend-kit@0.1.0.2/proof/AES_TraceProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_TraceProof.bend&start_line=13&end_line=27

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend as Core

def expand_step(+fuel: Nat, +i: U32, +rcon: U32, +words: List<&2, U32>,
    +next_words: List<&2, U32>, +next_rcon: U32,
    words_match: {List.append(&2, U32, words, [next_word(i, rcon, words)]) == next_words : List<&2, U32>},
    rcon_match: {Core.aes_rcon_kind(rcon, U32.is_eq(U32.mod(i, 8), 0)) == next_rcon : U32}) ->
    {Core.aes_expand.go(1n+fuel, i, rcon, words) ==
     Core.aes_expand.go(fuel, U32.add(i, 1), next_rcon, next_words) : List<&2, U32>}:
    +actual_rcon = Core.aes_rcon_kind(rcon, U32.is_eq(U32.mod(i, 8), 0))
    Equal.trans(List<&2, U32>, Core.aes_expand.go(1n+fuel, i, rcon, words),
        Core.aes_expand.go(fuel, U32.add(i, 1), actual_rcon, next_words),
        Core.aes_expand.go(fuel, U32.add(i, 1), next_rcon, next_words),
        Equal.cong(List<&2, U32>, List<&2, U32>,
            value => Core.aes_expand.go(fuel, U32.add(i, 1), actual_rcon, value),
            List.append(&2, U32, words, [next_word(i, rcon, words)]), next_words, words_match),
        Equal.cong(U32, List<&2, U32>, value => Core.aes_expand.go(fuel, U32.add(i, 1), value, next_words),
            actual_rcon, next_rcon, rcon_match))

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.mod
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=aes_expand.go
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=aes_rcon_kind
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_TraceProof.bend&name=next_word