def expand_step_at

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

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

38def expand_step_at(+fuel: Nat, +i: U32, +rcon: U32, +words: List<&2, U32>,
39    +next_words: List<&2, U32>, +next_rcon: U32, +next_i: U32,
40    words_match: {List.append(&2, U32, words, [next_word(i, rcon, words)]) == next_words : List<&2, U32>},
41    rcon_match: {Core.aes_rcon_kind(rcon, U32.is_eq(U32.mod(i, 8), 0)) == next_rcon : U32},
42    index_match: {U32.add(i, 1) == next_i : U32}) ->
43    {Core.aes_expand.go(1n+fuel, i, rcon, words) ==
44     Core.aes_expand.go(fuel, next_i, next_rcon, next_words) : List<&2, U32>}:
45    Equal.trans(List<&2, U32>, Core.aes_expand.go(1n+fuel, i, rcon, words),
46        Core.aes_expand.go(fuel, U32.add(i, 1), next_rcon, next_words),
47        Core.aes_expand.go(fuel, next_i, next_rcon, next_words),
48        expand_step(fuel, i, rcon, words, next_words, next_rcon, words_match, rcon_match),
49        Equal.cong(U32, List<&2, U32>, value => Core.aes_expand.go(fuel, value, next_rcon, next_words),
50            U32.add(i, 1), next_i, index_match))