Skip to content

Break mutually recursive type definitions with core_ref - #226

Draft
nikswamy wants to merge 1 commit into
mainfrom
nswamy/pal-pr12-mutually-recursive-types
Draft

Break mutually recursive type definitions with core_ref#226
nikswamy wants to merge 1 commit into
mainfrom
nswamy/pal-pr12-mutually-recursive-types

Conversation

@nikswamy

@nikswamy nikswamy commented Aug 19, 2026

Copy link
Copy Markdown
Contributor

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

Base: main. Depends on nothing; reviewable on its own.

A cycle among C types is both an F* module cycle and an ill-founded ownership predicate.
F* reports it as Error 308 from dependency analysis over the whole translation unit, so
a single recursive type reachable from a third-party header took every other module down
with it — and, because the failure was in --dep, a subsequent make ran off a partial
.depend and silently skipped most of the work. A new merge phase builds the definitional
dependency graph (descending into function-pointer signatures, which the emission-order
graph did not) and demotes a pointer to core_ref exactly when its pointee can reach back
to the declaration containing it, recomputing after each removal. Self-references are left
alone; a cycle no pointer can break is reported rather than handed to F*.

Commits

  • Break mutually recursive type definitions with core_ref

Testing

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

@nikswamy
Break mutually recursive type definitions with core_ref
30ff07c 
C lets a type refer to another type that refers back to it, because a
pointer only ever needs a forward declaration. The generated F* has no
such escape hatch: each C type becomes its own module, and a struct's
ownership predicate recurses through its pointer fields into the
pointee's predicate. A cycle among the C types is therefore both a
module cycle and an ill-founded predicate.

F* reports the module cycle as `Error 308: Recursive dependency` from
its dependency analysis, which covers the whole translation unit. A
single recursive type reachable from a third-party header consequently
took every other module down with it, and, because the failure was in
`--dep` rather than in a proof, a subsequent `make` ran off a partial
`.depend` and silently skipped most of the work instead of failing.

`core_ref` already models exactly what is needed here: an axiomatized,
non-parametric raw pointer that drops its pointee type and carries no
automatic ownership. It was reachable only by writing `_core_ref` in the
source, which is not an option for types defined in headers we do not
own. Apply it automatically instead, in a new merge phase that runs
before the declaration toposort:

  - Build the definitional dependency graph over typedef, struct and
    union declarations. This descends into function-pointer signatures,
    which the emission-order graph did not: emission names the argument
    and result modules, so a function-pointer field really does make its
    enclosing type depend on them.
  - Demote a pointer to `core_ref` exactly when its pointee can reach
    back to the declaration that contains it, and recompute, since
    removing an edge can split one component into several.
  - Leave self-references alone. A struct whose pointer field names its
    own type stays within a single module, which F* accepts and which
    the recursive-struct model already relies on.
  - Report a cycle that no pointer can break, rather than handing F* an
    unusable module graph.

Demotion loses the pointee type, so each one is reported as a warning.
Code that needs the type back can cast the `core_ref` to a typed
reference, which is the same discipline an explicit `_core_ref` requires
today.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d
(cherry picked from commit 451d605)
@gebner

gebner commented Aug 24, 2026

Copy link
Copy Markdown
Contributor

Hmm, _core_ref modifies not just the generated F* type, but also the slprop. I don't think we should lightly flip semantics here?

  • What system header file triggered this?
  • Where in the cycle is _core_ref inserted automatically? At every reference, or just in one struct?

@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 → 30ff07c).

Summary 
 /dev/null => head/mutually_recursive_types/Func_depth_of.fst                     |  14 ++++++++++++++
 /dev/null => head/mutually_recursive_types/Func_depth_of.fsti                    |  10 ++++++++++
 /dev/null => head/mutually_recursive_types/Func_peer_id_of.fst                   |  14 ++++++++++++++
 /dev/null => head/mutually_recursive_types/Func_peer_id_of.fsti                  |  10 ++++++++++
 /dev/null => head/mutually_recursive_types/Func_tag_of.fst                       |  14 ++++++++++++++
 /dev/null => head/mutually_recursive_types/Func_tag_of.fsti                      |  10 ++++++++++
 /dev/null => head/mutually_recursive_types/Func_weight_of.fst                    |  14 ++++++++++++++
 /dev/null => head/mutually_recursive_types/Func_weight_of.fsti                   |  10 ++++++++++
 /dev/null => head/mutually_recursive_types/Mutually_recursive_types_include1.fst |   7 +++++++
 /dev/null => head/mutually_recursive_types/Struct_link.fst                       | 103 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 /dev/null => head/mutually_recursive_types/Struct_middle.fst                     |  75 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 /dev/null => head/mutually_recursive_types/Struct_obj.fst                        | 104 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 /dev/null => head/mutually_recursive_types/Struct_outer.fst                      | 105 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 /dev/null => head/mutually_recursive_types/Struct_peer.fst                       | 106 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 /dev/null => head/mutually_recursive_types/Struct_selfnode.fst                   | 112 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 /dev/null => head/mutually_recursive_types/TranslationErrors.fst                 |   1 +
 /dev/null => head/mutually_recursive_types/Typedef___int32_t.fst                 |  12 ++++++++++++
 /dev/null => head/mutually_recursive_types/Typedef_int32_t.fst                   |  13 +++++++++++++
 /dev/null => head/mutually_recursive_types/Typedef_selfnode.fst                  |  13 +++++++++++++
 /dev/null => head/mutually_recursive_types/Typedef_vtable.fst                    |  11 +++++++++++
 /dev/null => head/mutually_recursive_types/diagnostics.json                      |  60 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 21 files changed, 818 insertions(+)

Full diff: full diff artifact

Diff 
diff --git head/mutually_recursive_types/Func_depth_of.fst head/mutually_recursive_types/Func_depth_of.fst
new file mode 100644
index 0000000..17e1e79
--- /dev/null
+++ head/mutually_recursive_types/Func_depth_of.fst
@@ -0,0 +1,14 @@
+module Func_depth_of
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_depth_of (var_o: (ref Struct_outer.struct_outer))
+  preserves (Pulse.Lib.Reference.pts_to var_o #'p_o_0 'val_o_0)
+  preserves (Struct_outer.struct_outer__pred (!var_o) 'p_o_0)
+  returns return_1 : Typedef_int32_t.ty_int32_t
+  ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
+{
+  let mut var_o = var_o;
+  return (!(Struct_outer.struct_outer__get_depth (!var_o)));
+}
\ No newline at end of file
diff --git head/mutually_recursive_types/Func_depth_of.fsti head/mutually_recursive_types/Func_depth_of.fsti
new file mode 100644
index 0000000..b8ec77a
--- /dev/null
+++ head/mutually_recursive_types/Func_depth_of.fsti
@@ -0,0 +1,10 @@
+module Func_depth_of
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_depth_of (var_o: (ref Struct_outer.struct_outer))
+preserves (Pulse.Lib.Reference.pts_to var_o #'p_o_0 'val_o_0)
+preserves (Struct_outer.struct_outer__pred (!var_o) 'p_o_0)
+returns return_1 : Typedef_int32_t.ty_int32_t
+ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
\ No newline at end of file
diff --git head/mutually_recursive_types/Func_peer_id_of.fst head/mutually_recursive_types/Func_peer_id_of.fst
new file mode 100644
index 0000000..92bd1f1
--- /dev/null
+++ head/mutually_recursive_types/Func_peer_id_of.fst
@@ -0,0 +1,14 @@
+module Func_peer_id_of
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_peer_id_of (var_p: (ref Struct_peer.struct_peer))
+  preserves (Pulse.Lib.Reference.pts_to var_p #'p_p_0 'val_p_0)
+  preserves (Struct_peer.struct_peer__pred (!var_p) 'p_p_0)
+  returns return_1 : Typedef_int32_t.ty_int32_t
+  ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
+{
+  let mut var_p = var_p;
+  return (!(Struct_peer.struct_peer__get_peer_id (!var_p)));
+}
\ No newline at end of file
diff --git head/mutually_recursive_types/Func_peer_id_of.fsti head/mutually_recursive_types/Func_peer_id_of.fsti
new file mode 100644
index 0000000..ab3b985
--- /dev/null
+++ head/mutually_recursive_types/Func_peer_id_of.fsti
@@ -0,0 +1,10 @@
+module Func_peer_id_of
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_peer_id_of (var_p: (ref Struct_peer.struct_peer))
+preserves (Pulse.Lib.Reference.pts_to var_p #'p_p_0 'val_p_0)
+preserves (Struct_peer.struct_peer__pred (!var_p) 'p_p_0)
+returns return_1 : Typedef_int32_t.ty_int32_t
+ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
\ No newline at end of file
diff --git head/mutually_recursive_types/Func_tag_of.fst head/mutually_recursive_types/Func_tag_of.fst
new file mode 100644
index 0000000..d73d2a5
--- /dev/null
+++ head/mutually_recursive_types/Func_tag_of.fst
@@ -0,0 +1,14 @@
+module Func_tag_of
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_tag_of (var_o: (ref Struct_obj.struct_obj))
+  preserves (Pulse.Lib.Reference.pts_to var_o #'p_o_0 'val_o_0)
+  preserves (Struct_obj.struct_obj__pred (!var_o) 'p_o_0)
+  returns return_1 : Typedef_int32_t.ty_int32_t
+  ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
+{
+  let mut var_o = var_o;
+  return (!(Struct_obj.struct_obj__get_tag (!var_o)));
+}
\ No newline at end of file
diff --git head/mutually_recursive_types/Func_tag_of.fsti head/mutually_recursive_types/Func_tag_of.fsti
new file mode 100644
index 0000000..2f9db6c
--- /dev/null
+++ head/mutually_recursive_types/Func_tag_of.fsti
@@ -0,0 +1,10 @@
+module Func_tag_of
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_tag_of (var_o: (ref Struct_obj.struct_obj))
+preserves (Pulse.Lib.Reference.pts_to var_o #'p_o_0 'val_o_0)
+preserves (Struct_obj.struct_obj__pred (!var_o) 'p_o_0)
+returns return_1 : Typedef_int32_t.ty_int32_t
+ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
\ No newline at end of file
diff --git head/mutually_recursive_types/Func_weight_of.fst head/mutually_recursive_types/Func_weight_of.fst
new file mode 100644
index 0000000..ad5758a
--- /dev/null
+++ head/mutually_recursive_types/Func_weight_of.fst
@@ -0,0 +1,14 @@
+module Func_weight_of
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_weight_of (var_l: (ref Struct_link.struct_link))
+  preserves (Pulse.Lib.Reference.pts_to var_l #'p_l_0 'val_l_0)
+  preserves (Struct_link.struct_link__pred (!var_l) 'p_l_0)
+  returns return_1 : Typedef_int32_t.ty_int32_t
+  ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
+{
+  let mut var_l = var_l;
+  return (!(Struct_link.struct_link__get_weight (!var_l)));
+}
\ No newline at end of file
diff --git head/mutually_recursive_types/Func_weight_of.fsti head/mutually_recursive_types/Func_weight_of.fsti
new file mode 100644
index 0000000..325c0cd
--- /dev/null
+++ head/mutually_recursive_types/Func_weight_of.fsti
@@ -0,0 +1,10 @@
+module Func_weight_of
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_weight_of (var_l: (ref Struct_link.struct_link))
+preserves (Pulse.Lib.Reference.pts_to var_l #'p_l_0 'val_l_0)
+preserves (Struct_link.struct_link__pred (!var_l) 'p_l_0)
+returns return_1 : Typedef_int32_t.ty_int32_t
+ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
\ No newline at end of file
diff --git head/mutually_recursive_types/Mutually_recursive_types_include1.fst head/mutually_recursive_types/Mutually_recursive_types_include1.fst
new file mode 100644
index 0000000..1a07480
--- /dev/null
+++ head/mutually_recursive_types/Mutually_recursive_types_include1.fst
@@ -0,0 +1,7 @@
+module Mutually_recursive_types_include1
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+let next_of (n: Typedef_selfnode.ty_selfnode) : (ref
+  Typedef_selfnode.ty_selfnode) = n.Struct_selfnode.struct_selfnode__next
\ No newline at end of file
diff --git head/mutually_recursive_types/Struct_link.fst head/mutually_recursive_types/Struct_link.fst
new file mode 100644
index 0000000..c1dc3cd
--- /dev/null
+++ head/mutually_recursive_types/Struct_link.fst
@@ -0,0 +1,103 @@
+module Struct_link
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+noeq type struct_link = {
+  struct_link__weight: Typedef_int32_t.ty_int32_t;
+  struct_link__owner: core_ref;
+}
+assume val struct_link__sizeof_pos (a: Type0 { a == struct_link }) :
+    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_link__pred ([@@@mkey] this: struct_link) (p: perm) =
+  ((Typedef_int32_t.ty_int32_t__pred this.struct_link__weight p))
+[@@pulse_eager_unfold] let predicate struct_link__uninit_pred ([@@@mkey] this: struct_link) =
+  ((Typedef_int32_t.ty_int32_t__uninit_pred this.struct_link__weight))
+assume val struct_link__aux_raw_unfolded ([@@@mkey] x: (ref struct_link)) (p: perm) : slprop
+assume val struct_link__weight_1 (x: (ref struct_link)) : GTot (ref Typedef_int32_t.ty_int32_t)
+assume val struct_link__owner_1 (x: (ref struct_link)) : GTot (ref core_ref)
+assume val struct_link__weight_container (r: (ref Typedef_int32_t.ty_int32_t)) : (ref struct_link)
+assume val struct_link__weight_container_inv (p: (ref struct_link)) :
+    Lemma
+      (ensures (struct_link__weight_container (struct_link__weight_1 p)) == p)
+      [SMTPat (struct_link__weight_container (struct_link__weight_1 p))]
+assume val struct_link__weight_proj_container_inv (r: (ref Typedef_int32_t.ty_int32_t)) :
+    Lemma
+      (ensures (struct_link__weight_1 (struct_link__weight_container r)) == r)
+      [SMTPat (struct_link__weight_1 (struct_link__weight_container r))]
+assume val struct_link__owner_container (r: (ref core_ref)) : (ref struct_link)
+assume val struct_link__owner_container_inv (p: (ref struct_link)) :
+    Lemma
+      (ensures (struct_link__owner_container (struct_link__owner_1 p)) == p)
+      [SMTPat (struct_link__owner_container (struct_link__owner_1 p))]
+assume val struct_link__owner_proj_container_inv (r: (ref core_ref)) :
+    Lemma
+      (ensures (struct_link__owner_1 (struct_link__owner_container r)) == r)
+      [SMTPat (struct_link__owner_1 (struct_link__owner_container r))]
+assume val struct_link__weight_proj_null :
+    (squash
+      ((struct_link__weight_1 (Pulse.Lib.Reference.null #(struct_link))) ==
+        (Pulse.Lib.Reference.null #(Typedef_int32_t.ty_int32_t))))
+[@@pulse_intro]
+assume val struct_link__aux_raw_unfold (x: (ref struct_link)) (#p: perm) (vx: struct_link) :
+    (stt_ghost
+      unit
+      emp_inames
+      (Pulse.Lib.Reference.pts_to x #p vx)
+      (fun _ ->
+        ((struct_link__aux_raw_unfolded x p) **
+          (Pulse.Lib.Reference.pts_to (struct_link__weight_1 x) #p vx.struct_link__weight) **
+          (Pulse.Lib.Reference.pts_to (struct_link__owner_1 x) #p vx.struct_link__owner))))
+[@@pulse_intro]
+assume val struct_link__aux_raw_fold (x: (ref struct_link)) (#p: perm) v_weight v_owner :
+    (stt_ghost
+      unit
+      emp_inames
+      ((struct_link__aux_raw_unfolded x p) **
+        (Pulse.Lib.Reference.pts_to (struct_link__weight_1 x) #p v_weight) **
+        (Pulse.Lib.Reference.pts_to (struct_link__owner_1 x) #p v_owner))
+      (fun _ ->
+        (Pulse.Lib.Reference.pts_to
+          x
+          #p
+          { struct_link__weight=v_weight; struct_link__owner=v_owner; })))
+[@@pulse_intro]
+assume val struct_link__aux_raw_fold_uninit (x: (ref struct_link)) :
+    (stt_ghost
+      unit
+      emp_inames
+      ((struct_link__aux_raw_unfolded x 1.0R) **
+        (Pulse.Lib.Reference.pts_to_uninit (struct_link__weight_1 x)) **
+        (Pulse.Lib.Reference.pts_to_uninit (struct_link__owner_1 x)))
+      (fun _ -> (Pulse.Lib.Reference.pts_to_uninit x)))
+assume val struct_link__aux_raw_unfold_uninit (x: (ref struct_link)) :
+    (stt_ghost
+      unit
+      emp_inames
+      (Pulse.Lib.Reference.pts_to_uninit x)
+      (fun _ ->
+        ((struct_link__aux_raw_unfolded x 1.0R) **
+          (Pulse.Lib.Reference.pts_to_uninit (struct_link__weight_1 x)) **
+          (Pulse.Lib.Reference.pts_to_uninit (struct_link__owner_1 x)))))
+[@@pulse_impure_spec_no_proof_required]
+assume val struct_link__get_weight (x: (ref struct_link)) (#p: perm) :
+    (stt_atomic
+      (ref Typedef_int32_t.ty_int32_t)
+      #PulseCore.Observability.Neutral
+      emp_inames
+      (struct_link__aux_raw_unfolded x p)
+      (fun vx' ->
+        ((struct_link__aux_raw_unfolded x p) ** (rewrites_to vx' (struct_link__weight_1 x)))))
+[@@pulse_impure_spec_no_proof_required]
+assume val struct_link__get_owner (x: (ref struct_link)) (#p: perm) :
+    (stt_atomic
+      (ref core_ref)
+      #PulseCore.Observability.Neutral
+      emp_inames
+      (struct_link__aux_raw_unfolded x p)
+      (fun vx' ->
+        ((struct_link__aux_raw_unfolded x p) ** (rewrites_to vx' (struct_link__owner_1 x)))))
+instance has_zero_default_struct_link : (has_zero_default struct_link) =
+  { zero_default = { struct_link__weight = zero_default; struct_link__owner = core_null; } }
\ No newline at end of file
diff --git head/mutually_recursive_types/Struct_middle.fst head/mutually_recursive_types/Struct_middle.fst
new file mode 100644
index 0000000..d0e13c8
--- /dev/null
+++ head/mutually_recursive_types/Struct_middle.fst
@@ -0,0 +1,75 @@
+module Struct_middle
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+noeq type struct_middle = {
+  struct_middle__up: core_ref;
+}
+assume val struct_middle__sizeof_pos (a: Type0 { a == struct_middle }) :
+    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_middle__pred ([@@@mkey] this: struct_middle) (p: perm) =
+  emp
+[@@pulse_eager_unfold] let predicate struct_middle__uninit_pred ([@@@mkey] this: struct_middle) =
+  emp
+assume val struct_middle__aux_raw_unfolded ([@@@mkey] x: (ref struct_middle)) (p: perm) : slprop
+assume val struct_middle__up_1 (x: (ref struct_middle)) : GTot (ref core_ref)
+assume val struct_middle__up_container (r: (ref core_ref)) : (ref struct_middle)
+assume val struct_middle__up_container_inv (p: (ref struct_middle)) :
+    Lemma
+      (ensures (struct_middle__up_container (struct_middle__up_1 p)) == p)
+      [SMTPat (struct_middle__up_container (struct_middle__up_1 p))]
+assume val struct_middle__up_proj_container_inv (r: (ref core_ref)) :
+    Lemma
+      (ensures (struct_middle__up_1 (struct_middle__up_container r)) == r)
+      [SMTPat (struct_middle__up_1 (struct_middle__up_container r))]
+assume val struct_middle__up_proj_null :
+    (squash
+      ((struct_middle__up_1 (Pulse.Lib.Reference.null #(struct_middle))) ==
+        (Pulse.Lib.Reference.null #(core_ref))))
+[@@pulse_intro]
+assume val struct_middle__aux_raw_unfold (x: (ref struct_middle)) (#p: perm) (vx: struct_middle) :
+    (stt_ghost
+      unit
+      emp_inames
+      (Pulse.Lib.Reference.pts_to x #p vx)
+      (fun _ ->
+        ((struct_middle__aux_raw_unfolded x p) **
+          (Pulse.Lib.Reference.pts_to (struct_middle__up_1 x) #p vx.struct_middle__up))))
+[@@pulse_intro]
+assume val struct_middle__aux_raw_fold (x: (ref struct_middle)) (#p: perm) v_up :
+    (stt_ghost
+      unit
+      emp_inames
+      ((struct_middle__aux_raw_unfolded x p) **
+        (Pulse.Lib.Reference.pts_to (struct_middle__up_1 x) #p v_up))
+      (fun _ -> (Pulse.Lib.Reference.pts_to x #p { struct_middle__up=v_up; })))
+[@@pulse_intro]
+assume val struct_middle__aux_raw_fold_uninit (x: (ref struct_middle)) :
+    (stt_ghost
+      unit
+      emp_inames
+      ((struct_middle__aux_raw_unfolded x 1.0R) **
+        (Pulse.Lib.Reference.pts_to_uninit (struct_middle__up_1 x)))
+      (fun _ -> (Pulse.Lib.Reference.pts_to_uninit x)))
+assume val struct_middle__aux_raw_unfold_uninit (x: (ref struct_middle)) :
+    (stt_ghost
+      unit
+      emp_inames
+      (Pulse.Lib.Reference.pts_to_uninit x)
+      (fun _ ->
+        ((struct_middle__aux_raw_unfolded x 1.0R) **
+          (Pulse.Lib.Reference.pts_to_uninit (struct_middle__up_1 x)))))
+[@@pulse_impure_spec_no_proof_required]
+assume val struct_middle__get_up (x: (ref struct_middle)) (#p: perm) :
+    (stt_atomic
+      (ref core_ref)
+      #PulseCore.Observability.Neutral
+      emp_inames
+      (struct_middle__aux_raw_unfolded x p)
+      (fun vx' ->
+        ((struct_middle__aux_raw_unfolded x p) ** (rewrites_to vx' (struct_middle__up_1 x)))))
+instance has_zero_default_struct_middle : (has_zero_default struct_middle) =
+  { zero_default = { struct_middle__up = core_null; } }
\ No newline at end of file
diff --git head/mutually_recursive_types/Struct_obj.fst head/mutually_recursive_types/Struct_obj.fst
new file mode 100644
index 0000000..be1affc
--- /dev/null
+++ head/mutually_recursive_types/Struct_obj.fst
@@ -0,0 +1,104 @@
+module Struct_obj
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+noeq type struct_obj = {
+  struct_obj__tag: Typedef_int32_t.ty_int32_t;
+  struct_obj__dispatch: Typedef_vtable.ty_vtable;
+}
+assume val struct_obj__sizeof_pos (a: Type0 { a == struct_obj }) :
+    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_obj__pred ([@@@mkey] this: struct_obj) (p: perm) =
+  ((Typedef_int32_t.ty_int32_t__pred this.struct_obj__tag p) **
+    (Typedef_vtable.ty_vtable__pred this.struct_obj__dispatch p))
+[@@pulse_eager_unfold] let predicate struct_obj__uninit_pred ([@@@mkey] this: struct_obj) =
+  ((Typedef_int32_t.ty_int32_t__uninit_pred this.struct_obj__tag) **
+    (Typedef_vtable.ty_vtable__uninit_pred this.struct_obj__dispatch))
+assume val struct_obj__aux_raw_unfolded ([@@@mkey] x: (ref struct_obj)) (p: perm) : slprop
+assume val struct_obj__tag_1 (x: (ref struct_obj)) : GTot (ref Typedef_int32_t.ty_int32_t)
+assume val struct_obj__dispatch_1 (x: (ref struct_obj)) : GTot (ref Typedef_vtable.ty_vtable)
+assume val struct_obj__tag_container (r: (ref Typedef_int32_t.ty_int32_t)) : (ref struct_obj)
+assume val struct_obj__tag_container_inv (p: (ref struct_obj)) :
+    Lemma
+      (ensures (struct_obj__tag_container (struct_obj__tag_1 p)) == p)
+      [SMTPat (struct_obj__tag_container (struct_obj__tag_1 p))]
+assume val struct_obj__tag_proj_container_inv (r: (ref Typedef_int32_t.ty_int32_t)) :
+    Lemma
+      (ensures (struct_obj__tag_1 (struct_obj__tag_container r)) == r)
+      [SMTPat (struct_obj__tag_1 (struct_obj__tag_container r))]
+assume val struct_obj__dispatch_container (r: (ref Typedef_vtable.ty_vtable)) : (ref struct_obj)
+assume val struct_obj__dispatch_container_inv (p: (ref struct_obj)) :
+    Lemma
+      (ensures (struct_obj__dispatch_container (struct_obj__dispatch_1 p)) == p)
+      [SMTPat (struct_obj__dispatch_container (struct_obj__dispatch_1 p))]
+assume val struct_obj__dispatch_proj_container_inv (r: (ref Typedef_vtable.ty_vtable)) :
+    Lemma
+      (ensures (struct_obj__dispatch_1 (struct_obj__dispatch_container r)) == r)
+      [SMTPat (struct_obj__dispatch_1 (struct_obj__dispatch_container r))]
+assume val struct_obj__tag_proj_null :
+    (squash
+      ((struct_obj__tag_1 (Pulse.Lib.Reference.null #(struct_obj))) ==
+        (Pulse.Lib.Reference.null #(Typedef_int32_t.ty_int32_t))))
+[@@pulse_intro]
+assume val struct_obj__aux_raw_unfold (x: (ref struct_obj)) (#p: perm) (vx: struct_obj) :
+    (stt_ghost
+      unit
+      emp_inames
+      (Pulse.Lib.Reference.pts_to x #p vx)
+      (fun _ ->
+        ((struct_obj__aux_raw_unfolded x p) **
+          (Pulse.Lib.Reference.pts_to (struct_obj__tag_1 x) #p vx.struct_obj__tag) **
+          (Pulse.Lib.Reference.pts_to (struct_obj__dispatch_1 x) #p vx.struct_obj__dispatch))))
+[@@pulse_intro]
+assume val struct_obj__aux_raw_fold (x: (ref struct_obj)) (#p: perm) v_tag v_dispatch :
+    (stt_ghost
+      unit
+      emp_inames
+      ((struct_obj__aux_raw_unfolded x p) **
+        (Pulse.Lib.Reference.pts_to (struct_obj__tag_1 x) #p v_tag) **
+        (Pulse.Lib.Reference.pts_to (struct_obj__dispatch_1 x) #p v_dispatch))
+      (fun _ ->
+        (Pulse.Lib.Reference.pts_to
+          x
+          #p
+          { struct_obj__tag=v_tag; struct_obj__dispatch=v_dispatch; })))
+[@@pulse_intro]
+assume val struct_obj__aux_raw_fold_uninit (x: (ref struct_obj)) :
+    (stt_ghost
+      unit
+      emp_inames
+      ((struct_obj__aux_raw_unfolded x 1.0R) **
+        (Pulse.Lib.Reference.pts_to_uninit (struct_obj__tag_1 x)) **
+        (Pulse.Lib.Reference.pts_to_uninit (struct_obj__dispatch_1 x)))
+      (fun _ -> (Pulse.Lib.Reference.pts_to_uninit x)))
+assume val struct_obj__aux_raw_unfold_uninit (x: (ref struct_obj)) :
+    (stt_ghost
+      unit
+      emp_inames
+      (Pulse.Lib.Reference.pts_to_uninit x)
+      (fun _ ->
+        ((struct_obj__aux_raw_unfolded x 1.0R) **
+          (Pulse.Lib.Reference.pts_to_uninit (struct_obj__tag_1 x)) **
+          (Pulse.Lib.Reference.pts_to_uninit (struct_obj__dispatch_1 x)))))
+[@@pulse_impure_spec_no_proof_required]
+assume val struct_obj__get_tag (x: (ref struct_obj)) (#p: perm) :
+    (stt_atomic
+      (ref Typedef_int32_t.ty_int32_t)
+      #PulseCore.Observability.Neutral
+      emp_inames
+      (struct_obj__aux_raw_unfolded x p)
+      (fun vx' -> ((struct_obj__aux_raw_unfolded x p) ** (rewrites_to vx' (struct_obj__tag_1 x)))))
+[@@pulse_impure_spec_no_proof_required]
+assume val struct_obj__get_dispatch (x: (ref struct_obj)) (#p: perm) :
+    (stt_atomic
+      (ref Typedef_vtable.ty_vtable)
+      #PulseCore.Observability.Neutral
+      emp_inames
+      (struct_obj__aux_raw_unfolded x p)
+      (fun vx' ->
+        ((struct_obj__aux_raw_unfolded x p) ** (rewrites_to vx' (struct_obj__dispatch_1 x)))))
+instance has_zero_default_struct_obj : (has_zero_default struct_obj) =
+  { zero_default = { struct_obj__tag = zero_default; struct_obj__dispatch = zero_default; } }
\ No newline at end of file
diff --git head/mutually_recursive_types/Struct_outer.fst head/mutually_recursive_types/Struct_outer.fst
new file mode 100644
index 0000000..6c0d49b
--- /dev/null
+++ head/mutually_recursive_types/Struct_outer.fst
@@ -0,0 +1,105 @@
+module Struct_outer
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+noeq type struct_outer = {
+  struct_outer__depth: Typedef_int32_t.ty_int32_t;
+  struct_outer__mid: Struct_middle.struct_middle;
+}
+assume val struct_outer__sizeof_pos (a: Type0 { a == struct_outer }) :
+    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_outer__pred ([@@@mkey] this: struct_outer) (p: perm) =
+  ((Typedef_int32_t.ty_int32_t__pred this.struct_outer__depth p) **
+    (Struct_middle.struct_middle__pred this.struct_outer__mid p))
+[@@pulse_eager_unfold] let predicate struct_outer__uninit_pred ([@@@mkey] this: struct_outer) =
+  ((Typedef_int32_t.ty_int32_t__uninit_pred this.struct_outer__depth) **
+    (Struct_middle.struct_middle__uninit_pred this.struct_outer__mid))
+assume val struct_outer__aux_raw_unfolded ([@@@mkey] x: (ref struct_outer)) (p: perm) : slprop
+assume val struct_outer__depth_1 (x: (ref struct_outer)) : GTot (ref Typedef_int32_t.ty_int32_t)
+assume val struct_outer__mid_1 (x: (ref struct_outer)) : GTot (ref Struct_middle.struct_middle)
+assume val struct_outer__depth_container (r: (ref Typedef_int32_t.ty_int32_t)) : (ref struct_outer)
+assume val struct_outer__depth_container_inv (p: (ref struct_outer)) :
+    Lemma
+      (ensures (struct_outer__depth_container (struct_outer__depth_1 p)) == p)
+      [SMTPat (struct_outer__depth_container (struct_outer__depth_1 p))]
+assume val struct_outer__depth_proj_container_inv (r: (ref Typedef_int32_t.ty_int32_t)) :
+    Lemma
+      (ensures (struct_outer__depth_1 (struct_outer__depth_container r)) == r)
+      [SMTPat (struct_outer__depth_1 (struct_outer__depth_container r))]
+assume val struct_outer__mid_container (r: (ref Struct_middle.struct_middle)) : (ref struct_outer)
+assume val struct_outer__mid_container_inv (p: (ref struct_outer)) :
+    Lemma
+      (ensures (struct_outer__mid_container (struct_outer__mid_1 p)) == p)
+      [SMTPat (struct_outer__mid_container (struct_outer__mid_1 p))]
+assume val struct_outer__mid_proj_container_inv (r: (ref Struct_middle.struct_middle)) :
+    Lemma
+      (ensures (struct_outer__mid_1 (struct_outer__mid_container r)) == r)
+      [SMTPat (struct_outer__mid_1 (struct_outer__mid_container r))]
+assume val struct_outer__depth_proj_null :
+    (squash
+      ((struct_outer__depth_1 (Pulse.Lib.Reference.null #(struct_outer))) ==
+        (Pulse.Lib.Reference.null #(Typedef_int32_t.ty_int32_t))))
+[@@pulse_intro]
+assume val struct_outer__aux_raw_unfold (x: (ref struct_outer)) (#p: perm) (vx: struct_outer) :
+    (stt_ghost
+      unit
+      emp_inames
+      (Pulse.Lib.Reference.pts_to x #p vx)
+      (fun _ ->
+        ((struct_outer__aux_raw_unfolded x p) **
+          (Pulse.Lib.Reference.pts_to (struct_outer__depth_1 x) #p vx.struct_outer__depth) **
+          (Pulse.Lib.Reference.pts_to (struct_outer__mid_1 x) #p vx.struct_outer__mid))))
+[@@pulse_intro]
+assume val struct_outer__aux_raw_fold (x: (ref struct_outer)) (#p: perm) v_depth v_mid :
+    (stt_ghost
+      unit
+      emp_inames
+      ((struct_outer__aux_raw_unfolded x p) **
+        (Pulse.Lib.Reference.pts_to (struct_outer__depth_1 x) #p v_depth) **
+        (Pulse.Lib.Reference.pts_to (struct_outer__mid_1 x) #p v_mid))
+      (fun _ ->
+        (Pulse.Lib.Reference.pts_to
+          x
+          #p
+          { struct_outer__depth=v_depth; struct_outer__mid=v_mid; })))
+[@@pulse_intro]
+assume val struct_outer__aux_raw_fold_uninit (x: (ref struct_outer)) :
+    (stt_ghost
+      unit
+      emp_inames
+      ((struct_outer__aux_raw_unfolded x 1.0R) **
+        (Pulse.Lib.Reference.pts_to_uninit (struct_outer__depth_1 x)) **
+        (Pulse.Lib.Reference.pts_to_uninit (struct_outer__mid_1 x)))
+      (fun _ -> (Pulse.Lib.Reference.pts_to_uninit x)))
+assume val struct_outer__aux_raw_unfold_uninit (x: (ref struct_outer)) :
+    (stt_ghost
+      unit
+      emp_inames
+      (Pulse.Lib.Reference.pts_to_uninit x)
+      (fun _ ->
+        ((struct_outer__aux_raw_unfolded x 1.0R) **
+          (Pulse.Lib.Reference.pts_to_uninit (struct_outer__depth_1 x)) **
+          (Pulse.Lib.Reference.pts_to_uninit (struct_outer__mid_1 x)))))
+[@@pulse_impure_spec_no_proof_required]
+assume val struct_outer__get_depth (x: (ref struct_outer)) (#p: perm) :
+    (stt_atomic
+      (ref Typedef_int32_t.ty_int32_t)
+      #PulseCore.Observability.Neutral
+      emp_inames
+      (struct_outer__aux_raw_unfolded x p)
+      (fun vx' ->
+        ((struct_outer__aux_raw_unfolded x p) ** (rewrites_to vx' (struct_outer__depth_1 x)))))
+[@@pulse_impure_spec_no_proof_required]
+assume val struct_outer__get_mid (x: (ref struct_outer)) (#p: perm) :
+    (stt_atomic
+      (ref Struct_middle.struct_middle)
+      #PulseCore.Observability.Neutral
+      emp_inames
+      (struct_outer__aux_raw_unfolded x p)
+      (fun vx' ->
+        ((struct_outer__aux_raw_unfolded x p) ** (rewrites_to vx' (struct_outer__mid_1 x)))))
+instance has_zero_default_struct_outer : (has_zero_default struct_outer) =
+  { zero_default = { struct_outer__depth = zero_default; struct_outer__mid = zero_default; } }
\ No newline at end of file
diff --git head/mutually_recursive_types/Struct_peer.fst head/mutually_recursive_types/Struct_peer.fst
new file mode 100644
index 0000000..2d66591
--- /dev/null
+++ head/mutually_recursive_types/Struct_peer.fst
@@ -0,0 +1,106 @@
+module Struct_peer
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+noeq type struct_peer = {
+  struct_peer__peer_id: Typedef_int32_t.ty_int32_t;
+  struct_peer__first_link: core_ref;
+}
+assume val struct_peer__sizeof_pos (a: Type0 { a == struct_peer }) :
+    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_peer__pred ([@@@mkey] this: struct_peer) (p: perm) =
+  ((Typedef_int32_t.ty_int32_t__pred this.struct_peer__peer_id p))
+[@@pulse_eager_unfold] let predicate struct_peer__uninit_pred ([@@@mkey] this: struct_peer) =
+  ((Typedef_int32_t.ty_int32_t__uninit_pred this.struct_peer__peer_id))
+assume val struct_peer__aux_raw_unfolded ([@@@mkey] x: (ref struct_peer)) (p: perm) : slprop
+assume val struct_peer__peer_id_1 (x: (ref struct_peer)) : GTot (ref Typedef_int32_t.ty_int32_t)
+assume val struct_peer__first_link_1 (x: (ref struct_peer)) : GTot (ref core_ref)
+assume val struct_peer__peer_id_container (r: (ref Typedef_int32_t.ty_int32_t)) : (ref struct_peer)
+assume val struct_peer__peer_id_container_inv (p: (ref struct_peer)) :
+    Lemma
+      (ensures (struct_peer__peer_id_container (struct_peer__peer_id_1 p)) == p)
+      [SMTPat (struct_peer__peer_id_container (struct_peer__peer_id_1 p))]
+assume val struct_peer__peer_id_proj_container_inv (r: (ref Typedef_int32_t.ty_int32_t)) :
+    Lemma
+      (ensures (struct_peer__peer_id_1 (struct_peer__peer_id_container r)) == r)
+      [SMTPat (struct_peer__peer_id_1 (struct_peer__peer_id_container r))]
+assume val struct_peer__first_link_container (r: (ref core_ref)) : (ref struct_peer)
+assume val struct_peer__first_link_container_inv (p: (ref struct_peer)) :
+    Lemma
+      (ensures (struct_peer__first_link_container (struct_peer__first_link_1 p)) == p)
+      [SMTPat (struct_peer__first_link_container (struct_peer__first_link_1 p))]
+assume val struct_peer__first_link_proj_container_inv (r: (ref core_ref)) :
+    Lemma
+      (ensures (struct_peer__first_link_1 (struct_peer__first_link_container r)) == r)
+      [SMTPat (struct_peer__first_link_1 (struct_peer__first_link_container r))]
+assume val struct_peer__peer_id_proj_null :
+    (squash
+      ((struct_peer__peer_id_1 (Pulse.Lib.Reference.null #(struct_peer))) ==
+        (Pulse.Lib.Reference.null #(Typedef_int32_t.ty_int32_t))))
+[@@pulse_intro]
+assume val struct_peer__aux_raw_unfold (x: (ref struct_peer)) (#p: perm) (vx: struct_peer) :
+    (stt_ghost
+      unit
+      emp_inames
+      (Pulse.Lib.Reference.pts_to x #p vx)
+      (fun _ ->
+        ((struct_peer__aux_raw_unfolded x p) **
+          (Pulse.Lib.Reference.pts_to (struct_peer__peer_id_1 x) #p vx.struct_peer__peer_id) **
+          (Pulse.Lib.Reference.pts_to
+            (struct_peer__first_link_1 x)
+            #p
+            vx.struct_peer__first_link))))
+[@@pulse_intro]
+assume val struct_peer__aux_raw_fold (x: (ref struct_peer)) (#p: perm) v_peer_id v_first_link :
+    (stt_ghost
+      unit
+      emp_inames
+      ((struct_peer__aux_raw_unfolded x p) **
+        (Pulse.Lib.Reference.pts_to (struct_peer__peer_id_1 x) #p v_peer_id) **
+        (Pulse.Lib.Reference.pts_to (struct_peer__first_link_1 x) #p v_first_link))
+      (fun _ ->
+        (Pulse.Lib.Reference.pts_to
+          x
+          #p
+          { struct_peer__peer_id=v_peer_id; struct_peer__first_link=v_first_link; })))
+[@@pulse_intro]
+assume val struct_peer__aux_raw_fold_uninit (x: (ref struct_peer)) :
+    (stt_ghost
+      unit
+      emp_inames
+      ((struct_peer__aux_raw_unfolded x 1.0R) **
+        (Pulse.Lib.Reference.pts_to_uninit (struct_peer__peer_id_1 x)) **
+        (Pulse.Lib.Reference.pts_to_uninit (struct_peer__first_link_1 x)))
+      (fun _ -> (Pulse.Lib.Reference.pts_to_uninit x)))
+assume val struct_peer__aux_raw_unfold_uninit (x: (ref struct_peer)) :
+    (stt_ghost
+      unit
+      emp_inames
+      (Pulse.Lib.Reference.pts_to_uninit x)
+      (fun _ ->
+        ((struct_peer__aux_raw_unfolded x 1.0R) **
+          (Pulse.Lib.Reference.pts_to_uninit (struct_peer__peer_id_1 x)) **
+          (Pulse.Lib.Reference.pts_to_uninit (struct_peer__first_link_1 x)))))
+[@@pulse_impure_spec_no_proof_required]
+assume val struct_peer__get_peer_id (x: (ref struct_peer)) (#p: perm) :
+    (stt_atomic
+      (ref Typedef_int32_t.ty_int32_t)
+      #PulseCore.Observability.Neutral
+      emp_inames
+      (struct_peer__aux_raw_unfolded x p)
+      (fun vx' ->
+        ((struct_peer__aux_raw_unfolded x p) ** (rewrites_to vx' (struct_peer__peer_id_1 x)))))
+[@@pulse_impure_spec_no_proof_required]
+assume val struct_peer__get_first_link (x: (ref struct_peer)) (#p: perm) :
+    (stt_atomic
+      (ref core_ref)
+      #PulseCore.Observability.Neutral
+      emp_inames
+      (struct_peer__aux_raw_unfolded x p)
+      (fun vx' ->
+        ((struct_peer__aux_raw_unfolded x p) ** (rewrites_to vx' (struct_peer__first_link_1 x)))))
+instance has_zero_default_struct_peer : (has_zero_default struct_peer) =
+  { zero_default = { struct_peer__peer_id = zero_default; struct_peer__first_link = core_null; } }
\ No newline at end of file
diff --git head/mutually_recursive_types/Struct_selfnode.fst head/mutually_recursive_types/Struct_selfnode.fst
new file mode 100644
index 0000000..e5de416
--- /dev/null
+++ head/mutually_recursive_types/Struct_selfnode.fst
@@ -0,0 +1,112 @@
+module Struct_selfnode
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+noeq type struct_selfnode = {
+  struct_selfnode__data: Typedef_int32_t.ty_int32_t;
+  struct_selfnode__next: (ref struct_selfnode);
+}
+assume val struct_selfnode__sizeof_pos (a: Type0 { a == struct_selfnode }) :
+    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_selfnode__pred
+      ([@@@mkey] this: struct_selfnode)
+      (p: perm) =
+  ((Typedef_int32_t.ty_int32_t__pred this.struct_selfnode__data p))
+[@@pulse_eager_unfold] let predicate struct_selfnode__uninit_pred
+      ([@@@mkey] this: struct_selfnode) =
+  ((Typedef_int32_t.ty_int32_t__uninit_pred this.struct_selfnode__data))
+assume val struct_selfnode__aux_raw_unfolded ([@@@mkey] x: (ref struct_selfnode)) (p: perm) : slprop
+assume val struct_selfnode__data_1 (x: (ref struct_selfnode)) :
+    GTot (ref Typedef_int32_t.ty_int32_t)
+assume val struct_selfnode__next_1 (x: (ref struct_selfnode)) : GTot (ref (ref struct_selfnode))
+assume val struct_selfnode__data_container (r: (ref Typedef_int32_t.ty_int32_t)) :
+    (ref struct_selfnode)
+assume val struct_selfnode__data_container_inv (p: (ref struct_selfnode)) :
+    Lemma
+      (ensures (struct_selfnode__data_container (struct_selfnode__data_1 p)) == p)
+      [SMTPat (struct_selfnode__data_container (struct_selfnode__data_1 p))]
+assume val struct_selfnode__data_proj_container_inv (r: (ref Typedef_int32_t.ty_int32_t)) :
+    Lemma
+      (ensures (struct_selfnode__data_1 (struct_selfnode__data_container r)) == r)
+      [SMTPat (struct_selfnode__data_1 (struct_selfnode__data_container r))]
+assume val struct_selfnode__next_container (r: (ref (ref struct_selfnode))) : (ref struct_selfnode)
+assume val struct_selfnode__next_container_inv (p: (ref struct_selfnode)) :
+    Lemma
+      (ensures (struct_selfnode__next_container (struct_selfnode__next_1 p)) == p)
+      [SMTPat (struct_selfnode__next_container (struct_selfnode__next_1 p))]
+assume val struct_selfnode__next_proj_container_inv (r: (ref (ref struct_selfnode))) :
+    Lemma
+      (ensures (struct_selfnode__next_1 (struct_selfnode__next_container r)) == r)
+      [SMTPat (struct_selfnode__next_1 (struct_selfnode__next_container r))]
+assume val struct_selfnode__data_proj_null :
+    (squash
+      ((struct_selfnode__data_1 (Pulse.Lib.Reference.null #(struct_selfnode))) ==
+        (Pulse.Lib.Reference.null #(Typedef_int32_t.ty_int32_t))))
+[@@pulse_intro]
+assume val struct_selfnode__aux_raw_unfold
+  (x: (ref struct_selfnode))
+  (#p: perm)
+  (vx: struct_selfnode)
+  :
+    (stt_ghost
+      unit
+      emp_inames
+      (Pulse.Lib.Reference.pts_to x #p vx)
+      (fun _ ->
+        ((struct_selfnode__aux_raw_unfolded x p) **
+          (Pulse.Lib.Reference.pts_to (struct_selfnode__data_1 x) #p vx.struct_selfnode__data) **
+          (Pulse.Lib.Reference.pts_to (struct_selfnode__next_1 x) #p vx.struct_selfnode__next))))
+[@@pulse_intro]
+assume val struct_selfnode__aux_raw_fold (x: (ref struct_selfnode)) (#p: perm) v_data v_next :
+    (stt_ghost
+      unit
+      emp_inames
+      ((struct_selfnode__aux_raw_unfolded x p) **
+        (Pulse.Lib.Reference.pts_to (struct_selfnode__data_1 x) #p v_data) **
+        (Pulse.Lib.Reference.pts_to (struct_selfnode__next_1 x) #p v_next))
+      (fun _ ->
+        (Pulse.Lib.Reference.pts_to
+          x
+          #p
+          { struct_selfnode__data=v_data; struct_selfnode__next=v_next; })))
+[@@pulse_intro]
+assume val struct_selfnode__aux_raw_fold_uninit (x: (ref struct_selfnode)) :
+    (stt_ghost
+      unit
+      emp_inames
+      ((struct_selfnode__aux_raw_unfolded x 1.0R) **
+        (Pulse.Lib.Reference.pts_to_uninit (struct_selfnode__data_1 x)) **
+        (Pulse.Lib.Reference.pts_to_uninit (struct_selfnode__next_1 x)))
+      (fun _ -> (Pulse.Lib.Reference.pts_to_uninit x)))
+assume val struct_selfnode__aux_raw_unfold_uninit (x: (ref struct_selfnode)) :
+    (stt_ghost
+      unit
+      emp_inames
+      (Pulse.Lib.Reference.pts_to_uninit x)
+      (fun _ ->
+        ((struct_selfnode__aux_raw_unfolded x 1.0R) **
+          (Pulse.Lib.Reference.pts_to_uninit (struct_selfnode__data_1 x)) **
+          (Pulse.Lib.Reference.pts_to_uninit (struct_selfnode__next_1 x)))))
+[@@pulse_impure_spec_no_proof_required]
+assume val struct_selfnode__get_data (x: (ref struct_selfnode)) (#p: perm) :
+    (stt_atomic
+      (ref Typedef_int32_t.ty_int32_t)
+      #PulseCore.Observability.Neutral
+      emp_inames
+      (struct_selfnode__aux_raw_unfolded x p)
+      (fun vx' ->
+        ((struct_selfnode__aux_raw_unfolded x p) ** (rewrites_to vx' (struct_selfnode__data_1 x)))))
+[@@pulse_impure_spec_no_proof_required]
+assume val struct_selfnode__get_next (x: (ref struct_selfnode)) (#p: perm) :
+    (stt_atomic
+      (ref (ref struct_selfnode))
+      #PulseCore.Observability.Neutral
+      emp_inames
+      (struct_selfnode__aux_raw_unfolded x p)
+      (fun vx' ->
+        ((struct_selfnode__aux_raw_unfolded x p) ** (rewrites_to vx' (struct_selfnode__next_1 x)))))
+instance has_zero_default_struct_selfnode : (has_zero_default struct_selfnode) =
+  { zero_default = { struct_selfnode__data = zero_default; struct_selfnode__next = null; } }
\ No newline at end of file
diff --git head/mutually_recursive_types/TranslationErrors.fst head/mutually_recursive_types/TranslationErrors.fst
new file mode 100644
index 0000000..bf62561
--- /dev/null
+++ head/mutually_recursive_types/TranslationErrors.fst
@@ -0,0 +1 @@
+module TranslationErrors
diff --git head/mutually_recursive_types/Typedef___int32_t.fst head/mutually_recursive_types/Typedef___int32_t.fst
new file mode 100644
index 0000000..516285c
--- /dev/null
+++ head/mutually_recursive_types/Typedef___int32_t.fst
@@ -0,0 +1,12 @@
+module Typedef___int32_t
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+unfold
+let ty___int32_t : Type = Int32.t
+[@@pulse_eager_unfold] let predicate ty___int32_t__pred ([@@@mkey] this: ty___int32_t) (p: perm) =
+  emp
+[@@pulse_eager_unfold] let predicate ty___int32_t__uninit_pred ([@@@mkey] this: ty___int32_t) = emp
+instance has_zero_default_ty___int32_t : (has_zero_default ty___int32_t) =
+  { zero_default = (Int32.int_to_t 0) }
\ No newline at end of file
diff --git head/mutually_recursive_types/Typedef_int32_t.fst head/mutually_recursive_types/Typedef_int32_t.fst
new file mode 100644
index 0000000..6996081
--- /dev/null
+++ head/mutually_recursive_types/Typedef_int32_t.fst
@@ -0,0 +1,13 @@
+module Typedef_int32_t
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+unfold
+let ty_int32_t : Type = Typedef___int32_t.ty___int32_t
+[@@pulse_eager_unfold] let predicate ty_int32_t__pred ([@@@mkey] this: ty_int32_t) (p: perm) =
+  ((Typedef___int32_t.ty___int32_t__pred this p))
+[@@pulse_eager_unfold] let predicate ty_int32_t__uninit_pred ([@@@mkey] this: ty_int32_t) =
+  ((Typedef___int32_t.ty___int32_t__uninit_pred this))
+instance has_zero_default_ty_int32_t : (has_zero_default ty_int32_t) =
+  { zero_default = zero_default }
\ No newline at end of file
diff --git head/mutually_recursive_types/Typedef_selfnode.fst head/mutually_recursive_types/Typedef_selfnode.fst
new file mode 100644
index 0000000..738cce6
--- /dev/null
+++ head/mutually_recursive_types/Typedef_selfnode.fst
@@ -0,0 +1,13 @@
+module Typedef_selfnode
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+unfold
+let ty_selfnode : Type = Struct_selfnode.struct_selfnode
+[@@pulse_eager_unfold] let predicate ty_selfnode__pred ([@@@mkey] this: ty_selfnode) (p: perm) =
+  ((Struct_selfnode.struct_selfnode__pred this p))
+[@@pulse_eager_unfold] let predicate ty_selfnode__uninit_pred ([@@@mkey] this: ty_selfnode) =
+  ((Struct_selfnode.struct_selfnode__uninit_pred this))
+instance has_zero_default_ty_selfnode : (has_zero_default ty_selfnode) =
+  { zero_default = zero_default }
\ No newline at end of file
diff --git head/mutually_recursive_types/Typedef_vtable.fst head/mutually_recursive_types/Typedef_vtable.fst
new file mode 100644
index 0000000..d733d5a
--- /dev/null
+++ head/mutually_recursive_types/Typedef_vtable.fst
@@ -0,0 +1,11 @@
+module Typedef_vtable
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+unfold
+let ty_vtable : Type = (Pulse.Lib.C.FuncPtr.func_ptr core_ref Typedef_int32_t.ty_int32_t)
+[@@pulse_eager_unfold] let predicate ty_vtable__pred ([@@@mkey] this: ty_vtable) (p: perm) = emp
+[@@pulse_eager_unfold] let predicate ty_vtable__uninit_pred ([@@@mkey] this: ty_vtable) = emp
+instance has_zero_default_ty_vtable : (has_zero_default ty_vtable) =
+  { zero_default = (Pulse.Lib.C.FuncPtr.null core_ref Typedef_int32_t.ty_int32_t) }
\ No newline at end of file
diff --git head/mutually_recursive_types/diagnostics.json head/mutually_recursive_types/diagnostics.json
new file mode 100644
index 0000000..ab8514c
--- /dev/null
+++ head/mutually_recursive_types/diagnostics.json
@@ -0,0 +1,60 @@
+{
+  "file://test/mutually_recursive_types/mutually_recursive_types.c": [
+    {
+      "range": {
+        "start": {
+          "line": 36,
+          "character": 0
+        },
+        "end": {
+          "line": 39,
+          "character": 0
+        }
+      },
+      "severity": 2,
+      "message": "'struct link' is part of a recursive type definition; the pointers that close the cycle are modeled as untyped 'core_ref' addresses and carry no ownership. Cast such a pointer to a typed reference to use it."
+    },
+    {
+      "range": {
+        "start": {
+          "line": 31,
+          "character": 0
+        },
+        "end": {
+          "line": 34,
+          "character": 0
+        }
+      },
+      "severity": 2,
+      "message": "'struct peer' is part of a recursive type definition; the pointers that close the cycle are modeled as untyped 'core_ref' addresses and carry no ownership. Cast such a pointer to a typed reference to use it."
+    },
+    {
+      "range": {
+        "start": {
+          "line": 44,
+          "character": 0
+        },
+        "end": {
+          "line": 44,
+          "character": 42
+        }
+      },
+      "severity": 2,
+      "message": "'typedef vtable' is part of a recursive type definition; the pointers that close the cycle are modeled as untyped 'core_ref' addresses and carry no ownership. Cast such a pointer to a typed reference to use it."
+    },
+    {
+      "range": {
+        "start": {
+          "line": 55,
+          "character": 0
+        },
+        "end": {
+          "line": 57,
+          "character": 0
+        }
+      },
+      "severity": 2,
+      "message": "'struct middle' is part of a recursive type definition; the pointers that close the cycle are modeled as untyped 'core_ref' addresses and carry no ownership. Cast such a pointer to a typed reference to use it."
+    }
+  ]
+}
\ 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