added talk demo files

_CoqProject

@@ -40,3 +40,6 @@
 -Q _build/default/examples/proofs/wrapping_add refinedc.examples.wrapping_add
 -Q _build/default/linux/proofs/early_alloc refinedc.linux.early_alloc
 -Q _build/default/examples/proofs/container_of refinedc.examples.container_of
+-Q _build/default/examples/proofs/talk_demo1 refinedc.examples.talk_demo1
+-Q _build/default/examples/proofs/talk_demo2 refinedc.examples.talk_demo2
+-Q _build/default/examples/proofs/talk_demo3 refinedc.examples.talk_demo3

examples/proofs/talk_demo1/dune

+; Generated by [refinedc], do not edit.
+(coq.theory
+ (flags -w -notation-overridden -w -redundant-canonical-projection)
+ (name refinedc.examples.talk_demo1)
+ (theories refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))

examples/proofs/talk_demo1/generated_code.v

+From refinedc.lang Require Export notation.
+From refinedc.lang Require Import tactics.
+From refinedc.typing Require Import annotations.
+Set Default Proof Using "Type".
+
+(* Generated from [examples/talk_demo1.c]. *)
+Section code.
+  Definition file_0 : string := "examples/talk_demo1.c".
+  Definition loc_2 : location_info := LocationInfo file_0 12 2 16 3.
+  Definition loc_3 : location_info := LocationInfo file_0 12 27 14 3.
+  Definition loc_4 : location_info := LocationInfo file_0 13 4 13 11.
+  Definition loc_5 : location_info := LocationInfo file_0 13 4 13 6.
+  Definition loc_6 : location_info := LocationInfo file_0 13 5 13 6.
+  Definition loc_7 : location_info := LocationInfo file_0 13 5 13 6.
+  Definition loc_8 : location_info := LocationInfo file_0 13 9 13 10.
+  Definition loc_9 : location_info := LocationInfo file_0 13 9 13 10.
+  Definition loc_10 : location_info := LocationInfo file_0 14 9 16 3.
+  Definition loc_11 : location_info := LocationInfo file_0 15 4 15 27.
+  Definition loc_12 : location_info := LocationInfo file_0 15 4 15 10.
+  Definition loc_13 : location_info := LocationInfo file_0 15 4 15 10.
+  Definition loc_14 : location_info := LocationInfo file_0 15 11 15 22.
+  Definition loc_15 : location_info := LocationInfo file_0 15 12 15 22.
+  Definition loc_16 : location_info := LocationInfo file_0 15 12 15 16.
+  Definition loc_17 : location_info := LocationInfo file_0 15 12 15 16.
+  Definition loc_18 : location_info := LocationInfo file_0 15 14 15 15.
+  Definition loc_19 : location_info := LocationInfo file_0 15 14 15 15.
+  Definition loc_20 : location_info := LocationInfo file_0 15 24 15 25.
+  Definition loc_21 : location_info := LocationInfo file_0 15 24 15 25.
+  Definition loc_22 : location_info := LocationInfo file_0 12 5 12 25.
+  Definition loc_23 : location_info := LocationInfo file_0 12 5 12 7.
+  Definition loc_24 : location_info := LocationInfo file_0 12 5 12 7.
+  Definition loc_25 : location_info := LocationInfo file_0 12 6 12 7.
+  Definition loc_26 : location_info := LocationInfo file_0 12 6 12 7.
+  Definition loc_27 : location_info := LocationInfo file_0 12 11 12 25.
+  Definition loc_30 : location_info := LocationInfo file_0 21 2 21 61.
+  Definition loc_31 : location_info := LocationInfo file_0 22 2 22 17.
+  Definition loc_32 : location_info := LocationInfo file_0 22 18 22 47.
+  Definition loc_33 : location_info := LocationInfo file_0 23 2 23 61.
+  Definition loc_34 : location_info := LocationInfo file_0 24 2 24 17.
+  Definition loc_35 : location_info := LocationInfo file_0 24 18 24 47.
+  Definition loc_36 : location_info := LocationInfo file_0 25 2 25 24.
+  Definition loc_37 : location_info := LocationInfo file_0 26 2 28 3.
+  Definition loc_38 : location_info := LocationInfo file_0 26 30 28 3.
+  Definition loc_39 : location_info := LocationInfo file_0 27 4 27 28.
+  Definition loc_40 : location_info := LocationInfo file_0 27 11 27 26.
+  Definition loc_41 : location_info := LocationInfo file_0 27 11 27 21.
+  Definition loc_42 : location_info := LocationInfo file_0 27 11 27 21.
+  Definition loc_43 : location_info := LocationInfo file_0 27 11 27 16.
+  Definition loc_44 : location_info := LocationInfo file_0 27 11 27 16.
+  Definition loc_45 : location_info := LocationInfo file_0 27 25 27 26.
+  Definition loc_47 : location_info := LocationInfo file_0 26 5 26 28.
+  Definition loc_48 : location_info := LocationInfo file_0 26 5 26 10.
+  Definition loc_49 : location_info := LocationInfo file_0 26 5 26 10.
+  Definition loc_50 : location_info := LocationInfo file_0 26 14 26 28.
+  Definition loc_51 : location_info := LocationInfo file_0 25 2 25 8.
+  Definition loc_52 : location_info := LocationInfo file_0 25 2 25 8.
+  Definition loc_53 : location_info := LocationInfo file_0 25 9 25 15.
+  Definition loc_54 : location_info := LocationInfo file_0 25 10 25 15.
+  Definition loc_55 : location_info := LocationInfo file_0 25 17 25 22.
+  Definition loc_56 : location_info := LocationInfo file_0 25 17 25 22.
+  Definition loc_57 : location_info := LocationInfo file_0 24 18 24 29.
+  Definition loc_58 : location_info := LocationInfo file_0 24 18 24 23.
+  Definition loc_59 : location_info := LocationInfo file_0 24 18 24 23.
+  Definition loc_60 : location_info := LocationInfo file_0 24 32 24 46.
+  Definition loc_61 : location_info := LocationInfo file_0 24 2 24 12.
+  Definition loc_62 : location_info := LocationInfo file_0 24 2 24 7.
+  Definition loc_63 : location_info := LocationInfo file_0 24 2 24 7.
+  Definition loc_64 : location_info := LocationInfo file_0 24 15 24 16.
+  Definition loc_65 : location_info := LocationInfo file_0 23 29 23 60.
+  Definition loc_66 : location_info := LocationInfo file_0 23 29 23 34.
+  Definition loc_67 : location_info := LocationInfo file_0 23 29 23 34.
+  Definition loc_68 : location_info := LocationInfo file_0 23 35 23 59.
+  Definition loc_71 : location_info := LocationInfo file_0 22 18 22 29.
+  Definition loc_72 : location_info := LocationInfo file_0 22 18 22 23.
+  Definition loc_73 : location_info := LocationInfo file_0 22 18 22 23.
+  Definition loc_74 : location_info := LocationInfo file_0 22 32 22 46.
+  Definition loc_75 : location_info := LocationInfo file_0 22 2 22 12.
+  Definition loc_76 : location_info := LocationInfo file_0 22 2 22 7.
+  Definition loc_77 : location_info := LocationInfo file_0 22 2 22 7.
+  Definition loc_78 : location_info := LocationInfo file_0 22 15 22 16.
+  Definition loc_79 : location_info := LocationInfo file_0 21 29 21 60.
+  Definition loc_80 : location_info := LocationInfo file_0 21 29 21 34.
+  Definition loc_81 : location_info := LocationInfo file_0 21 29 21 34.
+  Definition loc_82 : location_info := LocationInfo file_0 21 35 21 59.
+
+  (* Definition of struct [list_node]. *)
+  Program Definition struct_list_node := {|
+    sl_members := [
+      (Some "val", it_layout i32);
+      (None, Layout 4%nat 0%nat);
+      (Some "next", LPtr)
+    ];
+  |}.
+  Solve Obligations with solve_struct_obligations.
+
+  (* Definition of function [append]. *)
+  Definition impl_append (append : loc): function := {|
+    f_args := [
+      ("l", LPtr);
+      ("k", LPtr)
+    ];
+    f_local_vars := [
+    ];
+    f_init := "#0";
+    f_code := (
+      <[ "#0" :=
+        locinfo: loc_22 ;
+        if: LocInfoE loc_22 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_22 ((LocInfoE loc_23 (use{LPtr} (LocInfoE loc_25 (!{LPtr} (LocInfoE loc_26 ("l")))))) ={PtrOp, PtrOp} (LocInfoE loc_27 (NULL)))))
+        then
+        locinfo: loc_4 ;
+          Goto "#1"
+        else
+        locinfo: loc_11 ;
+          Goto "#2"
+      ]> $
+      <[ "#1" :=
+        locinfo: loc_4 ;
+        LocInfoE loc_6 (!{LPtr} (LocInfoE loc_7 ("l"))) <-{ LPtr }
+          LocInfoE loc_8 (use{LPtr} (LocInfoE loc_9 ("k"))) ;
+        Return (VOID)
+      ]> $
+      <[ "#2" :=
+        locinfo: loc_11 ;
+        "_" <- LocInfoE loc_13 (append) with
+          [ LocInfoE loc_14 (&(LocInfoE loc_15 ((LocInfoE loc_16 (!{LPtr} (LocInfoE loc_18 (!{LPtr} (LocInfoE loc_19 ("l")))))) at{struct_list_node} "next"))) ;
+          LocInfoE loc_20 (use{LPtr} (LocInfoE loc_21 ("k"))) ] ;
+        Return (VOID)
+      ]> $∅
+    )%E
+  |}.
+
+  (* Definition of function [test]. *)
+  Definition impl_test (alloc append : loc): function := {|
+    f_args := [
+    ];
+    f_local_vars := [
+      ("node1", LPtr);
+      ("node2", LPtr)
+    ];
+    f_init := "#0";
+    f_code := (
+      <[ "#0" :=
+        locinfo: loc_79 ;
+        "$1" <- LocInfoE loc_81 (alloc) with
+          [ LocInfoE loc_82 (i2v (layout_of struct_list_node).(ly_size) size_t) ] ;
+        "node1" <-{ LPtr }
+          LocInfoE loc_79 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_79 ("$1"))) ;
+        locinfo: loc_31 ;
+        LocInfoE loc_75 ((LocInfoE loc_76 (!{LPtr} (LocInfoE loc_77 ("node1")))) at{struct_list_node} "val") <-{ it_layout i32 }
+          LocInfoE loc_78 (i2v 1 i32) ;
+        locinfo: loc_32 ;
+        LocInfoE loc_71 ((LocInfoE loc_72 (!{LPtr} (LocInfoE loc_73 ("node1")))) at{struct_list_node} "next") <-{ LPtr }
+          LocInfoE loc_74 (NULL) ;
+        locinfo: loc_65 ;
+        "$0" <- LocInfoE loc_67 (alloc) with
+          [ LocInfoE loc_68 (i2v (layout_of struct_list_node).(ly_size) size_t) ] ;
+        "node2" <-{ LPtr }
+          LocInfoE loc_65 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_65 ("$0"))) ;
+        locinfo: loc_34 ;
+        LocInfoE loc_61 ((LocInfoE loc_62 (!{LPtr} (LocInfoE loc_63 ("node2")))) at{struct_list_node} "val") <-{ it_layout i32 }
+          LocInfoE loc_64 (i2v 2 i32) ;
+        locinfo: loc_35 ;
+        LocInfoE loc_57 ((LocInfoE loc_58 (!{LPtr} (LocInfoE loc_59 ("node2")))) at{struct_list_node} "next") <-{ LPtr }
+          LocInfoE loc_60 (NULL) ;
+        locinfo: loc_36 ;
+        "_" <- LocInfoE loc_52 (append) with
+          [ LocInfoE loc_53 (&(LocInfoE loc_54 ("node1"))) ;
+          LocInfoE loc_55 (use{LPtr} (LocInfoE loc_56 ("node2"))) ] ;
+        locinfo: loc_47 ;
+        if: LocInfoE loc_47 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_47 ((LocInfoE loc_48 (use{LPtr} (LocInfoE loc_49 ("node1")))) !={PtrOp, PtrOp} (LocInfoE loc_50 (NULL)))))
+        then
+        locinfo: loc_39 ;
+          Goto "#1"
+        else
+        Goto "#2"
+      ]> $
+      <[ "#1" :=
+        locinfo: loc_39 ;
+        assert: (LocInfoE loc_40 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_40 ((LocInfoE loc_41 (use{it_layout i32} (LocInfoE loc_42 ((LocInfoE loc_43 (!{LPtr} (LocInfoE loc_44 ("node1")))) at{struct_list_node} "val")))) ={IntOp i32, IntOp i32} (LocInfoE loc_45 (i2v 1 i32)))))) ;
+        Return (VOID)
+      ]> $
+      <[ "#2" :=
+        Return (VOID)
+      ]> $∅
+    )%E
+  |}.
+End code.

examples/proofs/talk_demo1/generated_proof_append.v

+(* You were too lazy to even write a spec for this function. *)

examples/proofs/talk_demo1/generated_proof_test.v

+(* You were too lazy to even write a spec for this function. *)

examples/proofs/talk_demo1/generated_spec.v

+From refinedc.typing Require Import typing.
+From refinedc.examples.talk_demo1 Require Import generated_code.
+Set Default Proof Using "Type".
+
+(* Generated from [examples/talk_demo1.c]. *)
+Section spec.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Inlined code. *)
+
+  Definition alloc_initialized := initialized "allocator_state" ().
+
+  (* Type definitions. *)
+
+  (* Specifications for function [alloc]. *)
+  Definition type_of_alloc :=
+    fn(∀ size : nat; (size @ (int (size_t))); ⌜size + 16 ≤ max_int size_t⌝ ∗ ⌜(8 | size)⌝ ∗ (alloc_initialized))
+      → ∃ () : (), (&own (uninit (Layout size 3))); True.
+
+  (* Specifications for function [free]. *)
+  Definition type_of_free :=
+    fn(∀ size : nat; (size @ (int (size_t))), (&own (uninit (Layout size 3))); (alloc_initialized) ∗ ⌜(8 | size)⌝)
+      → ∃ () : (), (void); True.
+
+  (* Specifications for function [alloc_array]. *)
+  Definition type_of_alloc_array :=
+    fn(∀ (size, n) : nat * nat; (size @ (int (size_t))), (n @ (int (size_t))); ⌜size * n + 16 ≤ max_int size_t⌝ ∗ ⌜(8 | size)⌝ ∗ (alloc_initialized))
+      → ∃ () : (), (&own (array (Layout size 3) (replicate n (uninit (Layout size 3))))); True.
+
+  (* Specifications for function [free_array]. *)
+  Definition type_of_free_array :=
+    fn(∀ (size, n) : nat * nat; (size @ (int (size_t))), (n @ (int (size_t))), (&own (array (Layout size 3) (replicate n (uninit (Layout size 3))))); ⌜size * n ≤ max_int size_t⌝ ∗ ⌜(8 | size)⌝ ∗ (alloc_initialized))
+      → ∃ () : (), (void); True.
+
+  (* Function [append] has been skipped. *)
+
+  (* Function [test] has been skipped. *)
+End spec.

examples/proofs/talk_demo1/proof_files

+generated_proof_alloc.v
+generated_proof_alloc_array.v
+generated_proof_append.v
+generated_proof_free.v
+generated_proof_free_array.v
+generated_proof_test.v

examples/proofs/talk_demo2/dune

+; Generated by [refinedc], do not edit.
+(coq.theory
+ (flags -w -notation-overridden -w -redundant-canonical-projection)
+ (name refinedc.examples.talk_demo2)
+ (theories refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))

examples/proofs/talk_demo2/generated_code.v

+From refinedc.lang Require Export notation.
+From refinedc.lang Require Import tactics.
+From refinedc.typing Require Import annotations.
+Set Default Proof Using "Type".
+
+(* Generated from [examples/talk_demo2.c]. *)
+Section code.
+  Definition file_0 : string := "examples/talk_demo2.c".
+  Definition loc_2 : location_info := LocationInfo file_0 17 2 21 3.
+  Definition loc_3 : location_info := LocationInfo file_0 17 27 19 3.
+  Definition loc_4 : location_info := LocationInfo file_0 18 4 18 11.
+  Definition loc_5 : location_info := LocationInfo file_0 18 4 18 6.
+  Definition loc_6 : location_info := LocationInfo file_0 18 5 18 6.
+  Definition loc_7 : location_info := LocationInfo file_0 18 5 18 6.
+  Definition loc_8 : location_info := LocationInfo file_0 18 9 18 10.
+  Definition loc_9 : location_info := LocationInfo file_0 18 9 18 10.
+  Definition loc_10 : location_info := LocationInfo file_0 19 9 21 3.
+  Definition loc_11 : location_info := LocationInfo file_0 20 4 20 27.
+  Definition loc_12 : location_info := LocationInfo file_0 20 4 20 10.
+  Definition loc_13 : location_info := LocationInfo file_0 20 4 20 10.
+  Definition loc_14 : location_info := LocationInfo file_0 20 11 20 22.
+  Definition loc_15 : location_info := LocationInfo file_0 20 12 20 22.
+  Definition loc_16 : location_info := LocationInfo file_0 20 12 20 16.
+  Definition loc_17 : location_info := LocationInfo file_0 20 12 20 16.
+  Definition loc_18 : location_info := LocationInfo file_0 20 14 20 15.
+  Definition loc_19 : location_info := LocationInfo file_0 20 14 20 15.
+  Definition loc_20 : location_info := LocationInfo file_0 20 24 20 25.
+  Definition loc_21 : location_info := LocationInfo file_0 20 24 20 25.
+  Definition loc_22 : location_info := LocationInfo file_0 17 5 17 25.
+  Definition loc_23 : location_info := LocationInfo file_0 17 5 17 7.
+  Definition loc_24 : location_info := LocationInfo file_0 17 5 17 7.
+  Definition loc_25 : location_info := LocationInfo file_0 17 6 17 7.
+  Definition loc_26 : location_info := LocationInfo file_0 17 6 17 7.
+  Definition loc_27 : location_info := LocationInfo file_0 17 11 17 25.
+  Definition loc_30 : location_info := LocationInfo file_0 26 2 26 61.
+  Definition loc_31 : location_info := LocationInfo file_0 27 2 27 17.
+  Definition loc_32 : location_info := LocationInfo file_0 27 18 27 47.
+  Definition loc_33 : location_info := LocationInfo file_0 28 2 28 61.
+  Definition loc_34 : location_info := LocationInfo file_0 29 2 29 17.
+  Definition loc_35 : location_info := LocationInfo file_0 29 18 29 47.
+  Definition loc_36 : location_info := LocationInfo file_0 30 2 30 24.
+  Definition loc_37 : location_info := LocationInfo file_0 31 2 33 3.
+  Definition loc_38 : location_info := LocationInfo file_0 31 30 33 3.
+  Definition loc_39 : location_info := LocationInfo file_0 32 4 32 28.
+  Definition loc_40 : location_info := LocationInfo file_0 32 11 32 26.
+  Definition loc_41 : location_info := LocationInfo file_0 32 11 32 21.
+  Definition loc_42 : location_info := LocationInfo file_0 32 11 32 21.
+  Definition loc_43 : location_info := LocationInfo file_0 32 11 32 16.
+  Definition loc_44 : location_info := LocationInfo file_0 32 11 32 16.
+  Definition loc_45 : location_info := LocationInfo file_0 32 25 32 26.
+  Definition loc_47 : location_info := LocationInfo file_0 31 5 31 28.
+  Definition loc_48 : location_info := LocationInfo file_0 31 5 31 10.
+  Definition loc_49 : location_info := LocationInfo file_0 31 5 31 10.
+  Definition loc_50 : location_info := LocationInfo file_0 31 14 31 28.
+  Definition loc_51 : location_info := LocationInfo file_0 30 2 30 8.
+  Definition loc_52 : location_info := LocationInfo file_0 30 2 30 8.
+  Definition loc_53 : location_info := LocationInfo file_0 30 9 30 15.
+  Definition loc_54 : location_info := LocationInfo file_0 30 10 30 15.
+  Definition loc_55 : location_info := LocationInfo file_0 30 17 30 22.
+  Definition loc_56 : location_info := LocationInfo file_0 30 17 30 22.
+  Definition loc_57 : location_info := LocationInfo file_0 29 18 29 29.
+  Definition loc_58 : location_info := LocationInfo file_0 29 18 29 23.
+  Definition loc_59 : location_info := LocationInfo file_0 29 18 29 23.
+  Definition loc_60 : location_info := LocationInfo file_0 29 32 29 46.
+  Definition loc_61 : location_info := LocationInfo file_0 29 2 29 12.
+  Definition loc_62 : location_info := LocationInfo file_0 29 2 29 7.
+  Definition loc_63 : location_info := LocationInfo file_0 29 2 29 7.
+  Definition loc_64 : location_info := LocationInfo file_0 29 15 29 16.
+  Definition loc_65 : location_info := LocationInfo file_0 28 29 28 60.
+  Definition loc_66 : location_info := LocationInfo file_0 28 29 28 34.
+  Definition loc_67 : location_info := LocationInfo file_0 28 29 28 34.
+  Definition loc_68 : location_info := LocationInfo file_0 28 35 28 59.
+  Definition loc_71 : location_info := LocationInfo file_0 27 18 27 29.
+  Definition loc_72 : location_info := LocationInfo file_0 27 18 27 23.
+  Definition loc_73 : location_info := LocationInfo file_0 27 18 27 23.
+  Definition loc_74 : location_info := LocationInfo file_0 27 32 27 46.
+  Definition loc_75 : location_info := LocationInfo file_0 27 2 27 12.
+  Definition loc_76 : location_info := LocationInfo file_0 27 2 27 7.
+  Definition loc_77 : location_info := LocationInfo file_0 27 2 27 7.
+  Definition loc_78 : location_info := LocationInfo file_0 27 15 27 16.
+  Definition loc_79 : location_info := LocationInfo file_0 26 29 26 60.
+  Definition loc_80 : location_info := LocationInfo file_0 26 29 26 34.
+  Definition loc_81 : location_info := LocationInfo file_0 26 29 26 34.
+  Definition loc_82 : location_info := LocationInfo file_0 26 35 26 59.
+
+  (* Definition of struct [list_node]. *)
+  Program Definition struct_list_node := {|
+    sl_members := [
+      (Some "val", it_layout i32);
+      (None, Layout 4%nat 0%nat);
+      (Some "next", LPtr)
+    ];
+  |}.
+  Solve Obligations with solve_struct_obligations.
+
+  (* Definition of function [append]. *)
+  Definition impl_append (append : loc): function := {|
+    f_args := [
+      ("l", LPtr);
+      ("k", LPtr)
+    ];
+    f_local_vars := [
+    ];
+    f_init := "#0";
+    f_code := (
+      <[ "#0" :=
+        locinfo: loc_22 ;
+        if: LocInfoE loc_22 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_22 ((LocInfoE loc_23 (use{LPtr} (LocInfoE loc_25 (!{LPtr} (LocInfoE loc_26 ("l")))))) ={PtrOp, PtrOp} (LocInfoE loc_27 (NULL)))))
+        then
+        locinfo: loc_4 ;
+          Goto "#1"
+        else
+        locinfo: loc_11 ;
+          Goto "#2"
+      ]> $
+      <[ "#1" :=
+        locinfo: loc_4 ;
+        LocInfoE loc_6 (!{LPtr} (LocInfoE loc_7 ("l"))) <-{ LPtr }
+          LocInfoE loc_8 (use{LPtr} (LocInfoE loc_9 ("k"))) ;
+        Return (VOID)
+      ]> $
+      <[ "#2" :=
+        locinfo: loc_11 ;
+        "_" <- LocInfoE loc_13 (append) with
+          [ LocInfoE loc_14 (&(LocInfoE loc_15 ((LocInfoE loc_16 (!{LPtr} (LocInfoE loc_18 (!{LPtr} (LocInfoE loc_19 ("l")))))) at{struct_list_node} "next"))) ;
+          LocInfoE loc_20 (use{LPtr} (LocInfoE loc_21 ("k"))) ] ;
+        Return (VOID)
+      ]> $∅
+    )%E
+  |}.
+
+  (* Definition of function [test]. *)
+  Definition impl_test (alloc append : loc): function := {|
+    f_args := [
+    ];
+    f_local_vars := [
+      ("node1", LPtr);
+      ("node2", LPtr)
+    ];
+    f_init := "#0";
+    f_code := (
+      <[ "#0" :=
+        locinfo: loc_79 ;
+        "$1" <- LocInfoE loc_81 (alloc) with
+          [ LocInfoE loc_82 (i2v (layout_of struct_list_node).(ly_size) size_t) ] ;
+        "node1" <-{ LPtr }
+          LocInfoE loc_79 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_79 ("$1"))) ;
+        locinfo: loc_31 ;
+        LocInfoE loc_75 ((LocInfoE loc_76 (!{LPtr} (LocInfoE loc_77 ("node1")))) at{struct_list_node} "val") <-{ it_layout i32 }
+          LocInfoE loc_78 (i2v 1 i32) ;
+        locinfo: loc_32 ;
+        LocInfoE loc_71 ((LocInfoE loc_72 (!{LPtr} (LocInfoE loc_73 ("node1")))) at{struct_list_node} "next") <-{ LPtr }
+          LocInfoE loc_74 (NULL) ;
+        locinfo: loc_65 ;
+        "$0" <- LocInfoE loc_67 (alloc) with
+          [ LocInfoE loc_68 (i2v (layout_of struct_list_node).(ly_size) size_t) ] ;
+        "node2" <-{ LPtr }
+          LocInfoE loc_65 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_65 ("$0"))) ;
+        locinfo: loc_34 ;
+        LocInfoE loc_61 ((LocInfoE loc_62 (!{LPtr} (LocInfoE loc_63 ("node2")))) at{struct_list_node} "val") <-{ it_layout i32 }
+          LocInfoE loc_64 (i2v 2 i32) ;
+        locinfo: loc_35 ;
+        LocInfoE loc_57 ((LocInfoE loc_58 (!{LPtr} (LocInfoE loc_59 ("node2")))) at{struct_list_node} "next") <-{ LPtr }
+          LocInfoE loc_60 (NULL) ;
+        locinfo: loc_36 ;
+        "_" <- LocInfoE loc_52 (append) with
+          [ LocInfoE loc_53 (&(LocInfoE loc_54 ("node1"))) ;
+          LocInfoE loc_55 (use{LPtr} (LocInfoE loc_56 ("node2"))) ] ;
+        locinfo: loc_47 ;
+        if: LocInfoE loc_47 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_47 ((LocInfoE loc_48 (use{LPtr} (LocInfoE loc_49 ("node1")))) !={PtrOp, PtrOp} (LocInfoE loc_50 (NULL)))))
+        then
+        locinfo: loc_39 ;
+          Goto "#1"
+        else
+        Goto "#2"
+      ]> $
+      <[ "#1" :=
+        locinfo: loc_39 ;
+        assert: (LocInfoE loc_40 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_40 ((LocInfoE loc_41 (use{it_layout i32} (LocInfoE loc_42 ((LocInfoE loc_43 (!{LPtr} (LocInfoE loc_44 ("node1")))) at{struct_list_node} "val")))) ={IntOp i32, IntOp i32} (LocInfoE loc_45 (i2v 1 i32)))))) ;
+        Return (VOID)
+      ]> $
+      <[ "#2" :=
+        Return (VOID)
+      ]> $∅
+    )%E
+  |}.
+End code.

examples/proofs/talk_demo2/generated_proof_append.v

+From refinedc.typing Require Import typing.
+From refinedc.examples.talk_demo2 Require Import generated_code.
+From refinedc.examples.talk_demo2 Require Import generated_spec.
+Set Default Proof Using "Type".
+
+(* Generated from [examples/talk_demo2.c]. *)
+Section proof_append.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Typing proof for [append]. *)
+  Lemma type_append (append : loc) :
+    append ◁ᵥ append @ function_ptr type_of_append -∗
+    typed_function (impl_append append) type_of_append.
+  Proof.
+    start_function "append" ([]) => arg_l arg_k.
+    split_blocks ((
+      ∅
+    )%I : gmap label (iProp Σ)) ((
+      ∅
+    )%I : gmap label (iProp Σ)).
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "append" "#0".
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+    all: print_sidecondition_goal "append".
+  Qed.
+End proof_append.

examples/proofs/talk_demo2/generated_proof_test.v

+(* You were too lazy to even write a spec for this function. *)

examples/proofs/talk_demo2/generated_spec.v

+From refinedc.typing Require Import typing.
+From refinedc.examples.talk_demo2 Require Import generated_code.
+Set Default Proof Using "Type".
+
+(* Generated from [examples/talk_demo2.c]. *)
+Section spec.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Inlined code. *)
+
+  Definition alloc_initialized := initialized "allocator_state" ().
+
+  (* Definition of type [list_t]. *)
+  Definition list_t_rec : (unit -d> typeO) → (unit -d> typeO) := (λ self u,
+    (optionalO (λ _ : unit,
+      &own (
+        struct struct_list_node [@{type}
+          (int (i32)) ;
+          (tyexists (λ rfmt__, guarded ("list_t_0") (apply_dfun self (rfmt__))))
+        ]
+      )
+    ) (null))
+  )%I.
+  Typeclasses Opaque list_t_rec.
+
+  Global Instance list_t_rec_ne : Contractive list_t_rec.
+  Proof. solve_type_proper. Qed.
+
+  Definition list_t : rtype := {|
+    rty_type := unit;
+    rty r__ := fixp list_t_rec r__
+  |}.
+
+  Lemma list_t_unfold (u : unit) :
+    (u @ list_t)%I ≡@{type} (
+      (optionalO (λ _ : unit,
+        &own (
+          struct struct_list_node [@{type}
+            (int (i32)) ;
+            (tyexists (λ rfmt__, guarded "list_t_0" (rfmt__ @ list_t)))
+          ]
+        )
+      ) (null))
+    )%I.
+  Proof. by rewrite {1}/with_refinement/=fixp_unfold. Qed.
+
+
+  Global Program Instance list_t_rmovable : RMovable list_t :=
+    {| rmovable 'u := movable_eq _ _ (list_t_unfold u) |}.
+  Next Obligation. solve_ty_layout_eq. Qed.
+
+  Global Instance list_t_simplify_hyp_place_inst l_ β_ (u : unit) :
+    SimplifyHypPlace l_ β_ (u @ list_t)%I (Some 100%N) :=
+    λ T, i2p (simplify_hyp_place_eq l_ β_ _ _ T (list_t_unfold _)).
+  Global Instance list_t_simplify_goal_place_inst l_ β_ (u : unit) :
+    SimplifyGoalPlace l_ β_ (u @ list_t)%I (Some 100%N) :=
+    λ T, i2p (simplify_goal_place_eq l_ β_ _ _ T (list_t_unfold _)).
+
+  Global Program Instance list_t_simplify_hyp_val_inst v_ (u : unit) :
+    SimplifyHypVal v_ (u @ list_t)%I (Some 100%N) :=
+    λ T, i2p (simplify_hyp_val_eq v_ _ _ (list_t_unfold _) T _).
+  Next Obligation. done. Qed.
+  Global Program Instance list_t_simplify_goal_val_inst v_ (u : unit) :
+    SimplifyGoalVal v_ (u @ list_t)%I (Some 100%N) :=
+    λ T, i2p (simplify_goal_val_eq v_ _ _ (list_t_unfold _) T _).
+  Next Obligation. done. Qed.
+
+  (* Type definitions. *)
+
+  (* Specifications for function [alloc]. *)
+  Definition type_of_alloc :=
+    fn(∀ size : nat; (size @ (int (size_t))); ⌜size + 16 ≤ max_int size_t⌝ ∗ ⌜(8 | size)⌝ ∗ (alloc_initialized))
+      → ∃ () : (), (&own (uninit (Layout size 3))); True.
+
+  (* Specifications for function [free]. *)
+  Definition type_of_free :=
+    fn(∀ size : nat; (size @ (int (size_t))), (&own (uninit (Layout size 3))); (alloc_initialized) ∗ ⌜(8 | size)⌝)
+      → ∃ () : (), (void); True.
+
+  (* Specifications for function [alloc_array]. *)
+  Definition type_of_alloc_array :=
+    fn(∀ (size, n) : nat * nat; (size @ (int (size_t))), (n @ (int (size_t))); ⌜size * n + 16 ≤ max_int size_t⌝ ∗ ⌜(8 | size)⌝ ∗ (alloc_initialized))
+      → ∃ () : (), (&own (array (Layout size 3) (replicate n (uninit (Layout size 3))))); True.
+
+  (* Specifications for function [free_array]. *)
+  Definition type_of_free_array :=
+    fn(∀ (size, n) : nat * nat; (size @ (int (size_t))), (n @ (int (size_t))), (&own (array (Layout size 3) (replicate n (uninit (Layout size 3))))); ⌜size * n ≤ max_int size_t⌝ ∗ ⌜(8 | size)⌝ ∗ (alloc_initialized))
+      → ∃ () : (), (void); True.
+
+  (* Specifications for function [append]. *)
+  Definition type_of_append :=
+    fn(∀ () : (); (&own (list_t)), (list_t); True)
+      → ∃ () : (), (void); True.
+
+  (* Function [test] has been skipped. *)
+End spec.
+
+Typeclasses Opaque list_t_rec.

examples/proofs/talk_demo2/proof_files

+generated_proof_alloc.v
+generated_proof_alloc_array.v
+generated_proof_append.v
+generated_proof_free.v
+generated_proof_free_array.v
+generated_proof_test.v

examples/proofs/talk_demo3/dune

+; Generated by [refinedc], do not edit.
+(coq.theory
+ (flags -w -notation-overridden -w -redundant-canonical-projection)
+ (name refinedc.examples.talk_demo3)
+ (theories refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))

examples/proofs/talk_demo3/generated_code.v

+From refinedc.lang Require Export notation.
+From refinedc.lang Require Import tactics.
+From refinedc.typing Require Import annotations.
+Set Default Proof Using "Type".
+
+(* Generated from [examples/talk_demo3.c]. *)
+Section code.
+  Definition file_0 : string := "examples/talk_demo3.c".
+  Definition loc_2 : location_info := LocationInfo file_0 21 2 25 3.
+  Definition loc_3 : location_info := LocationInfo file_0 21 27 23 3.
+  Definition loc_4 : location_info := LocationInfo file_0 22 4 22 11.
+  Definition loc_5 : location_info := LocationInfo file_0 22 4 22 6.
+  Definition loc_6 : location_info := LocationInfo file_0 22 5 22 6.
+  Definition loc_7 : location_info := LocationInfo file_0 22 5 22 6.
+  Definition loc_8 : location_info := LocationInfo file_0 22 9 22 10.
+  Definition loc_9 : location_info := LocationInfo file_0 22 9 22 10.
+  Definition loc_10 : location_info := LocationInfo file_0 23 9 25 3.
+  Definition loc_11 : location_info := LocationInfo file_0 24 4 24 27.
+  Definition loc_12 : location_info := LocationInfo file_0 24 4 24 10.
+  Definition loc_13 : location_info := LocationInfo file_0 24 4 24 10.
+  Definition loc_14 : location_info := LocationInfo file_0 24 11 24 22.
+  Definition loc_15 : location_info := LocationInfo file_0 24 12 24 22.
+  Definition loc_16 : location_info := LocationInfo file_0 24 12 24 16.
+  Definition loc_17 : location_info := LocationInfo file_0 24 12 24 16.
+  Definition loc_18 : location_info := LocationInfo file_0 24 14 24 15.
+  Definition loc_19 : location_info := LocationInfo file_0 24 14 24 15.
+  Definition loc_20 : location_info := LocationInfo file_0 24 24 24 25.
+  Definition loc_21 : location_info := LocationInfo file_0 24 24 24 25.
+  Definition loc_22 : location_info := LocationInfo file_0 21 5 21 25.
+  Definition loc_23 : location_info := LocationInfo file_0 21 5 21 7.
+  Definition loc_24 : location_info := LocationInfo file_0 21 5 21 7.
+  Definition loc_25 : location_info := LocationInfo file_0 21 6 21 7.
+  Definition loc_26 : location_info := LocationInfo file_0 21 6 21 7.
+  Definition loc_27 : location_info := LocationInfo file_0 21 11 21 25.
+  Definition loc_30 : location_info := LocationInfo file_0 30 2 30 61.
+  Definition loc_31 : location_info := LocationInfo file_0 31 2 31 17.
+  Definition loc_32 : location_info := LocationInfo file_0 31 18 31 47.
+  Definition loc_33 : location_info := LocationInfo file_0 32 2 32 61.
+  Definition loc_34 : location_info := LocationInfo file_0 33 2 33 17.
+  Definition loc_35 : location_info := LocationInfo file_0 33 18 33 47.
+  Definition loc_36 : location_info := LocationInfo file_0 34 2 34 24.
+  Definition loc_37 : location_info := LocationInfo file_0 35 2 37 3.
+  Definition loc_38 : location_info := LocationInfo file_0 35 30 37 3.
+  Definition loc_39 : location_info := LocationInfo file_0 36 4 36 28.
+  Definition loc_40 : location_info := LocationInfo file_0 36 11 36 26.
+  Definition loc_41 : location_info := LocationInfo file_0 36 11 36 21.
+  Definition loc_42 : location_info := LocationInfo file_0 36 11 36 21.
+  Definition loc_43 : location_info := LocationInfo file_0 36 11 36 16.
+  Definition loc_44 : location_info := LocationInfo file_0 36 11 36 16.
+  Definition loc_45 : location_info := LocationInfo file_0 36 25 36 26.
+  Definition loc_47 : location_info := LocationInfo file_0 35 5 35 28.
+  Definition loc_48 : location_info := LocationInfo file_0 35 5 35 10.
+  Definition loc_49 : location_info := LocationInfo file_0 35 5 35 10.
+  Definition loc_50 : location_info := LocationInfo file_0 35 14 35 28.
+  Definition loc_51 : location_info := LocationInfo file_0 34 2 34 8.
+  Definition loc_52 : location_info := LocationInfo file_0 34 2 34 8.
+  Definition loc_53 : location_info := LocationInfo file_0 34 9 34 15.
+  Definition loc_54 : location_info := LocationInfo file_0 34 10 34 15.
+  Definition loc_55 : location_info := LocationInfo file_0 34 17 34 22.
+  Definition loc_56 : location_info := LocationInfo file_0 34 17 34 22.
+  Definition loc_57 : location_info := LocationInfo file_0 33 18 33 29.
+  Definition loc_58 : location_info := LocationInfo file_0 33 18 33 23.
+  Definition loc_59 : location_info := LocationInfo file_0 33 18 33 23.
+  Definition loc_60 : location_info := LocationInfo file_0 33 32 33 46.
+  Definition loc_61 : location_info := LocationInfo file_0 33 2 33 12.
+  Definition loc_62 : location_info := LocationInfo file_0 33 2 33 7.
+  Definition loc_63 : location_info := LocationInfo file_0 33 2 33 7.
+  Definition loc_64 : location_info := LocationInfo file_0 33 15 33 16.
+  Definition loc_65 : location_info := LocationInfo file_0 32 29 32 60.
+  Definition loc_66 : location_info := LocationInfo file_0 32 29 32 34.
+  Definition loc_67 : location_info := LocationInfo file_0 32 29 32 34.
+  Definition loc_68 : location_info := LocationInfo file_0 32 35 32 59.
+  Definition loc_71 : location_info := LocationInfo file_0 31 18 31 29.
+  Definition loc_72 : location_info := LocationInfo file_0 31 18 31 23.
+  Definition loc_73 : location_info := LocationInfo file_0 31 18 31 23.
+  Definition loc_74 : location_info := LocationInfo file_0 31 32 31 46.
+  Definition loc_75 : location_info := LocationInfo file_0 31 2 31 12.
+  Definition loc_76 : location_info := LocationInfo file_0 31 2 31 7.
+  Definition loc_77 : location_info := LocationInfo file_0 31 2 31 7.
+  Definition loc_78 : location_info := LocationInfo file_0 31 15 31 16.
+  Definition loc_79 : location_info := LocationInfo file_0 30 29 30 60.
+  Definition loc_80 : location_info := LocationInfo file_0 30 29 30 34.
+  Definition loc_81 : location_info := LocationInfo file_0 30 29 30 34.
+  Definition loc_82 : location_info := LocationInfo file_0 30 35 30 59.
+
+  (* Definition of struct [list_node]. *)
+  Program Definition struct_list_node := {|
+    sl_members := [
+      (Some "val", it_layout i32);
+      (None, Layout 4%nat 0%nat);
+      (Some "next", LPtr)
+    ];
+  |}.
+  Solve Obligations with solve_struct_obligations.
+
+  (* Definition of function [append]. *)
+  Definition impl_append (append : loc): function := {|
+    f_args := [
+      ("l", LPtr);
+      ("k", LPtr)
+    ];
+    f_local_vars := [
+    ];
+    f_init := "#0";
+    f_code := (
+      <[ "#0" :=
+        locinfo: loc_22 ;
+        if: LocInfoE loc_22 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_22 ((LocInfoE loc_23 (use{LPtr} (LocInfoE loc_25 (!{LPtr} (LocInfoE loc_26 ("l")))))) ={PtrOp, PtrOp} (LocInfoE loc_27 (NULL)))))
+        then
+        locinfo: loc_4 ;
+          Goto "#1"
+        else
+        locinfo: loc_11 ;
+          Goto "#2"
+      ]> $
+      <[ "#1" :=
+        locinfo: loc_4 ;
+        LocInfoE loc_6 (!{LPtr} (LocInfoE loc_7 ("l"))) <-{ LPtr }
+          LocInfoE loc_8 (use{LPtr} (LocInfoE loc_9 ("k"))) ;
+        Return (VOID)
+      ]> $
+      <[ "#2" :=
+        locinfo: loc_11 ;
+        "_" <- LocInfoE loc_13 (append) with
+          [ LocInfoE loc_14 (&(LocInfoE loc_15 ((LocInfoE loc_16 (!{LPtr} (LocInfoE loc_18 (!{LPtr} (LocInfoE loc_19 ("l")))))) at{struct_list_node} "next"))) ;
+          LocInfoE loc_20 (use{LPtr} (LocInfoE loc_21 ("k"))) ] ;
+        Return (VOID)
+      ]> $∅
+    )%E
+  |}.
+
+  (* Definition of function [test]. *)
+  Definition impl_test (alloc append : loc): function := {|
+    f_args := [
+    ];
+    f_local_vars := [
+      ("node1", LPtr);
+      ("node2", LPtr)
+    ];
+    f_init := "#0";
+    f_code := (
+      <[ "#0" :=
+        locinfo: loc_79 ;
+        "$1" <- LocInfoE loc_81 (alloc) with
+          [ LocInfoE loc_82 (i2v (layout_of struct_list_node).(ly_size) size_t) ] ;
+        "node1" <-{ LPtr }
+          LocInfoE loc_79 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_79 ("$1"))) ;
+        locinfo: loc_31 ;
+        LocInfoE loc_75 ((LocInfoE loc_76 (!{LPtr} (LocInfoE loc_77 ("node1")))) at{struct_list_node} "val") <-{ it_layout i32 }
+          LocInfoE loc_78 (i2v 1 i32) ;
+        locinfo: loc_32 ;
+        LocInfoE loc_71 ((LocInfoE loc_72 (!{LPtr} (LocInfoE loc_73 ("node1")))) at{struct_list_node} "next") <-{ LPtr }
+          LocInfoE loc_74 (NULL) ;
+        locinfo: loc_65 ;
+        "$0" <- LocInfoE loc_67 (alloc) with
+          [ LocInfoE loc_68 (i2v (layout_of struct_list_node).(ly_size) size_t) ] ;
+        "node2" <-{ LPtr }
+          LocInfoE loc_65 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_65 ("$0"))) ;
+        locinfo: loc_34 ;
+        LocInfoE loc_61 ((LocInfoE loc_62 (!{LPtr} (LocInfoE loc_63 ("node2")))) at{struct_list_node} "val") <-{ it_layout i32 }
+          LocInfoE loc_64 (i2v 2 i32) ;
+        locinfo: loc_35 ;
+        LocInfoE loc_57 ((LocInfoE loc_58 (!{LPtr} (LocInfoE loc_59 ("node2")))) at{struct_list_node} "next") <-{ LPtr }
+          LocInfoE loc_60 (NULL) ;
+        locinfo: loc_36 ;
+        "_" <- LocInfoE loc_52 (append) with
+          [ LocInfoE loc_53 (&(LocInfoE loc_54 ("node1"))) ;
+          LocInfoE loc_55 (use{LPtr} (LocInfoE loc_56 ("node2"))) ] ;
+        locinfo: loc_47 ;
+        if: LocInfoE loc_47 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_47 ((LocInfoE loc_48 (use{LPtr} (LocInfoE loc_49 ("node1")))) !={PtrOp, PtrOp} (LocInfoE loc_50 (NULL)))))
+        then
+        locinfo: loc_39 ;
+          Goto "#1"
+        else
+        Goto "#2"
+      ]> $
+      <[ "#1" :=
+        locinfo: loc_39 ;
+        assert: (LocInfoE loc_40 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_40 ((LocInfoE loc_41 (use{it_layout i32} (LocInfoE loc_42 ((LocInfoE loc_43 (!{LPtr} (LocInfoE loc_44 ("node1")))) at{struct_list_node} "val")))) ={IntOp i32, IntOp i32} (LocInfoE loc_45 (i2v 1 i32)))))) ;
+        Return (VOID)
+      ]> $
+      <[ "#2" :=
+        Return (VOID)
+      ]> $∅
+    )%E
+  |}.
+End code.

examples/proofs/talk_demo3/generated_proof_append.v

+From refinedc.typing Require Import typing.
+From refinedc.examples.talk_demo3 Require Import generated_code.
+From refinedc.examples.talk_demo3 Require Import generated_spec.
+Set Default Proof Using "Type".
+
+(* Generated from [examples/talk_demo3.c]. *)
+Section proof_append.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Typing proof for [append]. *)
+  Lemma type_append (append : loc) :
+    append ◁ᵥ append @ function_ptr type_of_append -∗
+    typed_function (impl_append append) type_of_append.
+  Proof.
+    start_function "append" ([[p xs] ys]) => arg_l arg_k.
+    split_blocks ((
+      ∅
+    )%I : gmap label (iProp Σ)) ((
+      ∅
+    )%I : gmap label (iProp Σ)).
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "append" "#0".
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+    all: print_sidecondition_goal "append".
+  Qed.
+End proof_append.

examples/proofs/talk_demo3/generated_proof_test.v

+From refinedc.typing Require Import typing.
+From refinedc.examples.talk_demo3 Require Import generated_code.
+From refinedc.examples.talk_demo3 Require Import generated_spec.
+Set Default Proof Using "Type".
+
+(* Generated from [examples/talk_demo3.c]. *)
+Section proof_test.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Typing proof for [test]. *)
+  Lemma type_test (alloc append : loc) :
+    alloc ◁ᵥ alloc @ function_ptr type_of_alloc -∗
+    append ◁ᵥ append @ function_ptr type_of_append -∗
+    typed_function (impl_test alloc append) type_of_test.
+  Proof.
+    start_function "test" ([]) => local_node1 local_node2.
+    split_blocks ((
+      ∅
+    )%I : gmap label (iProp Σ)) ((
+      ∅
+    )%I : gmap label (iProp Σ)).
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "test" "#0".
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+    all: print_sidecondition_goal "test".
+  Qed.
+End proof_test.

examples/proofs/talk_demo3/generated_spec.v

+From refinedc.typing Require Import typing.
+From refinedc.examples.talk_demo3 Require Import generated_code.
+Set Default Proof Using "Type".
+
+(* Generated from [examples/talk_demo3.c]. *)
+Section spec.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Inlined code. *)
+
+  Definition alloc_initialized := initialized "allocator_state" ().
+
+  (* Definition of type [list_t]. *)
+  Definition list_t_rec : ((list Z) -d> typeO) → ((list Z) -d> typeO) := (λ self xs,
+    ((xs <> []) @ (optional (&own (
+      tyexists (λ y : Z,
+      tyexists (λ ys : list Z,
+      constrained (struct struct_list_node [@{type}
+        (y @ (int (i32))) ;
+        (guarded ("list_t_0") (apply_dfun self (ys)))
+      ]) (
+        ⌜xs = y :: ys⌝
+      )))
+    )) (null)))
+  )%I.
+  Typeclasses Opaque list_t_rec.
+
+  Global Instance list_t_rec_ne : Contractive list_t_rec.
+  Proof. solve_type_proper. Qed.
+
+  Definition list_t : rtype := {|
+    rty_type := (list Z);
+    rty r__ := fixp list_t_rec r__
+  |}.
+
+  Lemma list_t_unfold (xs : list Z) :
+    (xs @ list_t)%I ≡@{type} (
+      ((xs <> []) @ (optional (&own (
+        tyexists (λ y : Z,
+        tyexists (λ ys : list Z,
+        constrained (struct struct_list_node [@{type}
+          (y @ (int (i32))) ;
+          (guarded "list_t_0" (ys @ list_t))
+        ]) (
+          ⌜xs = y :: ys⌝
+        )))
+      )) (null)))
+    )%I.
+  Proof. by rewrite {1}/with_refinement/=fixp_unfold. Qed.
+
+
+  Global Program Instance list_t_rmovable : RMovable list_t :=
+    {| rmovable 'xs := movable_eq _ _ (list_t_unfold xs) |}.
+  Next Obligation. solve_ty_layout_eq. Qed.
+
+  Global Instance list_t_simplify_hyp_place_inst l_ β_ (xs : list Z) :
+    SimplifyHypPlace l_ β_ (xs @ list_t)%I (Some 100%N) :=
+    λ T, i2p (simplify_hyp_place_eq l_ β_ _ _ T (list_t_unfold _)).
+  Global Instance list_t_simplify_goal_place_inst l_ β_ (xs : list Z) :
+    SimplifyGoalPlace l_ β_ (xs @ list_t)%I (Some 100%N) :=
+    λ T, i2p (simplify_goal_place_eq l_ β_ _ _ T (list_t_unfold _)).
+
+  Global Program Instance list_t_simplify_hyp_val_inst v_ (xs : list Z) :
+    SimplifyHypVal v_ (xs @ list_t)%I (Some 100%N) :=
+    λ T, i2p (simplify_hyp_val_eq v_ _ _ (list_t_unfold _) T _).
+  Next Obligation. done. Qed.
+  Global Program Instance list_t_simplify_goal_val_inst v_ (xs : list Z) :
+    SimplifyGoalVal v_ (xs @ list_t)%I (Some 100%N) :=
+    λ T, i2p (simplify_goal_val_eq v_ _ _ (list_t_unfold _) T _).
+  Next Obligation. done. Qed.
+
+  (* Type definitions. *)
+
+  (* Specifications for function [alloc]. *)
+  Definition type_of_alloc :=
+    fn(∀ size : nat; (size @ (int (size_t))); ⌜size + 16 ≤ max_int size_t⌝ ∗ ⌜(8 | size)⌝ ∗ (alloc_initialized))
+      → ∃ () : (), (&own (uninit (Layout size 3))); True.
+
+  (* Specifications for function [free]. *)
+  Definition type_of_free :=
+    fn(∀ size : nat; (size @ (int (size_t))), (&own (uninit (Layout size 3))); (alloc_initialized) ∗ ⌜(8 | size)⌝)
+      → ∃ () : (), (void); True.
+
+  (* Specifications for function [alloc_array]. *)
+  Definition type_of_alloc_array :=
+    fn(∀ (size, n) : nat * nat; (size @ (int (size_t))), (n @ (int (size_t))); ⌜size * n + 16 ≤ max_int size_t⌝ ∗ ⌜(8 | size)⌝ ∗ (alloc_initialized))
+      → ∃ () : (), (&own (array (Layout size 3) (replicate n (uninit (Layout size 3))))); True.
+
+  (* Specifications for function [free_array]. *)
+  Definition type_of_free_array :=
+    fn(∀ (size, n) : nat * nat; (size @ (int (size_t))), (n @ (int (size_t))), (&own (array (Layout size 3) (replicate n (uninit (Layout size 3))))); ⌜size * n ≤ max_int size_t⌝ ∗ ⌜(8 | size)⌝ ∗ (alloc_initialized))
+      → ∃ () : (), (void); True.
+
+  (* Specifications for function [append]. *)
+  Definition type_of_append :=
+    fn(∀ (p, xs, ys) : loc * (list Z) * (list Z); (p @ (&own (xs @ (list_t)))), (ys @ (list_t)); True)
+      → ∃ () : (), (void); (p ◁ₗ ((xs ++ ys) @ (list_t))).
+
+  (* Specifications for function [test]. *)
+  Definition type_of_test :=
+    fn(∀ () : (); (alloc_initialized)) → ∃ () : (), (void); True.
+End spec.
+
+Typeclasses Opaque list_t_rec.

examples/proofs/talk_demo3/proof_files

+generated_proof_alloc.v
+generated_proof_alloc_array.v
+generated_proof_append.v
+generated_proof_free.v
+generated_proof_free_array.v
+generated_proof_test.v

examples/talk_demo1.c

+#include <stddef.h>
+#include <refinedc.h>
+#include <alloc.h>
+
+typedef struct
+list_node {
+  int val;
+  struct list_node *next;
+} *list_t;
+
+void append(list_t *l, list_t k) {
+  if(*l == NULL) {
+    *l = k;
+  } else {
+    append(&(*l)->next, k);
+  }
+}
+
+/* [[rc::requires("[alloc_initialized]")]] */
+void test() {
+  struct list_node * node1 = alloc(sizeof(struct list_node));
+  node1->val = 1; node1->next = NULL;
+  struct list_node * node2 = alloc(sizeof(struct list_node));
+  node2->val = 2; node2->next = NULL;
+  append(&node1, node2);
+  if(node1 != NULL) {
+    assert(node1->val == 1);
+  }
+  /* assert(node1->next->val == 2); */
+  /* free(sizeof(struct list_node), node1->next); */
+  /* free(sizeof(struct list_node), node1); */
+}