Commit d9f66ee0 authored by Michael Sammler's avatar Michael Sammler
Browse files

add lithium tutorial

parent 66af9445
Pipeline #53499 passed with stage
in 36 minutes and 49 seconds
......@@ -55,3 +55,4 @@
-Q _build/default/linux/casestudies/proofs/page_alloc_find_buddy refinedc.linux.casestudies.page_alloc_find_buddy
-Q _build/default/examples/proofs/pointers refinedc.examples.pointers
-Q _build/default/linux/casestudies/proofs/pgtable refinedc.linux.casestudies.pgtable
-Q _build/default/tutorial/proofs/lithium refinedc.tutorial.lithium
#include <stddef.h>
#include <stdbool.h>
#include <refinedc.h>
/**
Please look at proofs/lithium/lithium.v for the tutorial.
*/
//@rc::import lithium from refinedc.tutorial.lithium (for proofs only)
[[rc::parameters("n : Z")]]
[[rc::args("{n <> 0} @ optional<&own<n @ int<i32>>, null>")]]
[[rc::returns("n @ int<i32>")]]
[[rc::manual_proof("refinedc.tutorial.lithium:lithium, type_lithium_test")]]
int lithium_test(int *a) {
if (a != NULL) {
return *a + 0;
} else {
return 0;
}
}
From refinedc.typing Require Import typing.
From refinedc.tutorial.lithium Require Import generated_code.
From refinedc.tutorial.lithium Require Import generated_spec.
From refinedc.lang Require Import builtins_specs.
Set Default Proof Using "Type".
(** This file contains a tutorial for Lithium, the underlying proof
automation of RefinedC. See also Section 5 of the RefinedC paper. *)
Section lithium.
Context `{!typeG Σ}.
(*** Proof search in Lithium *)
(** Lithium is a logic programming language for separation logic for
goals G given by the following grammar:
Atom A ::= l ◁ₗ ty | v ◁ᵥ ty | ...
Basic goal F ::= subsume A1 A2 G | ...
Goal G ::= True | H ∗ G | H -∗ G | G1 ∧ G2 | ∀ x, G(x) | ∃ x, G(x)
Left goal H ::= ⌜φ⌝ | A | H ∗ H | ∃ x, H(x)
We explain the different constructs of this grammar on the following example:
*)
Lemma lithium_example P Q v:
P -
(Q n, v ◁ᵥ n @ int i32 n > 0) -
(P Q) n, v ◁ᵥ n @ int i32 n 0 (
n', n' = n - v ◁ᵥ n' @ int i32 -
(v ◁ᵥ n' @ int i32 True) (v ◁ᵥ n @ int i32 True)
).
Proof.
iStartProof.
(** First, it is easy to check that this separation logic
assertion fits into the grammar G. So let's run the Lithium
interpreter on it! The interpreter is implemented as a Coq tactic
liRStep which does a single step. So we can run it to the end with
[repeat liRStep]. For performance reasons, the interpreter
introduces some let-bindings, which we unfold via [liShow] to make
the goal readable. *)
(** (Note: Technically, the actually Lithium interpreter is given
by liStep. liRStep is a extended version of Lithium for the basic
goals RefinedC. We ignore this distinction in this tutorial and
just use liRStep. ) *)
repeat liRStep; liShow.
(** Lithium was able to solve this goal automatically (ignoring
the shelved subgoal that we will come back to later)! *)
Abort.
(** Let's revert this and go over how Lithium solves this goal. *)
Lemma lithium_example P Q v:
P -
(Q n, v ◁ᵥ n @ int i32 n > 0) -
(P Q) n, v ◁ᵥ n @ int i32 n 0 (
n', n' = n - v ◁ᵥ n' @ int i32 -
(v ◁ᵥ n' @ int i32 True) (v ◁ᵥ n @ int i32 True)
).
Proof.
iStartProof.
(** At the high-level, the implementation of the Lithium
interpreter is quite simple: It simply looks at the top-level
connective of the goal and applies the corresponding introduction
rule.
In particular, for the first step, the top-level connective is a
wand -∗ where the left hand side is an atom. Lithium treats all
assertions on the left hand side of wand and start that are not
syntactically left goals as atoms. Atoms are treated as opaque by
Lithium, but can be manipulated via rules for basic goals as we
will see later.
To introduce this wand, Lithium introduces P into the context. (case 7.d.
in Section 5 of the RefinedC paper) *)
liRStep; liShow.
(** Now the goal is a wand where the left hand side is a
separating conjunction. Here, Lithium splits the separating
conjunction. (7.a. in the RefinedC paper) *)
liRStep; liShow.
(** Now Lithium introduces Q like P above. *)
liRStep; liShow.
(** Now we have an existential quantifier on the left hand side of
a wand. Lithium introduces this quantifier as well, adding n
to the context. (7.b. in the RefinedC paper) *)
liRStep; liShow.
(** Splitting separating conjunction again. *)
liRStep; liShow.
(** Introducing atom again. *)
liRStep; liShow.
(** Now the goal is a wand with a pure proposition on the
left-hand side. The interpreter introduces this proposition into
the Coq context (7.c. in the RefinedC paper). This introduction
happens in two steps for technical reasons. *)
liRStep; liShow.
liRStep; liShow.
(** We are done with the wand. Now the top-level connective of the
goal is a separating conjunction.
Like for the wand, we look at the left hand side of the separating
conjunction. Here it is another separating conjunction. The
interpreter reassociates it such that it can analyze a smaller
formula. (6.a. in the RefinedC paper) *)
liRStep; liShow.
(** Now the left hand side of the separating conjunction is an
atom and the same atom appears in the context. In this case,
Lithium cancels the two atoms. *)
liRStep; liShow.
(** Same for Q *)
liRStep; liShow.
(** Now the top-level connective is an existential quantifier. The
interpreter instantiates it with an evar [protected Hevar]. (4. in
the RefinedC paper. For details of the handling of evars in
RefinedC, see t02_evars.c.) *)
liRStep; liShow.
(** Now the goal is a separating conjunction where the left hand
side is an atom that does not directly appear in the context. In
this case, Lithium searches for a "related" assertion in the
context. In this case, it finds the type assignment [v ◁ᵥ ...] in
the context since type assignments for the same value (and
location) are related. After finding such a type assignment, one
needs to prove a subsumption between the two atoms. This is
encoded via the subsumption judgment [subsume A1 A2 G] which is
defined as [A1 -∗ (A2 ∗ G)]. (6.d in the RefinedC paper) *)
liRStep; liShow.
(** The subsumption judgment is a basic goal F. These goals are
solved by applying a user-defined rule that transforms the basic
goal into a new Lithium goal (5. in the RefinedC paper).
Here, Lithium finds the following rule:
⌜x = y⌝ ∗ G
------------------------------------∗
subsume (v ◁ᵥ x @ ty) (v ◁ᵥ y @ ty) G
*)
(** We make make happens clearer by introducing a let-binding for the continuation: *)
set G := (X in (subsume _ _ X)).
liRStep; liShow.
rewrite {}/G.
(** Now the top-level connective of the goal is a separating
conjunction where the left hand side is a pure sidecondition that
contains an evar. Lithium solves this sidecondition via
unification and instantiates the evar (see t02_evars.c for
details). Similar to the wand, this happens in two steps. *)
liRStep; liShow.
liRStep; liShow.
(** Now we have a pure sidecondition without evars. Such
sideconditions are shelved to be solved later. (6.c. in the
RefinedC paper) *)
liRStep; liShow.
liRStep; liShow.
(** Next, we have an universal quantifier at the top-level.
Lithium introduces it. (3. in the RefinedC paper) *)
liRStep; liShow.
(** Now the top-level connective is again a magic wand with a pure
sidecondition on the left-hand side. Lithium introduces it and
directly substitutes the equality. *)
liRStep; liShow.
liRStep; liShow.
(** Introducing an atom into the context. *)
liRStep; liShow.
(** Now the top-level connective is a non-separating conjunction
∧. Lithium introduces it by splitting the proof into two subgoals.
Note that ∧ allows to keep the same (Iris) context in both subgoals. *)
liRStep; liShow.
(** The second goal is the same as the first so we just look at the first. *)
2: repeat liRStep; liShow.
(** Cancel atoms. *)
liRStep; liShow.
(** Now the top-level connective is True. This is solved trivially
by Lithium and we are done with the separation logic part of this proof! *)
liRStep; liShow.
(** As a last step, we need to solve the pure sideconditions that were
shelved during the separation logic proof. We first unshelve them all follows: *)
Unshelve. all: li_unshelve_sidecond.
(** Now we can solve this sidecondition with lia. *)
lia.
Qed.
(*** Adding rules for basic goals *)
(** The previous discussion showed Lithium automates separation
logic reasoning. We have also seen that this proof search relies on
user-defined rules for handling basic goals. Let's have a closer
look how such rules can be defined. In particular, we will define a
subsumption rule for a custom integer type [myint]. *)
Axiom myint : Z type.
(** Let's try to solve the following goal using Lithium: *)
Lemma myint_example l:
l ◁ₗ myint 5 - n', l ◁ₗ myint n' 0 < n' True.
Proof.
iStartProof.
repeat liRStep; liShow.
(** The Lithium automation gets stuck when trying to prove a
subsumption between two type assignments of myint since there is
no applicable rule. So let's add a rule to solve this problem. *)
Abort.
(** First, we prove a lemma [subsume_myint] of the form [G -∗ F]
where [F] is the basic goal we want to prove (here a subsumption
between myint) and [G] is the Lithium goal that the subsumption
should be transformed into (here we reduce proving the subsumption
to proving equality between the numbers). *)
Lemma subsume_myint l n n' G:
n = n' G -
subsume (l ◁ₗ myint n) (l ◁ₗ myint n') G.
Proof. iIntros "[-> HG]". iIntros "Hl". by iFrame. Qed.
(** The [subsume_myint] needs to be registered with the Lithium
automation, which we do as follows: *)
Global Instance subsume_myint_inst l n n' :
Subsume (l ◁ₗ myint n) (l ◁ₗ myint n') :=
λ G, i2p (subsume_myint l n n' G).
(** Now we are ready to try again: *)
Lemma myint_example l:
l ◁ₗ myint 5 - n', l ◁ₗ myint n' 0 < n' True.
Proof.
iStartProof.
repeat liRStep; liShow.
(** Success! Lithium now automatically solves this goal. *)
Qed.
(*** More complicated subsumption rules *)
(** We have seen a custom rule for a basic goal, but its premise was
quite simple and did not really exploit the fact that one can use
the full grammar of goals for the premise of rules for basic goals.
Thus, let's look at a more interesting subsumption rule. *)
(** For this subsumption rule, we assume an array type [myarray]
that is parametrized by a list of types, representing the types of
the array members. *)
Axiom myarray : list type type.
(** We also assume that we can extract an member of the array and
replace it with another type. (This is similar to [big_sepL_insert_acc]). *)
Axiom myarray_access : tys (i : nat) ty l,
tys !! i = Some ty
l ◁ₗ myarray tys -
(l + i) ◁ₗ ty ( ty', (l + i) ◁ₗ ty' - l ◁ₗ myarray (<[i := ty']>tys)).
(** Now we can look at the goal we want to prove: *)
Lemma my_array_example l i l' tys n:
(** Assuming we have ownership of an array with types tys at
location l where the ownership of element i has been taken out
(the type [place l'] asserts that it is stored at location l, but
it does not contain any ownership), *)
l ◁ₗ myarray (<[i := place l']> tys) -
(** Also assuming that we know that we l' has type [n @ int i32], *)
l' ◁ₗ n @ int i32 -
(** And assuming that the type at index i in tys is indeed [n @ int i32] *)
tys !! i = Some (n @ int i32) -
(** we can recombine the ownership of l and l' to conclude that l
has type [myarray tys]. *)
l ◁ₗ myarray tys True.
Proof.
iStartProof.
repeat liRStep; liShow.
(** However, Lithium does not know how to recombine this ownership
and gets stuck on the subsumption rule between the two myarray. So
we need to help Lithium by defining a suitable subsumption rule. *)
Abort.
(** To prove this subsumption, we reduce it to the following Lithium goal: *)
Lemma subsume_myarray l ty (i : nat) tys G:
(
(** First, one has to prove that i actually is in the range of the list *)
i < length tys%nat (
(** Then, one can assume that the location at the offset i has type ty *)
(l + i) ◁ₗ ty -
(** Then, one gets a type ty' ... *)
ty',
(** ... which is the type at index i of tys *)
tys !! i = Some ty' -
(** Finally, one has to prove that (l +ₗ i) has type ty' *)
(l + i) ◁ₗ ty'
(** and the continuation G. *)
G)
)
-
subsume (l ◁ₗ myarray (<[i:=ty]> tys)) (l ◁ₗ myarray tys) G.
Proof.
(** This lemma is easy to prove using myarray_access. *)
iIntros "[%Hlt HG] Harray".
iDestruct (myarray_access with "Harray") as "[Hl Harray]". { by apply: list_lookup_insert. }
move: Hlt => /lookup_lt_is_Some [ty' ?].
iDestruct ("HG" with "Hl [//]") as "[Hl $]".
iDestruct ("Harray" with "Hl") as "Harray".
by rewrite list_insert_insert list_insert_id.
Qed.
(** Again we register this rule. *)
Global Instance subsume_myarray_inst l ty (i : nat) tys :
Subsume (l ◁ₗ myarray (<[i:=ty]> tys)) (l ◁ₗ myarray tys) :=
λ G, i2p (subsume_myarray l ty i tys G).
Lemma my_array_example l i l' tys n:
tys !! i = Some (n @ int i32) -
l' ◁ₗ (n @ int i32) -
l ◁ₗ myarray (<[i := place l']> tys) -
l ◁ₗ myarray tys True.
Proof.
iStartProof.
repeat liRStep; liShow.
(** Success! Lithium can automatically solve this goal now. *)
Qed.
(*** Exercises *)
(** 1. Write some other goals that fall in the grammar of goals and run
the Lithium interpreter on it until you have an intuition how
Lithium works.
2. Why can Lithium not solve the goal [P -∗ P]? How should it be
modified such that Lithium can solve it?
3. Try defining your own subsumption rules.
*)
End lithium.
(* Generated from [tutorial/lithium.c]. *)
Section proof_lithium_test.
Context `{!typeG Σ} `{!globalG Σ}.
(* Typing proof for [lithium_test]. *)
Lemma type_lithium_test :
typed_function impl_lithium_test type_of_lithium_test.
Proof.
(** Boiler plate code at the start of a function, ignore this. *)
Open Scope printing_sugar.
start_function "lithium_test" (n) => arg_a.
(** The following tactic gives the loop invariants for this
function. In this case, there are none since the function does not
contain loops. *)
split_blocks ((
)%I : gmap label (iProp Σ)) ((
)%I : gmap label (iProp Σ)).
- (** We remove the location information for this proof to make
the code more readable. *)
unfold LocInfo in *.
(** Now we can start the actual proof. We already have the
ownership of the argument a in the context. *)
(** First, we need to prove [typed_stmt (Goto "#0")], which is a
basic goal that says that the the statement (Goto "#0") is
well-typed. The corresponding rule replaces the goto with the
statement of this block from the control-flow graph. *)
liRStep; liShow.
(** Now we need to show that the first if-statement is well-typed.
For this, we first apply the structural rule [type_if], which says that to
type-check an if, we first need to type-check the condition and
then prove the specialized [typed_if] judgement. *)
liRStep; liShow.
(** We know see the another kind of basic goal: [typed_val_expr e G].
It expresses, that the expression [e] is well-typed and it infers a type
(and value) for this expression, which is passed to the continuation G.
Here we need to type-check the != between the argument a and NULL
Again, we apply a structural rule [type_bin_op]. Here, we
first need to type-check the arguments and then prove a
[typed_bin_op] for the types inferred for the arguments. *)
liRStep; liShow.
(** Let's skip over the type-checking of arguments. *)
do 18 liRStep; liShow.
(** Now we have inferred the types of the two sides of the !=
and can apply a rule for type-checking comparison between
optional and NULL. This is the first rule that results in an
interesting goal. *)
liRStep; liShow.
(** The rule spawn three subgoals (all separated by ∧): *)
liRStep; liShow.
(** First, we need to check that the pointer we are comparing
with NULL is in bounds of its allocation. This is a technical
detail of C and we skip over this proof. *)
{ repeat liRStep; liShow. }
liRStep; liShow.
(** We also skip the last subgoal that corresponds to the else branch. *)
2: { repeat liRStep; liShow. }
(** We are now considering the case where the optional is not
NULL (i.e. the then branch). Our goal is destruct_hint, which is
a special instruction to Lithium that records the current branch
in the context such that it can be displayed when showing error
messages. It does not have an effect on the goal. *)
liRStep; liShow.
(** In this branch we can assume that [n ≠ 0]... *)
liRStep; liShow.
liRStep; liShow.
(** and we know that the value stored in a is actually an owned
pointer.
A refinement type (lie &own) without explicit refinement
contains an implicit existential quantifier for the refinement.
This quantifier is destructed automatically before introducing
such a type into the context. This works via the SimplifyHyp
typeclass, where one can register rules that should be used to
simplify hypothesis. *)
liRStep; liShow.
liRStep; liShow.
(** There is another SimplifyHyp rule for the value type
assignment of owned pointers that simplifies it to a location
type assignment. *)
liRStep; liShow.
liRStep; liShow.
liRStep; liShow.
liRStep; liShow.
(** Now we need to prove a if on a boolean. Since the boolean is
true, this rule automatically simplifies the goal to type-checking the
first branch. *)
liRStep; liShow.
liRStep; liShow.
(** We go to the body of the then branch. *)
liRStep; liShow.
(** Here we need to type-check the return. *)
liRStep; liShow.
(** For this we need to type-check the addition. *)
liRStep; liShow.
(** We skip over type-checking of the arguments to + *)
do 41 liRStep; liShow.
(** Now Lithium applies the typing rule for + *)
liRStep; liShow.
(** The rest of the proof is straightforward. *)
repeat liRStep; liShow.
all: print_typesystem_goal "lithium_test" "#0".
Unshelve. all: li_unshelve_sidecond; sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
all: print_sidecondition_goal "lithium_test".
Unshelve. all: try done; try apply: inhabitant; print_remaining_shelved_goal "lithium_test".
Qed.
End proof_lithium_test.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment