def expand_step

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

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

13def expand_step(+fuel: Nat, +i: U32, +rcon: U32, +words: List<&2, U32>,
14    +next_words: List<&2, U32>, +next_rcon: U32,
15    words_match: {List.append(&2, U32, words, [next_word(i, rcon, words)]) == next_words : List<&2, U32>},
16    rcon_match: {Core.aes_rcon_kind(rcon, U32.is_eq(U32.mod(i, 8), 0)) == next_rcon : U32}) ->
17    {Core.aes_expand.go(1n+fuel, i, rcon, words) ==
18     Core.aes_expand.go(fuel, U32.add(i, 1), next_rcon, next_words) : List<&2, U32>}:
19    +actual_rcon = Core.aes_rcon_kind(rcon, U32.is_eq(U32.mod(i, 8), 0))
20    Equal.trans(List<&2, U32>, Core.aes_expand.go(1n+fuel, i, rcon, words),
21        Core.aes_expand.go(fuel, U32.add(i, 1), actual_rcon, next_words),
22        Core.aes_expand.go(fuel, U32.add(i, 1), next_rcon, next_words),
23        Equal.cong(List<&2, U32>, List<&2, U32>,
24            value => Core.aes_expand.go(fuel, U32.add(i, 1), actual_rcon, value),
25            List.append(&2, U32, words, [next_word(i, rcon, words)]), next_words, words_match),
26        Equal.cong(U32, List<&2, U32>, value => Core.aes_expand.go(fuel, U32.add(i, 1), value, next_words),
27            actual_rcon, next_rcon, rcon_match))