def rounds_step

qasim-bend-kit@0.1.0.2 · proof/AES_TraceProof.bend:29

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

29def rounds_step(+fuel: Nat, +state: List<&2, U32>, +words: List<&2, U32>,
30    +round: Nat, +next_state: List<&2, U32>,
31    same: {Core.aes_middle_round(state, words, round) == next_state : List<&2, U32>}) ->
32    {Core.aes_rounds.go(1n+fuel, state, words, round) ==
33     Core.aes_rounds.go(fuel, next_state, words, (round + 1n : Nat)) : List<&2, U32>}:
34    Equal.cong(List<&2, U32>, List<&2, U32>,
35        value => Core.aes_rounds.go(fuel, value, words, (round + 1n : Nat)),
36        Core.aes_middle_round(state, words, round), next_state, same)