AESNistHashBlockComposeProof.chunk_6: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_NistHashBlockComposeProof.bend as AESNistHashBlockComposeProof
Lines 188-204 of qasim-bend-kit@0.1.0.2/proof/AES_NistHashBlockComposeProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistHashBlockComposeProof.bend&start_line=188&end_line=204

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend as Core
import qasim-bend-kit@0.1.0.2/proof/AES_NistKeyScheduleProof.bend as Key
import qasim-bend-kit@0.1.0.2/proof/AES_NistHashBlockProof.bend as Block
import qasim-bend-kit@0.1.0.2/proof/AES_TraceProof.bend as Trace

def chunk_6(+fuel: Nat) ->
    {Core.aes_rounds.go(1n+(1n+(1n+(fuel))), Block.state_6(), Key.words_60(), 7n) ==
     Core.aes_rounds.go(fuel, Block.state_9(), Key.words_60(), 10n) : List<&2, U32>}:
    Equal.trans(List<&2, U32>,
        Core.aes_rounds.go(1n+(1n+(1n+(fuel))), Block.state_6(), Key.words_60(), 7n),
        Core.aes_rounds.go(1n+(1n+(fuel)), Block.state_7(), Key.words_60(), 8n),
        Core.aes_rounds.go(fuel, Block.state_9(), Key.words_60(), 10n),
        Trace.rounds_step_at(1n+(1n+(fuel)), Block.state_6(), Key.words_60(), 7n,
            Block.state_7(), 8n, Block.round_7_matches(), {==}),
        Equal.trans(List<&2, U32>,
            Core.aes_rounds.go(1n+(1n+(fuel)), Block.state_7(), Key.words_60(), 8n),
            Core.aes_rounds.go(1n+(fuel), Block.state_8(), Key.words_60(), 9n),
            Core.aes_rounds.go(fuel, Block.state_9(), Key.words_60(), 10n),
            Trace.rounds_step_at(1n+(fuel), Block.state_7(), Key.words_60(), 8n,
                Block.state_8(), 9n, Block.round_8_matches(), {==}),
            Trace.rounds_step_at(fuel, Block.state_8(), Key.words_60(), 9n,
                Block.state_9(), 10n, Block.round_9_matches(), {==})))

Uses (14):
  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=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=aes_rounds.go
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistHashBlockProof.bend&name=round_7_matches
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistHashBlockProof.bend&name=round_8_matches
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistHashBlockProof.bend&name=round_9_matches
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistHashBlockProof.bend&name=state_6
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistHashBlockProof.bend&name=state_7
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistHashBlockProof.bend&name=state_8
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistHashBlockProof.bend&name=state_9
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistKeyScheduleProof.bend&name=words_60
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_TraceProof.bend&name=rounds_step_at