From 8aaa0188c7cfe1c3a0fbda1f3c3fa33253d78b86 Mon Sep 17 00:00:00 2001
From: Tahina Ramananandro <taramana@microsoft.com>
Date: Thu, 20 Jul 2023 11:07:58 -0700
Subject: [PATCH 1/3] unstruct_field_and_drop, struct_field1, and same for
 unions

---
 lib/steel/c/Steel.ST.C.Types.Struct.fsti | 40 ++++++++++++++++++++++++
 lib/steel/c/Steel.ST.C.Types.Union.fsti  | 34 ++++++++++++++++++++
 2 files changed, 74 insertions(+)

diff --git a/lib/steel/c/Steel.ST.C.Types.Struct.fsti b/lib/steel/c/Steel.ST.C.Types.Struct.fsti
index cc0ceecaa..3505f6238 100644
--- a/lib/steel/c/Steel.ST.C.Types.Struct.fsti
+++ b/lib/steel/c/Steel.ST.C.Types.Struct.fsti
@@ -222,6 +222,25 @@ val struct_field0
     (pts_to r v)
     (fun r' -> pts_to r (struct_set_field field (unknown (fields.fd_typedef field)) v) `star` pts_to r' (struct_get_field v field) `star` has_struct_field r field r')
 
+inline_for_extraction
+[@@noextract_to "krml"] // primitive
+let struct_field1
+  (#tn: Type0)
+  (#tf: Type0)
+  (t': Type0)
+  (#n: string)
+  (#fields: nonempty_field_description_t tf)
+  (#v: Ghost.erased (struct_t0 tn n fields))
+  (r: ref (struct0 tn n fields))
+  (field: field_t fields)
+  (td': typedef t')
+  (sq_t': squash (t' ==  fields.fd_type field))
+  (sq_td': squash (td' == fields.fd_typedef field))
+: STT (ref td')
+    (pts_to r v)
+    (fun r' -> pts_to r (struct_set_field field (unknown (fields.fd_typedef field)) v) `star` pts_to r' (struct_get_field v field) `star` has_struct_field r field r')
+= struct_field0 t' r field td'
+
 inline_for_extraction [@@noextract_to "krml"] // primitive
 let struct_field
   (#tn: Type0)
@@ -259,6 +278,27 @@ val unstruct_field
     )
     (fun _ -> True)
 
+let unstruct_field_and_drop
+  (#opened: _)
+  (#tn: Type0)
+  (#tf: Type0)
+  (#n: string)
+  (#fields: nonempty_field_description_t tf)
+  (#v: Ghost.erased (struct_t0 tn n fields))
+  (r: ref (struct0 tn n fields))
+  (field: field_t fields)
+  (#v': Ghost.erased (fields.fd_type field))
+  (r': ref (fields.fd_typedef field))
+: STGhost unit opened
+    (has_struct_field r field r' `star` pts_to r v `star` pts_to r' v')
+    (fun _ -> pts_to r (struct_set_field field v' v))
+    (
+      struct_get_field v field == unknown (fields.fd_typedef field)
+    )
+    (fun _ -> True)
+= unstruct_field r field r';
+  drop (has_struct_field _ _ _)
+
 let unstruct_field_alt
   (#opened: _)
   (#tn: Type0)
diff --git a/lib/steel/c/Steel.ST.C.Types.Union.fsti b/lib/steel/c/Steel.ST.C.Types.Union.fsti
index 831b4e15a..3624025f6 100644
--- a/lib/steel/c/Steel.ST.C.Types.Union.fsti
+++ b/lib/steel/c/Steel.ST.C.Types.Union.fsti
@@ -285,6 +285,24 @@ val union_field0
     (pts_to r v)
     (fun r' -> has_union_field r field r' `star` pts_to r' (union_get_field v field))
 
+[@@noextract_to "krml"] // primitive
+let union_field1
+  (#tn: Type0)
+  (#tf: Type0)
+  (t': Type0)
+  (#n: string)
+  (#fields: field_description_t tf)
+  (#v: Ghost.erased (union_t0 tn n fields))
+  (r: ref (union0 tn n fields))
+  (field: field_t fields {union_get_case v == Some field})
+  (td': typedef t')
+  (sq_t': squash (t' ==  fields.fd_type field))
+  (sq_td': squash (td' == fields.fd_typedef field))
+: STT (ref td')
+    (pts_to r v)
+    (fun r' -> has_union_field r field r' `star` pts_to r' (union_get_field v field))
+= union_field0 t' r field td'
+
 inline_for_extraction [@@noextract_to "krml"] // primitive
 let union_field
   (#tn: Type0)
@@ -317,6 +335,22 @@ val ununion_field
     (has_union_field r field r' `star` pts_to r' v')
     (fun _ -> has_union_field r field r' `star` pts_to r (union_set_field tn n fields field v'))
 
+let ununion_field_and_drop
+  (#opened: _)
+  (#tn: Type0)
+  (#tf: Type0)
+  (#n: string)
+  (#fields: field_description_t tf)
+  (r: ref (union0 tn n fields))
+  (field: field_t fields)
+  (#v': Ghost.erased (fields.fd_type field))
+  (r': ref (fields.fd_typedef field))
+: STGhostT unit opened
+    (has_union_field r field r' `star` pts_to r' v')
+    (fun _ -> pts_to r (union_set_field tn n fields field v'))
+= ununion_field r field r';
+  drop (has_union_field _ _ _)
+
 // NOTE: we DO NOT support preservation of struct prefixes
 
 [@@noextract_to "krml"] // primitive

From a35775c0d89f1fdced24ca9205f472afbb507873 Mon Sep 17 00:00:00 2001
From: Tahina Ramananandro <taramana@microsoft.com>
Date: Tue, 25 Jul 2023 13:16:02 -0700
Subject: [PATCH 2/3] has_struct_field, has_union_field: untie field ref type

---
 lib/steel/c/Steel.ST.C.Types.Fields.fsti      |   5 +
 lib/steel/c/Steel.ST.C.Types.Struct.fsti      | 114 ++++++++++----
 lib/steel/c/Steel.ST.C.Types.Union.fsti       | 147 ++++++++++++++----
 share/steel/examples/steelc/HaclExample2.fst  |   6 +-
 share/steel/examples/steelc/LList.fst         |  20 +--
 share/steel/examples/steelc/PointStruct.fst   |   8 +-
 .../examples/steelc/PointStructDirectDef.fst  |  10 +-
 share/steel/examples/steelc/ScalarUnion.fst   |   8 +-
 8 files changed, 231 insertions(+), 87 deletions(-)

diff --git a/lib/steel/c/Steel.ST.C.Types.Fields.fsti b/lib/steel/c/Steel.ST.C.Types.Fields.fsti
index 9371f7098..1a141e339 100644
--- a/lib/steel/c/Steel.ST.C.Types.Fields.fsti
+++ b/lib/steel/c/Steel.ST.C.Types.Fields.fsti
@@ -3,6 +3,11 @@ include Steel.ST.C.Types.Base
 open Steel.C.Typestring
 open Steel.ST.Util
 
+[@@noextract_to "krml"] // tactic
+let norm_fields () : FStar.Tactics.Tac unit =
+  FStar.Tactics.norm [delta_attr [`%norm_field_attr]; iota; zeta; primops];
+  FStar.Tactics.trefl ()
+
 [@@noextract_to "krml"] // primitive
 val field_t_nil: Type0
 [@@noextract_to "krml"] // primitive
diff --git a/lib/steel/c/Steel.ST.C.Types.Struct.fsti b/lib/steel/c/Steel.ST.C.Types.Struct.fsti
index 3505f6238..51875fe70 100644
--- a/lib/steel/c/Steel.ST.C.Types.Struct.fsti
+++ b/lib/steel/c/Steel.ST.C.Types.Struct.fsti
@@ -120,9 +120,31 @@ val has_struct_field
   (#fields: nonempty_field_description_t tf)
   (r: ref (struct0 tn n fields))
   (field: field_t fields)
-  (r': ref (fields.fd_typedef field))
+  (#t': Type0)
+  (#td': typedef t')
+  (r': ref td')
 : Tot vprop
 
+val has_struct_field_prop
+  (#opened: _)
+  (#tn: Type0)
+  (#tf: Type0)
+  (#n: string)
+  (#fields: nonempty_field_description_t tf)
+  (r: ref (struct0 tn n fields))
+  (field: field_t fields)
+  (#t': Type0)
+  (#td': typedef t')
+  (r': ref td')
+: STGhost unit opened
+    (has_struct_field r field r')
+    (fun _ -> has_struct_field r field r')
+    True
+    (fun _ ->
+      t' == fields.fd_type field /\
+      td' == fields.fd_typedef field
+    )
+
 val has_struct_field_dup
   (#opened: _)
   (#tn: Type0)
@@ -131,7 +153,9 @@ val has_struct_field_dup
   (#fields: nonempty_field_description_t tf)
   (r: ref (struct0 tn n fields))
   (field: field_t fields)
-  (r': ref (fields.fd_typedef field))
+  (#t': Type0)
+  (#td': typedef t')
+  (r': ref td')
 : STGhostT unit opened
     (has_struct_field r field r')
     (fun _ -> has_struct_field r field r' `star` has_struct_field r field r')
@@ -144,10 +168,15 @@ val has_struct_field_inj
   (#fields: nonempty_field_description_t tf)
   (r: ref (struct0 tn n fields))
   (field: field_t fields)
-  (r1 r2: ref (fields.fd_typedef field))
-: STGhostT unit opened
+  (#t1: Type0)
+  (#td1: typedef t1)
+  (r1: ref td1)
+  (#t2: Type0)
+  (#td2: typedef t2)
+  (r2: ref td2)
+: STGhostT (squash (t1 == t2 /\ td1 == td2)) opened
     (has_struct_field r field r1 `star` has_struct_field r field r2)
-    (fun _ -> has_struct_field r field r1 `star` has_struct_field r field r2 `star` ref_equiv r1 r2)
+    (fun _ -> has_struct_field r field r1 `star` has_struct_field r field r2 `star` ref_equiv r1 (coerce_eq () r2))
 
 val has_struct_field_equiv_from
   (#opened: _)
@@ -157,7 +186,9 @@ val has_struct_field_equiv_from
   (#fields: nonempty_field_description_t tf)
   (r1: ref (struct0 tn n fields))
   (field: field_t fields)
-  (r': ref (fields.fd_typedef field))
+  (#t': Type0)
+  (#td': typedef t')
+  (r': ref td')
   (r2: ref (struct0 tn n fields))
 : STGhostT unit opened
     (ref_equiv r1 r2 `star` has_struct_field r1 field r')
@@ -171,8 +202,9 @@ val has_struct_field_equiv_to
   (#fields: nonempty_field_description_t tf)
   (r: ref (struct0 tn n fields))
   (field: field_t fields)
-  (r1': ref (fields.fd_typedef field))
-  (r2': ref (fields.fd_typedef field))
+  (#t': Type0)
+  (#td': typedef t')
+  (r1' r2': ref td')
 : STGhostT unit opened
     (ref_equiv r1' r2' `star` has_struct_field r field r1')
     (fun _ -> ref_equiv r1' r2' `star` has_struct_field r field r2')
@@ -186,10 +218,15 @@ val ghost_struct_field_focus
   (#v: Ghost.erased (struct_t0 tn n fields))
   (r: ref (struct0 tn n fields))
   (field: field_t fields)
-  (r': ref (fields.fd_typedef field))
-: STGhostT unit opened
+  (#t': Type0)
+  (#td': typedef t')
+  (r': ref td')
+: STGhostT (squash (
+      t' == fields.fd_type field /\
+      td' == fields.fd_typedef field
+  )) opened
     (has_struct_field r field r' `star` pts_to r v)
-    (fun _ -> has_struct_field r field r' `star` pts_to r (struct_set_field field (unknown (fields.fd_typedef field)) v) `star` pts_to r' (struct_get_field v field))
+    (fun _ -> has_struct_field r field r' `star` pts_to r (struct_set_field field (unknown (fields.fd_typedef field)) v) `star` pts_to r' (Ghost.hide (coerce_eq () (struct_get_field v field))))
 
 val ghost_struct_field
   (#opened: _)
@@ -220,7 +257,7 @@ val struct_field0
   })
 : STT (ref td')
     (pts_to r v)
-    (fun r' -> pts_to r (struct_set_field field (unknown (fields.fd_typedef field)) v) `star` pts_to r' (struct_get_field v field) `star` has_struct_field r field r')
+    (fun r' -> pts_to r (struct_set_field field (unknown (fields.fd_typedef field)) v) `star` pts_to r' (Ghost.hide (coerce_eq () (struct_get_field v field))) `star` has_struct_field r field r')
 
 inline_for_extraction
 [@@noextract_to "krml"] // primitive
@@ -250,14 +287,19 @@ let struct_field
   (#v: Ghost.erased (struct_t0 tn n fields))
   (r: ref (struct0 tn n fields))
   (field: field_t fields)
-: STT (ref #(norm norm_field_steps (fields.fd_type field)) (fields.fd_typedef field))
+  (#t': Type0)
+  (#td': typedef t')
+  (# [ norm_fields () ] sq_t': squash (t' ==  fields.fd_type field))
+  (# [ norm_fields () ] sq_td': squash (td' == fields.fd_typedef field))
+  ()
+: STT (ref td')
     (pts_to r v)
-    (fun r' -> pts_to r (struct_set_field field (unknown (fields.fd_typedef field)) v) `star` pts_to #(norm norm_field_steps (fields.fd_type field)) r' (struct_get_field v field) `star` has_struct_field r field r')
+    (fun r' -> pts_to r (struct_set_field field (unknown (fields.fd_typedef field)) v) `star` pts_to r' (struct_get_field v field) `star` has_struct_field r field r')
 = struct_field0
-    (norm norm_field_steps (fields.fd_type field))
+    t'
     r
     field
-    (fields.fd_typedef field)
+    td'
 
 val unstruct_field
   (#opened: _)
@@ -268,15 +310,21 @@ val unstruct_field
   (#v: Ghost.erased (struct_t0 tn n fields))
   (r: ref (struct0 tn n fields))
   (field: field_t fields)
-  (#v': Ghost.erased (fields.fd_type field))
-  (r': ref (fields.fd_typedef field))
-: STGhost unit opened
+  (#t': Type0)
+  (#td': typedef t')
+  (#v': Ghost.erased t')
+  (r': ref td')
+: STGhost (Ghost.erased (struct_t0 tn n fields)) opened
     (has_struct_field r field r' `star` pts_to r v `star` pts_to r' v')
-    (fun _ -> has_struct_field r field r' `star` pts_to r (struct_set_field field v' v))
+    (fun res -> has_struct_field r field r' `star` pts_to r res)
     (
       struct_get_field v field == unknown (fields.fd_typedef field)
     )
-    (fun _ -> True)
+    (fun res ->
+      t' == fields.fd_type field /\
+      td' == fields.fd_typedef field /\
+      Ghost.reveal res == struct_set_field field (coerce_eq () (Ghost.reveal v')) v
+    )
 
 let unstruct_field_and_drop
   (#opened: _)
@@ -287,17 +335,24 @@ let unstruct_field_and_drop
   (#v: Ghost.erased (struct_t0 tn n fields))
   (r: ref (struct0 tn n fields))
   (field: field_t fields)
-  (#v': Ghost.erased (fields.fd_type field))
-  (r': ref (fields.fd_typedef field))
-: STGhost unit opened
+  (#t': Type0)
+  (#td': typedef t')
+  (#v': Ghost.erased t')
+  (r': ref td')
+: STGhost (Ghost.erased (struct_t0 tn n fields)) opened
     (has_struct_field r field r' `star` pts_to r v `star` pts_to r' v')
-    (fun _ -> pts_to r (struct_set_field field v' v))
+    (fun res -> pts_to r res)
     (
       struct_get_field v field == unknown (fields.fd_typedef field)
     )
-    (fun _ -> True)
-= unstruct_field r field r';
-  drop (has_struct_field _ _ _)
+    (fun res ->
+      t' == fields.fd_type field /\
+      td' == fields.fd_typedef field /\
+      Ghost.reveal res == struct_set_field field (coerce_eq () (Ghost.reveal v')) v
+    )
+= let res = unstruct_field r field r' in
+  drop (has_struct_field _ _ _);
+  res
 
 let unstruct_field_alt
   (#opened: _)
@@ -319,8 +374,7 @@ let unstruct_field_alt
     (fun s' -> 
       Ghost.reveal s' == struct_set_field field v' v
     )
-= unstruct_field r field r';
-  _
+= unstruct_field r field r'
 
 val fractionable_struct
   (#tn: Type0)
diff --git a/lib/steel/c/Steel.ST.C.Types.Union.fsti b/lib/steel/c/Steel.ST.C.Types.Union.fsti
index 3624025f6..21f05f9b7 100644
--- a/lib/steel/c/Steel.ST.C.Types.Union.fsti
+++ b/lib/steel/c/Steel.ST.C.Types.Union.fsti
@@ -185,9 +185,31 @@ val has_union_field
   (#fields: field_description_t tf)
   (r: ref (union0 tn n fields))
   (field: field_t fields)
-  (r': ref (fields.fd_typedef field))
+  (#t': Type0)
+  (#td': typedef t')
+  (r': ref td')
 : Tot vprop
 
+val has_union_field_prop
+  (#opened: _)
+  (#tn: Type0)
+  (#tf: Type0)
+  (#n: string)
+  (#fields: field_description_t tf)
+  (r: ref (union0 tn n fields))
+  (field: field_t fields)
+  (#t': Type0)
+  (#td': typedef t')
+  (r': ref td')
+: STGhost unit opened
+    (has_union_field r field r')
+    (fun _ -> has_union_field r field r')
+    True
+    (fun _ ->
+      t' == fields.fd_type field /\
+      td' == fields.fd_typedef field
+    )
+
 val has_union_field_dup
   (#opened: _)
   (#tn: Type0)
@@ -196,7 +218,9 @@ val has_union_field_dup
   (#fields: nonempty_field_description_t tf)
   (r: ref (union0 tn n fields))
   (field: field_t fields)
-  (r': ref (fields.fd_typedef field))
+  (#t': Type0)
+  (#td': typedef t')
+  (r': ref td')
 : STGhostT unit opened
     (has_union_field r field r')
     (fun _ -> has_union_field r field r' `star` has_union_field r field r')
@@ -209,10 +233,15 @@ val has_union_field_inj
   (#fields: nonempty_field_description_t tf)
   (r: ref (union0 tn n fields))
   (field: field_t fields)
-  (r1 r2: ref (fields.fd_typedef field))
-: STGhostT unit opened
+  (#t1: Type0)
+  (#td1: typedef t1)
+  (r1: ref td1)
+  (#t2: Type0)
+  (#td2: typedef t2)
+  (r2: ref td2)
+: STGhostT (squash (t1 == t2 /\ td1 == td2)) opened
     (has_union_field r field r1 `star` has_union_field r field r2)
-    (fun _ -> has_union_field r field r1 `star` has_union_field r field r2 `star` ref_equiv r1 r2)
+    (fun _ -> has_union_field r field r1 `star` has_union_field r field r2 `star` ref_equiv r1 (coerce_eq () r2))
 
 val has_union_field_equiv_from
   (#opened: _)
@@ -222,7 +251,9 @@ val has_union_field_equiv_from
   (#fields: nonempty_field_description_t tf)
   (r1 r2: ref (union0 tn n fields))
   (field: field_t fields)
-  (r': ref (fields.fd_typedef field))
+  (#t': Type0)
+  (#td': typedef t')
+  (r': ref td')
 : STGhostT unit opened
     (has_union_field r1 field r' `star` ref_equiv r1 r2)
     (fun _ -> has_union_field r2 field r' `star` ref_equiv r1 r2)
@@ -235,7 +266,9 @@ val has_union_field_equiv_to
   (#fields: nonempty_field_description_t tf)
   (r: ref (union0 tn n fields))
   (field: field_t fields)
-  (r1 r2: ref (fields.fd_typedef field))
+  (#t': Type0)
+  (#td': typedef t')
+  (r1 r2: ref td')
 : STGhostT unit opened
     (has_union_field r field r1 `star` ref_equiv r1 r2)
     (fun _ -> has_union_field r field r2 `star` ref_equiv r1 r2)
@@ -249,10 +282,15 @@ val ghost_union_field_focus
   (#v: Ghost.erased (union_t0 tn n fields))
   (r: ref (union0 tn n fields))
   (field: field_t fields {union_get_case v == Some field})
-  (r': ref (fields.fd_typedef field))
-: STGhostT unit opened
+  (#t': Type0)
+  (#td': typedef t')
+  (r': ref td')
+: STGhostT (squash (
+      t' == fields.fd_type field /\
+      td' == fields.fd_typedef field
+  )) opened
     (has_union_field r field r' `star` pts_to r v)
-    (fun _ -> has_union_field r field r' `star` pts_to r' (union_get_field v field))
+    (fun _ -> has_union_field r field r' `star` pts_to r' (Ghost.hide (coerce_eq () (union_get_field v field))))
 
 val ghost_union_field
   (#opened: _)
@@ -283,9 +321,9 @@ val union_field0
   })
 : STT (ref td')
     (pts_to r v)
-    (fun r' -> has_union_field r field r' `star` pts_to r' (union_get_field v field))
+    (fun r' -> has_union_field r field r' `star` pts_to r' (Ghost.hide (coerce_eq () (union_get_field v field))))
 
-[@@noextract_to "krml"] // primitive
+inline_for_extraction [@@noextract_to "krml"]
 let union_field1
   (#tn: Type0)
   (#tf: Type0)
@@ -312,14 +350,19 @@ let union_field
   (#v: Ghost.erased (union_t0 tn n fields))
   (r: ref (union0 tn n fields))
   (field: field_t fields {union_get_case v == Some field})
-: STT (ref #(norm norm_field_steps (fields.fd_type field)) (fields.fd_typedef field))
+  (#t': Type0)
+  (#td': typedef t')
+  (# [ norm_fields () ] sq_t': squash (t' ==  fields.fd_type field))
+  (# [ norm_fields () ] sq_td': squash (td' == fields.fd_typedef field))
+  ()
+: STT (ref td')
     (pts_to r v)
-    (fun r' -> has_union_field r field r' `star` pts_to #(norm norm_field_steps (fields.fd_type field)) r' (union_get_field v field))
+    (fun r' -> has_union_field r field r' `star` pts_to r' (union_get_field v field))
 = union_field0
-    (norm norm_field_steps (fields.fd_type field))
+    t'
     r
     field
-    (fields.fd_typedef field)
+    td'
 
 val ununion_field
   (#opened: _)
@@ -329,11 +372,19 @@ val ununion_field
   (#fields: field_description_t tf)
   (r: ref (union0 tn n fields))
   (field: field_t fields)
-  (#v': Ghost.erased (fields.fd_type field))
-  (r': ref (fields.fd_typedef field))
-: STGhostT unit opened
+  (#t': Type0)
+  (#td': typedef t')
+  (#v': Ghost.erased t')
+  (r': ref td')
+: STGhost (Ghost.erased (union_t0 tn n fields)) opened
     (has_union_field r field r' `star` pts_to r' v')
-    (fun _ -> has_union_field r field r' `star` pts_to r (union_set_field tn n fields field v'))
+    (fun res -> has_union_field r field r' `star` pts_to r res)
+    True
+    (fun res ->
+      t' == fields.fd_type field /\
+      td' == fields.fd_typedef field /\
+      Ghost.reveal res == union_set_field tn n fields field (coerce_eq () (Ghost.reveal v'))
+    )
 
 let ununion_field_and_drop
   (#opened: _)
@@ -343,13 +394,22 @@ let ununion_field_and_drop
   (#fields: field_description_t tf)
   (r: ref (union0 tn n fields))
   (field: field_t fields)
-  (#v': Ghost.erased (fields.fd_type field))
-  (r': ref (fields.fd_typedef field))
-: STGhostT unit opened
+  (#t': Type0)
+  (#td': typedef t')
+  (#v': Ghost.erased t')
+  (r': ref td')
+: STGhost (Ghost.erased (union_t0 tn n fields)) opened
     (has_union_field r field r' `star` pts_to r' v')
-    (fun _ -> pts_to r (union_set_field tn n fields field v'))
-= ununion_field r field r';
-  drop (has_union_field _ _ _)
+    (fun res -> pts_to r res)
+    True
+    (fun res ->
+      t' == fields.fd_type field /\
+      td' == fields.fd_typedef field /\
+      Ghost.reveal res == union_set_field tn n fields field (coerce_eq () (Ghost.reveal v'))
+    )
+= let res = ununion_field r field r' in
+  drop (has_union_field _ _ _);
+  res
 
 // NOTE: we DO NOT support preservation of struct prefixes
 
@@ -369,10 +429,30 @@ val union_switch_field0
   })
 : ST (ref td') // need to write the pcm carrier value, so this cannot be Ghost or Atomic
     (pts_to r v)
-    (fun r' -> has_union_field r field r' `star` pts_to r' (uninitialized (fields.fd_typedef field)))
+    (fun r' -> has_union_field r field r' `star` pts_to r' (uninitialized td'))
     (full (union0 tn n fields) v)
     (fun r' -> True)
 
+inline_for_extraction [@@noextract_to "krml"]
+let union_switch_field1
+  (#tn: Type0)
+  (#tf: Type0)
+  (t': Type0)
+  (#n: string)
+  (#fields: field_description_t tf)
+  (#v: Ghost.erased (union_t0 tn n fields))
+  (r: ref (union0 tn n fields))
+  (field: field_t fields)
+  (td': typedef t')
+  (sq_t': squash (t' ==  fields.fd_type field))
+  (sq_td': squash (td' == fields.fd_typedef field))
+: ST (ref td') // need to write the pcm carrier value, so this cannot be Ghost or Atomic
+    (pts_to r v)
+    (fun r' -> has_union_field r field r' `star` pts_to r' (uninitialized td'))
+    (full (union0 tn n fields) v)
+    (fun r' -> True)
+= union_switch_field0 t' r field td'
+
 inline_for_extraction [@@noextract_to "krml"]
 let union_switch_field
   (#tn: Type0)
@@ -382,13 +462,18 @@ let union_switch_field
   (#v: Ghost.erased (union_t0 tn n fields))
   (r: ref (union0 tn n fields))
   (field: field_t fields)
-: ST (ref #(norm norm_field_steps (fields.fd_type field)) (fields.fd_typedef field)) // need to write the pcm carrier value, so this cannot be Ghost or Atomic
+  (#t': Type0)
+  (#td': typedef t')
+  (# [ norm_fields () ] sq_t': squash (t' ==  fields.fd_type field))
+  (# [ norm_fields () ] sq_td': squash (td' == fields.fd_typedef field))
+  ()
+: ST (ref td') // need to write the pcm carrier value, so this cannot be Ghost or Atomic
     (pts_to r v)
-    (fun r' -> has_union_field r field r' `star` pts_to #(norm norm_field_steps (fields.fd_type field)) r' (uninitialized (fields.fd_typedef field)))
+    (fun r' -> has_union_field r field r' `star` pts_to r' (uninitialized td'))
     (full (union0 tn n fields) v)
     (fun r' -> True)
 = union_switch_field0
-    (norm norm_field_steps (fields.fd_type field))
+    t'
     r
     field
-    (fields.fd_typedef field)
+    td'
diff --git a/share/steel/examples/steelc/HaclExample2.fst b/share/steel/examples/steelc/HaclExample2.fst
index f0b7afccb..39c4dd812 100644
--- a/share/steel/examples/steelc/HaclExample2.fst
+++ b/share/steel/examples/steelc/HaclExample2.fst
@@ -110,10 +110,10 @@ let test
     (fun v' -> p `pts_to` v')
     (full comp v)
     (fun v' -> full comp v')
-= let q = p `struct_field` "limbs" in
+= let q = struct_field p "limbs" #_ #(base_array0 five (scalar U64.t) 5sz) () in
   let a = array_of_base q in
-  let r = p `struct_field` "precomp" in
-  let _ = vpattern_replace_erased (pts_to p) in // FIXME: WHY WHY WHY?
+  let r = struct_field p "precomp" #_ #(base_array0 twenty (scalar U64.t) 20sz) () in
+  let _ = vpattern_replace (pts_to p) in // FIXME: WHY WHY WHY?
   let b = array_of_base r in
   let _ = do_something_with_limbs a in
   let _ = do_something_with_precomp b in
diff --git a/share/steel/examples/steelc/LList.fst b/share/steel/examples/steelc/LList.fst
index f14025af0..276c8798a 100644
--- a/share/steel/examples/steelc/LList.fst
+++ b/share/steel/examples/steelc/LList.fst
@@ -128,13 +128,13 @@ let push
   end else begin
     rewrite (pts_to_or_null _ _) (pts_to c (uninitialized cell));
     rewrite (freeable_or_null c) (freeable c);
-    let p_tl = pllist_get p in
-    let c_hd = struct_field c "hd" in
-    let c_tl = struct_field c "tl" in
+    let p_tl : void_ptr = pllist_get p in // type ascription necessary to avoid C compiler warning -Wincompatible-pointer-types
+    let c_hd = struct_field c "hd" () in
+    let c_tl = struct_field c "tl" () in
     write c_hd a;
     write c_tl p_tl;
-    unstruct_field c "tl" c_tl;
-    unstruct_field c "hd" c_hd;
+    let _ = unstruct_field c "tl" c_tl in
+    let _ = unstruct_field c "hd" c_hd in
     intro_llist_cons c p_tl a l;
     pllist_put p c;
     drop (has_struct_field c "hd" _);
@@ -154,13 +154,13 @@ let pop
 = rewrite (pllist p l) (pllist p (List.Tot.hd l :: List.Tot.tl l));
   let c = pllist_get p in
   let _ = elim_llist_cons c (List.Tot.hd l) (List.Tot.tl l) in
-  let c_hd = struct_field c "hd" in
-  let c_tl = struct_field c "tl" in
+  let c_hd = struct_field c "hd" () in
+  let c_tl = struct_field c "tl" () in
   let res = read c_hd in
-  let p_tl = read c_tl in
+  let p_tl : void_ptr = read c_tl in // type ascription necessary to avoid C compiler warning -Wincompatible-pointer-types
   vpattern_rewrite (fun x -> llist x _) p_tl;
-  unstruct_field c "tl" c_tl;
-  unstruct_field c "hd" c_hd;
+  let _ = unstruct_field c "tl" c_tl in
+  let _ = unstruct_field c "hd" c_hd in
   free c;
   pllist_put p p_tl;
   drop (has_struct_field c "hd" _);
diff --git a/share/steel/examples/steelc/PointStruct.fst b/share/steel/examples/steelc/PointStruct.fst
index 68023857b..62f48a9ee 100644
--- a/share/steel/examples/steelc/PointStruct.fst
+++ b/share/steel/examples/steelc/PointStruct.fst
@@ -40,14 +40,14 @@ let swap_struct (p: ref point) (v: Ghost.erased (typeof point))
       struct_get_field v' "x" == struct_get_field v "y" /\
       struct_get_field v' "y" == struct_get_field v "x"
     )
-= let px = struct_field p "x" in
-  let py = struct_field p "y" in
+= let px = struct_field p "x" () in
+  let py = struct_field p "y" () in
   let x = read px in
   let y = read py in
   write px y;
   write py x;
-  unstruct_field p "x" px;
-  unstruct_field p "y" py;
+  let _ = unstruct_field p "x" px in
+  let _ = unstruct_field p "y" py in
   drop (has_struct_field _ _ px);
   drop (has_struct_field _ _ _);
   return _
diff --git a/share/steel/examples/steelc/PointStructDirectDef.fst b/share/steel/examples/steelc/PointStructDirectDef.fst
index e2e6d61de..9db3e93f9 100644
--- a/share/steel/examples/steelc/PointStructDirectDef.fst
+++ b/share/steel/examples/steelc/PointStructDirectDef.fst
@@ -27,7 +27,7 @@ let point_t = struct_t "dummy" point_fields
 noextract
 let point : typedef point_t = struct0 _ _ _
 
-#push-options "--query_stats --fuel 0"
+#push-options "--query_stats --fuel 0 --print_implicits"
 
 let swap_struct (p: ref point) (v: Ghost.erased (typeof point))
 : ST (Ghost.erased (typeof point))
@@ -40,14 +40,14 @@ let swap_struct (p: ref point) (v: Ghost.erased (typeof point))
       struct_get_field v' "x" == struct_get_field v "y" /\
       struct_get_field v' "y" == struct_get_field v "x"
     )
-= let px = struct_field p "x" in
-  let py = struct_field p "y" in
+= let px = struct_field p "x" () in
+  let py = struct_field p "y" () in
   let x = read px in
   let y = read py in
   write px y;
   write py x;
-  unstruct_field p "x" px;
-  unstruct_field p "y" py;
+  let _ = unstruct_field p "x" px in
+  let _ = unstruct_field p "y" py in
   drop (has_struct_field _ _ px);
   drop (has_struct_field _ _ _);
   return _
diff --git a/share/steel/examples/steelc/ScalarUnion.fst b/share/steel/examples/steelc/ScalarUnion.fst
index a74f7e32e..428a8dcc1 100644
--- a/share/steel/examples/steelc/ScalarUnion.fst
+++ b/share/steel/examples/steelc/ScalarUnion.fst
@@ -46,9 +46,9 @@ val switch_to_u16
 #push-options "--fuel 0 --print_bound_var_types"
 
 let switch_to_u16 p x =
-  let p16 = union_switch_field  p "as_u16" in
+  let p16 = union_switch_field p "as_u16" () in
   write p16 x;
-  ununion_field p "as_u16" _;
+  let _ = ununion_field p "as_u16" _ in
   drop (has_union_field _ _ _);
   return ()
 
@@ -71,8 +71,8 @@ val zero_u32_of_union (#v: Ghost.erased u32_or_u16_t) (p: ref u32_or_u16)
     (ensures fun _ -> True)
 
 let zero_u32_of_union #v p =
-  let q = union_field p "as_u32" in
+  let q = union_field p "as_u32" () in
   zero_u32_ref q;
-  ununion_field p "as_u32" _;
+  let _ = ununion_field p "as_u32" _ in
   drop (has_union_field _ _ _);
   return ()

From 4fd5caa19aabc977c249952389a3cd0b49dbc64d Mon Sep 17 00:00:00 2001
From: Tahina Ramananandro <taramana@microsoft.com>
Date: Tue, 25 Jul 2023 17:41:50 -0700
Subject: [PATCH 3/3] proof

---
 src/proofs/steelc/Steel.ST.C.Types.Struct.fst | 130 +++++--
 src/proofs/steelc/Steel.ST.C.Types.Union.fst  | 333 +++++++++++++++---
 2 files changed, 385 insertions(+), 78 deletions(-)

diff --git a/src/proofs/steelc/Steel.ST.C.Types.Struct.fst b/src/proofs/steelc/Steel.ST.C.Types.Struct.fst
index 9c537bc13..99155deb7 100644
--- a/src/proofs/steelc/Steel.ST.C.Types.Struct.fst
+++ b/src/proofs/steelc/Steel.ST.C.Types.Struct.fst
@@ -67,61 +67,151 @@ let struct_get_field_uninitialized
   tn n fields field
 = ()
 
+let has_struct_field_spec
+  (#tf: Type0)
+  (fields: nonempty_field_description_t tf)
+  (field: field_t fields)
+  (#t': Type0)
+  (#td': typedef t')
+  (r': ref td')
+  (r1: ref ((fd_gen_of_nonempty_fd fields).fd_typedef field))
+: Tot prop
+= t' == fields.fd_type field /\
+  td' == fields.fd_typedef field /\
+  r' == coerce_eq () r1
+
+[@@__reduce__]
+let has_struct_field9
+  (#tn: Type0)
+  (#tf: Type0)
+  (#n: string)
+  (#fields: nonempty_field_description_t tf)
+  (r: ref (struct0 tn n fields))
+  (field: field_t fields)
+  (#t': Type0)
+  (#td': typedef t')
+  (r': ref td')
+= exists_ (fun (r1: ref ((fd_gen_of_nonempty_fd fields).fd_typedef field)) ->
+    has_struct_field1 r field r1 `star`
+    pure (has_struct_field_spec fields field r' r1)
+  )
+
 let has_struct_field
   r field r'
-= has_struct_field1 r field r'
+= has_struct_field9 r field r'
+
+let intro_has_struct_field
+  (#opened: _)
+  (#tn: Type0)
+  (#tf: Type0)
+  (#n: string)
+  (#fields: nonempty_field_description_t tf)
+  (r: ref (struct0 tn n fields))
+  (field: field_t fields)
+  (#t': Type0)
+  (#td': typedef t')
+  (r': ref td')
+  (r1: ref ((fd_gen_of_nonempty_fd fields).fd_typedef field))
+: STGhost unit opened
+    (has_struct_field1 r field r1)
+    (fun _ -> has_struct_field r field r')
+    (has_struct_field_spec fields field r' r1)
+    (fun _ -> True)
+= noop ();
+  rewrite (has_struct_field9 r field r') (has_struct_field r field r')
+
+let elim_has_struct_field
+  (#opened: _)
+  (#tn: Type0)
+  (#tf: Type0)
+  (#n: string)
+  (#fields: nonempty_field_description_t tf)
+  (r: ref (struct0 tn n fields))
+  (field: field_t fields)
+  (#t': Type0)
+  (#td': typedef t')
+  (r': ref td')
+: STGhost (Ghost.erased (ref ((fd_gen_of_nonempty_fd fields).fd_typedef field))) opened
+    (has_struct_field r field r')
+    (fun r1 -> has_struct_field1 r field r1)
+    True
+    (fun r1 -> has_struct_field_spec fields field r' r1)
+= rewrite (has_struct_field r field r') (has_struct_field9 r field r');
+  let _ = gen_elim () in
+  vpattern_replace_erased (has_struct_field1 r field)
+
+let has_struct_field_prop
+  r field r'
+= let r1 = elim_has_struct_field r field r' in
+  intro_has_struct_field r field r' r1
 
 let has_struct_field_dup
   #opened #tn #tf #n #fields r field r'
-= let r'2 : ref ((fd_gen_of_nonempty_fd fields).fd_typedef field) = coerce_eq () r' in
-  has_struct_field_dup' r field r'2
+= let r'2 = elim_has_struct_field r field r' in
+  has_struct_field_dup' r field r'2;
+  intro_has_struct_field r field r' r'2;
+  intro_has_struct_field r field r' r'2
 
 let has_struct_field_inj
   #_ #tn #tf #n #fields r field r1 r2
-= let r1' : ref ((fd_gen_of_nonempty_fd fields).fd_typedef field) = coerce_eq () r1 in
-  let r2' : ref ((fd_gen_of_nonempty_fd fields).fd_typedef field) = coerce_eq () r2 in
-  has_struct_field_inj' r field r1' r2'
+= let r1' = elim_has_struct_field r field r1 in
+  let r2' = elim_has_struct_field r field r2 in
+  has_struct_field_inj' r field r1' r2';
+  intro_has_struct_field r field r1 r1';
+  intro_has_struct_field r field r2 r2';
+  rewrite (ref_equiv r1' r2') (ref_equiv r1 r2)
 
 let has_struct_field_equiv_from
   #_ #tn #tf #n #fields r1 field r' r2
-= let r'_ : ref ((fd_gen_of_nonempty_fd fields).fd_typedef field) = coerce_eq () r' in
-  has_struct_field_equiv_from' r1 field r'_ r2
+= let r'_ = elim_has_struct_field r1 field r' in
+  has_struct_field_equiv_from' r1 field r'_ r2;
+  intro_has_struct_field r2 field r' r'_
 
 let has_struct_field_equiv_to
   #_ #tn #tf #n #fields r field r1 r2
-= let r1' : ref ((fd_gen_of_nonempty_fd fields).fd_typedef field) = coerce_eq () r1 in
+= let r1' = elim_has_struct_field r field r1 in
   let r2' : ref ((fd_gen_of_nonempty_fd fields).fd_typedef field) = coerce_eq () r2 in
-  has_struct_field_equiv_to' r field r1' r2'
+  rewrite (ref_equiv r1 r2) (ref_equiv r1' r2');
+  has_struct_field_equiv_to' r field r1' r2';
+  rewrite (ref_equiv r1' r2') (ref_equiv r1 r2);
+  intro_has_struct_field r field r2 r2'
 
 let ghost_struct_field_focus
-  #_ #tn #tf #n #fields r field r'
-= let r'_ : ref ((fd_gen_of_nonempty_fd fields).fd_typedef field) = coerce_eq () r' in
-  ghost_struct_field_focus' r field r'_
+  #_ #tn #tf #n #fields #v r field #t' #td' r'
+= let r'_ = elim_has_struct_field r field r' in
+  let sq : squash (
+      t' == fields.fd_type field /\
+      td' == fields.fd_typedef field
+  ) = () in
+  ghost_struct_field_focus' r field r'_;
+  rewrite (pts_to r'_ _) (pts_to r' (Ghost.hide (coerce_eq () (struct_get_field v field))));
+  intro_has_struct_field r field r' r'_;
+  sq
 
 let ghost_struct_field
   #_ #tn #tf #n #fields #v r field
 = let r' = ghost_struct_field' r field in
   let r'2 : Ghost.erased (ref (fields.fd_typedef field)) = coerce_eq () r' in
   rewrite (pts_to r' _) (pts_to r'2 (struct_get_field v field));
-  rewrite (has_struct_field1 r field r') (has_struct_field r field r'2);
+  intro_has_struct_field r field r'2 r';
   r'2
 
 let struct_field0
   t' #_ #_ #v r field td'
 = let r1' = struct_field' r field in
-  let r' : ref td' = r1' in
+  let r' : ref td' = coerce_eq () r1' in
   rewrite (pts_to r1' _) (pts_to r' (struct_get_field v field));
-  rewrite (has_struct_field1 _ _ _) (has_struct_field r field r');
+  intro_has_struct_field r field r' r1';
   return r'
 
 let unstruct_field
-  #_ #tn #tf #n #fields #v r field #v' r'
-= let r'_ : ref ((fd_gen_of_nonempty_fd fields).fd_typedef field) = coerce_eq () r' in
+  #_ #tn #tf #n #fields #v r field #_ #_ #v' r'
+= let r'_ = elim_has_struct_field r field r' in
   let v'_ : Ghost.erased ((fd_gen_of_nonempty_fd fields).fd_type field) = coerce_eq () v' in
-  rewrite (has_struct_field r field r') (has_struct_field1 r field r'_);
   rewrite (pts_to r' v') (pts_to r'_ v'_);
   unstruct_field' r field r'_;
-  rewrite (has_struct_field1 r field r'_) (has_struct_field r field r')
+  intro_has_struct_field r field r' r'_;
+  _
 
 let fractionable_struct _ = ()
 let mk_fraction_struct _ _ _ = ()
diff --git a/src/proofs/steelc/Steel.ST.C.Types.Union.fst b/src/proofs/steelc/Steel.ST.C.Types.Union.fst
index c8190e696..29d26ecc6 100644
--- a/src/proofs/steelc/Steel.ST.C.Types.Union.fst
+++ b/src/proofs/steelc/Steel.ST.C.Types.Union.fst
@@ -380,40 +380,225 @@ let has_union_field05
 : Tot vprop
 = has_focus_ref r (U.union_field (union_field_pcm fields) (Some field)) r'
 
+let has_union_field'
+  (#tn: Type0)
+  (#tf: Type0)
+  (#n: string)
+  (#fields: field_description_t tf)
+  (r: ref (union0 tn n fields))
+  (field: field_t fields)
+  (r': ref (fields.fd_typedef field))
+: Tot vprop
+= has_union_field0 r field r'
+
+let has_union_field1_prop
+  (#tf: Type0)
+  (fields: field_description_t tf)
+  (field: field_t fields)
+  (#t': Type0)
+  (#td': typedef t')
+  (r': ref td')
+  (r1: ref (fields.fd_typedef field))
+: Tot prop
+= t' == fields.fd_type field /\
+  td' == fields.fd_typedef field /\
+  r1 == coerce_eq () r'
+
+[@@__reduce__]
+let has_union_field1
+  (#tn: Type0)
+  (#tf: Type0)
+  (#n: string)
+  (#fields: field_description_t tf)
+  (r: ref (union0 tn n fields))
+  (field: field_t fields)
+  (#t': Type0)
+  (#td': typedef t')
+  (r': ref td')
+: Tot vprop
+= exists_ (fun (r1: ref (fields.fd_typedef field)) ->
+    has_union_field' r field r1 `star`
+    pure (has_union_field1_prop fields field r' r1)
+  )
+
 let has_union_field
   r field r'
-= has_union_field0 r field r'
+= has_union_field1 r field r'
 
-let has_union_field_dup
+let intro_has_union_field
+  (#opened: _)
+  (#tn: Type0)
+  (#tf: Type0)
+  (#n: string)
+  (#fields: field_description_t tf)
+  (r: ref (union0 tn n fields))
+  (field: field_t fields)
+  (#t': Type0)
+  (#td': typedef t')
+  (r': ref td')
+  (r1: ref (fields.fd_typedef field))
+: STGhost unit opened
+    (has_union_field' r field r1)
+    (fun _ -> has_union_field r field r')
+    (has_union_field1_prop fields field r' r1)
+    (fun _ -> True)
+= noop ();
+  rewrite (has_union_field1 r field r') (has_union_field r field r')
+
+let elim_has_union_field
+  (#opened: _)
+  (#tn: Type0)
+  (#tf: Type0)
+  (#n: string)
+  (#fields: field_description_t tf)
+  (r: ref (union0 tn n fields))
+  (field: field_t fields)
+  (#t': Type0)
+  (#td': typedef t')
+  (r': ref td')
+: STGhost (Ghost.erased (ref (fields.fd_typedef field))) opened
+    (has_union_field r field r')
+    (fun r1 -> has_union_field' r field r1)
+    True
+    (fun r1 -> has_union_field1_prop fields field r' r1)
+= rewrite (has_union_field r field r') (has_union_field1 r field r');
+  let _ = gen_elim () in
+  vpattern_replace_erased (has_union_field' r field)
+
+let has_union_field_prop
+  r field r'
+= let r1 = elim_has_union_field r field r' in
+  intro_has_union_field r field r' _
+
+val has_union_field_dup'
+  (#opened: _)
+  (#tn: Type0)
+  (#tf: Type0)
+  (#n: string)
+  (#fields: nonempty_field_description_t tf)
+  (r: ref (union0 tn n fields))
+  (field: field_t fields)
+  (r': ref (fields.fd_typedef field))
+: STGhostT unit opened
+    (has_union_field' r field r')
+    (fun _ -> has_union_field' r field r' `star` has_union_field' r field r')
+
+let has_union_field_dup'
   r field r'
-= rewrite (has_union_field r field r') (has_union_field05 r field r');
+= rewrite (has_union_field' r field r') (has_union_field05 r field r');
   has_focus_ref_dup r _ r';
-  rewrite (has_union_field05 r field r') (has_union_field r field r');
-  rewrite (has_union_field05 r field r') (has_union_field r field r')
+  rewrite (has_union_field05 r field r') (has_union_field' r field r');
+  rewrite (has_union_field05 r field r') (has_union_field' r field r')
 
-let has_union_field_inj
+let has_union_field_dup
+  r field r'
+= let r1 = elim_has_union_field r field r' in
+  has_union_field_dup' r field r1;
+  intro_has_union_field r field r' r1;
+  intro_has_union_field r field r' r1
+
+val has_union_field_inj'
+  (#opened: _)
+  (#tn: Type0)
+  (#tf: Type0)
+  (#n: string)
+  (#fields: nonempty_field_description_t tf)
+  (r: ref (union0 tn n fields))
+  (field: field_t fields)
+  (r1 r2: ref (fields.fd_typedef field))
+: STGhostT unit opened
+    (has_union_field' r field r1 `star` has_union_field' r field r2)
+    (fun _ -> has_union_field' r field r1 `star` has_union_field' r field r2 `star` ref_equiv r1 r2)
+
+let has_union_field_inj'
   #_ #tn #_ #n r field r1 r2
-= rewrite (has_union_field r field r1) (has_union_field05 r field r1);
-  rewrite (has_union_field r field r2) (has_union_field05 r field r2);
+= rewrite (has_union_field' r field r1) (has_union_field05 r field r1);
+  rewrite (has_union_field' r field r2) (has_union_field05 r field r2);
   has_focus_ref_inj r _ r1 r2;
-  rewrite (has_union_field05 r field r1) (has_union_field r field r1);
-  rewrite (has_union_field05 r field r2) (has_union_field r field r2)
+  rewrite (has_union_field05 r field r1) (has_union_field' r field r1);
+  rewrite (has_union_field05 r field r2) (has_union_field' r field r2)
 
-let has_union_field_equiv_from
+let has_union_field_inj
+  #_ #tn #_ #n r field #t1 #td1 r1 #t2 #td2 r2
+= let r1' = elim_has_union_field r field r1 in
+  let r2' = elim_has_union_field r field r2 in
+  has_union_field_inj' r field r1' r2';
+  let sq : squash (t1 == t2 /\ td1 == td2) = () in
+  intro_has_union_field r field r1 r1';
+  intro_has_union_field r field r2 r2';
+  rewrite (ref_equiv r1' r2') (ref_equiv r1 (coerce_eq () r2));
+  sq
+
+val has_union_field_equiv_from'
+  (#opened: _)
+  (#tn: Type0)
+  (#tf: Type0)
+  (#n: string)
+  (#fields: nonempty_field_description_t tf)
+  (r1 r2: ref (union0 tn n fields))
+  (field: field_t fields)
+  (r': ref (fields.fd_typedef field))
+: STGhostT unit opened
+    (has_union_field' r1 field r' `star` ref_equiv r1 r2)
+    (fun _ -> has_union_field' r2 field r' `star` ref_equiv r1 r2)
+
+let has_union_field_equiv_from'
   r1 r2 field r'
-= rewrite (has_union_field r1 field r') (has_union_field05 r1 field r');
+= rewrite (has_union_field' r1 field r') (has_union_field05 r1 field r');
   has_focus_ref_equiv_from r1 _ r' r2;
-  rewrite (has_union_field05 r2 field r') (has_union_field r2 field r')
+  rewrite (has_union_field05 r2 field r') (has_union_field' r2 field r')
 
-let has_union_field_equiv_to
+let has_union_field_equiv_from
+  r1 r2 field r'
+= let r3 = elim_has_union_field r1 field r' in
+  has_union_field_equiv_from' r1 r2 field r3;
+  intro_has_union_field r2 field r' r3
+
+val has_union_field_equiv_to'
+  (#opened: _)
+  (#tn: Type0)
+  (#tf: Type0)
+  (#n: string)
+  (#fields: nonempty_field_description_t tf)
+  (r: ref (union0 tn n fields))
+  (field: field_t fields)
+  (r1 r2: ref (fields.fd_typedef field))
+: STGhostT unit opened
+    (has_union_field' r field r1 `star` ref_equiv r1 r2)
+    (fun _ -> has_union_field' r field r2 `star` ref_equiv r1 r2)
+
+let has_union_field_equiv_to'
   r field r1' r2'
-= rewrite (has_union_field r field r1') (has_union_field05 r field r1');
+= rewrite (has_union_field' r field r1') (has_union_field05 r field r1');
   has_focus_ref_equiv_to r _ r1' r2';
-  rewrite (has_union_field05 r field r2') (has_union_field r field r2')
+  rewrite (has_union_field05 r field r2') (has_union_field' r field r2')
 
-let ghost_union_field_focus
+let has_union_field_equiv_to
+  #_ #_ #_ #_ #fields r field r1' r2'
+= let r1 = elim_has_union_field r field r1' in
+  let r2 : ref (fields.fd_typedef field) = coerce_eq () r2' in
+  rewrite (ref_equiv r1' r2') (ref_equiv r1 r2);
+  has_union_field_equiv_to' r field r1 r2;
+  rewrite (ref_equiv r1 r2) (ref_equiv r1' r2');
+  intro_has_union_field r field r2' r2
+
+val ghost_union_field_focus'
+  (#opened: _)
+  (#tn: Type0)
+  (#tf: Type0)
+  (#n: string)
+  (#fields: field_description_t tf)
+  (#v: Ghost.erased (union_t0 tn n fields))
+  (r: ref (union0 tn n fields))
+  (field: field_t fields {union_get_case v == Some field})
+  (r': ref (fields.fd_typedef field))
+: STGhostT unit opened
+    (has_union_field' r field r' `star` pts_to r v)
+    (fun _ -> has_union_field' r field r' `star` pts_to r' (Ghost.hide (union_get_field v field)))
+
+let ghost_union_field_focus'
   #_ #tn #_ #n #fields #v r field r'
-= rewrite (has_union_field r field r') (has_union_field0 r field r');
+= rewrite (has_union_field' r field r') (has_union_field0 r field r');
   let _ = gen_elim () in
   let w = vpattern_replace (HR.pts_to r _) in
   let w' = vpattern_replace (HR.pts_to r' _) in
@@ -428,13 +613,44 @@ let ghost_union_field_focus
   hr_share r';
 //  pts_to_intro_rewrite r' rr' _ ;
   pts_to_intro_rewrite r' _ _ ;
-  rewrite (has_union_field0 r field r') (has_union_field r field r')
+  rewrite (has_union_field0 r field r') (has_union_field' r field r')
 
-let ghost_union_field
+let ghost_union_field_focus
+  #_ #tn #_ #n #fields #v r field #t' #td' r'
+= let r1 = elim_has_union_field r field r' in
+  let sq : squash (
+      t' == fields.fd_type field /\
+      td' == fields.fd_typedef field
+  ) = () in
+  ghost_union_field_focus' r field r1;
+  rewrite (pts_to r1 _) (pts_to r' (Ghost.hide (coerce_eq () (union_get_field v field))));
+  intro_has_union_field r field r' r1;
+  sq
+
+val ghost_union_field'
+  (#opened: _)
+  (#tn: Type0)
+  (#tf: Type0)
+  (#n: string)
+  (#fields: field_description_t tf)
+  (#v: Ghost.erased (union_t0 tn n fields))
+  (r: ref (union0 tn n fields))
+  (field: field_t fields {union_get_case v == Some field})
+: STGhostT (Ghost.erased (ref (fields.fd_typedef field))) opened
+    (pts_to r v)
+    (fun r' -> has_union_field' r field r' `star` pts_to r' (union_get_field v field))
+
+let ghost_union_field'
   #_ #tn #_ #n #fields #v r field
 = let r' = ghost_focus_ref r (fields.fd_typedef field) (U.union_field (union_field_pcm fields) (Some field)) in
-  rewrite (has_union_field05 r field r') (has_union_field r field r');
-  ghost_union_field_focus r field r';
+  rewrite (has_union_field05 r field r') (has_union_field' r field r');
+  ghost_union_field_focus' r field r';
+  r'
+
+let ghost_union_field
+  #_ #tn #_ #n #fields #v r field
+= let r' = ghost_union_field' r field in
+  intro_has_union_field r field r' r';
   r'
 
 [@@noextract_to "krml"] // primitive
@@ -448,27 +664,41 @@ let union_field'
   (field: field_t fields {union_get_case v == Some field})
 : STT (ref (fields.fd_typedef field))
     (pts_to r v)
-    (fun r' -> has_union_field r field r' `star` pts_to r' (union_get_field v field))
+    (fun r' -> has_union_field' r field r' `star` pts_to r' (union_get_field v field))
 = let r' = focus_ref r (fields.fd_typedef field) (U.union_field (union_field_pcm fields) (Some field)) in
-  rewrite (has_union_field05 r field r') (has_union_field r field r');
-  ghost_union_field_focus r field r';
+  rewrite (has_union_field05 r field r') (has_union_field' r field r');
+  ghost_union_field_focus' r field r';
   return r'
 
 let union_field0
   t' r field td'
 =
   let r' = union_field' r field in
-  let res : ref td' = r' in
+  let res : ref td' = coerce_eq () r' in
   rewrite (pts_to r' _) (pts_to res _);
-  rewrite (has_union_field r field _) (has_union_field r field res);
+  intro_has_union_field r field res r';
   return res
 
+val ununion_field'
+  (#opened: _)
+  (#tn: Type0)
+  (#tf: Type0)
+  (#n: string)
+  (#fields: field_description_t tf)
+  (r: ref (union0 tn n fields))
+  (field: field_t fields)
+  (#v': Ghost.erased (fields.fd_type field))
+  (r': ref (fields.fd_typedef field))
+: STGhostT unit opened
+    (has_union_field' r field r' `star` pts_to r' v')
+    (fun _ -> has_union_field' r field r' `star` pts_to r (union_set_field tn n fields field (Ghost.reveal v')))
+
 #push-options "--z3rlimit 16"
 #restart-solver
 
-let ununion_field
+let ununion_field'
   #_ #tn #_ #n #fields r field #v' r'
-= rewrite (has_union_field r field r') (has_union_field0 r field r');
+= rewrite (has_union_field' r field r') (has_union_field0 r field r');
   let _ = gen_elim () in
   let w = vpattern_replace (HR.pts_to r _) in
   let w' = vpattern_replace (HR.pts_to r' _) in
@@ -479,11 +709,20 @@ let ununion_field
   let rr' = get_ref r' in
   let x = r_unfocus rr' rr (coerce_eq () (U.union_field (union_field_pcm fields) (Some field))) _ in
   hr_share r;
-  rewrite (has_union_field0 r field r') (has_union_field r field r');
+  rewrite (has_union_field0 r field r') (has_union_field' r field r');
   pts_to_intro_rewrite r rr #x _
 
 #pop-options
 
+let ununion_field
+  #_ #tn #_ #n #fields r field #_ #_ #v' r'
+= let r1 = elim_has_union_field r field r' in
+  let v1 : Ghost.erased (fields.fd_type field) = Ghost.hide (coerce_eq () (Ghost.reveal v')) in
+  rewrite (pts_to r' v') (pts_to r1 v1);
+  ununion_field' r field r1;
+  intro_has_union_field r field r' r1;
+  _
+
 [@@noextract_to "krml"] // primitive
 let union_switch_field'
   (#tn: Type0)
@@ -495,7 +734,7 @@ let union_switch_field'
   (field: field_t fields)
 : ST (ref (fields.fd_typedef field))
     (pts_to r v)
-    (fun r' -> has_union_field r field r' `star` pts_to r' (uninitialized (fields.fd_typedef field)))
+    (fun r' -> has_union_field' r field r' `star` pts_to r' (uninitialized (fields.fd_typedef field)))
     (full (union0 tn n fields) v)
     (fun _ -> True)
 = rewrite (pts_to r v) (pts_to0 r v);
@@ -510,32 +749,10 @@ let union_switch_field'
   rewrite (pts_to r' _) (pts_to r' (uninitialized (fields.fd_typedef field)));
   return r'
 
-[@@noextract_to "krml"] // primitive
-let union_switch_field0'
-  (#tn: Type0)
-  (#tf: Type0)
-  (t': Type0)
-  (#n: string)
-  (#fields: field_description_t tf)
-  (#v: Ghost.erased (union_t0 tn n fields))
-  (r: ref (union0 tn n fields))
-  (field: field_t fields)
-  (td': typedef t')
-  (sq: squash (
-    t' ==  fields.fd_type field /\
-    td' == fields.fd_typedef field
-  ))
-: ST (ref td') // need to write the pcm carrier value, so this cannot be Ghost or Atomic
-    (pts_to r v)
-    (fun r' -> has_union_field r field (coerce_eq () r') `star` pts_to r' (Ghost.hide (coerce_eq () (uninitialized (fields.fd_typedef field)))))
-    (full (union0 tn n fields) v)
-    (fun _ -> True)
-= let r' = union_switch_field' #tn #tf #n #fields #v r field in
-  let res : ref td' = r' in
+let union_switch_field0
+  t' #_ #fields r field td'
+= let r' = union_switch_field' r field in
+  let res : ref td' = coerce_eq () r' in
   rewrite (pts_to r' _) (pts_to res (Ghost.hide (coerce_eq () (uninitialized (fields.fd_typedef field)))));
-  rewrite (has_union_field r field _) (has_union_field r field (coerce_eq () res));
+  intro_has_union_field r field res r';
   return res
-
-let union_switch_field0
-  t' r field td'
-= union_switch_field0' t' r field td' ()