Commit d1ce91a5 authored by Dan Frumin's avatar Dan Frumin

Get rid of some TODOs

parent cd40860f
...@@ -221,7 +221,6 @@ Section flock. ...@@ -221,7 +221,6 @@ Section flock.
(** * Lemmata **) (** * Lemmata **)
(** ** Basic properties of the CAPs *) (** ** Basic properties of the CAPs *)
(* TODO, we only have this for the "smart constructor" *)
Lemma flock_res_agree (γ : flock_name) (s : prop_id) (R1 R2 : iProp Σ) ρ1 ρ2 (π1 π2 : frac) : Lemma flock_res_agree (γ : flock_name) (s : prop_id) (R1 R2 : iProp Σ) ρ1 ρ2 (π1 π2 : frac) :
flock_res γ s (LockRes R1 π1 ρ1) - flock_res γ s (LockRes R1 π1 ρ1) -
flock_res γ s (LockRes R2 π2 ρ2) == flock_res γ s (LockRes R2 π2 ρ2) ==
...@@ -351,7 +350,7 @@ Section flock. ...@@ -351,7 +350,7 @@ Section flock.
{ remember (fa !! i) as fai. destruct fai as [[π ρ']|]; last done. { remember (fa !! i) as fai. destruct fai as [[π ρ']|]; last done.
symmetry in Heqfai. symmetry in Heqfai.
rewrite (big_sepM_lookup _ fa i (π, ρ')) //. rewrite (big_sepM_lookup _ fa i (π, ρ')) //.
(* TODO: RK, please look at this! *) (* TODO: RK, can this proof be simplified? *)
iDestruct (own_valid_2 with "Hi Hactives") as %Hbaz. iDestruct (own_valid_2 with "Hi Hactives") as %Hbaz.
exfalso. revert Hbaz. exfalso. revert Hbaz.
rewrite -auth_frag_op /=. intros Hbaz%auth_own_valid. rewrite -auth_frag_op /=. intros Hbaz%auth_own_valid.
......
...@@ -17,7 +17,6 @@ Definition gcd : val := λ: "x", ...@@ -17,7 +17,6 @@ Definition gcd : val := λ: "x",
Section gcd_spec. Section gcd_spec.
Context `{amonadG Σ}. Context `{amonadG Σ}.
(* TODO: use callᶜ *)
Lemma gcd_spec (a b : Z) (l r: cloc) R : Lemma gcd_spec (a b : Z) (l r: cloc) R :
0 a 0 b 0 a 0 b
l C #a - r C #b - l C #a - r C #b -
......
...@@ -31,8 +31,7 @@ Section tests_vcg. ...@@ -31,8 +31,7 @@ Section tests_vcg.
eauto 42 with iFrame. eauto 42 with iFrame.
Qed. Qed.
(* TODO: should we even allow to alloc arrays of size zero? (* According to the standrad, malloc'ing zero bytes is
According to the standrad, malloc'ing zero bytes is
implementation-defined behaviour *) implementation-defined behaviour *)
Lemma test3 (n : nat) (m : Z) : Lemma test3 (n : nat) (m : Z) :
1 n 1 n
......
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