Skip to content

Verify writes through an optional output pointer - #241

Draft
nikswamy wants to merge 2 commits into
mainfrom
nswamy/pal-pr27-nullable-out
Draft

Verify writes through an optional output pointer#241
nikswamy wants to merge 2 commits into
mainfrom
nswamy/pal-pr27-nullable-out

Conversation

@nikswamy

@nikswamy nikswamy commented Aug 19, 2026

Copy link
Copy Markdown
Contributor

Part of the upstreaming of nswamy/pal-c-project-integration (PR27 of 35 PRs) — see PR_PLAN.md on that branch for the whole plan and the dependency graph.

Base: nswamy/pal-pr05-refinement-scoping — a stacked PR. It depends on nswamy/pal-pr05-refinement-scoping, so only the commits listed below are its own; it will be retargeted at main once its parents land.

An _Out_opt_ parameter is a pointer the caller may pass as NULL and the callee writes
through only after testing it. The existential for the pointee now lives inside
unless_null, so the null branch does not have to name a value that is not there; the
intro and elim rules are stated per pointer flavor rather than through the typeclass, so
no has_is_null constraint is left unsolved; and the null test eliminates the guard on
entry to each branch. Pulse cannot discharge the slprop it infers when joining two
branches, so each branch restates the guarded resource on the way out — as an assert,
because a pointer's value is only resolved against the context in a slprop position.
Branches that return, break, continue or jump need no restatement and would be wrong to
receive one. The second commit does the same for the other conjunct that fails to match:
a borrowed structure the branch reads through, where reading a member splits the parameter
into per-member ownership. Splitting Nullable into an interface keeps unless_null
abstract.

Commits

  • Verify writes through an optional output pointer
  • Settle a guarded branch on one resource shape

Testing

Verified: make rust lib, test/check-template.sh, cargo fmt --check, clang-format --dry-run --Werror, and F* verification of test/nullable_out, test/nullable_out_struct.

@nikswamy2
nikswamy2 force-pushed the nswamy/pal-pr27-nullable-out branch from 7f4b7bf to fb7f33d Compare August 20, 2026 05:41
Base automatically changed from nswamy/pal-pr05-refinement-scoping to main August 20, 2026 19:56
nikswamy and others added 2 commits August 20, 2026 12:56
@nikswamy @gebner
Verify writes through an optional output pointer
8624ea9 
An _Out_opt_ parameter is a pointer the caller may pass as NULL, and the
callee writes through it only after testing it. Three things were missing.

The existential for the pointee now lives inside unless_null, so the null
branch does not have to name a value that is not there. The intro and elim
rules are stated once per pointer flavor rather than through the typeclass,
so the prover is not left with an unsolved has_is_null constraint. And the
null test itself now eliminates the guard on entry to each branch.

Pulse cannot discharge the slprop it infers when it joins two branches: the
join is a match on the test, and the branch hypothesis does not reduce it.
So on the way out of each branch we restate the guarded resource, leaving
both branches at the same slprop and nothing for Pulse to join. The
restatement is an assert rather than a call, because the value at a pointer
is only resolved against the context in a slprop position, never in a term
passed as an argument. Branches that return, break, continue or jump need no
restatement -- nothing joins them -- and would be wrong to receive one, since
the code after an early return on null is entitled to the opened resource.

Splitting Nullable into an interface keeps unless_null abstract, so a caller
never sees the match on the null test.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d
(cherry picked from commit f6e105b)
@nikswamy @gebner
Settle a guarded branch on one resource shape
bc8e4ee 
A guarded optional-output write is rarely in tail position, so Pulse has to
infer the postcondition of the `if`. It does that by matching the two branches'
resources conjunct by conjunct and wrapping whatever is left over in a
dependent match on the guard -- which the prover then cannot discharge, even
though the branch hypothesis fixes the guard.

Closing the guarded pointer back into `unless_null` handled the first conjunct
that fails to match. This is the second: a borrowed structure the branch reads
through. Reading a member splits the parameter into per-member ownership, so
the reading branch offers `Struct_X__aux_raw_unfolded x ** pts_to (field_1 x) v`
where the other branch still offers `pts_to x v`, and the matcher has no rule
relating the two.

Restate the borrowed parameter's entry-state resources at the end of both
branches, so the two sides settle on one shape before the join looks at them.
The restatement has to avoid existentials: the matcher gives up immediately on
an existentially quantified conjunct, which would trade this failure for a
worse one. A `const` parameter's value is already named by the signature's
implicits, so it can be quoted directly; a plain one is bound existentially in
the signature, so the body names it with a `with` binder placed after the
parameter redeclarations, where it scopes over every guarded branch in the
function. Each conjunct gets its own `assert`, because `!p` cannot resolve from
under a binder introduced by the same statement.

test/nullable_out_struct covers it: two optional outputs filled from members of
a shared borrowed structure, which is the shape a deserializer with optional
outputs has.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d
(cherry picked from commit c1c8f8d)
@gebner
gebner force-pushed the nswamy/pal-pr27-nullable-out branch from fb7f33d to bc8e4ee Compare August 20, 2026 19:56
@gebner

gebner commented Aug 26, 2026

Copy link
Copy Markdown
Contributor

!diff

@github-actions

github-actions Bot commented Aug 26, 2026

Copy link
Copy Markdown

Generated F* output diff

Effect of this pull request on the F* code pal generates for the test suite (f9d4dd2 → bc8e4ee).

Summary 
 {base => head}/func_pointer/Func_guarded_call.fst                   |   8 ++++----
 {base => head}/func_pointer/Func_guarded_call.fsti                  |   8 ++++----
 {base => head}/func_pointer/Func_is_set.fst                         |   4 ++--
 {base => head}/func_pointer/Func_is_set.fsti                        |   4 ++--
 {base => head}/nullable/Func_takes_nullable_array.fst               |  10 ++++++----
 {base => head}/nullable/Func_takes_nullable_array.fsti              |  10 ++++++----
 {base => head}/nullable/Func_takes_nullable_arrayptr.fst            |   4 ++--
 {base => head}/nullable/Func_takes_nullable_arrayptr.fsti           |   4 ++--
 {base => head}/nullable/Func_takes_nullable_ref.fst                 |  10 ++++++----
 {base => head}/nullable/Func_takes_nullable_ref.fsti                |  10 ++++++----
 {base => head}/nullable/Func_takes_nullable_refined.fst             |   4 ++--
 {base => head}/nullable/Func_takes_nullable_refined.fsti            |   4 ++--
 /dev/null => head/nullable_out/Func_fill_pair.fst                   |  17 +++++++++++++++++
 /dev/null => head/nullable_out/Func_opt_fill_pair.fst               |  44 ++++++++++++++++++++++++++++++++++++++++++++
 /dev/null => head/nullable_out/Func_opt_fill_pair.fsti              |  17 +++++++++++++++++
 /dev/null => head/nullable_out/Func_opt_forward_array.fst           |  34 ++++++++++++++++++++++++++++++++++
 /dev/null => head/nullable_out/Func_opt_forward_array.fsti          |  17 +++++++++++++++++
 /dev/null => head/nullable_out/Func_opt_write.fst                   |  45 +++++++++++++++++++++++++++++++++++++++++++++
 /dev/null => head/nullable_out/Func_opt_write.fsti                  |  19 +++++++++++++++++++
 /dev/null => head/nullable_out/Func_opt_write_early_return.fst      |  32 ++++++++++++++++++++++++++++++++
 /dev/null => head/nullable_out/Func_opt_write_early_return.fsti     |  19 +++++++++++++++++++
 /dev/null => head/nullable_out/Func_opt_write_many.fst              |  77 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 /dev/null => head/nullable_out/Func_opt_write_many.fsti             |  28 ++++++++++++++++++++++++++++
 /dev/null => head/nullable_out/Func_takes_array.fst                 |  14 ++++++++++++++
 /dev/null => head/nullable_out/Struct_pair.fst                      |  99 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 /dev/null => head/nullable_out/TranslationErrors.fst                |   1 +
 /dev/null => head/nullable_out/Typedef___uint32_t.fst               |  13 +++++++++++++
 /dev/null => head/nullable_out/Typedef___uint64_t.fst               |  13 +++++++++++++
 /dev/null => head/nullable_out/Typedef___uint8_t.fst                |  12 ++++++++++++
 /dev/null => head/nullable_out/Typedef_uint32_t.fst                 |  13 +++++++++++++
 /dev/null => head/nullable_out/Typedef_uint64_t.fst                 |  13 +++++++++++++
 /dev/null => head/nullable_out/Typedef_uint8_t.fst                  |  13 +++++++++++++
 /dev/null => head/nullable_out/diagnostics.json                     |   1 +
 /dev/null => head/nullable_out_struct/Func_opt_two_from_struct.fst  |  77 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 /dev/null => head/nullable_out_struct/Func_opt_two_from_struct.fsti |  28 ++++++++++++++++++++++++++++
 /dev/null => head/nullable_out_struct/Struct_pair.fst               | 102 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 /dev/null => head/nullable_out_struct/TranslationErrors.fst         |   1 +
 /dev/null => head/nullable_out_struct/Typedef___uint64_t.fst        |  13 +++++++++++++
 /dev/null => head/nullable_out_struct/Typedef_pair.fst              |  12 ++++++++++++
 /dev/null => head/nullable_out_struct/Typedef_uint64_t.fst          |  13 +++++++++++++
 /dev/null => head/nullable_out_struct/diagnostics.json              |   1 +
 41 files changed, 832 insertions(+), 36 deletions(-)

Full diff: full diff artifact

Diff 
diff --git base/func_pointer/Func_guarded_call.fst head/func_pointer/Func_guarded_call.fst
index 295f2ba..bc45d4a 100644
--- base/func_pointer/Func_guarded_call.fst
+++ head/func_pointer/Func_guarded_call.fst
@@ -11,14 +11,14 @@ divergent fn func_guarded_call
   requires
     ((unless_null
         var_fp
-        ((Pulse.Lib.C.FuncPtr.is_valid var_fp true
-(Pulse.Lib.C.FuncPtr.pre_of Funcptr_add.func_add__fp) (Pulse.Lib.C.FuncPtr.post_of Funcptr_add.func_add__fp)))))
+        (((Pulse.Lib.C.FuncPtr.is_valid var_fp true
+(Pulse.Lib.C.FuncPtr.pre_of Funcptr_add.func_add__fp) (Pulse.Lib.C.FuncPtr.post_of Funcptr_add.func_add__fp))))))
   returns return_1 : Typedef_int32_t.ty_int32_t
   ensures
     ((unless_null
         var_fp
-        ((Pulse.Lib.C.FuncPtr.is_valid var_fp true
-(Pulse.Lib.C.FuncPtr.pre_of Funcptr_add.func_add__fp) (Pulse.Lib.C.FuncPtr.post_of Funcptr_add.func_add__fp)))))
+        (((Pulse.Lib.C.FuncPtr.is_valid var_fp true
+(Pulse.Lib.C.FuncPtr.pre_of Funcptr_add.func_add__fp) (Pulse.Lib.C.FuncPtr.post_of Funcptr_add.func_add__fp))))))
   ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
   ensures (with_pure (((id #int (Int32.v return_1)) = 0) || ((id #int (Int32.v return_1)) = 5)))
 {
diff --git base/func_pointer/Func_guarded_call.fsti head/func_pointer/Func_guarded_call.fsti
index bbe0fe5..33643b5 100644
--- base/func_pointer/Func_guarded_call.fsti
+++ head/func_pointer/Func_guarded_call.fsti
@@ -11,13 +11,13 @@ divergent fn func_guarded_call
 requires
   ((unless_null
       var_fp
-      ((Pulse.Lib.C.FuncPtr.is_valid var_fp true
-(Pulse.Lib.C.FuncPtr.pre_of Funcptr_add.func_add__fp) (Pulse.Lib.C.FuncPtr.post_of Funcptr_add.func_add__fp)))))
+      (((Pulse.Lib.C.FuncPtr.is_valid var_fp true
+(Pulse.Lib.C.FuncPtr.pre_of Funcptr_add.func_add__fp) (Pulse.Lib.C.FuncPtr.post_of Funcptr_add.func_add__fp))))))
 returns return_1 : Typedef_int32_t.ty_int32_t
 ensures
   ((unless_null
       var_fp
-      ((Pulse.Lib.C.FuncPtr.is_valid var_fp true
-(Pulse.Lib.C.FuncPtr.pre_of Funcptr_add.func_add__fp) (Pulse.Lib.C.FuncPtr.post_of Funcptr_add.func_add__fp)))))
+      (((Pulse.Lib.C.FuncPtr.is_valid var_fp true
+(Pulse.Lib.C.FuncPtr.pre_of Funcptr_add.func_add__fp) (Pulse.Lib.C.FuncPtr.post_of Funcptr_add.func_add__fp))))))
 ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
 ensures (with_pure (((id #int (Int32.v return_1)) = 0) || ((id #int (Int32.v return_1)) = 5)))
\ No newline at end of file
diff --git base/func_pointer/Func_is_set.fst head/func_pointer/Func_is_set.fst
index 1af64f9..3585ea0 100644
--- base/func_pointer/Func_is_set.fst
+++ head/func_pointer/Func_is_set.fst
@@ -8,9 +8,9 @@ divergent fn func_is_set
       (Pulse.Lib.C.FuncPtr.func_ptr
         (Typedef_int32_t.ty_int32_t & Typedef_int32_t.ty_int32_t)
         Typedef_int32_t.ty_int32_t))
-  requires ((unless_null var_fp emp))
+  requires ((unless_null var_fp (emp)))
   returns return_1 : Typedef_int32_t.ty_int32_t
-  ensures ((unless_null var_fp emp))
+  ensures ((unless_null var_fp (emp)))
   ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
   ensures (with_pure (((id #int (Int32.v return_1)) = 0) || ((id #int (Int32.v return_1)) = 1)))
 {
diff --git base/func_pointer/Func_is_set.fsti head/func_pointer/Func_is_set.fsti
index fd9e9ae..35143ad 100644
--- base/func_pointer/Func_is_set.fsti
+++ head/func_pointer/Func_is_set.fsti
@@ -8,8 +8,8 @@ divergent fn func_is_set
     (Pulse.Lib.C.FuncPtr.func_ptr
       (Typedef_int32_t.ty_int32_t & Typedef_int32_t.ty_int32_t)
       Typedef_int32_t.ty_int32_t))
-requires ((unless_null var_fp emp))
+requires ((unless_null var_fp (emp)))
 returns return_1 : Typedef_int32_t.ty_int32_t
-ensures ((unless_null var_fp emp))
+ensures ((unless_null var_fp (emp)))
 ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
 ensures (with_pure (((id #int (Int32.v return_1)) = 0) || ((id #int (Int32.v return_1)) = 1)))
\ No newline at end of file
diff --git base/nullable/Func_takes_nullable_array.fst head/nullable/Func_takes_nullable_array.fst
index 6b31a14..60cb22b 100644
--- base/nullable/Func_takes_nullable_array.fst
+++ head/nullable/Func_takes_nullable_array.fst
@@ -5,12 +5,14 @@ open Pulse.Lib.C
 
 divergent fn func_takes_nullable_array (var_a: (array Int32.t))
   requires
-    exists* (val_a_0: (full_array_spec Int32.t)).
-    ((unless_null var_a ((array_pts_to_full var_a 1.0R val_a_0))))
+    ((unless_null
+        var_a
+        (exists* (val_a_0: (full_array_spec Int32.t)). ((array_pts_to_full var_a 1.0R val_a_0)))))
   returns return_1 : unit
   ensures
-    exists* (val_a_0: (full_array_spec Int32.t)).
-    ((unless_null var_a ((array_pts_to_full var_a 1.0R val_a_0))))
+    ((unless_null
+        var_a
+        (exists* (val_a_0: (full_array_spec Int32.t)). ((array_pts_to_full var_a 1.0R val_a_0)))))
 {
   let mut var_a = var_a;
 }
\ No newline at end of file
diff --git base/nullable/Func_takes_nullable_array.fsti head/nullable/Func_takes_nullable_array.fsti
index ddd1b7d..e589f58 100644
--- base/nullable/Func_takes_nullable_array.fsti
+++ head/nullable/Func_takes_nullable_array.fsti
@@ -5,9 +5,11 @@ open Pulse.Lib.C
 
 divergent fn func_takes_nullable_array (var_a: (array Int32.t))
 requires
-  exists* (val_a_0: (full_array_spec Int32.t)).
-  ((unless_null var_a ((array_pts_to_full var_a 1.0R val_a_0))))
+  ((unless_null
+      var_a
+      (exists* (val_a_0: (full_array_spec Int32.t)). ((array_pts_to_full var_a 1.0R val_a_0)))))
 returns return_1 : unit
 ensures
-  exists* (val_a_0: (full_array_spec Int32.t)).
-  ((unless_null var_a ((array_pts_to_full var_a 1.0R val_a_0))))
\ No newline at end of file
+  ((unless_null
+      var_a
+      (exists* (val_a_0: (full_array_spec Int32.t)). ((array_pts_to_full var_a 1.0R val_a_0)))))
\ No newline at end of file
diff --git base/nullable/Func_takes_nullable_arrayptr.fst head/nullable/Func_takes_nullable_arrayptr.fst
index d8a96ef..fa525cb 100644
--- base/nullable/Func_takes_nullable_arrayptr.fst
+++ head/nullable/Func_takes_nullable_arrayptr.fst
@@ -4,9 +4,9 @@ open Pulse.Lib.C
 #lang-pulse
 
 divergent fn func_takes_nullable_arrayptr (var_p: (array Int32.t))
-  requires ((unless_null var_p emp))
+  requires ((unless_null var_p (emp)))
   returns return_1 : unit
-  ensures ((unless_null var_p emp))
+  ensures ((unless_null var_p (emp)))
 {
   let mut var_p = var_p;
 }
\ No newline at end of file
diff --git base/nullable/Func_takes_nullable_arrayptr.fsti head/nullable/Func_takes_nullable_arrayptr.fsti
index d345653..4ef17f3 100644
--- base/nullable/Func_takes_nullable_arrayptr.fsti
+++ head/nullable/Func_takes_nullable_arrayptr.fsti
@@ -4,6 +4,6 @@ open Pulse.Lib.C
 #lang-pulse
 
 divergent fn func_takes_nullable_arrayptr (var_p: (array Int32.t))
-requires ((unless_null var_p emp))
+requires ((unless_null var_p (emp)))
 returns return_1 : unit
-ensures ((unless_null var_p emp))
\ No newline at end of file
+ensures ((unless_null var_p (emp)))
\ No newline at end of file
diff --git base/nullable/Func_takes_nullable_ref.fst head/nullable/Func_takes_nullable_ref.fst
index 635cd69..3e7b06d 100644
--- base/nullable/Func_takes_nullable_ref.fst
+++ head/nullable/Func_takes_nullable_ref.fst
@@ -5,12 +5,14 @@ open Pulse.Lib.C
 
 divergent fn func_takes_nullable_ref (var_r: (ref Int32.t))
   requires
-    exists* (val_r_0: Int32.t).
-    ((unless_null var_r ((Pulse.Lib.Reference.pts_to var_r #1.0R val_r_0))))
+    ((unless_null
+        var_r
+        (exists* (val_r_0: Int32.t). ((Pulse.Lib.Reference.pts_to var_r #1.0R val_r_0)))))
   returns return_1 : unit
   ensures
-    exists* (val_r_0: Int32.t).
-    ((unless_null var_r ((Pulse.Lib.Reference.pts_to var_r #1.0R val_r_0))))
+    ((unless_null
+        var_r
+        (exists* (val_r_0: Int32.t). ((Pulse.Lib.Reference.pts_to var_r #1.0R val_r_0)))))
 {
   let mut var_r = var_r;
 }
\ No newline at end of file
diff --git base/nullable/Func_takes_nullable_ref.fsti head/nullable/Func_takes_nullable_ref.fsti
index 9029e94..fd7320e 100644
--- base/nullable/Func_takes_nullable_ref.fsti
+++ head/nullable/Func_takes_nullable_ref.fsti
@@ -5,9 +5,11 @@ open Pulse.Lib.C
 
 divergent fn func_takes_nullable_ref (var_r: (ref Int32.t))
 requires
-  exists* (val_r_0: Int32.t).
-  ((unless_null var_r ((Pulse.Lib.Reference.pts_to var_r #1.0R val_r_0))))
+  ((unless_null
+      var_r
+      (exists* (val_r_0: Int32.t). ((Pulse.Lib.Reference.pts_to var_r #1.0R val_r_0)))))
 returns return_1 : unit
 ensures
-  exists* (val_r_0: Int32.t).
-  ((unless_null var_r ((Pulse.Lib.Reference.pts_to var_r #1.0R val_r_0))))
\ No newline at end of file
+  ((unless_null
+      var_r
+      (exists* (val_r_0: Int32.t). ((Pulse.Lib.Reference.pts_to var_r #1.0R val_r_0)))))
\ No newline at end of file
diff --git base/nullable/Func_takes_nullable_refined.fst head/nullable/Func_takes_nullable_refined.fst
index c72190f..299c5d8 100644
--- base/nullable/Func_takes_nullable_refined.fst
+++ head/nullable/Func_takes_nullable_refined.fst
@@ -4,9 +4,9 @@ open Pulse.Lib.C
 #lang-pulse
 
 divergent fn func_takes_nullable_refined (var_p: (array Int32.t))
-  requires ((unless_null var_p ((Nullable_include1.nonneg_offset var_p))))
+  requires ((unless_null var_p (((Nullable_include1.nonneg_offset var_p)))))
   returns return_1 : unit
-  ensures ((unless_null var_p ((Nullable_include1.nonneg_offset var_p))))
+  ensures ((unless_null var_p (((Nullable_include1.nonneg_offset var_p)))))
 {
   let mut var_p = var_p;
 }
\ No newline at end of file
diff --git base/nullable/Func_takes_nullable_refined.fsti head/nullable/Func_takes_nullable_refined.fsti
index 27bb5cb..1aa7626 100644
--- base/nullable/Func_takes_nullable_refined.fsti
+++ head/nullable/Func_takes_nullable_refined.fsti
@@ -4,6 +4,6 @@ open Pulse.Lib.C
 #lang-pulse
 
 divergent fn func_takes_nullable_refined (var_p: (array Int32.t))
-requires ((unless_null var_p ((Nullable_include1.nonneg_offset var_p))))
+requires ((unless_null var_p (((Nullable_include1.nonneg_offset var_p)))))
 returns return_1 : unit
-ensures ((unless_null var_p ((Nullable_include1.nonneg_offset var_p))))
\ No newline at end of file
+ensures ((unless_null var_p (((Nullable_include1.nonneg_offset var_p)))))
\ No newline at end of file
diff --git head/nullable_out/Func_fill_pair.fst head/nullable_out/Func_fill_pair.fst
new file mode 100644
index 0000000..685d23b
--- /dev/null
+++ head/nullable_out/Func_fill_pair.fst
@@ -0,0 +1,17 @@
+module Func_fill_pair
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_fill_pair (var_p: (ref Struct_pair.struct_pair))
+  requires ((Pulse.Lib.Reference.pts_to_uninit var_p))
+  returns return_1 : unit
+  ensures
+    exists* (val_p_0: Struct_pair.struct_pair).
+    ((Pulse.Lib.Reference.pts_to var_p #1.0R val_p_0) **
+      (Struct_pair.struct_pair__pred (!var_p) 1.0R))
+  ensures
+    (with_pure
+      (((id #int (UInt64.v (!(Struct_pair.struct_pair__get_lo var_p)))) = 0) &&
+        ((id #int (UInt64.v (!(Struct_pair.struct_pair__get_hi var_p)))) = 0)))
+{ assume pure False; unreachable () }
\ No newline at end of file
diff --git head/nullable_out/Func_opt_fill_pair.fst head/nullable_out/Func_opt_fill_pair.fst
new file mode 100644
index 0000000..323456e
--- /dev/null
+++ head/nullable_out/Func_opt_fill_pair.fst
@@ -0,0 +1,44 @@
+module Func_opt_fill_pair
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_opt_fill_pair (var_dst: (ref Struct_pair.struct_pair))
+  requires ((unless_null var_dst (((Pulse.Lib.Reference.pts_to_uninit var_dst)))))
+  returns return_1 : unit
+  ensures
+    ((unless_null
+        var_dst
+        (exists* (val_dst_0: Struct_pair.struct_pair).
+          ((Pulse.Lib.Reference.pts_to var_dst #1.0R val_dst_0) **
+            (Struct_pair.struct_pair__pred (!var_dst) 1.0R) **
+            (with_pure
+              (((id #int (UInt64.v (!(Struct_pair.struct_pair__get_lo var_dst)))) = 0) &&
+                ((id #int (UInt64.v (!(Struct_pair.struct_pair__get_hi var_dst)))) = 0)))))))
+{
+  let mut var_dst = var_dst;
+  if ((not (Pulse.Lib.Reference.is_null (!var_dst)))) {
+    let var___pal_guarded_5 = ((!var_dst));
+    Pulse.Lib.C.Nullable.elim_unless_null_ref var___pal_guarded_5;
+    (Func_fill_pair.func_fill_pair (!var_dst));
+    assert (Pulse.Lib.C.Nullable.unless_null var___pal_guarded_5 (exists*
+      (val___pal_guarded_5_0: Struct_pair.struct_pair).
+      ((Pulse.Lib.Reference.pts_to var___pal_guarded_5 #1.0R val___pal_guarded_5_0) **
+        (Struct_pair.struct_pair__pred (!var___pal_guarded_5) 1.0R) **
+        (with_pure
+          (((id #int (UInt64.v (!(Struct_pair.struct_pair__get_lo var___pal_guarded_5)))) = 0) &&
+            ((id #int (UInt64.v (!(Struct_pair.struct_pair__get_hi var___pal_guarded_5)))) =
+              0))))));
+  } else {
+    let var___pal_guarded_5 = ((!var_dst));
+    Pulse.Lib.C.Nullable.elim_null_ref var___pal_guarded_5;
+    assert (Pulse.Lib.C.Nullable.unless_null var___pal_guarded_5 (exists*
+      (val___pal_guarded_5_0: Struct_pair.struct_pair).
+      ((Pulse.Lib.Reference.pts_to var___pal_guarded_5 #1.0R val___pal_guarded_5_0) **
+        (Struct_pair.struct_pair__pred (!var___pal_guarded_5) 1.0R) **
+        (with_pure
+          (((id #int (UInt64.v (!(Struct_pair.struct_pair__get_lo var___pal_guarded_5)))) = 0) &&
+            ((id #int (UInt64.v (!(Struct_pair.struct_pair__get_hi var___pal_guarded_5)))) =
+              0))))));
+  };
+}
\ No newline at end of file
diff --git head/nullable_out/Func_opt_fill_pair.fsti head/nullable_out/Func_opt_fill_pair.fsti
new file mode 100644
index 0000000..f18bc76
--- /dev/null
+++ head/nullable_out/Func_opt_fill_pair.fsti
@@ -0,0 +1,17 @@
+module Func_opt_fill_pair
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_opt_fill_pair (var_dst: (ref Struct_pair.struct_pair))
+requires ((unless_null var_dst (((Pulse.Lib.Reference.pts_to_uninit var_dst)))))
+returns return_1 : unit
+ensures
+  ((unless_null
+      var_dst
+      (exists* (val_dst_0: Struct_pair.struct_pair).
+        ((Pulse.Lib.Reference.pts_to var_dst #1.0R val_dst_0) **
+          (Struct_pair.struct_pair__pred (!var_dst) 1.0R) **
+          (with_pure
+            (((id #int (UInt64.v (!(Struct_pair.struct_pair__get_lo var_dst)))) = 0) &&
+              ((id #int (UInt64.v (!(Struct_pair.struct_pair__get_hi var_dst)))) = 0)))))))
\ No newline at end of file
diff --git head/nullable_out/Func_opt_forward_array.fst head/nullable_out/Func_opt_forward_array.fst
new file mode 100644
index 0000000..85547c7
--- /dev/null
+++ head/nullable_out/Func_opt_forward_array.fst
@@ -0,0 +1,34 @@
+module Func_opt_forward_array
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_opt_forward_array (var_dst: (array Typedef_uint8_t.ty_uint8_t))
+  requires
+    ((unless_null
+        var_dst
+        (exists* (val_dst_0: (full_array_spec Typedef_uint8_t.ty_uint8_t)).
+          ((array_pts_to_full var_dst 1.0R val_dst_0)))))
+  returns return_1 : unit
+  ensures
+    ((unless_null
+        var_dst
+        (exists* (val_dst_0: (full_array_spec Typedef_uint8_t.ty_uint8_t)).
+          ((array_pts_to_full var_dst 1.0R val_dst_0)))))
+{
+  let mut var_dst = var_dst;
+  if ((not (array_is_null (!var_dst)))) {
+    let var___pal_guarded_4 = ((!var_dst));
+    Pulse.Lib.C.Nullable.elim_unless_null_arr var___pal_guarded_4;
+    (Func_takes_array.func_takes_array (!var_dst));
+    assert (Pulse.Lib.C.Nullable.unless_null var___pal_guarded_4 (exists*
+      (val___pal_guarded_4_0: (full_array_spec Typedef_uint8_t.ty_uint8_t)).
+      ((array_pts_to_full var___pal_guarded_4 1.0R val___pal_guarded_4_0))));
+  } else {
+    let var___pal_guarded_4 = ((!var_dst));
+    Pulse.Lib.C.Nullable.elim_null_arr var___pal_guarded_4;
+    assert (Pulse.Lib.C.Nullable.unless_null var___pal_guarded_4 (exists*
+      (val___pal_guarded_4_0: (full_array_spec Typedef_uint8_t.ty_uint8_t)).
+      ((array_pts_to_full var___pal_guarded_4 1.0R val___pal_guarded_4_0))));
+  };
+}
\ No newline at end of file
diff --git head/nullable_out/Func_opt_forward_array.fsti head/nullable_out/Func_opt_forward_array.fsti
new file mode 100644
index 0000000..bc6e42a
--- /dev/null
+++ head/nullable_out/Func_opt_forward_array.fsti
@@ -0,0 +1,17 @@
+module Func_opt_forward_array
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_opt_forward_array (var_dst: (array Typedef_uint8_t.ty_uint8_t))
+requires
+  ((unless_null
+      var_dst
+      (exists* (val_dst_0: (full_array_spec Typedef_uint8_t.ty_uint8_t)).
+        ((array_pts_to_full var_dst 1.0R val_dst_0)))))
+returns return_1 : unit
+ensures
+  ((unless_null
+      var_dst
+      (exists* (val_dst_0: (full_array_spec Typedef_uint8_t.ty_uint8_t)).
+        ((array_pts_to_full var_dst 1.0R val_dst_0)))))
\ No newline at end of file
diff --git head/nullable_out/Func_opt_write.fst head/nullable_out/Func_opt_write.fst
new file mode 100644
index 0000000..e22dadb
--- /dev/null
+++ head/nullable_out/Func_opt_write.fst
@@ -0,0 +1,45 @@
+module Func_opt_write
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_opt_write
+    (var_src: (ref Typedef_uint64_t.ty_uint64_t))
+    (var_dst: (ref Typedef_uint64_t.ty_uint64_t))
+  requires ((unless_null var_dst (((Pulse.Lib.Reference.pts_to_uninit var_dst)))))
+  preserves (Pulse.Lib.Reference.pts_to var_src #'p_src_0 'val_src_0)
+  preserves (Typedef_uint64_t.ty_uint64_t__pred (!var_src) 'p_src_0)
+  returns return_1 : unit
+  ensures
+    ((unless_null
+        var_dst
+        (exists* (val_dst_0: Typedef_uint64_t.ty_uint64_t).
+          ((Pulse.Lib.Reference.pts_to var_dst #1.0R val_dst_0) **
+            (Typedef_uint64_t.ty_uint64_t__pred (!var_dst) 1.0R) **
+            (with_pure ((!var_dst) = (!var_src)))))))
+{
+  let mut var_src = var_src;
+  let mut var_dst = var_dst;
+  if ((not (Pulse.Lib.Reference.is_null (!var_dst)))) {
+    let var___pal_guarded_0 = ((!var_dst));
+    Pulse.Lib.C.Nullable.elim_unless_null_ref var___pal_guarded_0;
+    (!var_dst) := (!(!var_src));
+    assert (Pulse.Lib.C.Nullable.unless_null var___pal_guarded_0 (exists*
+      (val___pal_guarded_0_0: Typedef_uint64_t.ty_uint64_t).
+      ((Pulse.Lib.Reference.pts_to var___pal_guarded_0 #1.0R val___pal_guarded_0_0) **
+        (Typedef_uint64_t.ty_uint64_t__pred (!var___pal_guarded_0) 1.0R) **
+        (with_pure ((!var___pal_guarded_0) = (!(!var_src)))))));
+    assert ((Pulse.Lib.Reference.pts_to (!var_src) #'p_src_0 'val_src_0));
+    assert ((Typedef_uint64_t.ty_uint64_t__pred (!(!var_src)) 'p_src_0));
+  } else {
+    let var___pal_guarded_0 = ((!var_dst));
+    Pulse.Lib.C.Nullable.elim_null_ref var___pal_guarded_0;
+    assert (Pulse.Lib.C.Nullable.unless_null var___pal_guarded_0 (exists*
+      (val___pal_guarded_0_0: Typedef_uint64_t.ty_uint64_t).
+      ((Pulse.Lib.Reference.pts_to var___pal_guarded_0 #1.0R val___pal_guarded_0_0) **
+        (Typedef_uint64_t.ty_uint64_t__pred (!var___pal_guarded_0) 1.0R) **
+        (with_pure ((!var___pal_guarded_0) = (!(!var_src)))))));
+    assert ((Pulse.Lib.Reference.pts_to (!var_src) #'p_src_0 'val_src_0));
+    assert ((Typedef_uint64_t.ty_uint64_t__pred (!(!var_src)) 'p_src_0));
+  };
+}
\ No newline at end of file
diff --git head/nullable_out/Func_opt_write.fsti head/nullable_out/Func_opt_write.fsti
new file mode 100644
index 0000000..fa096c6
--- /dev/null
+++ head/nullable_out/Func_opt_write.fsti
@@ -0,0 +1,19 @@
+module Func_opt_write
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_opt_write
+  (var_src: (ref Typedef_uint64_t.ty_uint64_t))
+  (var_dst: (ref Typedef_uint64_t.ty_uint64_t))
+requires ((unless_null var_dst (((Pulse.Lib.Reference.pts_to_uninit var_dst)))))
+preserves (Pulse.Lib.Reference.pts_to var_src #'p_src_0 'val_src_0)
+preserves (Typedef_uint64_t.ty_uint64_t__pred (!var_src) 'p_src_0)
+returns return_1 : unit
+ensures
+  ((unless_null
+      var_dst
+      (exists* (val_dst_0: Typedef_uint64_t.ty_uint64_t).
+        ((Pulse.Lib.Reference.pts_to var_dst #1.0R val_dst_0) **
+          (Typedef_uint64_t.ty_uint64_t__pred (!var_dst) 1.0R) **
+          (with_pure ((!var_dst) = (!var_src)))))))
\ No newline at end of file
diff --git head/nullable_out/Func_opt_write_early_return.fst head/nullable_out/Func_opt_write_early_return.fst
new file mode 100644
index 0000000..612c677
--- /dev/null
+++ head/nullable_out/Func_opt_write_early_return.fst
@@ -0,0 +1,32 @@
+module Func_opt_write_early_return
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_opt_write_early_return
+    (var_src: (ref Typedef_uint32_t.ty_uint32_t))
+    (var_dst: (ref Typedef_uint32_t.ty_uint32_t))
+  requires ((unless_null var_dst (((Pulse.Lib.Reference.pts_to_uninit var_dst)))))
+  preserves (Pulse.Lib.Reference.pts_to var_src #'p_src_0 'val_src_0)
+  preserves (Typedef_uint32_t.ty_uint32_t__pred (!var_src) 'p_src_0)
+  returns return_1 : unit
+  ensures
+    ((unless_null
+        var_dst
+        (exists* (val_dst_0: Typedef_uint32_t.ty_uint32_t).
+          ((Pulse.Lib.Reference.pts_to var_dst #1.0R val_dst_0) **
+            (Typedef_uint32_t.ty_uint32_t__pred (!var_dst) 1.0R) **
+            (with_pure ((!var_dst) = (!var_src)))))))
+{
+  let mut var_src = var_src;
+  let mut var_dst = var_dst;
+  if ((Pulse.Lib.Reference.is_null (!var_dst))) {
+    let var___pal_guarded_1 = ((!var_dst));
+    Pulse.Lib.C.Nullable.elim_null_ref var___pal_guarded_1;
+    return;
+  } else {
+    let var___pal_guarded_1 = ((!var_dst));
+    Pulse.Lib.C.Nullable.elim_unless_null_ref var___pal_guarded_1;
+  };
+  (!var_dst) := (!(!var_src));
+}
\ No newline at end of file
diff --git head/nullable_out/Func_opt_write_early_return.fsti head/nullable_out/Func_opt_write_early_return.fsti
new file mode 100644
index 0000000..26b6ab8
--- /dev/null
+++ head/nullable_out/Func_opt_write_early_return.fsti
@@ -0,0 +1,19 @@
+module Func_opt_write_early_return
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_opt_write_early_return
+  (var_src: (ref Typedef_uint32_t.ty_uint32_t))
+  (var_dst: (ref Typedef_uint32_t.ty_uint32_t))
+requires ((unless_null var_dst (((Pulse.Lib.Reference.pts_to_uninit var_dst)))))
+preserves (Pulse.Lib.Reference.pts_to var_src #'p_src_0 'val_src_0)
+preserves (Typedef_uint32_t.ty_uint32_t__pred (!var_src) 'p_src_0)
+returns return_1 : unit
+ensures
+  ((unless_null
+      var_dst
+      (exists* (val_dst_0: Typedef_uint32_t.ty_uint32_t).
+        ((Pulse.Lib.Reference.pts_to var_dst #1.0R val_dst_0) **
+          (Typedef_uint32_t.ty_uint32_t__pred (!var_dst) 1.0R) **
+          (with_pure ((!var_dst) = (!var_src)))))))
\ No newline at end of file
diff --git head/nullable_out/Func_opt_write_many.fst head/nullable_out/Func_opt_write_many.fst
new file mode 100644
index 0000000..28c027c
--- /dev/null
+++ head/nullable_out/Func_opt_write_many.fst
@@ -0,0 +1,77 @@
+module Func_opt_write_many
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_opt_write_many
+    (var_src: (ref Typedef_uint64_t.ty_uint64_t))
+    (var_first: (ref Typedef_uint64_t.ty_uint64_t))
+    (var_second: (ref Typedef_uint64_t.ty_uint64_t))
+  requires ((unless_null var_first (((Pulse.Lib.Reference.pts_to_uninit var_first)))))
+  requires ((unless_null var_second (((Pulse.Lib.Reference.pts_to_uninit var_second)))))
+  preserves (Pulse.Lib.Reference.pts_to var_src #'p_src_0 'val_src_0)
+  preserves (Typedef_uint64_t.ty_uint64_t__pred (!var_src) 'p_src_0)
+  returns return_1 : unit
+  ensures
+    ((unless_null
+        var_first
+        (exists* (val_first_0: Typedef_uint64_t.ty_uint64_t).
+          ((Pulse.Lib.Reference.pts_to var_first #1.0R val_first_0) **
+            (Typedef_uint64_t.ty_uint64_t__pred (!var_first) 1.0R) **
+            (with_pure ((!var_first) = (!var_src)))))))
+  ensures
+    ((unless_null
+        var_second
+        (exists* (val_second_0: Typedef_uint64_t.ty_uint64_t).
+          ((Pulse.Lib.Reference.pts_to var_second #1.0R val_second_0) **
+            (Typedef_uint64_t.ty_uint64_t__pred (!var_second) 1.0R) **
+            (with_pure ((!var_second) = (!var_src)))))))
+{
+  let mut var_src = var_src;
+  let mut var_first = var_first;
+  let mut var_second = var_second;
+  if ((not (Pulse.Lib.Reference.is_null (!var_first)))) {
+    let var___pal_guarded_2 = ((!var_first));
+    Pulse.Lib.C.Nullable.elim_unless_null_ref var___pal_guarded_2;
+    (!var_first) := (!(!var_src));
+    assert (Pulse.Lib.C.Nullable.unless_null var___pal_guarded_2 (exists*
+      (val___pal_guarded_2_0: Typedef_uint64_t.ty_uint64_t).
+      ((Pulse.Lib.Reference.pts_to var___pal_guarded_2 #1.0R val___pal_guarded_2_0) **
+        (Typedef_uint64_t.ty_uint64_t__pred (!var___pal_guarded_2) 1.0R) **
+        (with_pure ((!var___pal_guarded_2) = (!(!var_src)))))));
+    assert ((Pulse.Lib.Reference.pts_to (!var_src) #'p_src_0 'val_src_0));
+    assert ((Typedef_uint64_t.ty_uint64_t__pred (!(!var_src)) 'p_src_0));
+  } else {
+    let var___pal_guarded_2 = ((!var_first));
+    Pulse.Lib.C.Nullable.elim_null_ref var___pal_guarded_2;
+    assert (Pulse.Lib.C.Nullable.unless_null var___pal_guarded_2 (exists*
+      (val___pal_guarded_2_0: Typedef_uint64_t.ty_uint64_t).
+      ((Pulse.Lib.Reference.pts_to var___pal_guarded_2 #1.0R val___pal_guarded_2_0) **
+        (Typedef_uint64_t.ty_uint64_t__pred (!var___pal_guarded_2) 1.0R) **
+        (with_pure ((!var___pal_guarded_2) = (!(!var_src)))))));
+    assert ((Pulse.Lib.Reference.pts_to (!var_src) #'p_src_0 'val_src_0));
+    assert ((Typedef_uint64_t.ty_uint64_t__pred (!(!var_src)) 'p_src_0));
+  };
+  if ((not (Pulse.Lib.Reference.is_null (!var_second)))) {
+    let var___pal_guarded_3 = ((!var_second));
+    Pulse.Lib.C.Nullable.elim_unless_null_ref var___pal_guarded_3;
+    (!var_second) := (!(!var_src));
+    assert (Pulse.Lib.C.Nullable.unless_null var___pal_guarded_3 (exists*
+      (val___pal_guarded_3_0: Typedef_uint64_t.ty_uint64_t).
+      ((Pulse.Lib.Reference.pts_to var___pal_guarded_3 #1.0R val___pal_guarded_3_0) **
+        (Typedef_uint64_t.ty_uint64_t__pred (!var___pal_guarded_3) 1.0R) **
+        (with_pure ((!var___pal_guarded_3) = (!(!var_src)))))));
+    assert ((Pulse.Lib.Reference.pts_to (!var_src) #'p_src_0 'val_src_0));
+    assert ((Typedef_uint64_t.ty_uint64_t__pred (!(!var_src)) 'p_src_0));
+  } else {
+    let var___pal_guarded_3 = ((!var_second));
+    Pulse.Lib.C.Nullable.elim_null_ref var___pal_guarded_3;
+    assert (Pulse.Lib.C.Nullable.unless_null var___pal_guarded_3 (exists*
+      (val___pal_guarded_3_0: Typedef_uint64_t.ty_uint64_t).
+      ((Pulse.Lib.Reference.pts_to var___pal_guarded_3 #1.0R val___pal_guarded_3_0) **
+        (Typedef_uint64_t.ty_uint64_t__pred (!var___pal_guarded_3) 1.0R) **
+        (with_pure ((!var___pal_guarded_3) = (!(!var_src)))))));
+    assert ((Pulse.Lib.Reference.pts_to (!var_src) #'p_src_0 'val_src_0));
+    assert ((Typedef_uint64_t.ty_uint64_t__pred (!(!var_src)) 'p_src_0));
+  };
+}
\ No newline at end of file
diff --git head/nullable_out/Func_opt_write_many.fsti head/nullable_out/Func_opt_write_many.fsti
new file mode 100644
index 0000000..2806a5b
--- /dev/null
+++ head/nullable_out/Func_opt_write_many.fsti
@@ -0,0 +1,28 @@
+module Func_opt_write_many
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_opt_write_many
+  (var_src: (ref Typedef_uint64_t.ty_uint64_t))
+  (var_first: (ref Typedef_uint64_t.ty_uint64_t))
+  (var_second: (ref Typedef_uint64_t.ty_uint64_t))
+requires ((unless_null var_first (((Pulse.Lib.Reference.pts_to_uninit var_first)))))
+requires ((unless_null var_second (((Pulse.Lib.Reference.pts_to_uninit var_second)))))
+preserves (Pulse.Lib.Reference.pts_to var_src #'p_src_0 'val_src_0)
+preserves (Typedef_uint64_t.ty_uint64_t__pred (!var_src) 'p_src_0)
+returns return_1 : unit
+ensures
+  ((unless_null
+      var_first
+      (exists* (val_first_0: Typedef_uint64_t.ty_uint64_t).
+        ((Pulse.Lib.Reference.pts_to var_first #1.0R val_first_0) **
+          (Typedef_uint64_t.ty_uint64_t__pred (!var_first) 1.0R) **
+          (with_pure ((!var_first) = (!var_src)))))))
+ensures
+  ((unless_null
+      var_second
+      (exists* (val_second_0: Typedef_uint64_t.ty_uint64_t).
+        ((Pulse.Lib.Reference.pts_to var_second #1.0R val_second_0) **
+          (Typedef_uint64_t.ty_uint64_t__pred (!var_second) 1.0R) **
+          (with_pure ((!var_second) = (!var_src)))))))
\ No newline at end of file
diff --git head/nullable_out/Func_takes_array.fst head/nullable_out/Func_takes_array.fst
new file mode 100644
index 0000000..57a5609
--- /dev/null
+++ head/nullable_out/Func_takes_array.fst
@@ -0,0 +1,14 @@
+module Func_takes_array
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_takes_array (var_a: (array Typedef_uint8_t.ty_uint8_t))
+  requires
+    exists* (val_a_0: (full_array_spec Typedef_uint8_t.ty_uint8_t)).
+    ((array_pts_to_full var_a 1.0R val_a_0))
+  returns return_1 : unit
+  ensures
+    exists* (val_a_0: (full_array_spec Typedef_uint8_t.ty_uint8_t)).
+    ((array_pts_to_full var_a 1.0R val_a_0))
+{ assume pure False; unreachable () }
\ No newline at end of file
diff --git head/nullable_out/Struct_pair.fst head/nullable_out/Struct_pair.fst
new file mode 100644
index 0000000..1eeb6d3
--- /dev/null
+++ head/nullable_out/Struct_pair.fst
@@ -0,0 +1,99 @@
+module Struct_pair
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+noeq type struct_pair = {
+  struct_pair__lo: Typedef_uint64_t.ty_uint64_t;
+  struct_pair__hi: Typedef_uint64_t.ty_uint64_t;
+}
+assume val struct_pair__sizeof_pos (a: Type0 { a == struct_pair }) :
+    Lemma
+    ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
+    [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+[@@pulse_eager_unfold] let predicate struct_pair__pred ([@@@mkey] this: struct_pair) (p: perm) =
+  ((Typedef_uint64_t.ty_uint64_t__pred this.struct_pair__lo p) **
+    (Typedef_uint64_t.ty_uint64_t__pred this.struct_pair__hi p))
+[@@pulse_eager_unfold] let predicate struct_pair__uninit_pred ([@@@mkey] this: struct_pair) =
+  ((Typedef_uint64_t.ty_uint64_t__uninit_pred this.struct_pair__lo) **
+    (Typedef_uint64_t.ty_uint64_t__uninit_pred this.struct_pair__hi))
+assume val struct_pair__aux_raw_unfolded ([@@@mkey] x: (ref struct_pair)) (p: perm) : slprop
+assume val struct_pair__lo_1 (x: (ref struct_pair)) : GTot (ref Typedef_uint64_t.ty_uint64_t)
+assume val struct_pair__hi_1 (x: (ref struct_pair)) : GTot (ref Typedef_uint64_t.ty_uint64_t)
+assume val struct_pair__lo_container (r: (ref Typedef_uint64_t.ty_uint64_t)) : (ref struct_pair)
+assume val struct_pair__lo_container_inv (p: (ref struct_pair)) :
+    Lemma
+      (ensures (struct_pair__lo_container (struct_pair__lo_1 p)) == p)
+      [SMTPat (struct_pair__lo_container (struct_pair__lo_1 p))]
+assume val struct_pair__lo_proj_container_inv (r: (ref Typedef_uint64_t.ty_uint64_t)) :
+    Lemma
+      (ensures (struct_pair__lo_1 (struct_pair__lo_container r)) == r)
+      [SMTPat (struct_pair__lo_1 (struct_pair__lo_container r))]
+assume val struct_pair__hi_container (r: (ref Typedef_uint64_t.ty_uint64_t)) : (ref struct_pair)
+assume val struct_pair__hi_container_inv (p: (ref struct_pair)) :
+    Lemma
+      (ensures (struct_pair__hi_container (struct_pair__hi_1 p)) == p)
+      [SMTPat (struct_pair__hi_container (struct_pair__hi_1 p))]
+assume val struct_pair__hi_proj_container_inv (r: (ref Typedef_uint64_t.ty_uint64_t)) :
+    Lemma
+      (ensures (struct_pair__hi_1 (struct_pair__hi_container r)) == r)
+      [SMTPat (struct_pair__hi_1 (struct_pair__hi_container r))]
+assume val struct_pair__lo_proj_null :
+    (squash
+      ((struct_pair__lo_1 (Pulse.Lib.Reference.null #(struct_pair))) ==
+        (Pulse.Lib.Reference.null #(Typedef_uint64_t.ty_uint64_t))))
+[@@pulse_intro]
+assume val struct_pair__aux_raw_unfold (x: (ref struct_pair)) (#p: perm) (vx: struct_pair) :
+    (stt_ghost
+      unit
+      emp_inames
+      (Pulse.Lib.Reference.pts_to x #p vx)
+      (fun _ ->
+        ((struct_pair__aux_raw_unfolded x p) **
+          (Pulse.Lib.Reference.pts_to (struct_pair__lo_1 x) #p vx.struct_pair__lo) **
+          (Pulse.Lib.Reference.pts_to (struct_pair__hi_1 x) #p vx.struct_pair__hi))))
+[@@pulse_intro]
+assume val struct_pair__aux_raw_fold (x: (ref struct_pair)) (#p: perm) v_lo v_hi :
+    (stt_ghost
+      unit
+      emp_inames
+      ((struct_pair__aux_raw_unfolded x p) **
+        (Pulse.Lib.Reference.pts_to (struct_pair__lo_1 x) #p v_lo) **
+        (Pulse.Lib.Reference.pts_to (struct_pair__hi_1 x) #p v_hi))
+      (fun _ -> (Pulse.Lib.Reference.pts_to x #p { struct_pair__lo=v_lo; struct_pair__hi=v_hi; })))
+[@@pulse_intro]
+assume val struct_pair__aux_raw_fold_uninit (x: (ref struct_pair)) :
+    (stt_ghost
+      unit
+      emp_inames
+      ((struct_pair__aux_raw_unfolded x 1.0R) **
+        (Pulse.Lib.Reference.pts_to_uninit (struct_pair__lo_1 x)) **
+        (Pulse.Lib.Reference.pts_to_uninit (struct_pair__hi_1 x)))
+      (fun _ -> (Pulse.Lib.Reference.pts_to_uninit x)))
+assume val struct_pair__aux_raw_unfold_uninit (x: (ref struct_pair)) :
+    (stt_ghost
+      unit
+      emp_inames
+      (Pulse.Lib.Reference.pts_to_uninit x)
+      (fun _ ->
+        ((struct_pair__aux_raw_unfolded x 1.0R) **
+          (Pulse.Lib.Reference.pts_to_uninit (struct_pair__lo_1 x)) **
+          (Pulse.Lib.Reference.pts_to_uninit (struct_pair__hi_1 x)))))
+[@@pulse_impure_spec_no_proof_required]
+assume val struct_pair__get_lo (x: (ref struct_pair)) (#p: perm) :
+    (stt_atomic
+      (ref Typedef_uint64_t.ty_uint64_t)
+      #PulseCore.Observability.Neutral
+      emp_inames
+      (struct_pair__aux_raw_unfolded x p)
+      (fun vx' -> ((struct_pair__aux_raw_unfolded x p) ** (rewrites_to vx' (struct_pair__lo_1 x)))))
+[@@pulse_impure_spec_no_proof_required]
+assume val struct_pair__get_hi (x: (ref struct_pair)) (#p: perm) :
+    (stt_atomic
+      (ref Typedef_uint64_t.ty_uint64_t)
+      #PulseCore.Observability.Neutral
+      emp_inames
+      (struct_pair__aux_raw_unfolded x p)
+      (fun vx' -> ((struct_pair__aux_raw_unfolded x p) ** (rewrites_to vx' (struct_pair__hi_1 x)))))
+instance has_zero_default_struct_pair : (has_zero_default struct_pair) =
+  { zero_default = { struct_pair__lo = zero_default; struct_pair__hi = zero_default; } }
\ No newline at end of file
diff --git head/nullable_out/TranslationErrors.fst head/nullable_out/TranslationErrors.fst
new file mode 100644
index 0000000..bf62561
--- /dev/null
+++ head/nullable_out/TranslationErrors.fst
@@ -0,0 +1 @@
+module TranslationErrors
diff --git head/nullable_out/Typedef___uint32_t.fst head/nullable_out/Typedef___uint32_t.fst
new file mode 100644
index 0000000..b9a5b44
--- /dev/null
+++ head/nullable_out/Typedef___uint32_t.fst
@@ -0,0 +1,13 @@
+module Typedef___uint32_t
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+unfold
+let ty___uint32_t : Type = UInt32.t
+[@@pulse_eager_unfold] let predicate ty___uint32_t__pred ([@@@mkey] this: ty___uint32_t) (p: perm) =
+  emp
+[@@pulse_eager_unfold] let predicate ty___uint32_t__uninit_pred ([@@@mkey] this: ty___uint32_t) =
+  emp
+instance has_zero_default_ty___uint32_t : (has_zero_default ty___uint32_t) =
+  { zero_default = (UInt32.uint_to_t 0) }
\ No newline at end of file
diff --git head/nullable_out/Typedef___uint64_t.fst head/nullable_out/Typedef___uint64_t.fst
new file mode 100644
index 0000000..d25b7c4
--- /dev/null
+++ head/nullable_out/Typedef___uint64_t.fst
@@ -0,0 +1,13 @@
+module Typedef___uint64_t
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+unfold
+let ty___uint64_t : Type = UInt64.t
+[@@pulse_eager_unfold] let predicate ty___uint64_t__pred ([@@@mkey] this: ty___uint64_t) (p: perm) =
+  emp
+[@@pulse_eager_unfold] let predicate ty___uint64_t__uninit_pred ([@@@mkey] this: ty___uint64_t) =
+  emp
+instance has_zero_default_ty___uint64_t : (has_zero_default ty___uint64_t) =
+  { zero_default = (UInt64.uint_to_t 0) }
\ No newline at end of file
diff --git head/nullable_out/Typedef___uint8_t.fst head/nullable_out/Typedef___uint8_t.fst
new file mode 100644
index 0000000..ad40932
--- /dev/null
+++ head/nullable_out/Typedef___uint8_t.fst
@@ -0,0 +1,12 @@
+module Typedef___uint8_t
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+unfold
+let ty___uint8_t : Type = UInt8.t
+[@@pulse_eager_unfold] let predicate ty___uint8_t__pred ([@@@mkey] this: ty___uint8_t) (p: perm) =
+  emp
+[@@pulse_eager_unfold] let predicate ty___uint8_t__uninit_pred ([@@@mkey] this: ty___uint8_t) = emp
+instance has_zero_default_ty___uint8_t : (has_zero_default ty___uint8_t) =
+  { zero_default = (UInt8.uint_to_t 0) }
\ No newline at end of file
diff --git head/nullable_out/Typedef_uint32_t.fst head/nullable_out/Typedef_uint32_t.fst
new file mode 100644
index 0000000..aa0f488
--- /dev/null
+++ head/nullable_out/Typedef_uint32_t.fst
@@ -0,0 +1,13 @@
+module Typedef_uint32_t
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+unfold
+let ty_uint32_t : Type = Typedef___uint32_t.ty___uint32_t
+[@@pulse_eager_unfold] let predicate ty_uint32_t__pred ([@@@mkey] this: ty_uint32_t) (p: perm) =
+  ((Typedef___uint32_t.ty___uint32_t__pred this p))
+[@@pulse_eager_unfold] let predicate ty_uint32_t__uninit_pred ([@@@mkey] this: ty_uint32_t) =
+  ((Typedef___uint32_t.ty___uint32_t__uninit_pred this))
+instance has_zero_default_ty_uint32_t : (has_zero_default ty_uint32_t) =
+  { zero_default = zero_default }
\ No newline at end of file
diff --git head/nullable_out/Typedef_uint64_t.fst head/nullable_out/Typedef_uint64_t.fst
new file mode 100644
index 0000000..0d4740d
--- /dev/null
+++ head/nullable_out/Typedef_uint64_t.fst
@@ -0,0 +1,13 @@
+module Typedef_uint64_t
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+unfold
+let ty_uint64_t : Type = Typedef___uint64_t.ty___uint64_t
+[@@pulse_eager_unfold] let predicate ty_uint64_t__pred ([@@@mkey] this: ty_uint64_t) (p: perm) =
+  ((Typedef___uint64_t.ty___uint64_t__pred this p))
+[@@pulse_eager_unfold] let predicate ty_uint64_t__uninit_pred ([@@@mkey] this: ty_uint64_t) =
+  ((Typedef___uint64_t.ty___uint64_t__uninit_pred this))
+instance has_zero_default_ty_uint64_t : (has_zero_default ty_uint64_t) =
+  { zero_default = zero_default }
\ No newline at end of file
diff --git head/nullable_out/Typedef_uint8_t.fst head/nullable_out/Typedef_uint8_t.fst
new file mode 100644
index 0000000..f758bc7
--- /dev/null
+++ head/nullable_out/Typedef_uint8_t.fst
@@ -0,0 +1,13 @@
+module Typedef_uint8_t
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+unfold
+let ty_uint8_t : Type = Typedef___uint8_t.ty___uint8_t
+[@@pulse_eager_unfold] let predicate ty_uint8_t__pred ([@@@mkey] this: ty_uint8_t) (p: perm) =
+  ((Typedef___uint8_t.ty___uint8_t__pred this p))
+[@@pulse_eager_unfold] let predicate ty_uint8_t__uninit_pred ([@@@mkey] this: ty_uint8_t) =
+  ((Typedef___uint8_t.ty___uint8_t__uninit_pred this))
+instance has_zero_default_ty_uint8_t : (has_zero_default ty_uint8_t) =
+  { zero_default = zero_default }
\ No newline at end of file
diff --git head/nullable_out/diagnostics.json head/nullable_out/diagnostics.json
new file mode 100644
index 0000000..9e26dfe
--- /dev/null
+++ head/nullable_out/diagnostics.json
@@ -0,0 +1 @@
+{}
\ No newline at end of file
diff --git head/nullable_out_struct/Func_opt_two_from_struct.fst head/nullable_out_struct/Func_opt_two_from_struct.fst
new file mode 100644
index 0000000..5d2d972
--- /dev/null
+++ head/nullable_out_struct/Func_opt_two_from_struct.fst
@@ -0,0 +1,77 @@
+module Func_opt_two_from_struct
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_opt_two_from_struct
+    (var_src: (ref Typedef_pair.ty_pair))
+    (var_a: (ref Typedef_uint64_t.ty_uint64_t))
+    (var_b: (ref Typedef_uint64_t.ty_uint64_t))
+  requires ((unless_null var_a (((Pulse.Lib.Reference.pts_to_uninit var_a)))))
+  requires ((unless_null var_b (((Pulse.Lib.Reference.pts_to_uninit var_b)))))
+  preserves (Pulse.Lib.Reference.pts_to var_src #'p_src_0 'val_src_0)
+  preserves (Typedef_pair.ty_pair__pred (!var_src) 'p_src_0)
+  returns return_1 : unit
+  ensures
+    ((unless_null
+        var_a
+        (exists* (val_a_0: Typedef_uint64_t.ty_uint64_t).
+          ((Pulse.Lib.Reference.pts_to var_a #1.0R val_a_0) **
+            (Typedef_uint64_t.ty_uint64_t__pred (!var_a) 1.0R) **
+            (with_pure ((!var_a) = (!(Struct_pair.struct_pair__get_fst var_src))))))))
+  ensures
+    ((unless_null
+        var_b
+        (exists* (val_b_0: Typedef_uint64_t.ty_uint64_t).
+          ((Pulse.Lib.Reference.pts_to var_b #1.0R val_b_0) **
+            (Typedef_uint64_t.ty_uint64_t__pred (!var_b) 1.0R) **
+            (with_pure ((!var_b) = (!(Struct_pair.struct_pair__get_snd var_src))))))))
+{
+  let mut var_src = var_src;
+  let mut var_a = var_a;
+  let mut var_b = var_b;
+  if ((not (Pulse.Lib.Reference.is_null (!var_a)))) {
+    let var___pal_guarded_0 = ((!var_a));
+    Pulse.Lib.C.Nullable.elim_unless_null_ref var___pal_guarded_0;
+    (!var_a) := (!(Struct_pair.struct_pair__get_fst (!var_src)));
+    assert (Pulse.Lib.C.Nullable.unless_null var___pal_guarded_0 (exists*
+      (val___pal_guarded_0_0: Typedef_uint64_t.ty_uint64_t).
+      ((Pulse.Lib.Reference.pts_to var___pal_guarded_0 #1.0R val___pal_guarded_0_0) **
+        (Typedef_uint64_t.ty_uint64_t__pred (!var___pal_guarded_0) 1.0R) **
+        (with_pure ((!var___pal_guarded_0) = (!(Struct_pair.struct_pair__get_fst (!var_src))))))));
+    assert ((Pulse.Lib.Reference.pts_to (!var_src) #'p_src_0 'val_src_0));
+    assert ((Typedef_pair.ty_pair__pred (!(!var_src)) 'p_src_0));
+  } else {
+    let var___pal_guarded_0 = ((!var_a));
+    Pulse.Lib.C.Nullable.elim_null_ref var___pal_guarded_0;
+    assert (Pulse.Lib.C.Nullable.unless_null var___pal_guarded_0 (exists*
+      (val___pal_guarded_0_0: Typedef_uint64_t.ty_uint64_t).
+      ((Pulse.Lib.Reference.pts_to var___pal_guarded_0 #1.0R val___pal_guarded_0_0) **
+        (Typedef_uint64_t.ty_uint64_t__pred (!var___pal_guarded_0) 1.0R) **
+        (with_pure ((!var___pal_guarded_0) = (!(Struct_pair.struct_pair__get_fst (!var_src))))))));
+    assert ((Pulse.Lib.Reference.pts_to (!var_src) #'p_src_0 'val_src_0));
+    assert ((Typedef_pair.ty_pair__pred (!(!var_src)) 'p_src_0));
+  };
+  if ((not (Pulse.Lib.Reference.is_null (!var_b)))) {
+    let var___pal_guarded_1 = ((!var_b));
+    Pulse.Lib.C.Nullable.elim_unless_null_ref var___pal_guarded_1;
+    (!var_b) := (!(Struct_pair.struct_pair__get_snd (!var_src)));
+    assert (Pulse.Lib.C.Nullable.unless_null var___pal_guarded_1 (exists*
+      (val___pal_guarded_1_0: Typedef_uint64_t.ty_uint64_t).
+      ((Pulse.Lib.Reference.pts_to var___pal_guarded_1 #1.0R val___pal_guarded_1_0) **
+        (Typedef_uint64_t.ty_uint64_t__pred (!var___pal_guarded_1) 1.0R) **
+        (with_pure ((!var___pal_guarded_1) = (!(Struct_pair.struct_pair__get_snd (!var_src))))))));
+    assert ((Pulse.Lib.Reference.pts_to (!var_src) #'p_src_0 'val_src_0));
+    assert ((Typedef_pair.ty_pair__pred (!(!var_src)) 'p_src_0));
+  } else {
+    let var___pal_guarded_1 = ((!var_b));
+    Pulse.Lib.C.Nullable.elim_null_ref var___pal_guarded_1;
+    assert (Pulse.Lib.C.Nullable.unless_null var___pal_guarded_1 (exists*
+      (val___pal_guarded_1_0: Typedef_uint64_t.ty_uint64_t).
+      ((Pulse.Lib.Reference.pts_to var___pal_guarded_1 #1.0R val___pal_guarded_1_0) **
+        (Typedef_uint64_t.ty_uint64_t__pred (!var___pal_guarded_1) 1.0R) **
+        (with_pure ((!var___pal_guarded_1) = (!(Struct_pair.struct_pair__get_snd (!var_src))))))));
+    assert ((Pulse.Lib.Reference.pts_to (!var_src) #'p_src_0 'val_src_0));
+    assert ((Typedef_pair.ty_pair__pred (!(!var_src)) 'p_src_0));
+  };
+}
\ No newline at end of file
diff --git head/nullable_out_struct/Func_opt_two_from_struct.fsti head/nullable_out_struct/Func_opt_two_from_struct.fsti
new file mode 100644
index 0000000..a67e44b
--- /dev/null
+++ head/nullable_out_struct/Func_opt_two_from_struct.fsti
@@ -0,0 +1,28 @@
+module Func_opt_two_from_struct
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_opt_two_from_struct
+  (var_src: (ref Typedef_pair.ty_pair))
+  (var_a: (ref Typedef_uint64_t.ty_uint64_t))
+  (var_b: (ref Typedef_uint64_t.ty_uint64_t))
+requires ((unless_null var_a (((Pulse.Lib.Reference.pts_to_uninit var_a)))))
+requires ((unless_null var_b (((Pulse.Lib.Reference.pts_to_uninit var_b)))))
+preserves (Pulse.Lib.Reference.pts_to var_src #'p_src_0 'val_src_0)
+preserves (Typedef_pair.ty_pair__pred (!var_src) 'p_src_0)
+returns return_1 : unit
+ensures
+  ((unless_null
+      var_a
+      (exists* (val_a_0: Typedef_uint64_t.ty_uint64_t).
+        ((Pulse.Lib.Reference.pts_to var_a #1.0R val_a_0) **
+          (Typedef_uint64_t.ty_uint64_t__pred (!var_a) 1.0R) **
+          (with_pure ((!var_a) = (!(Struct_pair.struct_pair__get_fst var_src))))))))
+ensures
+  ((unless_null
+      var_b
+      (exists* (val_b_0: Typedef_uint64_t.ty_uint64_t).
+        ((Pulse.Lib.Reference.pts_to var_b #1.0R val_b_0) **
+          (Typedef_uint64_t.ty_uint64_t__pred (!var_b) 1.0R) **
+          (with_pure ((!var_b) = (!(Struct_pair.struct_pair__get_snd var_src))))))))
\ No newline at end of file
diff --git head/nullable_out_struct/Struct_pair.fst head/nullable_out_struct/Struct_pair.fst
new file mode 100644
index 0000000..bd7af14
--- /dev/null
+++ head/nullable_out_struct/Struct_pair.fst
@@ -0,0 +1,102 @@
+module Struct_pair
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+noeq type struct_pair = {
+  struct_pair__fst: Typedef_uint64_t.ty_uint64_t;
+  struct_pair__snd: Typedef_uint64_t.ty_uint64_t;
+}
+assume val struct_pair__sizeof_pos (a: Type0 { a == struct_pair }) :
+    Lemma
+    ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
+    [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+[@@pulse_eager_unfold] let predicate struct_pair__pred ([@@@mkey] this: struct_pair) (p: perm) =
+  ((Typedef_uint64_t.ty_uint64_t__pred this.struct_pair__fst p) **
+    (Typedef_uint64_t.ty_uint64_t__pred this.struct_pair__snd p))
+[@@pulse_eager_unfold] let predicate struct_pair__uninit_pred ([@@@mkey] this: struct_pair) =
+  ((Typedef_uint64_t.ty_uint64_t__uninit_pred this.struct_pair__fst) **
+    (Typedef_uint64_t.ty_uint64_t__uninit_pred this.struct_pair__snd))
+assume val struct_pair__aux_raw_unfolded ([@@@mkey] x: (ref struct_pair)) (p: perm) : slprop
+assume val struct_pair__fst_1 (x: (ref struct_pair)) : GTot (ref Typedef_uint64_t.ty_uint64_t)
+assume val struct_pair__snd_1 (x: (ref struct_pair)) : GTot (ref Typedef_uint64_t.ty_uint64_t)
+assume val struct_pair__fst_container (r: (ref Typedef_uint64_t.ty_uint64_t)) : (ref struct_pair)
+assume val struct_pair__fst_container_inv (p: (ref struct_pair)) :
+    Lemma
+      (ensures (struct_pair__fst_container (struct_pair__fst_1 p)) == p)
+      [SMTPat (struct_pair__fst_container (struct_pair__fst_1 p))]
+assume val struct_pair__fst_proj_container_inv (r: (ref Typedef_uint64_t.ty_uint64_t)) :
+    Lemma
+      (ensures (struct_pair__fst_1 (struct_pair__fst_container r)) == r)
+      [SMTPat (struct_pair__fst_1 (struct_pair__fst_container r))]
+assume val struct_pair__snd_container (r: (ref Typedef_uint64_t.ty_uint64_t)) : (ref struct_pair)
+assume val struct_pair__snd_container_inv (p: (ref struct_pair)) :
+    Lemma
+      (ensures (struct_pair__snd_container (struct_pair__snd_1 p)) == p)
+      [SMTPat (struct_pair__snd_container (struct_pair__snd_1 p))]
+assume val struct_pair__snd_proj_container_inv (r: (ref Typedef_uint64_t.ty_uint64_t)) :
+    Lemma
+      (ensures (struct_pair__snd_1 (struct_pair__snd_container r)) == r)
+      [SMTPat (struct_pair__snd_1 (struct_pair__snd_container r))]
+assume val struct_pair__fst_proj_null :
+    (squash
+      ((struct_pair__fst_1 (Pulse.Lib.Reference.null #(struct_pair))) ==
+        (Pulse.Lib.Reference.null #(Typedef_uint64_t.ty_uint64_t))))
+[@@pulse_intro]
+assume val struct_pair__aux_raw_unfold (x: (ref struct_pair)) (#p: perm) (vx: struct_pair) :
+    (stt_ghost
+      unit
+      emp_inames
+      (Pulse.Lib.Reference.pts_to x #p vx)
+      (fun _ ->
+        ((struct_pair__aux_raw_unfolded x p) **
+          (Pulse.Lib.Reference.pts_to (struct_pair__fst_1 x) #p vx.struct_pair__fst) **
+          (Pulse.Lib.Reference.pts_to (struct_pair__snd_1 x) #p vx.struct_pair__snd))))
+[@@pulse_intro]
+assume val struct_pair__aux_raw_fold (x: (ref struct_pair)) (#p: perm) v_fst v_snd :
+    (stt_ghost
+      unit
+      emp_inames
+      ((struct_pair__aux_raw_unfolded x p) **
+        (Pulse.Lib.Reference.pts_to (struct_pair__fst_1 x) #p v_fst) **
+        (Pulse.Lib.Reference.pts_to (struct_pair__snd_1 x) #p v_snd))
+      (fun _ ->
+        (Pulse.Lib.Reference.pts_to x #p { struct_pair__fst=v_fst; struct_pair__snd=v_snd; })))
+[@@pulse_intro]
+assume val struct_pair__aux_raw_fold_uninit (x: (ref struct_pair)) :
+    (stt_ghost
+      unit
+      emp_inames
+      ((struct_pair__aux_raw_unfolded x 1.0R) **
+        (Pulse.Lib.Reference.pts_to_uninit (struct_pair__fst_1 x)) **
+        (Pulse.Lib.Reference.pts_to_uninit (struct_pair__snd_1 x)))
+      (fun _ -> (Pulse.Lib.Reference.pts_to_uninit x)))
+assume val struct_pair__aux_raw_unfold_uninit (x: (ref struct_pair)) :
+    (stt_ghost
+      unit
+      emp_inames
+      (Pulse.Lib.Reference.pts_to_uninit x)
+      (fun _ ->
+        ((struct_pair__aux_raw_unfolded x 1.0R) **
+          (Pulse.Lib.Reference.pts_to_uninit (struct_pair__fst_1 x)) **
+          (Pulse.Lib.Reference.pts_to_uninit (struct_pair__snd_1 x)))))
+[@@pulse_impure_spec_no_proof_required]
+assume val struct_pair__get_fst (x: (ref struct_pair)) (#p: perm) :
+    (stt_atomic
+      (ref Typedef_uint64_t.ty_uint64_t)
+      #PulseCore.Observability.Neutral
+      emp_inames
+      (struct_pair__aux_raw_unfolded x p)
+      (fun vx' ->
+        ((struct_pair__aux_raw_unfolded x p) ** (rewrites_to vx' (struct_pair__fst_1 x)))))
+[@@pulse_impure_spec_no_proof_required]
+assume val struct_pair__get_snd (x: (ref struct_pair)) (#p: perm) :
+    (stt_atomic
+      (ref Typedef_uint64_t.ty_uint64_t)
+      #PulseCore.Observability.Neutral
+      emp_inames
+      (struct_pair__aux_raw_unfolded x p)
+      (fun vx' ->
+        ((struct_pair__aux_raw_unfolded x p) ** (rewrites_to vx' (struct_pair__snd_1 x)))))
+instance has_zero_default_struct_pair : (has_zero_default struct_pair) =
+  { zero_default = { struct_pair__fst = zero_default; struct_pair__snd = zero_default; } }
\ No newline at end of file
diff --git head/nullable_out_struct/TranslationErrors.fst head/nullable_out_struct/TranslationErrors.fst
new file mode 100644
index 0000000..bf62561
--- /dev/null
+++ head/nullable_out_struct/TranslationErrors.fst
@@ -0,0 +1 @@
+module TranslationErrors
diff --git head/nullable_out_struct/Typedef___uint64_t.fst head/nullable_out_struct/Typedef___uint64_t.fst
new file mode 100644
index 0000000..d25b7c4
--- /dev/null
+++ head/nullable_out_struct/Typedef___uint64_t.fst
@@ -0,0 +1,13 @@
+module Typedef___uint64_t
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+unfold
+let ty___uint64_t : Type = UInt64.t
+[@@pulse_eager_unfold] let predicate ty___uint64_t__pred ([@@@mkey] this: ty___uint64_t) (p: perm) =
+  emp
+[@@pulse_eager_unfold] let predicate ty___uint64_t__uninit_pred ([@@@mkey] this: ty___uint64_t) =
+  emp
+instance has_zero_default_ty___uint64_t : (has_zero_default ty___uint64_t) =
+  { zero_default = (UInt64.uint_to_t 0) }
\ No newline at end of file
diff --git head/nullable_out_struct/Typedef_pair.fst head/nullable_out_struct/Typedef_pair.fst
new file mode 100644
index 0000000..ddfe7f2
--- /dev/null
+++ head/nullable_out_struct/Typedef_pair.fst
@@ -0,0 +1,12 @@
+module Typedef_pair
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+unfold
+let ty_pair : Type = Struct_pair.struct_pair
+[@@pulse_eager_unfold] let predicate ty_pair__pred ([@@@mkey] this: ty_pair) (p: perm) =
+  ((Struct_pair.struct_pair__pred this p))
+[@@pulse_eager_unfold] let predicate ty_pair__uninit_pred ([@@@mkey] this: ty_pair) =
+  ((Struct_pair.struct_pair__uninit_pred this))
+instance has_zero_default_ty_pair : (has_zero_default ty_pair) = { zero_default = zero_default }
\ No newline at end of file
diff --git head/nullable_out_struct/Typedef_uint64_t.fst head/nullable_out_struct/Typedef_uint64_t.fst
new file mode 100644
index 0000000..0d4740d
--- /dev/null
+++ head/nullable_out_struct/Typedef_uint64_t.fst
@@ -0,0 +1,13 @@
+module Typedef_uint64_t
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+unfold
+let ty_uint64_t : Type = Typedef___uint64_t.ty___uint64_t
+[@@pulse_eager_unfold] let predicate ty_uint64_t__pred ([@@@mkey] this: ty_uint64_t) (p: perm) =
+  ((Typedef___uint64_t.ty___uint64_t__pred this p))
+[@@pulse_eager_unfold] let predicate ty_uint64_t__uninit_pred ([@@@mkey] this: ty_uint64_t) =
+  ((Typedef___uint64_t.ty___uint64_t__uninit_pred this))
+instance has_zero_default_ty_uint64_t : (has_zero_default ty_uint64_t) =
+  { zero_default = zero_default }
\ No newline at end of file
diff --git head/nullable_out_struct/diagnostics.json head/nullable_out_struct/diagnostics.json
new file mode 100644
index 0000000..9e26dfe
--- /dev/null
+++ head/nullable_out_struct/diagnostics.json
@@ -0,0 +1 @@
+{}
\ No newline at end of file

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@nikswamy @gebner