Commit 9fc45564 authored by Lennard Gäher's avatar Lennard Gäher
Browse files

bump

parent 825e5099
......@@ -4,52 +4,52 @@
# Cannot use non-canonical projections as it causes massive unification failures
# (https://github.com/coq/coq/issues/6294).
-arg -w -arg -redundant-canonical-projection
-Q _build/default/examples/proofs/spinlock refinedc.examples.spinlock
-Q _build/default/examples/proofs/mpool_simpl refinedc.examples.mpool_simpl
-Q _build/default/examples/proofs/mpool refinedc.examples.mpool
-Q _build/default/examples/proofs/malloc1 refinedc.examples.malloc1
-Q _build/default/examples/proofs/mutable_map refinedc.examples.mutable_map
-Q _build/default/examples/proofs/latch refinedc.examples.latch
-Q _build/default/examples/proofs/simple_union refinedc.examples.simple_union
-Q _build/default/examples/proofs/queue refinedc.examples.queue
-Q _build/default/examples/proofs/reverse refinedc.examples.reverse
-Q _build/default/examples/proofs/btree refinedc.examples.btree
-Q _build/default/examples/proofs/lock refinedc.examples.lock
-Q _build/default/examples/proofs/flags refinedc.examples.flags
-Q _build/default/examples/proofs/shift refinedc.examples.shift
-Q _build/default/tutorial/proofs/binary_search_defs refinedc.tutorial.binary_search_defs
-Q _build/default/tutorial/proofs/t00_intro refinedc.tutorial.t00_intro
-Q _build/default/tutorial/proofs/t01_basic refinedc.tutorial.t01_basic
-Q _build/default/tutorial/proofs/t02_pointers refinedc.tutorial.t02_pointers
-Q _build/default/tutorial/proofs/t03_list refinedc.tutorial.t03_list
-Q _build/default/tutorial/proofs/t04_alloc refinedc.tutorial.t04_alloc
-Q _build/default/tutorial/proofs/t05_main refinedc.tutorial.t05_main
-Q _build/default/tutorial/proofs/t06_struct refinedc.tutorial.t06_struct
-Q _build/default/tutorial/proofs/t07_arrays refinedc.tutorial.t07_arrays
-Q _build/default/tutorial/proofs/t08_tree refinedc.tutorial.t08_tree
-Q _build/default/tutorial/proofs/t09_switch refinedc.tutorial.t09_switch
-Q _build/default/tutorial/proofs/t10_loops refinedc.tutorial.t10_loops
-Q _build/default/tutorial/proofs/t11_tree_set refinedc.tutorial.t11_tree_set
-Q _build/default/tutorial/adequacy refinedc.tutorial.adequacy
-Q _build/default/tutorial/proofs/quicksort_solution refinedc.tutorial.quicksort_solution
-Q _build/default/tutorial/proofs/quicksort_exercise refinedc.tutorial.quicksort_exercise
-Q _build/default/examples/proofs/binary_search refinedc.examples.binary_search
-Q _build/default/examples/proofs/paper_example_2_1 refinedc.examples.paper_example_2_1
-Q _build/default/examples/proofs/paper_example_2_2 refinedc.examples.paper_example_2_2
-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
-Q _build/default/examples/proofs/intptr refinedc.examples.intptr
-Q _build/default/examples/proofs/tests refinedc.examples.tests
-Q _build/default/linux/casestudies/proofs/page_alloc refinedc.linux.casestudies.page_alloc
-Q _build/default/linux/pkvm/proofs/spinlock refinedc.linux.pkvm.spinlock
-Q _build/default/linux/pkvm/proofs/early_alloc refinedc.linux.pkvm.early_alloc
-Q _build/default/linux/proofs/early_alloc_simplified refinedc.linux.early_alloc_simplified
-Q _build/default/linux/casestudies/proofs/early_alloc refinedc.linux.casestudies.early_alloc
-Q _build/default/examples/proofs/quick_sort refinedc.examples.quick_sort
-Q _build/default/examples/proofs/tagged_ptr refinedc.examples.tagged_ptr
-Q _build/default/examples/proofs/ocaml_runtime refinedc.examples.ocaml_runtime
-Q _build/default/linux/casestudies/proofs/page_alloc_find_buddy refinedc.linux.casestudies.page_alloc_find_buddy
#-Q _build/default/examples/proofs/spinlock refinedc.examples.spinlock
#-Q _build/default/examples/proofs/mpool_simpl refinedc.examples.mpool_simpl
#-Q _build/default/examples/proofs/mpool refinedc.examples.mpool
#-Q _build/default/examples/proofs/malloc1 refinedc.examples.malloc1
#-Q _build/default/examples/proofs/mutable_map refinedc.examples.mutable_map
#-Q _build/default/examples/proofs/latch refinedc.examples.latch
#-Q _build/default/examples/proofs/simple_union refinedc.examples.simple_union
#-Q _build/default/examples/proofs/queue refinedc.examples.queue
#-Q _build/default/examples/proofs/reverse refinedc.examples.reverse
#-Q _build/default/examples/proofs/btree refinedc.examples.btree
#-Q _build/default/examples/proofs/lock refinedc.examples.lock
#-Q _build/default/examples/proofs/flags refinedc.examples.flags
#-Q _build/default/examples/proofs/shift refinedc.examples.shift
#-Q _build/default/tutorial/proofs/binary_search_defs refinedc.tutorial.binary_search_defs
#-Q _build/default/tutorial/proofs/t00_intro refinedc.tutorial.t00_intro
#-Q _build/default/tutorial/proofs/t01_basic refinedc.tutorial.t01_basic
#-Q _build/default/tutorial/proofs/t02_pointers refinedc.tutorial.t02_pointers
#-Q _build/default/tutorial/proofs/t03_list refinedc.tutorial.t03_list
#-Q _build/default/tutorial/proofs/t04_alloc refinedc.tutorial.t04_alloc
#-Q _build/default/tutorial/proofs/t05_main refinedc.tutorial.t05_main
#-Q _build/default/tutorial/proofs/t06_struct refinedc.tutorial.t06_struct
#-Q _build/default/tutorial/proofs/t07_arrays refinedc.tutorial.t07_arrays
#-Q _build/default/tutorial/proofs/t08_tree refinedc.tutorial.t08_tree
#-Q _build/default/tutorial/proofs/t09_switch refinedc.tutorial.t09_switch
#-Q _build/default/tutorial/proofs/t10_loops refinedc.tutorial.t10_loops
#-Q _build/default/tutorial/proofs/t11_tree_set refinedc.tutorial.t11_tree_set
#-Q _build/default/tutorial/adequacy refinedc.tutorial.adequacy
#-Q _build/default/tutorial/proofs/quicksort_solution refinedc.tutorial.quicksort_solution
#-Q _build/default/tutorial/proofs/quicksort_exercise refinedc.tutorial.quicksort_exercise
#-Q _build/default/examples/proofs/binary_search refinedc.examples.binary_search
#-Q _build/default/examples/proofs/paper_example_2_1 refinedc.examples.paper_example_2_1
#-Q _build/default/examples/proofs/paper_example_2_2 refinedc.examples.paper_example_2_2
#-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
#-Q _build/default/examples/proofs/intptr refinedc.examples.intptr
#-Q _build/default/examples/proofs/tests refinedc.examples.tests
#-Q _build/default/linux/casestudies/proofs/page_alloc refinedc.linux.casestudies.page_alloc
#-Q _build/default/linux/pkvm/proofs/spinlock refinedc.linux.pkvm.spinlock
#-Q _build/default/linux/pkvm/proofs/early_alloc refinedc.linux.pkvm.early_alloc
#-Q _build/default/linux/proofs/early_alloc_simplified refinedc.linux.early_alloc_simplified
#-Q _build/default/linux/casestudies/proofs/early_alloc refinedc.linux.casestudies.early_alloc
#-Q _build/default/examples/proofs/quick_sort refinedc.examples.quick_sort
#-Q _build/default/examples/proofs/tagged_ptr refinedc.examples.tagged_ptr
#-Q _build/default/examples/proofs/ocaml_runtime refinedc.examples.ocaml_runtime
#-Q _build/default/linux/casestudies/proofs/page_alloc_find_buddy refinedc.linux.casestudies.page_alloc_find_buddy
......@@ -432,9 +432,11 @@ Ltac convert_to_i2p P cont :=
| _ => let converted := convert_to_i2p_tac P in cont converted
end.
Ltac extensible_judgment_hook := idtac.
Ltac pre_extensible_judgment_hook := idtac.
Ltac liExtensibleJudgement :=
lazymatch goal with
| |- envs_entails _ ?P =>
pre_extensible_judgment_hook;
convert_to_i2p P ltac:(fun converted =>
simple notypeclasses refine (tac_fast_apply converted _); [solve [refine _] |]; extensible_judgment_hook
)end.
......
......@@ -5,6 +5,195 @@ From refinedc.rust_typing.automation Require Export proof_state.
From refinedc.rust_typing Require Import programs functions int uninit.
Set Default Proof Using "Type".
(** * Reification of types and ltypes for place operations *)
Module W.
Local Unset Elimination Schemes.
Section bla.
Context `{typeGS Σ}.
(* TODO place_wrap *)
Inductive ty : Type Type :=
| Atom (rt : Type) (t : type rt) : ty rt
| MutRef (rt : Type) (H : ghost_varG Σ rt) (t : ty rt) (κ : lft) : ty (rt * gname)%type
| ShrRef (rt : Type) (t : ty rt) (κ : lft) : ty rt
(*| Box (rt : Type) (t : ty rt) : ty rt*)
.
(* TODO place_wrap *)
Inductive lty : Type Type :=
| BlockedLty (rt : Type) (H : ghost_varG Σ (place_rfn rt)) (t : type rt) (κ : lft) (γ : gname) : lty (place_rfn rt)
| OfTy (rt : Type) (H : ghost_varG Σ rt) (t : ty rt) : lty rt
| MutLty (rt : Type) (H : ghost_varG Σ (rt * gname)) (H : ghost_varG Σ rt) (lt1 lt2 : lty rt) (κ : lft) : lty (rt * gname)%type
| ShrLty (rt : Type) (H : ghost_varG Σ rt) (lt : lty rt) (κ : lft) : lty rt
(*| BoxLty (rt : Type) (lt : lty rt) : lty rt*)
.
Fixpoint to_type {rt} (t : ty rt) : type rt :=
match t with
| Atom _ t => t
| MutRef rt _ t κ => mut_ref (to_type t) κ
| ShrRef _ t κ => shr_ref (to_type t) κ
(*| Box _ t => *)
end.
Fixpoint to_ltype {rt} (lt : lty rt) : ltype rt :=
match lt with
| BlockedLty _ _ t κ γ => blocked t κ γ
| OfTy _ _ t => lty_of_ty (to_type t)
| MutLty _ _ _ lt1 lt2 κ => mut_ltype (to_ltype lt1) κ (to_ltype lt2)
| ShrLty _ _ lt κ => shr_ltype κ (to_ltype lt)
end.
(**
Unfold the [OfTy] conversion by one step, if there is [OfTy] at the head.
Return [Some(lty, b)] if the conversion can be done, where [lty] is the new ltype
and [b] indicates that an unfolding had to be done.
*)
Program Definition unfold_step {rt} (lt : lty rt) : option ((lty rt) * bool) :=
match lt in lty T return option (lty T * bool) with
| OfTy _ H t =>
match t in (ty T) return (ghost_varG Σ T option (lty T * bool)) with
| Atom _ _ => λ _, None
| MutRef _ _ t κ =>
λ _, Some (MutLty _ _ _ (OfTy _ _ t) (OfTy _ _ t) κ, true)
| ShrRef _ t κ =>
λ _, Some (ShrLty _ _ (OfTy _ _ t) κ, true)
end H
| MutLty _ _ _ lt1 lt2 κ => Some $ (MutLty _ _ _ lt1 lt2 κ, false)
| ShrLty _ _ lt κ => Some $ (ShrLty _ _ lt κ, false)
| BlockedLty _ _ t κ γ => None
end
.
Fixpoint unfold_lty {rt} (lt : lty rt) (K : list place_ectx_item) : option (lty rt * bool) :=
match K with
| [] => Some (lt, false)
| Ki :: K =>
match Ki with
| DerefPCtx _ _ =>
'(lt, changed) unfold_step lt;
match lt in lty T return option (lty T * bool) with
| MutLty _ _ _ lt1 lt2 κ =>
'(lt1', changed1) unfold_lty lt1 K;
'(lt2', changed2) unfold_lty lt2 K;
Some $ (MutLty _ _ _ lt1' lt2' κ, changed || changed1 || changed2)
| ShrLty _ _ lt κ =>
'(lt', changed') unfold_lty lt K;
Some $ (ShrLty _ _ lt' κ, changed || changed')
| _ => None
end
| _ => Some (lt, false)
end
end.
Fixpoint is_ty_strongly_writable {rt} (t : ty rt) (K : list place_ectx_item) : option bool :=
match K with
| [] => Some true
| Ki :: K =>
match Ki with
| DerefPCtx _ _ =>
match t with
| MutRef _ _ t1 κ =>
Some false
| ShrRef _ t κ =>
Some false
| _ =>
None
end
| _ => None
end
end.
Fixpoint is_lty_strongly_writable {rt} (lt : lty rt) (K : list place_ectx_item) : option bool :=
match K with
| [] => Some true
| Ki :: K =>
match Ki with
| DerefPCtx _ _ =>
'(lt, _) unfold_step lt;
match lt with
| MutLty _ _ _ lt1 lt2 κ =>
Some false
| ShrLty _ _ lt κ =>
Some false
| _ =>
None
end
| _ => None
end
end.
(* TODO: find out a good way to check for equality of lt1' and lt2' in the mut case.
is there a better way to do this than using an equality decider?
*)
(*
Fixpoint fold_lty {rt} (lt : lty rt) : lty rt :=
match lt in lty T return lty T with
| OfTy rt _ t => OfTy rt _ t
| MutLty rt _ _ lt1 lt2 κ =>
let lt1' := fold_lty lt1 in
let lt2' := fold_lty lt2 in
match lt1', lt2' with
| OfTy _ _ t1, OfTy _ _ t2 =>
end.
end.
*)
End bla.
Section test.
Context `{typeGS Σ} `{ghost_varG Σ Z} `{ghost_varG Σ (Z * gname)%type} `{ghost_varG Σ ((Z * gname) * gname)%type}.
Definition folded_ty := (MutRef _ _ (MutRef _ _ (Atom Z (int i32)) static) static).
Definition folded_lty := OfTy _ _ (MutRef _ _ (MutRef _ _ (Atom Z (int i32)) static) static).
Eval cbn in (unfold_lty folded_lty [DerefPCtx Na1Ord (IntOp i32); DerefPCtx Na1Ord (IntOp i32)]).
Eval cbn in (is_lty_strongly_writable folded_lty [DerefPCtx Na1Ord (IntOp i32); DerefPCtx Na1Ord (IntOp i32)]).
Eval cbn in (is_ty_strongly_writable folded_ty [DerefPCtx Na1Ord (IntOp i32); DerefPCtx Na1Ord (IntOp i32)]).
Eval cbn in (is_ty_strongly_writable folded_ty []).
End test.
End W.
Ltac of_type t :=
lazymatch t with
| @mut_ref _ _ ?rt ?t ?H ?κ =>
let t := of_type t in
constr:(W.MutRef rt H t κ)
| @shr_ref _ _ ?rt ?t ?κ =>
let t := of_type t in
constr:(W.ShrRef rt t κ)
| _ => constr:(W.Atom _ t)
end.
Ltac of_ltype lt :=
lazymatch lt with
| @lty_of_ty _ _ ?rt ?t ?H =>
let t := of_type t in
constr:(W.OfTy rt H t)
| @mut_ltype _ _ ?rt ?H ?lt1 ?κ ?lt2 => constr:(W.MutLty rt H _ lt1 lt2 κ)
| @shr_ltype _ _ ?rt ?H ?κ ?lt => constr:(W.ShrLty rt H lt κ)
| @blocked _ _ ?rt ?t ?H ?κ ?γ => constr:(W.BlockedLty rt H t κ γ)
end.
(* Reshape a place by unfolding [lty_of_ty] to ltypes *)
Ltac liRReshapePlace :=
lazymatch goal with
| |- envs_entails ?Δ (typed_place ?π ?E ?L ?l ?lty ?r ?b ?K ?T) =>
let reified_lty := of_ltype lty in
let unfolded := eval cbn in (W.unfold_lty reified_lty K) in
match unfolded with
| Some (?unfolded, ?needs_unfold) =>
match needs_unfold with
| true =>
let lty2 := eval cbn in (W.to_ltype unfolded) in
refine (tac_fast_apply (place_eqltype _ _ _ _ lty2 _ _ _ _ _) _); simpl
| false =>
fail 2 "typed_place: does not need reshaping"
end
| _ => fail 1000 "typed_place: cannot unfold ltype"
end
end.
(** * Registering extensions *)
(** More automation for modular arithmetics. *)
Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations.
......@@ -59,7 +248,8 @@ Ltac convert_to_i2p_tac P ::=
| typed_bin_op ?E ?L ?v1 ?ty1 ?v2 ?ty2 ?o ?ot1 ?ot2 ?π ?T => uconstr:(((_ : TypedBinOp E L v1 ty1 v2 ty2 o ot1 ot2 π) T).(i2p_proof))
| typed_un_op ?E ?L ?v ?ty ?o ?ot ?π ?T => uconstr:(((_ : TypedUnOp E L v ty o ot π) T).(i2p_proof))
| typed_call ?E ?L ?v ?P ?vl ?tys ?π ?T => uconstr:(((_ : TypedCall E L π v P vl tys) T).(i2p_proof))
| typed_place ?π ?E ?L ?l ?ty ?r ?b ?P ?T => uconstr:(((_ : TypedPlace E L π l ty r b P) T).(i2p_proof))
| typed_place ?π ?E ?L ?l ?lty ?r ?b ?P ?T => uconstr:(((_ : TypedPlace E L π l lty r b P) T).(i2p_proof))
| typed_place_strong ?π ?E ?L ?l ?lty ?r ?b ?P ?T => uconstr:(((_ : TypedPlaceStrong E L π l lty r b P) T).(i2p_proof))
| typed_if ?E ?L ?ot ?v ?ty ?T1 ?T2 => uconstr:(((_ : TypedIf E L ot v ty) T1 T2).(i2p_proof))
| typed_switch ?E ?L ?v ?rt ?ty ?r ?it ?m ?ss ?def ?fn ?ls ?R ?Q ?π => uconstr:(((_ : TypedSwitch E L v rt ty r it π) m ss def fn ls R Q).(i2p_proof))
| typed_assert ?E ?L ?ot ?v ?rt ?ty ?r ?s ?fn ?ls ?R ?Q ?π => uconstr:(((_ : TypedAssert E L ot v rt ty r π) s fn ls R Q).(i2p_proof))
......@@ -208,13 +398,62 @@ Ltac liRExpr :=
end
end.
(* NOTE: this currently cannot support BinOp/UnOp (as find_place_ctx does), since we cannot evaluate here.
This seems to be a relatively fundamental limitation.
Possibly completely switch to type_write_strong? (and generalize type_place_strong to only determine later on in the checking process if we can do a strong update)
*)
Fixpoint decompose_place_ctx `{typeGS Σ} (e : W.expr) : option (list place_ectx_item * loc)%type :=
match e with
| W.Loc l => Some ([], l)
| W.Deref o ot e => '(K, l) decompose_place_ctx e; Some (K ++ [DerefPCtx o ot], l)
| W.GetMember e sl m => '(K, l) decompose_place_ctx e; Some (K ++ [GetMemberPCtx sl m], l)
| W.AnnotExpr n x e => '(K, l) decompose_place_ctx e; Some (K ++ [AnnotExprPCtx n x], l)
| W.LocInfoE a e => decompose_place_ctx e
| _ => None
end.
(* TODO: this is broken. we don't even know the type of the location at that point.
To solve these problems, we should really pick a common definition for writing.
i.e.: set up lemmas for typed_place_strong that also allows the possibility that it is not strongly writable after all.
Then have one common lemma that always works. *)
(*
Ltac liRWrite :=
lazymatch goal with
| |- envs_entails ?Δ (typed_write ?E ?L ?e ?ot ?v ?rt ?ty ?r ?π ?T) =>
let reified_ty := of_type ty in
let e' := W.of_expr e in
let K0 := eval cbn in (decompose_place_ctx e') in
match K0 with
| Some (?K, ?l) =>
idtac K;
let writable := eval cbn in (W.is_ty_strongly_writable reified_ty K) in
idtac writable;
match writable with
| Some true =>
notypeclasses refine (tac_fast_apply (type_write_strong E L T _ _ _ _ rt ty r π _) _); [ solve [refine _ ] |]
| Some false =>
notypeclasses refine (tac_fast_apply (type_write E L T _ _ _ _ rt ty r π _) _); [ solve [refine _ ] |]
| _ => fail 1000 "liRWrite: cannot determine writeability"
end
| None => fail 1000 "liRWrite: unable to decompose context"
end
end.
*)
Ltac liRJudgement :=
lazymatch goal with
| |- envs_entails _ (typed_write ?E ?L _ _ _ ?rt ?ty ?r ?π ?T) => notypeclasses refine (tac_fast_apply (type_write E L T _ _ _ _ rt ty r π _) _); [ solve [refine _ ] |]
| |- envs_entails _ (typed_write ?E ?L _ _ _ ?rt ?ty ?r ?π ?T) =>
notypeclasses refine (tac_fast_apply (type_write E L T _ _ _ _ rt ty r π _) _); [ solve [refine _ ] |]
(*liRWrite *)
| |- envs_entails _ (typed_read ?E ?L _ _ ?π ?T) => notypeclasses refine (tac_fast_apply (type_read E L T _ _ _ π _) _); [ solve [refine _ ] |]
| |- envs_entails _ (typed_borrow_mut ?E ?L _ _ ?π ?T) => notypeclasses refine (tac_fast_apply (type_borrow_mut E L T _ _ _ π _) _); [solve [refine _] |]
(*| |- envs_entails _ (typed_place _ ?E ?L _ ?lty ?r ?b ?K ?T) =>*)
(*liRReshapePlace*)
end.
(* This does everything *)
Ltac liRStep :=
liEnforceInvariantAndUnfoldInstantiatedEvars;
......@@ -222,6 +461,7 @@ Ltac liRStep :=
first [
liRInstantiateEvars (* must be before do_side_cond and do_extensible_judgement *)
| liRStmt
| liRReshapePlace
| liRIntroduceTypedStmt
| liRExpr
| liRJudgement
......@@ -332,3 +572,6 @@ Ltac split_blocks Pfull Ps :=
repeat (iApply tac_split_big_sepM; [reflexivity|]; iIntros "?"); iIntros "_".
*)
(coq.theory
(name refinedc.rust_typing.automation)
(package refinedc)
(flags -w -notation-overridden -w -redundant-canonical-projection)
(synopsis "Lithium")
(theories refinedc.lang refinedc.rust_typing refinedc.lithium))
From refinedc.rust_typing Require Import type.
From refinedc.lithium Require Import tactics.
Definition BLOCK_PRECOND `{!typeGS Σ} (bid : label) (P : iProp Σ) : Set := unit.
Arguments BLOCK_PRECOND : simpl never.
Definition CODE_MARKER (bs : gmap label stmt) : gmap label stmt := bs.
Notation "'HIDDEN'" := (CODE_MARKER _) (only printing).
Arguments CODE_MARKER : simpl never.
Ltac unfold_code_marker_and_compute_map_lookup :=
unfold CODE_MARKER in *; compute_map_lookup.
Definition RETURN_MARKER `{!typeGS Σ} (R : val rt: Type, type rt rt iProp Σ) : val rt: Type, type rt rt iProp Σ := R.
Notation "'HIDDEN'" := (RETURN_MARKER _) (only printing).
(* simplify RETURN_MARKER as soon as it is applied enough in the goal *)
Arguments RETURN_MARKER _ _ _ _ _ /.
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.
Ltac solve_goal_prepare_tac ::=
prepare_sideconditions.
......@@ -54,13 +54,18 @@ Lemma foobo_typed `{ghost_varG Σ (place_rfn unit)} `{ghost_varG Σ Z} π :
Proof.
iStartProof.
start_function "foobo" ( n ).
repeat liRStep. liShow.
(* TODO: currently not allowed yet, as typed_place_cond does not allow changing the refinement type even under Owned *)
(* same problem for boxes , moving out, ........*)
(* same for structs *)
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.
......@@ -80,17 +85,6 @@ Definition foobo' : function := {|
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).
Proof.
iStartProof.
start_function "foobo" ( n ).
repeat liRStep. liShow.
iApply type_write_copy.
do 15 liRStep; liShow.
(* return does not work anymore of course *)
Abort.
(** Example *)
(*
fn bar(r : &mut i32) -> i32 {
......
From refinedc.lang Require Import lang notation rust tactics.
From refinedc.rust_typing Require Import functions programs int references automation.
From refinedc.rust_typing Require Import functions programs int references automation uninit.
From iris.proofmode Require Import coq_tactics reduction string_ident.
Section test.
Arguments ltype_own : simpl never.
......@@ -10,7 +13,9 @@ Section test.
typed_read E L (l) (IntOp i32) π T.
Proof.
iIntros "Hl HT".
do 3 liRStep; liShow.
do 2 liRStep; liShow.
iApply place_strong.
liRStep; liShow.
iExists (int i32). iSplitR.
{ iPureIntro. apply eqltype_refl. }
repeat liRStep; liShow.
......@@ -37,6 +42,16 @@ Section test.
repeat liRStep. liShow.
Abort.
Lemma test35 E L `{ghost_varG Σ unit} (l : loc) π fn (s : stmt) (T : val rt, type rt rt iProp Σ) :
l ◁ₗ[π, Owned false] () @ ( uninit i32) -
typed_stmt E L (l <-{IntOp i32} (i2v 42 i32); s)%E fn [] T π.
Proof.
iIntros "Hl".
repeat liRStep; liShow.
unshelve iApply type_write_own_copy. done.
repeat liRStep. liShow.
Abort.
Context `{ghost_varG Σ (Z * gname)}.
Lemma test4 E L (l : loc) π fn γ κ (s : stmt) (T : val rt, type rt rt iProp Σ) :
lctx_lft_alive E L κ
......@@ -44,13 +59,13 @@ Section test.
typed_stmt E L ((!{PtrOp} l) <-{IntOp i32} (i2v 42 i32); s)%E fn [] T π.
Proof.
iIntros (?) "Hl".
repeat liRStep. liShow.
iApply (place_eqltype _ _ _ _ (mut_ltype ( int i32)%I κ ( int i32)%I)).
{ admit. }
iApply place_mut_owned.
repeat liRStep. liShow.
do 8 liRStep. liShow.
iApply type_write. simpl.
repeat liRStep; liShow.
iApply place_strong. iApply place_id.
iApply type_write_copy.
repeat liRStep. liShow.
Unshelve.
Abort.
......@@ -65,10 +80,12 @@ Section test.
iFrame "Hlfts". iSplitR.
{ iPureIntro. reflexivity. }
iIntros "Hlfts".
do 3 liRStep; liShow.
do 2 liRStep; liShow.
iApply place_strong. iApply place_id.
iExists _. iSplitR; first done.
iApply type_borrow_mut_end.
repeat liRStep. liShow.
cbn.
Abort.
......@@ -84,13 +101,12 @@ Section test.
repeat liRStep. liShow.
iFrame "Hlfts". iSplitR.
{ iPureIntro. reflexivity. }
repeat liRStep.
iApply (place_eqltype _ _ _ _ (mut_ltype ( (place_wrap (int i32)))%I κ' ( place_wrap (int i32))%I)).
{ admit. }
do 5 liRStep. liShow.
repeat liRStep. liShow.
iApply place_strong. iApply place_id.
iExists _. iSplitR; first done.
iApply type_borrow_mut_end.
repeat liRStep. liShow.
cbn.
Abort.
......