Add infrastructure to destruct products in function parameters.

theories/lithium/interpreter.v

@@ -525,6 +525,7 @@ Ltac liForall :=
        dependent variables to distinguish between dependent and non dependent forall *)
     | |- ?P -> ?Q => fail "implication, not forall"
     | |- forall _ : ?P, _ =>
+      (* When changing this, also change [prepare_initial_coq_context] in automation.v *)
       lazymatch P with
       | (prod _ _) => case
       | unit => case

theories/typing/automation.v

@@ -213,6 +213,25 @@ Ltac liRStep :=
 ]; liSimpl.
 
 (** * Tactics for starting a function *)
+(* Recursively destruct a product in hypothesis H, using the given name as template. *)
+Ltac destruct_product_hypothesis name H :=
+  match goal with
+  | H : _ * _ |- _ => let tmp1 := fresh "tmp" in
+                      let tmp2 := fresh "tmp" in
+                      destruct H as [tmp1 tmp2];
+                      destruct_product_hypothesis name tmp1;
+                      destruct_product_hypothesis name tmp2
+  |           |- _ => let id := fresh name in
+                      rename H into id
+  end.
+
+Ltac prepare_initial_coq_context :=
+  (* The automation assumes that all products in the context are destructed, see liForall *)
+  repeat lazymatch goal with
+  | H : _ * _ |- _ => destruct_product_hypothesis H H
+  | H : unit |- _ => destruct H
+  end.
+
 (* IMPORTANT: We need to make sure to never call simpl while the code
 (Q) is part of the goal, because simpl seems to take exponential time
 in the number of blocks! *)
@@ -224,7 +243,7 @@ Tactic Notation "start_function" constr(fnname) "(" simple_intropattern(x) ")" :
   iIntros ( x );
   iSplit; [iPureIntro; simpl; by [repeat constructor] || fail "in" fnname "argument types don't match layout of arguments" |];
   let lsa := fresh "lsa" in let lsv := fresh "lsv" in
-  iIntros "!#" (lsa lsv); inv_vec lsv; inv_vec lsa.
+  iIntros "!#" (lsa lsv); inv_vec lsv; inv_vec lsa; prepare_initial_coq_context.
 
 Ltac liRSplitBlocksIntro :=
   repeat (

tutorial/proofs/t06_struct/generated_code.v

@@ -39,17 +39,38 @@ Section code.
   Definition loc_52 : location_info := LocationInfo file_0 49 9 49 12.
   Definition loc_53 : location_info := LocationInfo file_0 49 9 49 12.
   Definition loc_54 : location_info := LocationInfo file_0 49 9 49 10.
-  Definition loc_57 : location_info := LocationInfo file_0 54 2 54 41.
-  Definition loc_58 : location_info := LocationInfo file_0 54 9 54 39.
-  Definition loc_59 : location_info := LocationInfo file_0 54 9 54 25.
-  Definition loc_60 : location_info := LocationInfo file_0 54 9 54 16.
-  Definition loc_61 : location_info := LocationInfo file_0 54 9 54 16.
-  Definition loc_62 : location_info := LocationInfo file_0 54 17 54 24.
-  Definition loc_63 : location_info := LocationInfo file_0 54 17 54 21.
-  Definition loc_64 : location_info := LocationInfo file_0 54 17 54 21.
-  Definition loc_65 : location_info := LocationInfo file_0 54 22 54 23.
-  Definition loc_66 : location_info := LocationInfo file_0 54 29 54 39.
-  Definition loc_67 : location_info := LocationInfo file_0 54 38 54 39.
+  Definition loc_57 : location_info := LocationInfo file_0 56 2 56 13.
+  Definition loc_58 : location_info := LocationInfo file_0 56 2 56 8.
+  Definition loc_59 : location_info := LocationInfo file_0 56 2 56 6.
+  Definition loc_60 : location_info := LocationInfo file_0 56 4 56 5.
+  Definition loc_61 : location_info := LocationInfo file_0 56 4 56 5.
+  Definition loc_62 : location_info := LocationInfo file_0 56 11 56 12.
+  Definition loc_63 : location_info := LocationInfo file_0 56 11 56 12.
+  Definition loc_66 : location_info := LocationInfo file_0 63 2 63 13.
+  Definition loc_67 : location_info := LocationInfo file_0 63 2 63 8.
+  Definition loc_68 : location_info := LocationInfo file_0 63 2 63 6.
+  Definition loc_69 : location_info := LocationInfo file_0 63 4 63 5.
+  Definition loc_70 : location_info := LocationInfo file_0 63 4 63 5.
+  Definition loc_71 : location_info := LocationInfo file_0 63 11 63 12.
+  Definition loc_72 : location_info := LocationInfo file_0 63 11 63 12.
+  Definition loc_75 : location_info := LocationInfo file_0 70 2 70 13.
+  Definition loc_76 : location_info := LocationInfo file_0 70 2 70 8.
+  Definition loc_77 : location_info := LocationInfo file_0 70 2 70 6.
+  Definition loc_78 : location_info := LocationInfo file_0 70 4 70 5.
+  Definition loc_79 : location_info := LocationInfo file_0 70 4 70 5.
+  Definition loc_80 : location_info := LocationInfo file_0 70 11 70 12.
+  Definition loc_81 : location_info := LocationInfo file_0 70 11 70 12.
+  Definition loc_84 : location_info := LocationInfo file_0 75 2 75 41.
+  Definition loc_85 : location_info := LocationInfo file_0 75 9 75 39.
+  Definition loc_86 : location_info := LocationInfo file_0 75 9 75 25.
+  Definition loc_87 : location_info := LocationInfo file_0 75 9 75 16.
+  Definition loc_88 : location_info := LocationInfo file_0 75 9 75 16.
+  Definition loc_89 : location_info := LocationInfo file_0 75 17 75 24.
+  Definition loc_90 : location_info := LocationInfo file_0 75 17 75 21.
+  Definition loc_91 : location_info := LocationInfo file_0 75 17 75 21.
+  Definition loc_92 : location_info := LocationInfo file_0 75 22 75 23.
+  Definition loc_93 : location_info := LocationInfo file_0 75 29 75 39.
+  Definition loc_94 : location_info := LocationInfo file_0 75 38 75 39.
 
   (* Definition of struct [color]. *)
   Program Definition struct_color := {|
@@ -166,6 +187,63 @@ Section code.
     )%E
   |}.
 
+  (* Definition of function [set_red]. *)
+  Definition impl_set_red : function := {|
+    f_args := [
+      ("c", LPtr);
+      ("r", it_layout u8)
+    ];
+    f_local_vars := [
+    ];
+    f_init := "#0";
+    f_code := (
+      <[ "#0" :=
+        locinfo: loc_57 ;
+        LocInfoE loc_58 ((LocInfoE loc_60 (!{LPtr} (LocInfoE loc_61 ("c")))) at{struct_color} "r") <-{ it_layout u8 }
+          LocInfoE loc_62 (use{it_layout u8} (LocInfoE loc_63 ("r"))) ;
+        Return (VOID)
+      ]> $∅
+    )%E
+  |}.
+
+  (* Definition of function [set_green]. *)
+  Definition impl_set_green : function := {|
+    f_args := [
+      ("c", LPtr);
+      ("g", it_layout u8)
+    ];
+    f_local_vars := [
+    ];
+    f_init := "#0";
+    f_code := (
+      <[ "#0" :=
+        locinfo: loc_66 ;
+        LocInfoE loc_67 ((LocInfoE loc_69 (!{LPtr} (LocInfoE loc_70 ("c")))) at{struct_color} "g") <-{ it_layout u8 }
+          LocInfoE loc_71 (use{it_layout u8} (LocInfoE loc_72 ("g"))) ;
+        Return (VOID)
+      ]> $∅
+    )%E
+  |}.
+
+  (* Definition of function [set_blue]. *)
+  Definition impl_set_blue : function := {|
+    f_args := [
+      ("c", LPtr);
+      ("b", it_layout u8)
+    ];
+    f_local_vars := [
+    ];
+    f_init := "#0";
+    f_code := (
+      <[ "#0" :=
+        locinfo: loc_75 ;
+        LocInfoE loc_76 ((LocInfoE loc_78 (!{LPtr} (LocInfoE loc_79 ("c")))) at{struct_color} "b") <-{ it_layout u8 }
+          LocInfoE loc_80 (use{it_layout u8} (LocInfoE loc_81 ("b"))) ;
+        Return (VOID)
+      ]> $∅
+    )%E
+  |}.
+
   (* Definition of function [argtest]. *)
   Definition impl_argtest (global_blue global_getblue : loc): function := {|
     f_args := [
@@ -175,14 +253,14 @@ Section code.
     f_init := "#0";
     f_code := (
       <[ "#0" :=
-        locinfo: loc_62 ;
-        "$0" <- LocInfoE loc_64 (global_blue) with
-          [ LocInfoE loc_65 (UnOp (CastOp $ IntOp u8) (IntOp i32) (LocInfoE loc_65 (i2v 5 i32))) ] ;
-        locinfo: loc_59 ;
-        "$1" <- LocInfoE loc_61 (global_getblue) with
-          [ LocInfoE loc_62 ("$0") ] ;
-        locinfo: loc_57 ;
-        assert: (LocInfoE loc_58 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_58 ((LocInfoE loc_59 ("$1")) ={IntOp u8, IntOp u8} (LocInfoE loc_66 (UnOp (CastOp $ IntOp u8) (IntOp i32) (LocInfoE loc_67 (i2v 5 i32)))))))) ;
+        locinfo: loc_89 ;
+        "$0" <- LocInfoE loc_91 (global_blue) with
+          [ LocInfoE loc_92 (UnOp (CastOp $ IntOp u8) (IntOp i32) (LocInfoE loc_92 (i2v 5 i32))) ] ;
+        locinfo: loc_86 ;
+        "$1" <- LocInfoE loc_88 (global_getblue) with
+          [ LocInfoE loc_89 ("$0") ] ;
+        locinfo: loc_84 ;
+        assert: (LocInfoE loc_85 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_85 ((LocInfoE loc_86 ("$1")) ={IntOp u8, IntOp u8} (LocInfoE loc_93 (UnOp (CastOp $ IntOp u8) (IntOp i32) (LocInfoE loc_94 (i2v 5 i32)))))))) ;
         Return (VOID)
       ]> $∅
     )%E

tutorial/proofs/t06_struct/generated_proof_set_blue.v

+From refinedc.typing Require Import typing.
+From refinedc.tutorial.t06_struct Require Import generated_code.
+From refinedc.tutorial.t06_struct Require Import generated_spec.
+Set Default Proof Using "Type".
+
+(* Generated from [tutorial/t06_struct.c]. *)
+Section proof_set_blue.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Typing proof for [set_blue]. *)
+  Lemma type_set_blue :
+    ⊢ typed_function impl_set_blue type_of_set_blue.
+  Proof.
+    start_function "set_blue" ([[p c] b]) => arg_c arg_b.
+    split_blocks ((
+      ∅
+    )%I : gmap label (iProp Σ)) ((
+      ∅
+    )%I : gmap label (iProp Σ)).
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "set_blue" "#0".
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+    all: print_sidecondition_goal "set_blue".
+  Qed.
+End proof_set_blue.

tutorial/proofs/t06_struct/generated_proof_set_green.v

+From refinedc.typing Require Import typing.
+From refinedc.tutorial.t06_struct Require Import generated_code.
+From refinedc.tutorial.t06_struct Require Import generated_spec.
+Set Default Proof Using "Type".
+
+(* Generated from [tutorial/t06_struct.c]. *)
+Section proof_set_green.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Typing proof for [set_green]. *)
+  Lemma type_set_green :
+    ⊢ typed_function impl_set_green type_of_set_green.
+  Proof.
+    start_function "set_green" ([[p c] g]) => arg_c arg_g.
+    split_blocks ((
+      ∅
+    )%I : gmap label (iProp Σ)) ((
+      ∅
+    )%I : gmap label (iProp Σ)).
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "set_green" "#0".
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+    all: print_sidecondition_goal "set_green".
+  Qed.
+End proof_set_green.

tutorial/proofs/t06_struct/generated_proof_set_red.v

+From refinedc.typing Require Import typing.
+From refinedc.tutorial.t06_struct Require Import generated_code.
+From refinedc.tutorial.t06_struct Require Import generated_spec.
+Set Default Proof Using "Type".
+
+(* Generated from [tutorial/t06_struct.c]. *)
+Section proof_set_red.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Typing proof for [set_red]. *)
+  Lemma type_set_red :
+    ⊢ typed_function impl_set_red type_of_set_red.
+  Proof.
+    start_function "set_red" ([[p c] r]) => arg_c arg_r.
+    split_blocks ((
+      ∅
+    )%I : gmap label (iProp Σ)) ((
+      ∅
+    )%I : gmap label (iProp Σ)).
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "set_red" "#0".
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+    all: print_sidecondition_goal "set_red".
+  Qed.
+End proof_set_red.

tutorial/proofs/t06_struct/generated_spec.v

@@ -85,6 +85,21 @@ Section spec.
     fn(∀ (r, g, b) : nat * nat * nat; (((r, g, b)) @ (color)); True)
       → ∃ () : (), ((b) @ (int (u8))); True.
 
+  (* Specifications for function [set_red]. *)
+  Definition type_of_set_red :=
+    fn(∀ (p, c, r) : loc * (nat * nat * nat) * nat; (p @ (&own (c @ (color)))), (r @ (int (u8))); True)
+      → ∃ () : (), (void); (p ◁ₗ (((r, c.1.2, c.2)) @ (color))).
+
+  (* Specifications for function [set_green]. *)
+  Definition type_of_set_green :=
+    fn(∀ (p, c, g) : loc * (nat * nat * nat) * nat; (p @ (&own (c @ (color)))), (g @ (int (u8))); True)
+      → ∃ () : (), (void); (p ◁ₗ (((c.1.1, g, c.2)) @ (color))).
+
+  (* Specifications for function [set_blue]. *)
+  Definition type_of_set_blue :=
+    fn(∀ (p, c, b) : loc * (nat * nat * nat) * nat; (p @ (&own (c @ (color)))), (b @ (int (u8))); True)
+      → ∃ () : (), (void); (p ◁ₗ (((c.1, b)) @ (color))).
+
   (* Specifications for function [argtest]. *)
   Definition type_of_argtest :=
     fn(∀ () : (); True) → ∃ () : (), (void); ⌜True⌝.

tutorial/proofs/t06_struct/proof_files

@@ -4,3 +4,6 @@ generated_proof_getblue.v
 generated_proof_green.v
 generated_proof_red.v
 generated_proof_rgb.v
+generated_proof_set_blue.v
+generated_proof_set_green.v
+generated_proof_set_red.v

tutorial/t06_struct.c

@@ -49,6 +49,27 @@ uint8_t getblue(struct color b) {
   return b.b;
 }
 
+[[rc::parameters("p : loc", "c : {nat * nat * nat}", "r : nat")]]
+[[rc::args("p @ &own<c @ color>", "r @ int<u8>")]]
+[[rc::ensures("p @ &own<{(r, c.1.2, c.2)} @ color>")]]
+void set_red(struct color *c, uint8_t r){
+  (*c).r = r;
+}
+
+[[rc::parameters("p : loc", "c : {nat * nat * nat}", "g : nat")]]
+[[rc::args("p @ &own<c @ color>", "g @ int<u8>")]]
+[[rc::ensures("p @ &own<{(c.1.1, g, c.2)} @ color>")]]
+void set_green(struct color *c, uint8_t g){
+  (*c).g = g;
+}
+
+[[rc::parameters("p : loc", "c : {nat * nat * nat}", "b : nat")]]
+[[rc::args("p @ &own<c @ color>", "b @ int<u8>")]]
+[[rc::ensures("p @ &own<{(c.1, b)} @ color>")]]
+void set_blue(struct color *c, uint8_t b){
+  (*c).b = b;
+}
+
 [[rc::ensures("True")]]
 void argtest() {
   assert(getblue(blue(5)) == (uint8_t)5);