proof/AES_NistCtr2ComposeProof.bend source

proof/AES_NistCtr2ComposeProof.bend on the hub · documented module

import Baseimport ../libs/AES256GCMCore.bend as Coreimport ./AES_NistKeyScheduleProof.bend as Keyimport ./AES_NistCtr2BlockProof.bend as Blockimport ./AES_TraceProof.bend as Traceimport ./AES_BlockBridgeProof.bend as Bridge# Symbolic remaining fuel prevents every suffix from recomputing the rounds after it.def suffix_1(+fuel: Nat) ->    {Core.aes_rounds.go(1n+(fuel), Block.state_12(), Key.words_60(), 13n) ==     Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:    Equal.trans(List<&2, U32>,        Core.aes_rounds.go(1n+(fuel), Block.state_12(), Key.words_60(), 13n),        Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),        Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),        Trace.rounds_step_at(fuel, Block.state_12(), Key.words_60(), 13n,            Block.state_13(), 14n, Block.round_13_matches(), {==}), {==})def suffix_2(+fuel: Nat) ->    {Core.aes_rounds.go(1n+(1n+(fuel)), Block.state_11(), Key.words_60(), 12n) ==     Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:    Equal.trans(List<&2, U32>,        Core.aes_rounds.go(1n+(1n+(fuel)), Block.state_11(), Key.words_60(), 12n),        Core.aes_rounds.go(1n+(fuel), Block.state_12(), Key.words_60(), 13n),        Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),        Trace.rounds_step_at(1n+(fuel), Block.state_11(), Key.words_60(), 12n,            Block.state_12(), 13n, Block.round_12_matches(), {==}),        suffix_1(fuel))def suffix_3(+fuel: Nat) ->    {Core.aes_rounds.go(1n+(1n+(1n+(fuel))), Block.state_10(), Key.words_60(), 11n) ==     Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:    Equal.trans(List<&2, U32>,        Core.aes_rounds.go(1n+(1n+(1n+(fuel))), Block.state_10(), Key.words_60(), 11n),        Core.aes_rounds.go(1n+(1n+(fuel)), Block.state_11(), Key.words_60(), 12n),        Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),        Trace.rounds_step_at(1n+(1n+(fuel)), Block.state_10(), Key.words_60(), 11n,            Block.state_11(), 12n, Block.round_11_matches(), {==}),        suffix_2(fuel))def suffix_4(+fuel: Nat) ->    {Core.aes_rounds.go(1n+(1n+(1n+(1n+(fuel)))), Block.state_9(), Key.words_60(), 10n) ==     Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:    Equal.trans(List<&2, U32>,        Core.aes_rounds.go(1n+(1n+(1n+(1n+(fuel)))), Block.state_9(), Key.words_60(), 10n),        Core.aes_rounds.go(1n+(1n+(1n+(fuel))), Block.state_10(), Key.words_60(), 11n),        Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),        Trace.rounds_step_at(1n+(1n+(1n+(fuel))), Block.state_9(), Key.words_60(), 10n,            Block.state_10(), 11n, Block.round_10_matches(), {==}),        suffix_3(fuel))def suffix_5(+fuel: Nat) ->    {Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(fuel))))), Block.state_8(), Key.words_60(), 9n) ==     Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:    Equal.trans(List<&2, U32>,        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(fuel))))), Block.state_8(), Key.words_60(), 9n),        Core.aes_rounds.go(1n+(1n+(1n+(1n+(fuel)))), Block.state_9(), Key.words_60(), 10n),        Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),        Trace.rounds_step_at(1n+(1n+(1n+(1n+(fuel)))), Block.state_8(), Key.words_60(), 9n,            Block.state_9(), 10n, Block.round_9_matches(), {==}),        suffix_4(fuel))def suffix_6(+fuel: Nat) ->    {Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))), Block.state_7(), Key.words_60(), 8n) ==     Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:    Equal.trans(List<&2, U32>,        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))), Block.state_7(), Key.words_60(), 8n),        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(fuel))))), Block.state_8(), Key.words_60(), 9n),        Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),        Trace.rounds_step_at(1n+(1n+(1n+(1n+(1n+(fuel))))), Block.state_7(), Key.words_60(), 8n,            Block.state_8(), 9n, Block.round_8_matches(), {==}),        suffix_5(fuel))def suffix_7(+fuel: Nat) ->    {Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))), Block.state_6(), Key.words_60(), 7n) ==     Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:    Equal.trans(List<&2, U32>,        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))), Block.state_6(), Key.words_60(), 7n),        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))), Block.state_7(), Key.words_60(), 8n),        Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),        Trace.rounds_step_at(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))), Block.state_6(), Key.words_60(), 7n,            Block.state_7(), 8n, Block.round_7_matches(), {==}),        suffix_6(fuel))def suffix_8(+fuel: Nat) ->    {Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))))), Block.state_5(), Key.words_60(), 6n) ==     Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:    Equal.trans(List<&2, U32>,        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))))), Block.state_5(), Key.words_60(), 6n),        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))), Block.state_6(), Key.words_60(), 7n),        Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),        Trace.rounds_step_at(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))), Block.state_5(), Key.words_60(), 6n,            Block.state_6(), 7n, Block.round_6_matches(), {==}),        suffix_7(fuel))def suffix_9(+fuel: Nat) ->    {Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))), Block.state_4(), Key.words_60(), 5n) ==     Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:    Equal.trans(List<&2, U32>,        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))), Block.state_4(), Key.words_60(), 5n),        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))))), Block.state_5(), Key.words_60(), 6n),        Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),        Trace.rounds_step_at(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))))), Block.state_4(), Key.words_60(), 5n,            Block.state_5(), 6n, Block.round_5_matches(), {==}),        suffix_8(fuel))def suffix_10(+fuel: Nat) ->    {Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))))))), Block.state_3(), Key.words_60(), 4n) ==     Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:    Equal.trans(List<&2, U32>,        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))))))), Block.state_3(), Key.words_60(), 4n),        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))), Block.state_4(), Key.words_60(), 5n),        Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),        Trace.rounds_step_at(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))), Block.state_3(), Key.words_60(), 4n,            Block.state_4(), 5n, Block.round_4_matches(), {==}),        suffix_9(fuel))def suffix_11(+fuel: Nat) ->    {Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))))), Block.state_2(), Key.words_60(), 3n) ==     Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:    Equal.trans(List<&2, U32>,        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))))), Block.state_2(), Key.words_60(), 3n),        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))))))), Block.state_3(), Key.words_60(), 4n),        Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),        Trace.rounds_step_at(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))))))), Block.state_2(), Key.words_60(), 3n,            Block.state_3(), 4n, Block.round_3_matches(), {==}),        suffix_10(fuel))def suffix_12(+fuel: Nat) ->    {Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))))))))), Block.state_1(), Key.words_60(), 2n) ==     Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:    Equal.trans(List<&2, U32>,        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))))))))), Block.state_1(), Key.words_60(), 2n),        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))))), Block.state_2(), Key.words_60(), 3n),        Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),        Trace.rounds_step_at(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))))), Block.state_1(), Key.words_60(), 2n,            Block.state_2(), 3n, Block.round_2_matches(), {==}),        suffix_11(fuel))def suffix_13(+fuel: Nat) ->    {Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))))))), Block.state_0(), Key.words_60(), 1n) ==     Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:    Equal.trans(List<&2, U32>,        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))))))), Block.state_0(), Key.words_60(), 1n),        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))))))))), Block.state_1(), Key.words_60(), 2n),        Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),        Trace.rounds_step_at(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))))))))), Block.state_0(), Key.words_60(), 1n,            Block.state_1(), 2n, Block.round_1_matches(), {==}),        suffix_12(fuel))def chunk_0(+fuel: Nat) ->    {Core.aes_rounds.go(1n+(1n+(1n+(fuel))), Block.state_0(), Key.words_60(), 1n) ==     Core.aes_rounds.go(fuel, Block.state_3(), Key.words_60(), 4n) : List<&2, U32>}:    Equal.trans(List<&2, U32>,        Core.aes_rounds.go(1n+(1n+(1n+(fuel))), Block.state_0(), Key.words_60(), 1n),        Core.aes_rounds.go(1n+(1n+(fuel)), Block.state_1(), Key.words_60(), 2n),        Core.aes_rounds.go(fuel, Block.state_3(), Key.words_60(), 4n),        Trace.rounds_step_at(1n+(1n+(fuel)), Block.state_0(), Key.words_60(), 1n,            Block.state_1(), 2n, Block.round_1_matches(), {==}),        Equal.trans(List<&2, U32>,            Core.aes_rounds.go(1n+(1n+(fuel)), Block.state_1(), Key.words_60(), 2n),            Core.aes_rounds.go(1n+(fuel), Block.state_2(), Key.words_60(), 3n),            Core.aes_rounds.go(fuel, Block.state_3(), Key.words_60(), 4n),            Trace.rounds_step_at(1n+(fuel), Block.state_1(), Key.words_60(), 2n,                Block.state_2(), 3n, Block.round_2_matches(), {==}),            Trace.rounds_step_at(fuel, Block.state_2(), Key.words_60(), 3n,                Block.state_3(), 4n, Block.round_3_matches(), {==})))def chunk_3(+fuel: Nat) ->    {Core.aes_rounds.go(1n+(1n+(1n+(fuel))), Block.state_3(), Key.words_60(), 4n) ==     Core.aes_rounds.go(fuel, Block.state_6(), Key.words_60(), 7n) : List<&2, U32>}:    Equal.trans(List<&2, U32>,        Core.aes_rounds.go(1n+(1n+(1n+(fuel))), Block.state_3(), Key.words_60(), 4n),        Core.aes_rounds.go(1n+(1n+(fuel)), Block.state_4(), Key.words_60(), 5n),        Core.aes_rounds.go(fuel, Block.state_6(), Key.words_60(), 7n),        Trace.rounds_step_at(1n+(1n+(fuel)), Block.state_3(), Key.words_60(), 4n,            Block.state_4(), 5n, Block.round_4_matches(), {==}),        Equal.trans(List<&2, U32>,            Core.aes_rounds.go(1n+(1n+(fuel)), Block.state_4(), Key.words_60(), 5n),            Core.aes_rounds.go(1n+(fuel), Block.state_5(), Key.words_60(), 6n),            Core.aes_rounds.go(fuel, Block.state_6(), Key.words_60(), 7n),            Trace.rounds_step_at(1n+(fuel), Block.state_4(), Key.words_60(), 5n,                Block.state_5(), 6n, Block.round_5_matches(), {==}),            Trace.rounds_step_at(fuel, Block.state_5(), Key.words_60(), 6n,                Block.state_6(), 7n, Block.round_6_matches(), {==})))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(), {==})))def chunk_9(+fuel: Nat) ->    {Core.aes_rounds.go(1n+(1n+(1n+(fuel))), Block.state_9(), Key.words_60(), 10n) ==     Core.aes_rounds.go(fuel, Block.state_12(), Key.words_60(), 13n) : List<&2, U32>}:    Equal.trans(List<&2, U32>,        Core.aes_rounds.go(1n+(1n+(1n+(fuel))), Block.state_9(), Key.words_60(), 10n),        Core.aes_rounds.go(1n+(1n+(fuel)), Block.state_10(), Key.words_60(), 11n),        Core.aes_rounds.go(fuel, Block.state_12(), Key.words_60(), 13n),        Trace.rounds_step_at(1n+(1n+(fuel)), Block.state_9(), Key.words_60(), 10n,            Block.state_10(), 11n, Block.round_10_matches(), {==}),        Equal.trans(List<&2, U32>,            Core.aes_rounds.go(1n+(1n+(fuel)), Block.state_10(), Key.words_60(), 11n),            Core.aes_rounds.go(1n+(fuel), Block.state_11(), Key.words_60(), 12n),            Core.aes_rounds.go(fuel, Block.state_12(), Key.words_60(), 13n),            Trace.rounds_step_at(1n+(fuel), Block.state_10(), Key.words_60(), 11n,                Block.state_11(), 12n, Block.round_11_matches(), {==}),            Trace.rounds_step_at(fuel, Block.state_11(), Key.words_60(), 12n,                Block.state_12(), 13n, Block.round_12_matches(), {==})))def rounds_0_to_6(+fuel: Nat) ->    {Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))))))), Block.state_0(), Key.words_60(), 1n) == Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))), Block.state_6(), Key.words_60(), 7n) : List<&2, U32>}:    Equal.trans(List<&2, U32>,        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))))))), Block.state_0(), Key.words_60(), 1n), Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))))))), Block.state_3(), Key.words_60(), 4n), Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))), Block.state_6(), Key.words_60(), 7n),        chunk_0(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))))),        chunk_3(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))))))def rounds_6_to_12(+fuel: Nat) ->    {Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))), Block.state_6(), Key.words_60(), 7n) == Core.aes_rounds.go(1n+(fuel), Block.state_12(), Key.words_60(), 13n) : List<&2, U32>}:    Equal.trans(List<&2, U32>,        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))), Block.state_6(), Key.words_60(), 7n), Core.aes_rounds.go(1n+(1n+(1n+(1n+(fuel)))), Block.state_9(), Key.words_60(), 10n), Core.aes_rounds.go(1n+(fuel), Block.state_12(), Key.words_60(), 13n),        chunk_6(1n+(1n+(1n+(1n+(fuel))))),        chunk_9(1n+(fuel)))def full_rounds_match(+fuel: Nat) ->    {Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))))))), Block.state_0(), Key.words_60(), 1n) == Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:    Equal.trans(List<&2, U32>,        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))))))), Block.state_0(), Key.words_60(), 1n), Core.aes_rounds.go(1n+(fuel), Block.state_12(), Key.words_60(), 13n), Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),        Equal.trans(List<&2, U32>,            Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))))))), Block.state_0(), Key.words_60(), 1n), Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))), Block.state_6(), Key.words_60(), 7n), Core.aes_rounds.go(1n+(fuel), Block.state_12(), Key.words_60(), 13n), rounds_0_to_6(fuel), rounds_6_to_12(fuel)),        suffix_1(fuel))def full_nist_rounds_match() ->    {Core.aes_rounds.go(13n, Block.state_0(), Key.words_60(), 1n) == Core.aes_rounds.go(0n, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:    Equal.trans(List<&2, U32>,        Core.aes_rounds.go(13n, Block.state_0(), Key.words_60(), 1n),        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(0n))))))))))))), Block.state_0(), Key.words_60(), 1n),        Core.aes_rounds.go(0n, Block.state_13(), Key.words_60(), 14n),        Trace.rounds_fuel_matches(13n, 1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(0n))))))))))))), Block.state_0(), Key.words_60(), 1n, {==}), full_rounds_match(0n))def final_nist_block_match() ->    {Core.aes_rounds.go(13n, Block.state_0(), Key.words_60(), 1n) == Block.result() : List<&2, U32>}:    Equal.trans(List<&2, U32>,        Core.aes_rounds.go(13n, Block.state_0(), Key.words_60(), 1n),        Core.aes_rounds.go(0n, Block.state_13(), Key.words_60(), 14n),        Block.result(), full_nist_rounds_match(), Block.final_matches())def expanded_block_matches() ->    {Core.aes256_encrypt_expanded(Key.words_60(), Block.block()) == Block.result() : List<&2, U32>}:    Bridge.expanded_block_from_initial(Key.words_60(), Block.block(), Block.state_0(),        Block.result(), Block.initial_matches(), final_nist_block_match())