val sigma256_1_1: x:nat32 -> Tot (nat32)
let sigma256_1_1 x = v (_Sigma1 SHA2_256 (uint_to_t x))
val sigma256_1_1: x:nat32 -> Tot (nat32)
let sigma256_1_1 x =
v (_Sigma1 SHA2_256 (uint_to_t x))
Vale.SHA2.Wrapper.fst.checked
Spec.SHA2.fst.checked Spec.SHA2.fst.checked Spec.Agile.Hash.fsti.checked prims.fst.checked Lib.IntTypes.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked
Vale.SHA2.Wrapper.fst
Vale.Def.Words_s.nat32 FStar.UInt32.v Spec.SHA2._Sigma1 Spec.Hash.Definitions.SHA2_256 FStar.UInt32.uint_to_t
module Vale.SHA2.Wrapper

open FStar.UInt32
open Spec.Agile.Hash
open Spec.SHA2
friend Lib.IntTypes
friend Spec.SHA2

let sigma256_0_0 x = v (_sigma0 SHA2_256 (uint_to_t x))

let sigma256_0_1 x = v (_sigma1 SHA2_256 (uint_to_t x))

let sigma256_1_0 x = v (_Sigma0 SHA2_256 (uint_to_t x))
val sigma256_1_1: x:nat32 -> Tot (nat32)
x: Vale.Def.Words_s.nat32 -> Vale.Def.Words_s.nat32