Commit 05e3c269 authored by Lennard Gäher's avatar Lennard Gäher
Browse files

last upd before changing ltype model

parent bd257222
......@@ -56,3 +56,6 @@
#-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
#
-Q _build/default/rr_frontend/output refinedc.rust_examples.mod
let g:ycm_rust_toolchain_root = '/home/lennard/.rustup/toolchains/refinedrust'
// adapted from Prusti
//
extern crate rustc_driver;
extern crate rustc_errors;
extern crate rustc_interface;
extern crate rustc_middle;
extern crate rustc_hir;
use rustc_hir::{Crate, def_id::DefId, def_id::LocalDefId, itemlikevisit::ItemLikeVisitor, ImplItem, TraitItem};
use rustc_middle::ty::{Ty, TyCtxt};
use rustc_hir as hir;
pub struct CollectFunctionVisitor<'tcx> {
tcx: TyCtxt<'tcx>,
result: Vec<LocalDefId>,
}
impl<'tcx> CollectFunctionVisitor<'tcx> {
pub fn new(tcx: &TyCtxt<'tcx>) -> Self {
CollectFunctionVisitor {
tcx: *tcx,
result: Vec::new(),
}
}
pub fn get_functions(self) -> Vec<LocalDefId> {
self.result
}
}
impl<'tcx> ItemLikeVisitor<'tcx> for CollectFunctionVisitor<'tcx> {
fn visit_item(&mut self, item: &hir::Item) {
let attrs = self.tcx.get_attrs(item.def_id.to_def_id());
if let hir::ItemKind::Fn(..) = item.kind {
let def_id = self.tcx.hir().local_def_id(item.hir_id());
self.result.push(def_id);
}
}
fn visit_trait_item(&mut self, trait_item: &hir::TraitItem) {
return;
}
fn visit_impl_item(&mut self, impl_item: &hir::ImplItem) {
let attrs = self.tcx.get_attrs(impl_item.def_id.to_def_id());
// Skip associated types and other non-methods items
if let hir::ImplItemKind::Fn(..) = impl_item.kind {
// continue
} else {
return;
}
// TODO
//let def_id = self.tcx.hir().local_def_id(impl_item.hir_id()).to_def_id();
//self.result.push(def_id);
}
fn visit_foreign_item(&mut self, _foreign_item: &hir::ForeignItem) {
// Nothing
}
}
......@@ -849,7 +849,7 @@ Proof.
by iApply (wp_call_bind_ind []).
Qed.
Lemma wp_alloc E Φ (l : loc) ly (v : val) :
Lemma wp_alloc E Φ ly (v : val) :
has_layout_val v ly
( l, l v - freeable l (length v) HeapAlloc - l `has_layout_loc` ly - Φ (val_of_loc l)) -
WP (Alloc ly (Val v)) @ E {{ Φ }}.
......
......@@ -142,6 +142,11 @@ Notation "'move{' ot } e" := (Move Na1Ord (UntypedOp ot) e%E) (at level 9, forma
Arguments Move : simpl never.
Typeclasses Opaque Move.
Definition Box (ly : layout) := Alloc ly (Val $ repeat MPoison ly.(ly_size) ).
Notation "'box{' ly '}'" := (Box ly) (at level 9, format "'box{' ly }") : expr_scope.
Arguments Box : simpl never.
Typeclasses Opaque Box.
Inductive location_info :=
| LocationInfo (file : string) (line_start column_start line_end column_end : Z).
......@@ -233,7 +238,7 @@ Example test_get_member (l : loc) (s : struct_layout) ot :
Proof. simpl. reflexivity. Abort.
Definition unit_layout : layout := {| ly_size := 1; ly_align_log := 0 |}.
(*Definition unit_layout : layout := {| ly_size := 1; ly_align_log := 0 |}.*)
Definition ref_layout := void_ptr.
......
......@@ -36,6 +36,7 @@ Inductive expr :=
| StructInit (ly : struct_layout) (fs : list (string * expr))
| MacroE (m : list lang.expr lang.expr) (es : list expr) (wf : MacroWfSubst m)
| Borrow (m : mutability) (κn : string) (e : expr)
| Box (ly : layout)
(* for opaque expressions*)
| Expr (e : lang.expr)
.
......@@ -70,10 +71,11 @@ Lemma expr_ind (P : expr → Prop) :
( (ly : struct_layout) (fs : list (string * expr)), Forall P fs.*2 P (StructInit ly fs))
( (m : list lang.expr lang.expr) (es : list expr) (wf : MacroWfSubst m), Forall P es P (MacroE m es wf))
( (m : mutability) (κn : string) (e : expr), P e P (Borrow m κn e))
( (ly : layout), P (Box ly))
( (e : lang.expr), P (Expr e)) (e : expr), P e.
Proof.
move => *. generalize dependent P => P. match goal with | e : expr |- _ => revert e end.
fix FIX 1. move => [ ^e] => ???????? Hcall Hconcat ??????????????? Hstruct Hmacro Hbor ?.
fix FIX 1. move => [ ^e] => ???????? Hcall Hconcat ??????????????? Hstruct Hmacro Hbor ??.
9: {
apply Hcall; [ |apply Forall_true => ?]; by apply: FIX.
}
......@@ -119,6 +121,7 @@ Fixpoint to_expr (e : expr) : lang.expr :=
| OffsetOfUnion ul m => notation.OffsetOfUnion ul m
| MacroE m es _ => notation.MacroE m (to_expr <$> es)
| Borrow m κn e => notation.Ref m κn (to_expr e)
| Box ly => notation.Box ly
| Expr e => e
end.
......@@ -185,6 +188,7 @@ Ltac of_expr e :=
constr:(IfE ot e1 e2 e3)
| lang.Alloc ?ly ?e =>
let e := of_expr e in constr:(Alloc ly e)
| notation.Box ?ly => constr:(Box ly)
| lang.SkipE ?e =>
let e := of_expr e in constr:(SkipE e)
| lang.StuckE => constr:(StuckE e)
......@@ -293,7 +297,7 @@ Fixpoint find_expr_fill (e : expr) (bind_val : bool) : option (list ectx_item *
if find_expr_fill f bind_val is Some (Ks, e') then
Some (Ks ++ [CallLCtx args], e') else
(* TODO: handle arguments? *) None
| Concat _ | MacroE _ _ _ | OffsetOf _ _ | OffsetOfUnion _ _ | LogicalAnd _ _ _ _ _ | LogicalOr _ _ _ _ _ => None
| Concat _ | MacroE _ _ _ | OffsetOf _ _ | OffsetOfUnion _ _ | LogicalAnd _ _ _ _ _ | LogicalOr _ _ _ _ _ | Box _ => None
| IfE ot e1 e2 e3 =>
if find_expr_fill e1 bind_val is Some (Ks, e') then
Some (Ks ++ [IfECtx ot e2 e3], e') else Some ([], e)
......@@ -395,7 +399,6 @@ Inductive stmt :=
| SkipS (s : stmt)
| StuckS
| ExprS (e : expr) (s : stmt)
| Assert (ot : op_type) (e : expr) (s : stmt)
| AnnotStmt (n : nat) {A} (a : A) (s : stmt)
| LocInfoS (a : location_info) (s : stmt)
......@@ -461,7 +464,7 @@ Ltac of_stmt s :=
let e := of_expr e in
let s := of_stmt s in
constr:(Assert ot e s)
| IfS ?ot ?e ?s1 ?s2 =>
| lang.IfS ?ot ?e ?s1 ?s2 =>
let e := of_expr e in
let s1 := of_stmt s1 in
let s2 := of_stmt s2 in
......@@ -581,6 +584,7 @@ Fixpoint subst_l (xs : list (var_name * val)) (e : expr) : expr :=
| OffsetOfUnion ul m => OffsetOfUnion ul m
| MacroE m es wf => MacroE m (subst_l xs <$> es) wf
| Borrow m κn e => Borrow m κn (subst_l xs e)
| Box ly => Box ly
| Expr e => Expr (lang.subst_l xs e)
end.
......
......@@ -487,6 +487,21 @@ Global Instance simpl_and_lookup_lookup_total {A} (l : list A) (i : nat) `{Inhab
SimplBothRel (=) (l !! i) (Some (l !!! i)) (i < length l).
Proof. rewrite /SimplBothRel list_lookup_alt. naive_solver lia. Qed.
(* TODO: these instances seem broken, typeclass search diverges when it should find them... *)
Global Instance simpl_lookup_insert_map_eq `{Countable K} `{EqDecision K} {V} (m : gmap K V) i j x x' `{!CanSolve (i = j)} :
SimplBothRel (=) (<[i := x']> m !! j) (Some x) (x = x').
Proof.
unfold SimplBothRel, CanSolve in *; subst.
rewrite lookup_insert. naive_solver.
Qed.
Global Instance simpl_lookup_insert_map_neq `{Countable K} `{EqDecision K} {V} (m : gmap K V) i j x x' `{!CanSolve (i j)} :
SimplBothRel (=) (<[i := x']> m !! j) (Some x) (m !! j = Some x).
Proof.
unfold SimplBothRel, CanSolve in *; subst.
rewrite lookup_insert_ne; naive_solver.
Qed.
Global Instance simpl_learn_insert_some_len_impl {A} l i (x : A) :
(* The false is important here as we learn additional information,
but don't want to get stuck in an endless loop. *)
......
......@@ -14,3 +14,6 @@ Inductive endlft_annot : Type :=
Inductive extend_annot : Type :=
ExtendLftAnnot (n : string).
Inductive shortenlft_annot : Type :=
ShortenLftAnnot (sup : list string).
This diff is collapsed.
......@@ -15,13 +15,125 @@ Notation "'HIDDEN'" := (RETURN_MARKER _) (only printing).
(* simplify RETURN_MARKER as soon as it is applied enough in the goal *)
Arguments RETURN_MARKER _ _ _ _ _ /.
(** * Tactics cleaning the proof state *)
Ltac clear_unused_vars :=
repeat match goal with
| H : ?T |- _ =>
(* Keep current location and case distinction info. *)
lazymatch T with
(*| CURRENT_LOCATION _ _ => fail*)
(*| CASE_DISTINCTION_INFO _ _ _ => fail*)
| _ => idtac
end;
let ty := (type of T) in
match ty with | Type => clear H | Set => clear H end
end.
Ltac prepare_sideconditions :=
liUnfoldLetsInContext;
liUnfoldAllEvars;
repeat match goal with | H : BLOCK_PRECOND _ _ |- _ => clear H end;
(* get rid of Q *)
repeat match goal with | H := CODE_MARKER _ |- _ => clear H end;
repeat match goal with | H := RETURN_MARKER _ |- _ => clear H end.
repeat match goal with | H := RETURN_MARKER _ |- _ => clear H end;
clear_unused_vars.
Ltac solve_goal_prepare_tac ::=
prepare_sideconditions.
prepare_sideconditions;
(*repeat match goal with | H : CASE_DISTINCTION_INFO _ _ _ |- _ => clear H end.*)
idtac.
(** * Tactics for showing failures to the user *)
(*Ltac print_current_location :=*)
(*try lazymatch reverse goal with*)
(*| H : CURRENT_LOCATION ?l ?up_to_date |- _ =>*)
(*let rec print_loc_info l :=*)
(*match l with*)
(*| ?i :: ?l =>*)
(*lazymatch eval unfold i in i with*)
(*| LocationInfo ?f ?ls ?cs ?le ?ce =>*)
(*let f := eval unfold f in f in*)
(*idtac "Location:" f "[" ls ":" cs "-" le ":" ce "]";*)
(*print_loc_info l*)
(*end*)
(*| [] => idtac "up to date:" up_to_date*)
(*end in*)
(*print_loc_info l;*)
(*clear H*)
(*end.*)
(*Ltac print_case_distinction_info :=*)
(*repeat lazymatch reverse goal with*)
(*| H : CASE_DISTINCTION_INFO ?hint ?i ?l |- _ =>*)
(*lazymatch i with*)
(*| (?a, ?b) => idtac "Case distinction" a "->" b*)
(*| ?a => idtac "Case distinction" a*)
(*end;*)
(*lazymatch l with*)
(*| ?i :: ?l =>*)
(*lazymatch eval unfold i in i with*)
(*| LocationInfo ?f ?ls ?cs ?le ?ce =>*)
(*let f := eval unfold f in f in*)
(*idtac "at" f "[" ls ":" cs "-" le ":" ce "]"*)
(*end*)
(*| [] => idtac*)
(*end;*)
(*clear H*)
(*end.*)
Ltac print_coq_hyps :=
try match reverse goal with
| H : ?X |- _ =>
lazymatch X with
| BLOCK_PRECOND _ _ => fail
| gFunctors => fail
| typeGS _ => fail
| ghost_varG _ _ => fail
(*| globalGS _ => fail*)
| _ => idtac H ":" X; fail
end
end.
Ltac print_goal :=
(*print_current_location;*)
(*print_case_distinction_info;*)
idtac "Goal:";
print_coq_hyps;
idtac "---------------------------------------";
match goal with
| |- ?G => idtac G
end;
idtac "";
idtac "".
Ltac print_typesystem_goal fn block :=
lazymatch goal with
| |- ?P ?Q =>
idtac "Cannot instantiate evar in" fn "in block" block "!";
(*print_current_location;*)
(*print_case_distinction_info;*)
idtac "Goal:";
print_coq_hyps;
idtac "---------------------------------------";
idtac P;
(* TODO: Should we print the continuation? It might confuse the user and
it usually is not helpful. *)
(* idtac ""; *)
(* idtac "Continuation:"; *)
(* idtac Q; *)
idtac "";
idtac "";
admit
| |- _ =>
idtac "Type system got stuck in function" fn "in block" block "!";
print_goal; admit
end.
Ltac print_sidecondition_goal fn :=
idtac "Cannot solve side condition in function" fn "!";
print_goal; admit.
Ltac print_remaining_shelved_goal fn :=
idtac "Shelved goal remaining in " fn "!";
print_goal; admit.
......@@ -142,3 +142,42 @@ Export pinned_borrows.
Notation "'&pin{' κ } [ P ] Q" := (pinned_bor κ P Q) (at level 40) : bi_scope.
Notation "'&pin{' κ } P" := (pinned_bor κ P P) (at level 40) : bi_scope.
(* TODO upstream ? *)
From iris.bi Require Import fractional.
From Coq Require Import QArith Qcanon.
Program Definition Qp_total_sub (p q : Qp) : (q < p)%Qp Qp :=
match p, q with
| mk_Qp p Hp, mk_Qp q Hq =>
λ (Hle : (mk_Qp q Hq < mk_Qp p Hp)%Qp),
let pq := (p - q)%Qc in (mk_Qp pq _)
end.
Next Obligation.
rewrite -Qclt_minus_iff. apply Hle.
Qed.
Lemma Qp_total_sub_eq (q p : Qp) Hlt :
(Qp_total_sub p q Hlt + q)%Qp = p.
Proof.
destruct p as [p ], q as [q ].
simpl. unfold Qp_add.
match goal with
| |- mk_Qp ?a ?pr = _ => generalize pr as prf; assert (a = p) as Heq by ring
end.
revert Heq. generalize (p - q + q).
intros ? -> ?. f_equal. apply proof_irrel.
Qed.
Lemma fractional_le {Σ} (Φ : Qp iProp Σ) `{Fractional _ Φ} (q q' : Qp):
(q' q)%Qp
Φ q -
Φ q' (Φ q' - Φ q).
Proof.
iIntros (Hle) "HΦ".
destruct (decide (q = q')) as [<- | ?].
{ eauto with iFrame. }
assert (q' < q)%Qp as Hlt.
{ apply Qp_le_lteq in Hle as [ | ]; done. }
specialize (Qp_total_sub_eq q' q Hlt) as <-.
iPoseProof (fractional with "HΦ") as "[H1 $]".
iIntros "H2". iApply fractional; iFrame.
Qed.
......@@ -8,6 +8,14 @@ From refinedc.rust_typing Require Export ghost_var_dfrac gvar_refinement.
They fully own their memory, and thus allow deallocation (in their drop implementation).
TODO: actually have drop impls for types.
*)
(* NOTE:
this is not an accurate model of Rust's box type.
(Rust's actual box is a struct with two fields: a Unique and an Allocator)
We can instead use this as a simplified model for now,
as long as we don't actually strive to verify Rust's actual Box implementation.
*)
Section box.
Context `{typeGS Σ} {rt} (inner : type rt).
......
......@@ -33,9 +33,19 @@ fn foobo(abc: u32) -> i32 {
*)
Context `{ghost_varG Σ Z} `{ghost_varG Σ unit} `{ghost_varG Σ bool}.
Definition type_of_foo :=
fn( (n, b) : (Z * bool), (λ ϝ, []); n @ (int i32); (True - True) (False))
(x) : (Z), x @ int i32; ( (x > n)%Z ).
Definition type_of_foo' :=
fn( (n, b) : (Z * bool), (λ ϝ, []); n @ int i32, b @ boolean i8; (True - True) (False))
(x) : (Z), x @ int i32; ( (x > n)%Z ).
Definition foobo : function := {|
f_args := [
("abc", it_layout u32)
("abc", it_layout i32)
];
f_local_vars := [
("__0", it_layout i32)
......@@ -43,47 +53,23 @@ Definition foobo : function := {|
f_code :=
<["_bb0" :=
"__0" <-{ IntOp i32 } i2v (42) i32;
annot: (StartLftAnnot "κ" []);
annot: (EndLftAnnot "κ");
Return (use{ IntOp i32 } ("__0"))
]>%E $
;
f_init := "_bb0";
|}.
Lemma foobo_typed `{ghost_varG Σ (place_rfn unit)} `{ghost_varG Σ Z} π :
typed_function π foobo (fn( n : Z, (λ f, []); n @ (int i32); True) () : unit, 42 @ (int i32) ; True).
Lemma foobo_typed `{ghost_varG Σ unit} `{ghost_varG Σ Z} π :
typed_function π foobo (fn( (n, κ) : (Z * lft), (λ f, []); n @ (int i32); True) () : unit, 42 @ (int i32) ; True).
Proof.
iStartProof.
start_function "foobo" ( n ).
do 30 liRStep. liShow.
iApply type_write_strong.
simpl.
repeat liRStep. liShow.
unshelve iApply type_write_own_copy.
done.
repeat liRStep. liShow.
iApply place_strong.
iApply place_id.
iExists (int i32).
iSplitR. { done.}
repeat liRStep. liShow.
Abort.
Definition foobo' : function := {|
f_args := [
("abc", it_layout u32)
];
f_local_vars := [
("__0", it_layout i32)
];
f_code :=
<["_bb0" :=
"abc" <-{ IntOp i32 } i2v (42) i32;
Return (use{ IntOp i32 } ("__0"))
]>%E $
;
f_init := "_bb0";
|}.
start_function "foobo" ( (n & κ) ) => arg_n local_0.
intros.
init_lfts (<[ "κ" := κ]> ).
repeat liRStep.
Qed.
(** Example *)
(*
......@@ -101,7 +87,6 @@ Definition bar : function := {|
];
f_local_vars := [
(* name specially.
are there ways to make MIR temporaries nicer?
*)
("__0", it_layout i32);
......@@ -122,25 +107,41 @@ Definition bar : function := {|
f_init := "_bb0";
|}.
(* copy Prusti code for Polonius ? / reuse that *)
(* talk to people about sharing Rust code for interfacing rustc
*)
Lemma bar_typed `{ghost_varG Σ (place_rfn unit)} `{ghost_varG Σ (place_rfn Z)} `{ghost_varG Σ ((place_rfn Z) * gname)} π :
Lemma bar_typed `{ghost_varG Σ (unit)} `{ghost_varG Σ Z} `{ghost_varG Σ (place_rfn Z)} `{ghost_varG Σ ((place_rfn Z) * gname)} π :
typed_function π bar (fn( (κ, n, γ) : lft * Z * gname, (λ f, []); (PlaceIn n, γ) @ (mut_ref (place_wrap $ int i32) κ); True) () : unit, n @ (int i32); gvar_obs γ (PlaceIn n)).
Proof.
iStartProof.
start_function "bar" ([[κ n] γ] ).
intros.
iPoseProof (named_lfts_init (<[ "κ" := κ]> )) as "Ha".
init_lfts (<[ "κ0" := κ]> ).
repeat liRStep.
liShow.
(* problem: x1 does not have a place_wrap at the right point, so we can't actually do a borrow.. *)
(*
how do we in general enforce that we get a place wrap at the right place?
when do we need to generate the wrapping?
- essentially only when we write to a place. then we should wrap the written thing.
(that way, when writing, we don't need to descend below the place_wrap, but just overwrite it if there's a strong update)
-> when processing typed_place, we always take the place_wrap together with the type directly contained in it (also matches with the fact that descending below the place_wrap does not correspond to a wp step)
-
How can we potentially handle this?
- it cannot be accomodated by the subtype thing: weak_subtype is aimed at solving goals without evars (solving a solid constraint).
in contrast, here we need to force a less rigid constraint.
- subtype can be used as the underlying machinery, but not as the core typing judgment for this.
-> Subtype needs to be extended with rules for place_wrap: if the LHS already contains a place_wrap, then subtyping forces us to also put it on the RHS.
-> the point where explicit new wrapping is mostly relevant is for writing with strong writing rules, because there we do not have the structure of the LHS type to guide us and enforce wrapping.
wrap_type judgment: takes as input a type + refinement (+
*)
iApply type_write_own_copy.
repeat liRStep.
liShow.
Unshelve.
Abort.
......
......@@ -6,133 +6,211 @@ From iris.proofmode Require Import coq_tactics reduction string_ident.
Section test.
Arguments ltype_own : simpl never.
Context `{typeGS Σ} `{ghost_varG Σ Z} `{ghost_varG Σ ()}.
Context `{typeGS Σ} `{ghost_varG Σ Z} `{ghost_varG Σ (place_rfn Z)} `{ghost_varG Σ ()}.
Lemma subsume_test l π :
Lemma subsume_test l π :
l ◁ₗ[π, Owned false] 42 @ ( int i32) -
(l ◁ₗ[π, Owned false] () @ uninit i32) True.
(l ◁ₗ[π, Owned false] () @ uninit i32) True.
Proof.
iStartProof.
repeat liRStep.
Qed.
Lemma gvar_test γ (z : Z):
gvar_pobs γ z -
Lemma gvar_test γ (z : Z):
gvar_pobs γ z -
gvar_pobs γ z True.
Proof.
iStartProof.
iStartProof.
repeat liRStep; liShow.
Qed.