Commit 048c1078 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'lang_lemmas' into 'master'

Lang lemmas

See merge request !324
parents 68a003e0 be6a65e5
Pipeline #20919 passed with stage
in 15 minutes and 32 seconds
...@@ -11,6 +11,12 @@ Coq development, but not every API-breaking change is listed. Changes marked ...@@ -11,6 +11,12 @@ Coq development, but not every API-breaking change is listed. Changes marked
splitting and other forms of weakening. splitting and other forms of weakening.
* Updated the strong variant of the opening lemma for cancellable invariants * Updated the strong variant of the opening lemma for cancellable invariants
to match that of regular invariants, where you can pick the mask at a later time. to match that of regular invariants, where you can pick the mask at a later time.
**Changes in program logic:**
* In the axiomatization of ectx languages we replace the axiom of positivity of
context composition with an axiom that says if `fill K e` takes a head step,
then either `K` is the empty evaluation context or `e` is a value.
**Changes in Coq:** **Changes in Coq:**
......
...@@ -722,7 +722,7 @@ Canonical Structure heap_lang := LanguageOfEctx heap_ectx_lang. ...@@ -722,7 +722,7 @@ Canonical Structure heap_lang := LanguageOfEctx heap_ectx_lang.
(* Prefer heap_lang names over ectx_language names. *) (* Prefer heap_lang names over ectx_language names. *)
Export heap_lang. Export heap_lang.
(* The following lemma is not provable using the axioms of [ectxi_language]. (** The following lemma is not provable using the axioms of [ectxi_language].
The proof requires a case analysis over context items ([destruct i] on the The proof requires a case analysis over context items ([destruct i] on the
last line), which in all cases yields a non-value. To prove this lemma for last line), which in all cases yields a non-value. To prove this lemma for
[ectxi_language] in general, we would require that a term of the form [ectxi_language] in general, we would require that a term of the form
...@@ -747,6 +747,13 @@ Proof. ...@@ -747,6 +747,13 @@ Proof.
apply to_val_fill_some in H3 as [-> ->]. subst e. done. apply to_val_fill_some in H3 as [-> ->]. subst e. done.
Qed. Qed.
(** If [e1] makes a head step to a value under some state [σ1] then any head
step from [e1] under any other state [σ1'] must necessarily be to a value. *)
Lemma head_step_to_val e1 σ1 κ e2 σ2 efs σ1' κ' e2' σ2' efs' :
head_step e1 σ1 κ e2 σ2 efs
head_step e1 σ1' κ' e2' σ2' efs' is_Some (to_val e2) is_Some (to_val e2').
Proof. destruct 1; inversion 1; naive_solver. Qed.
Lemma irreducible_resolve e v1 v2 σ : Lemma irreducible_resolve e v1 v2 σ :
irreducible e σ irreducible (Resolve e (Val v1) (Val v2)) σ. irreducible e σ irreducible (Resolve e (Val v1) (Val v2)) σ.
Proof. Proof.
......
...@@ -67,11 +67,10 @@ Proof. ...@@ -67,11 +67,10 @@ Proof.
by iApply (IH with "Hσ He Ht"). by iApply (IH with "Hσ He Ht").
Qed. Qed.
Lemma wp_safe κs m e σ Φ : Lemma wp_not_stuck κs m e σ Φ :
state_interp σ κs m - state_interp σ κs m - WP e {{ Φ }} ={}= not_stuck e σ⌝.
WP e {{ Φ }} ={}= is_Some (to_val e) reducible e σ⌝.
Proof. Proof.
rewrite wp_unfold /wp_pre. iIntros "Hσ H". rewrite wp_unfold /wp_pre /not_stuck. iIntros "Hσ H".
destruct (to_val e) as [v|] eqn:?; first by eauto. destruct (to_val e) as [v|] eqn:?; first by eauto.
iSpecialize ("H" $! σ [] κs with "Hσ"). rewrite sep_elim_l. iSpecialize ("H" $! σ [] κs with "Hσ"). rewrite sep_elim_l.
iMod (fupd_plain_mask with "H") as %?; eauto. iMod (fupd_plain_mask with "H") as %?; eauto.
...@@ -98,8 +97,8 @@ Proof. ...@@ -98,8 +97,8 @@ Proof.
with "[$Hσ $Hwp $Ht]") as "(Hsafe&Hσ&Hwp&Hvs)". with "[$Hσ $Hwp $Ht]") as "(Hsafe&Hσ&Hwp&Hvs)".
{ iIntros "(Hσ & Hwp & Ht)" (e' -> He'). { iIntros "(Hσ & Hwp & Ht)" (e' -> He').
apply elem_of_cons in He' as [<-|(t1''&t2''&->)%elem_of_list_split]. apply elem_of_cons in He' as [<-|(t1''&t2''&->)%elem_of_list_split].
- iMod (wp_safe with "Hσ Hwp") as "$"; auto. - iMod (wp_not_stuck with "Hσ Hwp") as "$"; auto.
- iDestruct "Ht" as "(_ & He' & _)". by iMod (wp_safe with "Hσ He'"). } - iDestruct "Ht" as "(_ & He' & _)". by iMod (wp_not_stuck with "Hσ He'"). }
iApply step_fupd_fupd. iApply step_fupd_intro; first done. iNext. iApply step_fupd_fupd. iApply step_fupd_intro; first done. iNext.
iExists _, _. iSplitL ""; first done. iFrame "Hsafe Hσ". iExists _, _. iSplitL ""; first done. iFrame "Hsafe Hσ".
iSplitL "Hwp". iSplitL "Hwp".
...@@ -166,14 +165,14 @@ Record adequate {Λ} (s : stuckness) (e1 : expr Λ) (σ1 : state Λ) ...@@ -166,14 +165,14 @@ Record adequate {Λ} (s : stuckness) (e1 : expr Λ) (σ1 : state Λ)
adequate_not_stuck t2 σ2 e2 : adequate_not_stuck t2 σ2 e2 :
s = NotStuck s = NotStuck
rtc erased_step ([e1], σ1) (t2, σ2) rtc erased_step ([e1], σ1) (t2, σ2)
e2 t2 (is_Some (to_val e2) reducible e2 σ2) e2 t2 not_stuck e2 σ2
}. }.
Lemma adequate_alt {Λ} s e1 σ1 (φ : val Λ state Λ Prop) : Lemma adequate_alt {Λ} s e1 σ1 (φ : val Λ state Λ Prop) :
adequate s e1 σ1 φ t2 σ2, adequate s e1 σ1 φ t2 σ2,
rtc erased_step ([e1], σ1) (t2, σ2) rtc erased_step ([e1], σ1) (t2, σ2)
( v2 t2', t2 = of_val v2 :: t2' φ v2 σ2) ( v2 t2', t2 = of_val v2 :: t2' φ v2 σ2)
( e2, s = NotStuck e2 t2 (is_Some (to_val e2) reducible e2 σ2)). ( e2, s = NotStuck e2 t2 not_stuck e2 σ2).
Proof. split. intros []; naive_solver. constructor; naive_solver. Qed. Proof. split. intros []; naive_solver. constructor; naive_solver. Qed.
Theorem adequate_tp_safe {Λ} (e1 : expr Λ) t2 σ1 σ2 φ : Theorem adequate_tp_safe {Λ} (e1 : expr Λ) t2 σ1 σ2 φ :
......
...@@ -29,17 +29,17 @@ Section ectx_language_mixin. ...@@ -29,17 +29,17 @@ Section ectx_language_mixin.
mixin_fill_inj K : Inj (=) (=) (fill K); mixin_fill_inj K : Inj (=) (=) (fill K);
mixin_fill_val K e : is_Some (to_val (fill K e)) is_Some (to_val e); mixin_fill_val K e : is_Some (to_val (fill K e)) is_Some (to_val e);
(* There are a whole lot of sensible axioms (like associativity, and left and
right identity, we could demand for [comp_ectx] and [empty_ectx]. However,
positivity suffices. *)
mixin_ectx_positive K1 K2 :
comp_ectx K1 K2 = empty_ectx K1 = empty_ectx K2 = empty_ectx;
mixin_step_by_val K K' e1 e1' σ1 κ e2 σ2 efs : mixin_step_by_val K K' e1 e1' σ1 κ e2 σ2 efs :
fill K e1 = fill K' e1' fill K e1 = fill K' e1'
to_val e1 = None to_val e1 = None
head_step e1' σ1 κ e2 σ2 efs head_step e1' σ1 κ e2 σ2 efs
K'', K' = comp_ectx K K''; K'', K' = comp_ectx K K'';
(* If [fill K e] takes a head step, then either [e] is a value or [K] is
the empty evaluation context. In other words, if [e] is not a value then
there cannot be another redex position elsewhere in [fill K e]. *)
mixin_head_ctx_step_val K e σ1 κ e2 σ2 efs :
head_step (fill K e) σ1 κ e2 σ2 efs is_Some (to_val e) K = empty_ectx;
}. }.
End ectx_language_mixin. End ectx_language_mixin.
...@@ -87,15 +87,15 @@ Section ectx_language. ...@@ -87,15 +87,15 @@ Section ectx_language.
Proof. apply ectx_language_mixin. Qed. Proof. apply ectx_language_mixin. Qed.
Lemma fill_val K e : is_Some (to_val (fill K e)) is_Some (to_val e). Lemma fill_val K e : is_Some (to_val (fill K e)) is_Some (to_val e).
Proof. apply ectx_language_mixin. Qed. Proof. apply ectx_language_mixin. Qed.
Lemma ectx_positive K1 K2 :
comp_ectx K1 K2 = empty_ectx K1 = empty_ectx K2 = empty_ectx.
Proof. apply ectx_language_mixin. Qed.
Lemma step_by_val K K' e1 e1' σ1 κ e2 σ2 efs : Lemma step_by_val K K' e1 e1' σ1 κ e2 σ2 efs :
fill K e1 = fill K' e1' fill K e1 = fill K' e1'
to_val e1 = None to_val e1 = None
head_step e1' σ1 κ e2 σ2 efs head_step e1' σ1 κ e2 σ2 efs
K'', K' = comp_ectx K K''. K'', K' = comp_ectx K K''.
Proof. apply ectx_language_mixin. Qed. Proof. apply ectx_language_mixin. Qed.
Lemma head_ctx_step_val K e σ1 κ e2 σ2 efs :
head_step (fill K e) σ1 κ e2 σ2 efs is_Some (to_val e) K = empty_ectx.
Proof. apply ectx_language_mixin. Qed.
Definition head_reducible (e : expr Λ) (σ : state Λ) := Definition head_reducible (e : expr Λ) (σ : state Λ) :=
κ e' σ' efs, head_step e σ κ e' σ' efs. κ e' σ' efs, head_step e σ κ e' σ' efs.
...@@ -151,6 +151,8 @@ Section ectx_language. ...@@ -151,6 +151,8 @@ Section ectx_language.
Lemma not_head_reducible e σ : ¬head_reducible e σ head_irreducible e σ. Lemma not_head_reducible e σ : ¬head_reducible e σ head_irreducible e σ.
Proof. unfold head_reducible, head_irreducible. naive_solver. Qed. Proof. unfold head_reducible, head_irreducible. naive_solver. Qed.
Lemma head_step_not_stuck e σ κ e' σ' efs : head_step e σ κ e' σ' efs not_stuck e σ.
Proof. rewrite /not_stuck /reducible /=. eauto 10 using head_prim_step. Qed.
Lemma fill_prim_step K e1 σ1 κ e2 σ2 efs : Lemma fill_prim_step K e1 σ1 κ e2 σ2 efs :
prim_step e1 σ1 κ e2 σ2 efs prim_step (fill K e1) σ1 κ (fill K e2) σ2 efs. prim_step e1 σ1 κ e2 σ2 efs prim_step (fill K e1) σ1 κ (fill K e2) σ2 efs.
...@@ -211,16 +213,30 @@ Section ectx_language. ...@@ -211,16 +213,30 @@ Section ectx_language.
rewrite fill_empty. eapply Hatomic_step. by rewrite fill_empty. rewrite fill_empty. eapply Hatomic_step. by rewrite fill_empty.
Qed. Qed.
Lemma head_reducible_prim_step_ctx K e1 σ1 κ e2 σ2 efs :
head_reducible e1 σ1
prim_step (fill K e1) σ1 κ e2 σ2 efs
e2', e2 = fill K e2' head_step e1 σ1 κ e2' σ2 efs.
Proof.
intros (κ'&e2''&σ2''&efs''&?HhstepK) [K' e1' e2' HKe1 -> Hstep].
edestruct (step_by_val K) as [K'' ?];
eauto using val_head_stuck; simplify_eq/=.
rewrite -fill_comp in HKe1; simplify_eq.
exists (fill K'' e2'). rewrite fill_comp; split; first done.
apply head_ctx_step_val in HhstepK as [[v ?]|?]; simplify_eq.
{ apply val_head_stuck in Hstep; simplify_eq. }
by rewrite !fill_empty.
Qed.
Lemma head_reducible_prim_step e1 σ1 κ e2 σ2 efs : Lemma head_reducible_prim_step e1 σ1 κ e2 σ2 efs :
head_reducible e1 σ1 head_reducible e1 σ1
prim_step e1 σ1 κ e2 σ2 efs prim_step e1 σ1 κ e2 σ2 efs
head_step e1 σ1 κ e2 σ2 efs. head_step e1 σ1 κ e2 σ2 efs.
Proof. Proof.
intros (κ'&e2''&σ2''&efs''&?) [K e1' e2' -> -> Hstep]. intros.
destruct (step_by_val K empty_ectx e1' (fill K e1') σ1 κ' e2'' σ2'' efs'') edestruct (head_reducible_prim_step_ctx empty_ectx) as (?&?&?);
as [K' [-> _]%symmetry%ectx_positive]; rewrite ?fill_empty; eauto.
eauto using fill_empty, fill_not_val, val_head_stuck. by simplify_eq; rewrite fill_empty.
by rewrite !fill_empty.
Qed. Qed.
(* Every evaluation context is a context. *) (* Every evaluation context is a context. *)
......
...@@ -109,7 +109,6 @@ Section ectxi_language. ...@@ -109,7 +109,6 @@ Section ectxi_language.
- intros K1 K2 e. by rewrite /fill /= foldl_app. - intros K1 K2 e. by rewrite /fill /= foldl_app.
- intros K; induction K as [|Ki K IH]; rewrite /Inj; naive_solver. - intros K; induction K as [|Ki K IH]; rewrite /Inj; naive_solver.
- done. - done.
- by intros [] [].
- intros K K' e1 κ e1' σ1 e2 σ2 efs Hfill Hred Hstep; revert K' Hfill. - intros K K' e1 κ e1' σ1 e2 σ2 efs Hfill Hred Hstep; revert K' Hfill.
induction K as [|Ki K IH] using rev_ind=> /= K' Hfill; eauto using app_nil_r. induction K as [|Ki K IH] using rev_ind=> /= K' Hfill; eauto using app_nil_r.
destruct K' as [|Ki' K' _] using @rev_ind; simplify_eq/=. destruct K' as [|Ki' K' _] using @rev_ind; simplify_eq/=.
...@@ -121,6 +120,10 @@ Section ectxi_language. ...@@ -121,6 +120,10 @@ Section ectxi_language.
apply fill_not_val. revert Hstep. apply ectxi_language_mixin. } apply fill_not_val. revert Hstep. apply ectxi_language_mixin. }
simplify_eq. destruct (IH K') as [K'' ->]; auto. simplify_eq. destruct (IH K') as [K'' ->]; auto.
exists K''. by rewrite assoc. exists K''. by rewrite assoc.
- intros K e1 σ1 κ e2 σ2 efs.
destruct K as [|Ki K _] using rev_ind; simpl; first by auto.
rewrite fill_app /=.
intros ?%head_ctx_step_val; eauto using fill_val.
Qed. Qed.
Canonical Structure ectxi_lang_ectx := EctxLanguage ectxi_lang_ectx_mixin. Canonical Structure ectxi_lang_ectx := EctxLanguage ectxi_lang_ectx_mixin.
......
...@@ -80,6 +80,8 @@ Section language. ...@@ -80,6 +80,8 @@ Section language.
κ e' σ' efs, ¬prim_step e σ κ e' σ' efs. κ e' σ' efs, ¬prim_step e σ κ e' σ' efs.
Definition stuck (e : expr Λ) (σ : state Λ) := Definition stuck (e : expr Λ) (σ : state Λ) :=
to_val e = None irreducible e σ. to_val e = None irreducible e σ.
Definition not_stuck (e : expr Λ) (σ : state Λ) :=
is_Some (to_val e) reducible e σ.
(* [Atomic WeaklyAtomic]: This (weak) form of atomicity is enough to open (* [Atomic WeaklyAtomic]: This (weak) form of atomicity is enough to open
invariants when WP ensures safety, i.e., programs never can get stuck. We invariants when WP ensures safety, i.e., programs never can get stuck. We
...@@ -140,6 +142,11 @@ Section language. ...@@ -140,6 +142,11 @@ Section language.
Proof. intros [??] ???? ?%val_stuck. by destruct (to_val e). Qed. Proof. intros [??] ???? ?%val_stuck. by destruct (to_val e). Qed.
Global Instance of_val_inj : Inj (=) (=) (@of_val Λ). Global Instance of_val_inj : Inj (=) (=) (@of_val Λ).
Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed. Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
Lemma not_not_stuck e σ : ¬not_stuck e σ stuck e σ.
Proof.
rewrite /stuck /not_stuck -not_eq_None_Some -not_reducible.
destruct (decide (to_val e = None)); naive_solver.
Qed.
Lemma strongly_atomic_atomic e a : Lemma strongly_atomic_atomic e a :
Atomic StronglyAtomic e Atomic a e. Atomic StronglyAtomic e Atomic a e.
...@@ -175,6 +182,18 @@ Section language. ...@@ -175,6 +182,18 @@ Section language.
by rewrite -!Permutation_middle !assoc_L Ht. by rewrite -!Permutation_middle !assoc_L Ht.
Qed. Qed.
Lemma step_insert i t2 σ2 e κ e' σ3 efs :
t2 !! i = Some e
prim_step e σ2 κ e' σ3 efs
step (t2, σ2) κ (<[i:=e']>t2 ++ efs, σ3).
Proof.
intros.
edestruct (elem_of_list_split_length t2) as (t21&t22&?&?);
first (by eauto using elem_of_list_lookup_2); simplify_eq.
econstructor; eauto.
by rewrite insert_app_r_alt // Nat.sub_diag /= -assoc_L.
Qed.
Lemma erased_step_Permutation (t1 t1' t2 : list (expr Λ)) σ1 σ2 : Lemma erased_step_Permutation (t1 t1' t2 : list (expr Λ)) σ1 σ2 :
t1 t1' erased_step (t1,σ1) (t2,σ2) t2', t2 t2' erased_step (t1',σ1) (t2',σ2). t1 t1' erased_step (t1,σ1) (t2,σ2) t2', t2 t2' erased_step (t1',σ1) (t2',σ2).
Proof. Proof.
...@@ -188,6 +207,8 @@ Section language. ...@@ -188,6 +207,8 @@ Section language.
prim_step e1 σ1 κ e2' σ2 efs κ = [] σ2 = σ1 e2' = e2 efs = [] prim_step e1 σ1 κ e2' σ2 efs κ = [] σ2 = σ1 e2' = e2 efs = []
}. }.
Notation pure_steps_tp := (Forall2 (rtc pure_step)).
(* TODO: Exclude the case of [n=0], either here, or in [wp_pure] to avoid it (* TODO: Exclude the case of [n=0], either here, or in [wp_pure] to avoid it
succeeding when it did not actually do anything. *) succeeding when it did not actually do anything. *)
Class PureExec (φ : Prop) (n : nat) (e1 e2 : expr Λ) := Class PureExec (φ : Prop) (n : nat) (e1 e2 : expr Λ) :=
...@@ -208,7 +229,21 @@ Section language. ...@@ -208,7 +229,21 @@ Section language.
Lemma pure_step_nsteps_ctx K `{!@LanguageCtx Λ K} n e1 e2 : Lemma pure_step_nsteps_ctx K `{!@LanguageCtx Λ K} n e1 e2 :
relations.nsteps pure_step n e1 e2 relations.nsteps pure_step n e1 e2
relations.nsteps pure_step n (K e1) (K e2). relations.nsteps pure_step n (K e1) (K e2).
Proof. induction 1; econstructor; eauto using pure_step_ctx. Qed. Proof. eauto using nsteps_congruence, pure_step_ctx. Qed.
Lemma rtc_pure_step_ctx K `{!@LanguageCtx Λ K} e1 e2 :
rtc pure_step e1 e2 rtc pure_step (K e1) (K e2).
Proof. eauto using rtc_congruence, pure_step_ctx. Qed.
Lemma not_stuck_under_ectx K `{!@LanguageCtx Λ K} e σ :
not_stuck (K e) σ not_stuck e σ.
Proof.
rewrite /not_stuck /reducible /=.
intros [[? HK]|(?&?&?&?&Hstp)]; simpl in *.
- left. apply not_eq_None_Some; intros ?%fill_not_val; simplify_eq.
- destruct (to_val e) eqn:?; first by left; eauto.
apply fill_step_inv in Hstp; naive_solver.
Qed.
(* We do not make this an instance because it is awfully general. *) (* We do not make this an instance because it is awfully general. *)
Lemma pure_exec_ctx K `{!@LanguageCtx Λ K} φ n e1 e2 : Lemma pure_exec_ctx K `{!@LanguageCtx Λ K} φ n e1 e2 :
...@@ -228,7 +263,58 @@ Section language. ...@@ -228,7 +263,58 @@ Section language.
apply TCForall_Forall, Forall_fmap, Forall_true=> v. apply TCForall_Forall, Forall_fmap, Forall_true=> v.
rewrite /AsVal /=; eauto. rewrite /AsVal /=; eauto.
Qed. Qed.
Lemma as_val_is_Some e : Lemma as_val_is_Some e :
( v, of_val v = e) is_Some (to_val e). ( v, of_val v = e) is_Some (to_val e).
Proof. intros [v <-]. rewrite to_of_val. eauto. Qed. Proof. intros [v <-]. rewrite to_of_val. eauto. Qed.
Lemma prim_step_not_stuck e σ κ e' σ' efs :
prim_step e σ κ e' σ' efs not_stuck e σ.
Proof. rewrite /not_stuck /reducible. eauto 10. Qed.
Lemma rtc_pure_step_val `{!Inhabited (state Λ)} v e :
rtc pure_step (of_val v) e to_val e = Some v.
Proof.
intros ?; rewrite <- to_of_val.
f_equal; symmetry; eapply rtc_nf; first done.
intros [e' [Hstep _]].
destruct (Hstep inhabitant) as (?&?&?&Hval%val_stuck).
by rewrite to_of_val in Hval.
Qed.
(** Let thread pools [t1] and [t3] be such that each thread in [t1] makes
(zero or more) pure steps to the corresponding thread in [t3]. Furthermore,
let [t2] be a thread pool such that [t1] under state [σ1] makes a (single)
step to thread pool [t2] and state [σ2]. In this situation, either the step
from [t1] to [t2] corresponds to one of the pure steps between [t1] and [t3],
or, there is an [i] such that [i]th thread does not participate in the
pure steps between [t1] and [t3] and [t2] corresponds to taking a step in
the [i]th thread starting from [t1]. *)
Lemma erased_step_pure_step_tp t1 σ1 t2 σ2 t3 :
erased_step (t1, σ1) (t2, σ2)
pure_steps_tp t1 t3
(σ1 = σ2 pure_steps_tp t2 t3)
( i e efs e' κ,
t1 !! i = Some e t3 !! i = Some e
t2 = <[i:=e']>t1 ++ efs
prim_step e σ1 κ e' σ2 efs).
Proof.
intros [κ [e σ e' σ' ? t11 t12 ?? Hstep]] Hps; simplify_eq/=.
apply Forall2_app_inv_l in Hps
as (t31&?&Hpsteps&(e''&t32&Hps&?&->)%Forall2_cons_inv_l&->).
destruct Hps as [e|e1 e2 e3 [_ Hprs]].
- right.
exists (length t11), e, efs, e', κ; split_and!; last done.
+ by rewrite lookup_app_r // Nat.sub_diag.
+ apply Forall2_length in Hpsteps.
by rewrite lookup_app_r Hpsteps // Nat.sub_diag.
+ by rewrite insert_app_r_alt // Nat.sub_diag /= -assoc_L.
- edestruct Hprs as (?&?&?&?); first done; simplify_eq.
left; split; first done.
rewrite right_id_L.
eauto using Forall2_app.
Qed.
End language. End language.
Notation pure_steps_tp := (Forall2 (rtc pure_step)).
Markdown is supported
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