val lemma_reveal_expand_key_256 (key: aes_key_LE AES_256) (round: nat)
    : Lemma
    (expand_key_256 key round ==
      (if round = 0
        then Mkfour key.[ 0 ] key.[ 1 ] key.[ 2 ] key.[ 3 ]
        else
          if round = 1
          then Mkfour key.[ 4 ] key.[ 5 ] key.[ 6 ] key.[ 7 ]
          else round_key_256 (expand_key_256 key (round - 2)) (expand_key_256 key (round - 1)) round
      ))
let lemma_reveal_expand_key_256 (key:aes_key_LE AES_256) (round:nat) : Lemma
  (expand_key_256 key round == (
    if round = 0 then Mkfour key.[0] key.[1] key.[2] key.[3]
    else if round = 1 then Mkfour key.[4] key.[5] key.[6] key.[7]
    else round_key_256 (expand_key_256 key (round - 2)) (expand_key_256 key (round - 1)) round
  ))
  =
  expand_key_256_reveal ()
val lemma_reveal_expand_key_256 (key: aes_key_LE AES_256) (round: nat)
    : Lemma
    (expand_key_256 key round ==
      (if round = 0
        then Mkfour key.[ 0 ] key.[ 1 ] key.[ 2 ] key.[ 3 ]
        else
          if round = 1
          then Mkfour key.[ 4 ] key.[ 5 ] key.[ 6 ] key.[ 7 ]
          else round_key_256 (expand_key_256 key (round - 2)) (expand_key_256 key (round - 1)) round
      ))
let lemma_reveal_expand_key_256 (key: aes_key_LE AES_256) (round: nat)
    : Lemma
    (expand_key_256 key round ==
      (if round = 0
        then Mkfour key.[ 0 ] key.[ 1 ] key.[ 2 ] key.[ 3 ]
        else
          if round = 1
          then Mkfour key.[ 4 ] key.[ 5 ] key.[ 6 ] key.[ 7 ]
          else round_key_256 (expand_key_256 key (round - 2)) (expand_key_256 key (round - 1)) round
      )) =
expand_key_256_reveal ()
Vale.AES.AES256_helpers.fst.checked
Vale.Arch.Types.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.AES.AES256_helpers.fst
Vale.AES.AES_s.aes_key_LE Vale.AES.AES_common_s.AES_256 Prims.nat Vale.AES.AES256_helpers.expand_key_256_reveal Prims.unit Prims.l_True Prims.squash Prims.eq2 Vale.Def.Words_s.four Vale.Def.Types_s.nat32 Vale.AES.AES256_helpers.expand_key_256 Prims.op_Equality Prims.int Vale.Def.Words_s.Mkfour Vale.AES.AES256_helpers.op_String_Access Prims.bool Vale.AES.AES256_helpers.round_key_256 Prims.op_Subtraction Prims.Nil FStar.Pervasives.pattern
module Vale.AES.AES256_helpers

let lemma_reveal_expand_key_256 (key:aes_key_LE AES_256) (round:nat) : Lemma
  (expand_key_256 key round == (
    if round = 0 then Mkfour key.[0] key.[1] key.[2] key.[3]
    else if round = 1 then Mkfour key.[4] key.[5] key.[6] key.[7]
    else round_key_256 (expand_key_256 key (round - 2)) (expand_key_256 key (round - 1)) round
  ))
val lemma_reveal_expand_key_256 (key: aes_key_LE AES_256) (round: nat)
    : Lemma
    (expand_key_256 key round ==
      (if round = 0
        then Mkfour key.[ 0 ] key.[ 1 ] key.[ 2 ] key.[ 3 ]
        else
          if round = 1
          then Mkfour key.[ 4 ] key.[ 5 ] key.[ 6 ] key.[ 7 ]
          else round_key_256 (expand_key_256 key (round - 2)) (expand_key_256 key (round - 1)) round
      ))
key: Vale.AES.AES_s.aes_key_LE Vale.AES.AES_common_s.AES_256 -> round: Prims.nat
  -> FStar.Pervasives.Lemma
    (ensures
      Vale.AES.AES256_helpers.expand_key_256 key round ==
      (match round = 0 with
        | true -> Vale.Def.Words_s.Mkfour key.[ 0 ] key.[ 1 ] key.[ 2 ] key.[ 3 ]
        | _ ->
          (match round = 1 with
            | true -> Vale.Def.Words_s.Mkfour key.[ 4 ] key.[ 5 ] key.[ 6 ] key.[ 7 ]
            | _ ->
              Vale.AES.AES256_helpers.round_key_256 (Vale.AES.AES256_helpers.expand_key_256 key
                    (round - 2))
                (Vale.AES.AES256_helpers.expand_key_256 key (round - 1))
                round)
          <:
          Vale.Def.Words_s.four Vale.Def.Types_s.nat32))