Commit 825e5099 authored by Lennard Gäher's avatar Lennard Gäher
Browse files

upd typesystem

parent f6f0b35a
......@@ -11,3 +11,6 @@ Inductive startlft_annot : Type :=
Inductive endlft_annot : Type :=
EndLftAnnot (n : string).
Inductive extend_annot : Type :=
ExtendLftAnnot (n : string).
From iris.proofmode Require Import coq_tactics reduction.
From iris.proofmode Require Import coq_tactics reduction string_ident.
From refinedc.rust_typing Require Export type.
From refinedc.lithium Require Export tactics.
(*From refinedc.typing.automation Require Export normalize solvers simplification proof_state loc_eq.*)
From refinedc.rust_typing Require Import programs.
(*function singleton own struct bytes int.*)
From refinedc.rust_typing.automation Require Export proof_state.
From refinedc.rust_typing Require Import programs functions int uninit.
Set Default Proof Using "Type".
(*From refinedc.rust_typing Require Import int.*)
(*Lemma test `{typeGS Σ} π v T : *)
(*v ◁ᵥ{π} 42 @ (int i32) -∗*)
(*find_in_context (FindVal v π) T.*)
(*Proof.*)
(*iIntros "Hv". liFindInContext.*)
(** * Registering extensions *)
(** More automation for modular arithmetics. *)
Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations.
(** We use autorewrite for the moment. *)
Ltac normalize_tac ::= normalize_autorewrite.
(*Goal ∀ l i (x : Z), *)
(*0 < length (<[i:=x]> $ <[i:=x]> (<[length (<[i:=x]>l) :=x]> l ++ <[length (<[i:=x]>l) :=x]> l)). *)
(*move => ???. normalize_goal. *)
(*Abort. *)
Ltac li_pm_reduce_tac H ::= eval cbv [t2mt mt_type mt_movable] in H.
(*Ltac li_pm_reduce_tac H ::= eval cbv [t2mt mt_type mt_movable] in H.*)
(*
Ltac custom_exist_tac A protect ::=
lazymatch A with
| mtype =>
......@@ -37,12 +28,12 @@ Ltac custom_exist_tac A protect ::=
end
| Movable _ => eexists _
end.
*)
Global Hint Transparent ly_size : solve_protected_eq_db.
Ltac solve_protected_eq_unfold_tac ::=
lazymatch goal with
(* unfold constants for function types *)
(*
| |- @eq (_ fn_params) ?a (λ x, _) =>
lazymatch a with
| (λ x, _) => idtac
......@@ -53,28 +44,27 @@ Ltac solve_protected_eq_unfold_tac ::=
opaqueness settings for unification *)
liSimpl
end
*)
(* don't fail if nothing matches *)
| |- _ => idtac
end.
Ltac can_solve_tac ::= solve_goal.
(*Ltac record_destruct_hint hint info ::= add_case_distinction_info hint info.*)
(*Ltac record_destruct_hint hint info ::= *)
(*add_case_distinction_info hint info.*)
(*Hook that is called by Lithium to deal with atomic goals it doesn't know how to solve *)
Ltac convert_to_i2p_tac P ::=
lazymatch P with
| typed_value ?v ?π ?T => uconstr:(((_ : TypedValue _ _) _).(i2p_proof))
| typed_bin_op ?v1 ?ty1 ?v2 ?ty2 ?o ?ot1 ?ot2 ?π ?T => uconstr:(((_ : TypedBinOp _ _ _ _ _ _ _ _) _).(i2p_proof))
| typed_un_op ?v ?ty ?o ?ot ?π ?T => uconstr:(((_ : TypedUnOp _ _ _ _ _) _).(i2p_proof))
(*| typed_call ?v ?P ?vl ?tys ?T => uconstr:(((_ : TypedCall _ _ _ _) _).(i2p_proof))*)
(*| typed_place ?P ?l1 ?β1 ?ty1 ?T => uconstr:(((_ : TypedPlace _ _ _ _) _).(i2p_proof))*)
(*| typed_if ?ot ?v ?ty ?T1 ?T2 => uconstr:(((_ : TypedIf _ _ _) _ _).(i2p_proof))*)
(*| typed_switch ?v ?ty ?it ?m ?ss ?def ?fn ?ls ?fr ?Q => uconstr:(((_ : TypedSwitch _ _ _) _ _ _ _ _ _ _).(i2p_proof))*)
(*| typed_assert ?ot ?v ?ty ?s ?fn ?ls ?fr ?Q => uconstr:(((_ : TypedAssert _ _ _) _ _ _ _ _).(i2p_proof))*)
(*| typed_read_end ?a ?l ?β ?ty ?ly ?T => uconstr:(((_ : TypedReadEnd _ _ _ _ _) _).(i2p_proof))*)
(*| typed_write_end ?a ?ot ?v1 ?ty1 ?l2 ?β2 ?ty2 ?T => uconstr:(((_ : TypedWriteEnd _ _ _ _ _ _ _) _).(i2p_proof))*)
| typed_value ?v ?π ?T => uconstr:(((_ : TypedValue v π) T).(i2p_proof))
| 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_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))
| typed_read_end ?E ?L ?π ?l ?rt ?ty ?r ?b2 ?bmin ?ot ?T => uconstr:(((_ : TypedReadEnd E L π l ty r b2 bmin ot) T).(i2p_proof))
| typed_write_end ?E ?L ?π ?ot ?v1 ?rt1 ?ty1 ?r1 ?b2 ?bmin ?l2 ?rt2 ?lty2 ?r2 ?T => uconstr:(((_ : TypedWriteEnd E L π ot v1 rt1 ty1 r1 b2 bmin l2 rt2 lty2 r2) T).(i2p_proof))
(*| typed_addr_of_end ?l ?β ?ty ?T => uconstr:(((_ : TypedAddrOfEnd _ _ _) _).(i2p_proof))*)
(*| typed_cas ?ot ?v1 ?P1 ?v2 ?P2 ?v3 ?P3 ?T => uconstr:(((_ : TypedCas _ _ _ _ _ _ _) _).(i2p_proof))*)
(*| typed_annot_expr ?n ?a ?v ?P ?T => uconstr:(((_ : TypedAnnotExpr _ _ _ _) _) .(i2p_proof))*)
......@@ -86,41 +76,43 @@ Ltac convert_to_i2p_tac P ::=
Section automation.
Context `{!typeGS Σ}.
Lemma tac_simpl_subst xs s fn ls Q R π :
typed_stmt (W.to_stmt (W.subst_stmt xs s)) fn ls R Q π -
typed_stmt (subst_stmt xs (W.to_stmt s)) fn ls R Q π.
Lemma tac_simpl_subst E L π xs s fn ls Q R:
typed_stmt E L (W.to_stmt (W.subst_stmt xs s)) fn ls R Q π -
typed_stmt E L (subst_stmt xs (W.to_stmt s)) fn ls R Q π.
Proof. by rewrite W.to_stmt_subst. Qed.
(*Lemma tac_typed_single_block_rec P b Q fn ls R s:*)
(*Q !! b = Some s →*)
(*(P ∗ accu (λ A, typed_block (P ∗ A) b fn ls R Q -∗ P -∗ A -∗ typed_stmt s fn ls R Q)) -∗*)
(*typed_stmt (Goto b) fn ls R Q.*)
(*Proof.*)
(*iIntros (HQ) "[HP Hs]". iIntros (Hls). unfold accu, typed_block.*)
(*iDestruct "Hs" as (A) "[HA #Hs]". iLöb as "Hl".*)
(*iApply wps_goto =>//. iModIntro. iApply ("Hs" with "[] HP HA") => //.*)
(*iIntros "!# [HP HA]". by iApply ("Hl" with "HP HA").*)
(*Qed.*)
(*
Lemma tac_typed_single_block_rec P b Q fn ls R s:
Q !! b = Some s →
(P ∗ accu (λ A, typed_block (P ∗ A) b fn ls R Q -∗ P -∗ A -∗ typed_stmt s fn ls R Q)) -∗
typed_stmt (Goto b) fn ls R Q.
Proof.
iIntros (HQ) "[HP Hs]". iIntros (Hls). unfold accu, typed_block.
iDestruct "Hs" as (A) "[HA #Hs]". iLöb as "Hl".
iApply wps_goto =>//. iModIntro. iApply ("Hs" with "[] HP HA") => //.
iIntros "!# [HP HA]". by iApply ("Hl" with "HP HA").
Qed.
*)
End automation.
(* TODO: i have no idea what's this for lol *)
(*Ltac liRIntroduceLetInGoal :=*)
(*lazymatch goal with*)
(*| |- @envs_entails ?PROP ?Δ ?P =>*)
(*let H := fresh "GOAL" in*)
(*lazymatch P with*)
(*| @bi_wand ?PROP ?Q ?T =>*)
(*pose H := (LET_ID T); change_no_check (@envs_entails PROP Δ (@bi_wand PROP Q H))*)
(*| @typed_val_expr ?Σ ?tG ?e ?T =>*)
(*pose (H := LET_ID T); change_no_check (@envs_entails PROP Δ (@typed_val_expr Σ tG e H))*)
Ltac liRIntroduceLetInGoal :=
lazymatch goal with
| |- @envs_entails ?PROP ?Δ ?P =>
let H := fresh "GOAL" in
lazymatch P with
| @bi_wand ?PROP ?Q ?T =>
pose H := (LET_ID T); change_no_check (@envs_entails PROP Δ (@bi_wand PROP Q H))
| @typed_val_expr ?Σ ?tG ?E ?L ?e ?π ?T =>
pose (H := LET_ID T); change_no_check (@envs_entails PROP Δ (@typed_val_expr Σ tG E L e π H))
(* TODO *)
(*| @typed_write ?Σ ?tG ?b ?e ?ot ?v ?ty ?Mov ?T =>*)
(*pose (H := LET_ID T); change_no_check (@envs_entails PROP Δ (@typed_write Σ tG b e ot v ty Mov H))*)
(*| @typed_place ?Σ ?tG ?P ?l1 ?β1 ?ty1 ?T =>*)
(*pose (H := LET_ID T); change_no_check (@envs_entails PROP Δ (@typed_place Σ tG P l1 β1 ty1 H))*)
(*| @typed_bin_op ?Σ ?tG ?v1 ?P1 ?v2 ?P2 ?op ?ot1 ?ot2 ?T =>*)
(*pose (H := LET_ID T); change_no_check (@envs_entails PROP Δ (@typed_bin_op Σ tG v1 P1 v2 P2 op ot1 ot2 H))*)
(*end*)
(*end.*)
end
end.
Ltac liRInstantiateEvars_hook := idtac.
Ltac liRInstantiateEvars :=
......@@ -131,107 +123,108 @@ Ltac liRInstantiateEvars :=
but this causes a Error: No such section variable or assumption
at Qed. time. Maybe this is related to https://github.com/coq/coq/issues/9937 *)
instantiate_protected (protected H) ltac:(fun H => instantiate (1:=((S (protected (EVAR_ID _))))) in (Value of H))
(* This is very hard to figure out for unification because of the
dependent types in with refinement. Unificaiton likes to unfold the
definition of ty without this. This is the reason why do_instantiate
evars must come before do_side_cond *)
| |- protected ?H = ( _ @ ?ty)%I _ =>
instantiate_protected (protected H) ltac:(fun H => instantiate (1:=((protected (EVAR_ID _)) @ ty)%I) in (Value of H))
(*| |- protected ?H = ty_of_rty (frac_ptr ?β _)%I ∧ _ =>*)
(*instantiate_protected (protected H) ltac:(fun H => instantiate (1:=((frac_ptr β (protected (EVAR_ID _)))%I)) in (Value of H))*)
(*| |- envs_entails _ (subsume (?x ◁ₗ{?β} ?ty) (_ ◁ₗ{_} (protected ?H)) _) => liInst H ty*)
(*| |- envs_entails _ (subsume (?x ◁ₗ{?β} ?ty) (_ ◁ₗ{protected ?H} _) _) => liInst H β*)
(* TODO: figure out how/when to instantiate evars *)
end.
Ltac liRStmt :=
lazymatch goal with
| |- envs_entails ?Δ (typed_stmt ?s ?fn ?ls ?fr ?Q ?π) =>
| |- envs_entails ?Δ (typed_stmt ?E ?L ?s ?fn ?ls ?R ?Q ?π) =>
lazymatch s with
| subst_stmt ?xs ?s =>
let s' := W.of_stmt s in
change (subst_stmt xs s) with (subst_stmt xs (W.to_stmt s'));
refine (tac_fast_apply (tac_simpl_subst _ _ _ _ _ _ _) _); simpl; unfold W.to_stmt, W.to_expr
refine (tac_fast_apply (tac_simpl_subst E L π _ _ fn ls Q R) _); simpl; unfold W.to_stmt, W.to_expr
| _ =>
let s' := W.of_stmt s in
lazymatch s' with
(*| W.Assign _ _ _ _ _ => notypeclasses refine (tac_fast_apply (type_assign _ _ _ _ _ _ _ _ _) _)*)
(*| W.Return _ => notypeclasses refine (tac_fast_apply (type_return _ _ _ _ _) _)*)
| W.Assign _ _ _ _ _ => notypeclasses refine (tac_fast_apply (type_assign E L π _ _ _ Q _ fn ls R _) _)
(* TODO *)
| W.Return _ => notypeclasses refine (tac_fast_apply (type_return E L π Q _ fn ls R) _)
(* TODO *)
(*| W.IfS _ _ _ _ => notypeclasses refine (tac_fast_apply (type_if _ _ _ _ _ _ _ _) _)*)
(* TODO *)
(*| W.Switch _ _ _ _ _ => notypeclasses refine (tac_fast_apply (type_switch _ _ _ _ _ _ _ _ _) _)*)
| W.Assert _ _ _ => notypeclasses refine (tac_fast_apply (type_assert _ _ _ _ _ _ _ _) _)
(*| W.Goto ?bid => first [*)
(*notypeclasses refine (tac_fast_apply (type_goto_precond _ _ _ _ _ _) _); progress liFindHyp FICSyntactic*)
| W.Assert _ _ _ => notypeclasses refine (tac_fast_apply (type_assert E L Q _ _ _ fn ls π R) _)
| W.Goto ?bid => first [
notypeclasses refine (tac_fast_apply (type_goto_precond E L π _ Q _ fn ls R) _);
progress liFindHyp FICSyntactic
(* TODO *)
(*| lazymatch goal with*)
(*| H : BLOCK_PRECOND bid ?P |- _ =>*)
(*notypeclasses refine (tac_fast_apply (tac_typed_single_block_rec P _ _ _ _ _ _ _) _);[unfold_code_marker_and_compute_map_lookup|]*)
(*end*)
(*| notypeclasses refine (tac_fast_apply (type_goto _ _ _ _ _ _ _) _); [unfold_code_marker_and_compute_map_lookup|]*)
(*]*)
| W.ExprS _ _ => notypeclasses refine (tac_fast_apply (type_exprs _ _ _ _ _ _ _) _)
| W.SkipS _ => notypeclasses refine (tac_fast_apply (type_skips' _ _ _ _ _ _) _)
| W.AnnotStmt _ ?a _ => notypeclasses refine (tac_fast_apply (type_annot_stmt _ _ _ _ _ _ _ _) _)
| notypeclasses refine (tac_fast_apply (type_goto E L π Q _ fn ls R _ _) _); [unfold_code_marker_and_compute_map_lookup|]
]
| W.ExprS _ _ => notypeclasses refine (tac_fast_apply (type_exprs E L _ _ fn ls R Q π) _)
| W.SkipS _ => notypeclasses refine (tac_fast_apply (type_skips' E L _ fn ls Q R π) _)
| W.AnnotStmt _ (StartLftAnnot ?κ ?κs) _ => notypeclasses refine (tac_fast_apply (type_startlft _ E L _ κ κs _ fn ls Q R π) _)
(* TODO other annotations *)
(*| W.AnnotStmt _ ?a _ => notypeclasses refine (tac_fast_apply (type_annot_stmt _ _ _ _ _ _ _) _)*)
| _ => fail "do_stmt: unknown stmt" s
end
end
end.
(*Ltac liRIntroduceTypedStmt :=*)
(*lazymatch goal with*)
(*| |- @envs_entails ?PROP ?Δ (introduce_typed_stmt ?fn ?ls ?R) =>*)
(*iEval (rewrite /introduce_typed_stmt !fmap_insert fmap_empty; simpl_subst);*)
(*lazymatch goal with*)
(*| |- @envs_entails ?PROP ?Δ (@typed_stmt ?Σ ?tG ?s ?fn ?ls ?R ?Q) =>*)
(*let HQ := fresh "Q" in*)
(*let HR := fresh "R" in*)
(*pose (HQ := (CODE_MARKER Q));*)
(*pose (HR := (RETURN_MARKER R));*)
(*change_no_check (@envs_entails PROP Δ (@typed_stmt Σ tG s fn ls HR HQ));*)
(*iEval (simpl) [> To simplify f_init <]*)
(*end*)
(*end.*)
Ltac liRIntroduceTypedStmt :=
lazymatch goal with
| |- @envs_entails ?PROP ?Δ (introduce_typed_stmt ?E ?L ?π ?fn ?ls ?R) =>
iEval (rewrite /introduce_typed_stmt !fmap_insert fmap_empty; simpl_subst);
lazymatch goal with
| |- @envs_entails ?PROP ?Δ (@typed_stmt ?Σ ?tG ?E ?L ?s ?fn ?ls ?R ?Q ?π) =>
let HQ := fresh "Q" in
let HR := fresh "R" in
pose (HQ := (CODE_MARKER Q));
pose (HR := (RETURN_MARKER R));
change_no_check (@envs_entails PROP Δ (@typed_stmt Σ tG E L s fn ls HR HQ π));
iEval (simpl) (* To simplify f_init *)
end
end.
Ltac liRExpr :=
lazymatch goal with
| |- envs_entails ?Δ (typed_val_expr ?e ?π ?T) =>
| |- envs_entails ?Δ (typed_val_expr ?E ?L ?e ?π ?T) =>
let e' := W.of_expr e in
lazymatch e' with
| W.Val _ => notypeclasses refine (tac_fast_apply (type_val _ _ _) _)
(*| W.Loc _ => notypeclasses refine (tac_fast_apply (type_val _ _) _)*)
(*| W.Use _ _ _ => notypeclasses refine (tac_fast_apply (type_use _ _ _ _) _)*)
| W.Val _ => notypeclasses refine (tac_fast_apply (type_val E L _ π T) _)
| W.Loc _ => notypeclasses refine (tac_fast_apply (type_val E L _ π T) _)
| W.Use _ _ _ => notypeclasses refine (tac_fast_apply (type_use E L _ T _ _ π) _)
| W.Borrow Mut _ _ => notypeclasses refine (tac_fast_apply (type_mut_bor E L T _ π _ _ _) _)
(* TODO *)
(*| W.Borrow Shr _ _ => *)
(*| W.AddrOf _ => notypeclasses refine (tac_fast_apply (type_addr_of _ _) _)*)
| W.BinOp _ _ _ _ _ => notypeclasses refine (tac_fast_apply (type_bin_op _ _ _ _ _ _ _) _)
| W.UnOp _ _ _ => notypeclasses refine (tac_fast_apply (type_un_op _ _ _ _ _) _)
| W.BinOp _ _ _ _ _ => notypeclasses refine (tac_fast_apply (type_bin_op E L _ _ _ _ _ π T) _)
| W.UnOp _ _ _ => notypeclasses refine (tac_fast_apply (type_un_op E L _ _ _ π T) _)
(*| W.CAS _ _ _ _ => notypeclasses refine (tac_fast_apply (type_cas _ _ _ _ _) _)*)
(*| W.Call _ _ => notypeclasses refine (tac_fast_apply (type_call _ _ _) _)*)
| W.Call _ _ => notypeclasses refine (tac_fast_apply (type_call E L π T _ _) _)
(*| W.OffsetOf _ _ => notypeclasses refine (tac_fast_apply (type_offset_of _ _ _) _)*)
| W.AnnotExpr _ ?a _ => notypeclasses refine (tac_fast_apply (type_annot_expr _ _ _ _ _) _)
| W.AnnotExpr _ ?a _ => notypeclasses refine (tac_fast_apply (type_annot_expr E L _ _ a _ π T) _)
(*| W.StructInit _ _ => notypeclasses refine (tac_fast_apply (type_struct_init _ _ _) _)*)
(*| W.IfE _ _ _ _ => notypeclasses refine (tac_fast_apply (type_ife _ _ _ _ _) _)*)
| W.LogicalAnd _ _ _ _ _ => notypeclasses refine (tac_fast_apply (type_logical_and _ _ _ _ _ _) _)
| W.LogicalOr _ _ _ _ _ => notypeclasses refine (tac_fast_apply (type_logical_or _ _ _ _ _ _) _)
| W.IfE _ _ _ _ => notypeclasses refine (tac_fast_apply (type_ife E L _ _ _ _ π T) _)
| W.LogicalAnd _ _ _ _ _ => notypeclasses refine (tac_fast_apply (type_logical_and E L _ _ _ _ π T) _)
| W.LogicalOr _ _ _ _ _ => notypeclasses refine (tac_fast_apply (type_logical_or E L _ _ _ _ π T) _)
(*| W.SkipE _ => notypeclasses refine (tac_fast_apply (type_skipe' _ _) _)*)
(*| W.MacroE _ _ _ => notypeclasses refine (tac_fast_apply (type_macro_expr _ _ _) _)*)
| _ => fail "do_expr: unknown expr" e
end
end.
(*Ltac liRJudgement :=*)
(*lazymatch goal with*)
(*| |- envs_entails _ (typed_write _ _ _ _ _ _) => notypeclasses refine (tac_fast_apply (type_write _ _ _ _ _ _ _ _) _); [ solve [refine _ ] |]*)
(*| |- envs_entails _ (typed_read _ _ _ _) => notypeclasses refine (tac_fast_apply (type_read _ _ _ _ _ _) _); [ solve [refine _ ] |]*)
(*| |- envs_entails _ (typed_addr_of _ _) => notypeclasses refine (tac_fast_apply (type_addr_of_place _ _ _ _) _); [solve [refine _] |]*)
(*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_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 _] |]
end.
(* This does everything *)
Ltac liRStep :=
liEnforceInvariantAndUnfoldInstantiatedEvars;
(*try liRIntroduceLetInGoal;*)
try liRIntroduceLetInGoal;
first [
liRInstantiateEvars (* must be before do_side_cond and do_extensible_judgement *)
| liRStmt
(*| liRIntroduceTypedStmt*)
| liRIntroduceTypedStmt
| liRExpr
(*| liRJudgement*)
| liRJudgement
| liStep
]; liSimpl.
......@@ -278,6 +271,10 @@ 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 : named_binder ?n |- _ =>*)
(*let temp := fresh "tmp" in*)
(*destruct H as [tmp];*)
(*rename_by_string tmp n*)
| H : unit |- _ => destruct H
end.
......@@ -285,14 +282,14 @@ Ltac prepare_initial_coq_context :=
(Q) is part of the goal, because simpl seems to take exponential time
in the number of blocks! *)
(* TODO: don't use i... tactics here *)
(*Tactic Notation "start_function" constr(fnname) "(" simple_intropattern(x) ")" :=*)
(*intros;*)
(*repeat iIntros "#?";*)
(*rewrite /typed_function;*)
(*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; prepare_initial_coq_context.*)
Tactic Notation "start_function" constr(fnname) "(" simple_intropattern(x) ")" :=
intros;
repeat iIntros "#?";
rewrite /typed_function;
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; prepare_initial_coq_context.
Ltac liRSplitBlocksIntro :=
repeat (
......@@ -306,8 +303,9 @@ Ltac liRSplitBlocksIntro :=
| liUnfoldLetGoal]; liSimpl);
liShow.
(* TODO
(* TODO: don't use i... tactics here *)
(*
Ltac split_blocks Pfull Ps :=
(* cbn in * is important here to simplify the types of local
variables, otherwise unification gets confused later *)
......@@ -332,4 +330,5 @@ Ltac split_blocks Pfull Ps :=
repeat (iApply big_sepM_insert; [reflexivity|]; iSplitL); last by [iApply big_sepM_empty];
iExists _; (iSplitR; [iPureIntro; unfold_code_marker_and_compute_map_lookup|]); iModIntro ];
repeat (iApply tac_split_big_sepM; [reflexivity|]; iIntros "?"); iIntros "_".
*)
......@@ -48,7 +48,7 @@ Module pinned_borrows.
(*
&κ {P} {Q} := ∃ γ, ghost_var γ (1/2) P ∗ &κ {∃ P', ghost_var γ (1/2) P' ∗ P ∗ ([† κ] -* P' ==∗ Q)}
needs saved props (clear)
needs saved props (clear)
*)
......@@ -73,8 +73,13 @@ Module pinned_borrows.
( R, ( R - [†κ'] ={lft_userE}= P) -
R ={E}= pinned_bor κ' P R q.[κ]).
Axiom pinned_bor_shorten :
{Σ : gFunctors} `{invGS Σ} `{lftGS Σ lft_userE},
κ κ' P Q,
κ κ' - pinned_bor κ' P Q - pinned_bor κ P Q.
(* derived variant where we go back to [P] *)
Lemma pinned_bor_acc_back {Σ : gFunctors} `{invGS Σ} `{lftGS Σ lft_userE} :
Lemma pinned_bor_acc_back_strong {Σ : gFunctors} `{invGS Σ} `{lftGS Σ lft_userE} :
E q κ P Q,
lftN E
lft_ctx -
......@@ -90,10 +95,34 @@ Module pinned_borrows.
eauto.
Qed.
Axiom pinned_bor_shorten :
{Σ : gFunctors} `{invGS Σ} `{lftGS Σ lft_userE},
κ κ' P Q,
κ κ' - pinned_bor κ' P Q - pinned_bor κ P Q.
Lemma pinned_bor_acc_back {Σ : gFunctors} `{invGS Σ} `{lftGS Σ lft_userE} :
E q κ P Q,
lftN E
lft_ctx -
pinned_bor κ P Q -
q.[κ] ={E}=
Q ( P ={E}= pinned_bor κ P P q.[κ]).
Proof.
iIntros (E q κ P Q ?) "#LFT Hb Htok".
iMod (pinned_bor_acc_back_strong with "LFT Hb Htok") as (κ') "(Hincl & $ & Hclose)"; first solve_ndisj.
iModIntro. iIntros "HP". iMod ("Hclose" with "HP") as "[Hb Htok]".
iFrame. iApply (pinned_bor_shorten with "Hincl Hb").
Qed.
(* NOTE: this is not derivable from [acc_strong].
It might become derivable if [acc_strong] hands out the viewshift from [Q] to [P] too.
*)
(*
Axiom pinned_bor_acc :
∀ {Σ : gFunctors} `{invGS Σ} `{lftGS Σ lft_userE} E q κ P Q,
↑lftN ⊆ E →
lft_ctx -∗
pinned_bor κ P Q -∗
q.[κ] ={E}=∗
▷ Q ∗ (▷ Q ={E}=∗ pinned_bor κ P Q ∗ q.[κ]).
*)
(* a version of [bor_iff] that just goes in one direction, if we can restore the Q *)
(* should be sound in the potential model, by modifying the equivalence closure suitably *)
......@@ -102,6 +131,11 @@ Module pinned_borrows.
κ (P Q R : iProp Σ),
( ((P R) (R Q))) - pinned_bor κ Q P - pinned_bor κ Q R.
Axiom pinned_bor_iff :
{Σ : gFunctors} `{invGS Σ} `{lftGS Σ lft_userE},
κ (P Q : iProp Σ),
( ((P Q) (Q P))) - pinned_bor κ P P - pinned_bor κ Q Q.
End pinned_borrows.
Export pinned_borrows.
Notation "'&pin{' κ } [ P ] Q" := (pinned_bor κ P Q) (at level 40) : bi_scope.
......
From refinedc.lang Require Import lang notation rust tactics.
From refinedc.rust_typing Require Import functions programs int references.
From refinedc.lithium Require Export tactics.
From refinedc.rust_typing Require Import functions programs int references uninit automation.
Section lithium.
Context {Σ : gFunctors}.
Context (named_lfts' : gmap Z Z iProp Σ).
Lemma foo :
True - named_lfts' - True.
Proof.
iStartProof.
liEnforceInvariantAndUnfoldInstantiatedEvars.
liStep.
liStep. liStep. liStep.
Abort.
End lithium.
Section typing.
......@@ -32,10 +49,156 @@ Definition foobo : function := {|
f_init := "_bb0";
|}.
Lemma foobo_typed `{ghost_varG Σ unit} `{ghost_varG Σ Z} π :
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.
(* 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 *)
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";
|}.
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 {
let mut x = 43;
let xr = &mut x;
*r
}
*)
(**
what definitely needs to be done:
- lifetimes
- structs/ADTs in general
- drop
- impl