val twenty : Type0
let twenty = normalize (nat_t_of_nat 20)
module HaclExample
open Steel.ST.GenElim
open Steel.ST.C.Types
open Steel.C.Typenat
open Steel.C.Typestring
open Steel.ST.C.Types.Struct.Aux
open Steel.ST.C.Types.UserStruct // hides Struct

module SZ = FStar.SizeT
module U64 = FStar.UInt64

(** In this file we demonstrate how Steel could be used to manipulate the following data type used in Hacl*:
      https://github.com/project-everest/hacl-star/blob/master/code/poly1305/Hacl.Impl.Poly1305.fsti#L18
    This Low* definition amounts to the struct definition
      struct poly1305_ctx { uint64_t limbs[5]; uint64_t precomp[20]; };
    and, with our new model of structs and arrays and pointer-to-field, can be expresesd directly in Steel.

    See PointStruct.fst for more detailed explanations of the various definitions needed below.
*)
/
Steel.ST.GenElim.fsti.checked Steel.ST.C.Types.UserStruct.fsti.checked Steel.ST.C.Types.Struct.Aux.fsti.checked Steel.ST.C.Types.fst.checked Steel.C.Typestring.fsti.checked Steel.C.Typenat.fsti.checked prims.fst.checked FStar.UInt64.fsti.checked FStar.SizeT.fsti.checked FStar.Set.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked
HaclExample.fst
Type0
FStar.Pervasives.normalize Steel.C.Typenat.nat_t_of_nat
let twenty =
  
normalize (nat_t_of_nat 20)