val full_union_set_field
      (#tn #tf: Type0)
      (#n: string)
      (#fields: field_description_t tf)
      (field: field_t fields)
      (v: fields.fd_type field)
    : Lemma (requires True)
      (ensures
        (full (union0 tn n fields) (union_set_field tn n fields field v) <==>
          full (fields.fd_typedef field) v))
      [SMTPat (full (union0 tn n fields) (union_set_field tn n fields field v))]
let full_union_set_field
  (#tn: Type0)
  (#tf: Type0)
  (#n: string)
  (#fields: field_description_t tf)
  (field: field_t fields)
  (v: fields.fd_type field)
: Lemma
  (requires True)
  (ensures (
    full (union0 tn n fields) (union_set_field tn n fields field v) <==> full (fields.fd_typedef field) v
  ))
  [SMTPat (full (union0 tn n fields) (union_set_field tn n fields field v))]
= Classical.move_requires (full_union_set_field_intro #tn #tf #n #fields field) v;
  Classical.move_requires (full_union_set_field_elim #tn #tf #n #fields field) v
val full_union_set_field
      (#tn #tf: Type0)
      (#n: string)
      (#fields: field_description_t tf)
      (field: field_t fields)
      (v: fields.fd_type field)
    : Lemma (requires True)
      (ensures
        (full (union0 tn n fields) (union_set_field tn n fields field v) <==>
          full (fields.fd_typedef field) v))
      [SMTPat (full (union0 tn n fields) (union_set_field tn n fields field v))]
let full_union_set_field
      (#tn #tf: Type0)
      (#n: string)
      (#fields: field_description_t tf)
      (field: field_t fields)
      (v: fields.fd_type field)
    : Lemma (requires True)
      (ensures
        (full (union0 tn n fields) (union_set_field tn n fields field v) <==>
          full (fields.fd_typedef field) v))
      [SMTPat (full (union0 tn n fields) (union_set_field tn n fields field v))] =
Classical.move_requires (full_union_set_field_intro #tn #tf #n #fields field) v;
Classical.move_requires (full_union_set_field_elim #tn #tf #n #fields field) v
Steel.ST.C.Types.Union.fsti.checked
Steel.ST.Util.fsti.checked Steel.ST.C.Types.Fields.fsti.checked Steel.FractionalPermission.fst.checked Steel.C.Typestring.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked FStar.Classical.fsti.checked
Steel.ST.C.Types.Union.fsti
Prims.string Steel.ST.C.Types.Fields.field_description_t Steel.ST.C.Types.Fields.field_t Steel.ST.C.Types.Fields.__proj__Mkfield_description_t__item__fd_type FStar.Classical.move_requires Steel.ST.C.Types.Base.full Steel.ST.C.Types.Union.union_t0 Steel.ST.C.Types.Union.union0 Steel.ST.C.Types.Union.union_set_field Steel.ST.C.Types.Fields.__proj__Mkfield_description_t__item__fd_typedef Steel.ST.C.Types.Union.full_union_set_field_elim Prims.unit Steel.ST.C.Types.Union.full_union_set_field_intro Prims.l_True Prims.squash Prims.l_iff Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.prop Prims.Nil
module Steel.ST.C.Types.Union
open Steel.ST.Util
include Steel.ST.C.Types.Fields
open Steel.C.Typestring

module P = Steel.FractionalPermission

[@@noextract_to "krml"] // primitive
val define_union0 (tn: Type0) (#tf: Type0) (n: string) (fields: field_description_t tf) : Tot Type0
inline_for_extraction [@@noextract_to "krml"]
let define_union (n: string) (#tf: Type0) (#tn: Type0) (#[solve_mk_string_t ()] prf: squash (norm norm_typestring (mk_string_t n == tn))) (fields: field_description_t tf) : Tot Type0
= define_union0 tn #tf n fields

// To be extracted as: union t
[@@noextract_to "krml"] // primitive
val union_t0 (tn: Type0) (#tf: Type0) (n: string) (fields: field_description_t tf) : Tot Type0
inline_for_extraction [@@noextract_to "krml"]
let union_t (#tf: Type0) (n: string) (#tn: Type0) (# [solve_mk_string_t ()] prf: squash (norm norm_typestring (mk_string_t n == tn))) (fields: field_description_t tf) : Tot Type0
= union_t0 tn #tf n fields

val union_set_field (tn: Type0) (#tf: Type0) (n: string) (fields: field_description_t tf) (f: field_t fields) (v: fields.fd_type f) : GTot (union_t0 tn n fields)

val union_get_case
  (#tn: Type0)
  (#tf: Type0)
  (#n: string)
  (#fields: field_description_t tf)
  (u: union_t0 tn n fields)
: GTot (option (field_t fields))

val union_get_field
  (#tn: Type0)
  (#tf: Type0)
  (#n: string)
  (#fields: field_description_t tf)
  (u: union_t0 tn n fields)
  (field: field_t fields)
: Ghost (fields.fd_type field)
    (requires (union_get_case u == Some field))
    (ensures (fun _ -> True))

val union_get_field_same
  (tn: Type0)
  (#tf: Type0)
  (n: string)
  (fields: field_description_t tf)
  (field: field_t fields)
  (v: fields.fd_type field)
: Lemma
  (requires (~ (v == unknown (fields.fd_typedef field))))
  (ensures (
    let u = union_set_field tn n fields field v in
    union_get_case u == Some field /\
    union_get_field u field == v
  ))
  [SMTPatOr [
    [SMTPat (union_get_case (union_set_field tn n fields field v))];
    [SMTPat (union_get_field (union_set_field tn n fields field v) field)];
  ]]

val union_set_field_same
  (#tn: Type0)
  (#tf: Type0)
  (#n: string)
  (#fields: field_description_t tf)
  (s: union_t0 tn n fields)
  (field: field_t fields)
: Lemma
  (requires (union_get_case s == Some field))
  (ensures (
    union_set_field tn n fields field (union_get_field s field) == s
  ))
  [SMTPat (union_set_field tn n fields (union_get_field s field))]

[@@noextract_to "krml"] // proof-only
val union0 (tn: Type0) (#tf: Type0) (n: string) (fields: field_description_t tf) : Tot (typedef (union_t0 tn n fields))

inline_for_extraction
[@@noextract_to "krml"; norm_field_attr] // proof-only
let union (#tf: Type0) (n: string) (#tn: Type0) (# [solve_mk_string_t ()] prf: squash (norm norm_typestring (mk_string_t n == tn))) (fields: field_description_t tf) : Tot (typedef (union_t0 tn n fields))
= union0 tn #tf n fields

val union_get_case_unknown
  (tn: Type0)
  (#tf: Type0)
  (n: string)
  (fields: field_description_t tf)
: Lemma
  (union_get_case (unknown (union0 tn n fields)) == None)
  [SMTPat (unknown (union0 tn n fields))]

val union_set_field_unknown
  (tn: Type0)
  (#tf: Type0)
  (n: string)
  (fields: field_description_t tf)
  (field: field_t fields)
: Lemma
  (union_set_field tn n fields field (unknown (fields.fd_typedef field)) == unknown (union0 tn n fields))
  [SMTPat (union_set_field tn n fields field (unknown (fields.fd_typedef field)))]

val union_get_case_uninitialized
  (tn: Type0)
  (#tf: Type0)
  (n: string)
  (fields: field_description_t tf)
: Lemma
  (union_get_case (uninitialized (union0 tn n fields)) == None)
  [SMTPat (uninitialized (union0 tn n fields))]

val mk_fraction_union_get_case
  (#tn: Type0)
  (#tf: Type0)
  (#n: string)
  (#fields: field_description_t tf)
  (s: union_t0 tn n fields)
  (p: P.perm)
: Lemma
  (requires (fractionable (union0 tn n fields) s))
  (ensures (
    union_get_case (mk_fraction (union0 tn n fields) s p) == union_get_case s
  ))
  [SMTPat (union_get_case (mk_fraction (union0 tn n fields) s p))]

val fractionable_union_get_field
  (#tn: Type0)
  (#tf: Type0)
  (#n: string)
  (#fields: field_description_t tf)
  (s: union_t0 tn n fields)
  (field: field_t fields)
: Lemma
  (requires (union_get_case s == Some field))
  (ensures (
    fractionable (union0 tn n fields) s <==> fractionable (fields.fd_typedef field) (union_get_field s field)
  ))
  [SMTPat (fractionable (union0 tn n fields) s); SMTPat (union_get_field s field)]

val mk_fraction_union_get_field
  (#tn: Type0)
  (#tf: Type0)
  (#n: string)
  (#fields: field_description_t tf)
  (s: union_t0 tn n fields)
  (p: P.perm)
  (field: field_t fields)
: Lemma
  (requires (fractionable (union0 tn n fields) s /\ union_get_case s == Some field))
  (ensures (union_get_field (mk_fraction (union0 tn n fields) s p) field == mk_fraction (fields.fd_typedef field) (union_get_field s field) p))
  [SMTPat (union_get_field (mk_fraction (union0 tn n fields) s p) field)]

val mk_fraction_union_set_field
  (tn: Type0)
  (#tf: Type0)
  (n: string)
  (fields: field_description_t tf)
  (field: field_t fields)
  (v: fields.fd_type field)
  (p: P.perm)
: Lemma
  (requires (fractionable (fields.fd_typedef field) v))
  (ensures (
    fractionable (union0 tn n fields) (union_set_field tn n fields field v) /\
    mk_fraction (union0 tn n fields) (union_set_field tn n fields field v) p == union_set_field tn n fields field (mk_fraction (fields.fd_typedef field) v p)
  ))

val full_union
  (#tn: Type0)
  (#tf: Type0)
  (#n: string)
  (#fields: field_description_t tf)
  (s: union_t0 tn n fields)
  (field: field_t fields)
: Lemma
  (requires (union_get_case s == Some field))
  (ensures (
    full (union0 tn n fields) s <==> full (fields.fd_typedef field) (union_get_field s field)
  ))
  [SMTPat (full (union0 tn n fields) s); SMTPat (union_get_field s field)]

let full_union_set_field_intro
  (#tn: Type0)
  (#tf: Type0)
  (#n: string)
  (#fields: field_description_t tf)
  (field: field_t fields)
  (v: fields.fd_type field)
: Lemma
  (requires (full (fields.fd_typedef field) v))
  (ensures (
    full (union0 tn n fields) (union_set_field tn n fields field v)
  ))
= full_union (union_set_field tn n fields field v) field

let full_union_set_field_elim
  (#tn: Type0)
  (#tf: Type0)
  (#n: string)
  (#fields: field_description_t tf)
  (field: field_t fields)
  (v: fields.fd_type field)
: Lemma
  (requires (
    full (union0 tn n fields) (union_set_field tn n fields field v)
  ))
  (ensures (
    full (fields.fd_typedef field) v
  ))
= full_union (union_set_field tn n fields field v) field

let full_union_set_field
  (#tn: Type0)
  (#tf: Type0)
  (#n: string)
  (#fields: field_description_t tf)
  (field: field_t fields)
  (v: fields.fd_type field)
: Lemma
  (requires True)
  (ensures (
    full (union0 tn n fields) (union_set_field tn n fields field v) <==> full (fields.fd_typedef field) v
  ))
val full_union_set_field
      (#tn #tf: Type0)
      (#n: string)
      (#fields: field_description_t tf)
      (field: field_t fields)
      (v: fields.fd_type field)
    : Lemma (requires True)
      (ensures
        (full (union0 tn n fields) (union_set_field tn n fields field v) <==>
          full (fields.fd_typedef field) v))
      [SMTPat (full (union0 tn n fields) (union_set_field tn n fields field v))]
field: Steel.ST.C.Types.Fields.field_t fields -> v: Mkfield_description_t?.fd_type fields field
  -> FStar.Pervasives.Lemma
      (ensures
        Steel.ST.C.Types.Base.full (Steel.ST.C.Types.Union.union0 tn n fields)
          (Steel.ST.C.Types.Union.union_set_field tn n fields field v) <==>
        Steel.ST.C.Types.Base.full (Mkfield_description_t?.fd_typedef fields field) v)
      [
        SMTPat (Steel.ST.C.Types.Base.full (Steel.ST.C.Types.Union.union0 tn n fields)
              (Steel.ST.C.Types.Union.union_set_field tn n fields field v))
      ]