Skip to content

Commit

Permalink
Change state update to take in two mask
Browse files Browse the repository at this point in the history
  • Loading branch information
hei411 committed Nov 15, 2024
1 parent 82ace8a commit 7fca095
Show file tree
Hide file tree
Showing 8 changed files with 64 additions and 73 deletions.
4 changes: 2 additions & 2 deletions theories/coneris/error_rules.v
Original file line number Diff line number Diff line change
Expand Up @@ -1154,7 +1154,7 @@ Qed.
Lemma state_update_presample_iterM_exp E α N ns p (ε1 : R) (ε2 : list (fin (S N)) → R) :
(∀ n, 0<=ε2 n)%R ->
(SeriesC (λ n, if (length n =? p) then (1/((S N)^ p)) * ε2 n else 0%R )<= ε1)%R →
α ↪N (N; ns) -∗ ↯ ε1 -∗ state_update E (∃ n, α ↪N (N; ns ++ (fin_to_nat <$> n)) ∗
α ↪N (N; ns) -∗ ↯ ε1 -∗ state_update E E (∃ n, α ↪N (N; ns ++ (fin_to_nat <$> n)) ∗
↯ (ε2 n) ∗
⌜length n = p⌝
).
Expand Down Expand Up @@ -1196,7 +1196,7 @@ Qed.
Lemma state_update_presample_exp E α N ns (ε1 : R) (ε2 : fin (S N) → R) :
(∀ n, 0<=ε2 n)%R ->
(SeriesC (λ n, 1 / (S N) * ε2 n)%R <= ε1)%R →
α ↪N (N; ns) -∗ ↯ ε1 -∗ state_update E (∃ n, α ↪N (N; ns ++ [fin_to_nat n]) ∗ ↯ (ε2 n)).
α ↪N (N; ns) -∗ ↯ ε1 -∗ state_update E E (∃ n, α ↪N (N; ns ++ [fin_to_nat n]) ∗ ↯ (ε2 n)).
Proof.
rewrite state_update_unseal/state_update_def.
iIntros (Hpos Hsum) "Hα Hε".
Expand Down
2 changes: 1 addition & 1 deletion theories/coneris/examples/random_counter/impl1.v
Original file line number Diff line number Diff line change
Expand Up @@ -135,7 +135,7 @@ Section impl1.
is_counter1 N c γ1 -∗
rand_tapes (L:=L) α (3%nat, ns) -∗
↯ ε -∗
state_update E (∃ n, ↯ (ε2 n) ∗ rand_tapes (L:=L) α (3%nat, ns++[fin_to_nat n])).
state_update E E (∃ n, ↯ (ε2 n) ∗ rand_tapes (L:=L) α (3%nat, ns++[fin_to_nat n])).
Proof.
iIntros (Hsubset Hpos Hineq) "#Hinv Hfrag Herr".
iMod (rand_tapes_presample with "[$][$]") as "(%&$&$)"; try done.
Expand Down
2 changes: 1 addition & 1 deletion theories/coneris/examples/random_counter/impl2.v
Original file line number Diff line number Diff line change
Expand Up @@ -274,7 +274,7 @@ Section impl2.
is_counter2 N c γ1 -∗
(flip_tapes (L:=L) α (expander ns) ∗ ⌜Forall (λ x, x<4) ns⌝) -∗
↯ ε -∗
state_update E (∃ n, ↯ (ε2 n) ∗
state_update E E (∃ n, ↯ (ε2 n) ∗
(flip_tapes (L:=L) α (expander (ns++[fin_to_nat n])) ∗ ⌜Forall (λ x, x<4) (ns++[fin_to_nat n])⌝)).
Proof.
iIntros (Hsubset Hpos Hineq) "#Hinv' [Hfrag %Hforall] Herr".
Expand Down
2 changes: 1 addition & 1 deletion theories/coneris/examples/random_counter/impl3.v
Original file line number Diff line number Diff line change
Expand Up @@ -122,7 +122,7 @@ Section impl3.
is_counter3 N c γ1 -∗
(∃ ls, ⌜filter filter_f ls = ns⌝ ∗ rand_tapes (L:=L) α (4, ls)) -∗
↯ ε -∗
state_update E (∃ n, ↯ (ε2 n) ∗
state_update E E (∃ n, ↯ (ε2 n) ∗
(∃ ls, ⌜filter filter_f ls = (ns++[fin_to_nat n])⌝ ∗ rand_tapes (L:=L) α (4, ls))).
Proof.
iIntros (Hsubset Hpos Hineq) "#Hinv Hfrag Herr".
Expand Down
3 changes: 1 addition & 2 deletions theories/coneris/examples/random_counter/random_counter.v
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,7 @@ Class random_counter `{!conerisGS Σ} := RandCounter
is_counter(L:=L) N c γ -∗
counter_tapes (L:=L) α (ns) -∗
↯ ε -∗
state_update E (∃ n, ↯ (ε2 n) ∗ counter_tapes (L:=L) α (ns ++ [fin_to_nat n]));
state_update E E (∃ n, ↯ (ε2 n) ∗ counter_tapes (L:=L) α (ns ++ [fin_to_nat n]));

counter_content_auth_exclusive {L : counterG Σ} γ z1 z2:
counter_content_auth (L:=L) γ z1 -∗ counter_content_auth (L:=L) γ z2 -∗ False;
Expand Down Expand Up @@ -148,7 +148,6 @@ Section lemmas.
- iDestruct "H" as "(%ε & %ε2 & Herr & %Hpos & %Hineq & Hrest)".
iMod (counter_tapes_presample _ _ _ _ _ _ _ (λ x, ε2 (fin_to_nat x)) with "[//][$][$Herr]") as "(%n & Herr & ?)"; try done.
{ rewrite SeriesC_finite_foldr/=. lra. }
iModIntro.
iMod (fupd_mask_frame _ (E) ∅ (E∖↑N) with "[Hrest Herr]") as "H"; first set_solver.
+ iMod ("Hrest" with "[$]") as "H". iModIntro.
replace (_∖_∪_) with E; first (iModIntro; iExact "H").
Expand Down
2 changes: 1 addition & 1 deletion theories/coneris/lib/hocap_flip.v
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ Class flip_spec `{!conerisGS Σ} := FlipSpec
(* is_flip (L:=L) N γ -∗ *)
flip_tapes (L:=L) α (ns) -∗
↯ ε -∗
state_update E (∃ n, ↯ (ε2 n) ∗ flip_tapes (L:=L) α (ns ++ [n]));
state_update E E (∃ n, ↯ (ε2 n) ∗ flip_tapes (L:=L) α (ns ++ [n]));

(** * Program specs *)
(* flip_inv_create_spec {L : flipG Σ} N E: *)
Expand Down
2 changes: 1 addition & 1 deletion theories/coneris/lib/hocap_rand.v
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,7 @@ Class rand_spec `{!conerisGS Σ} := RandSpec
(* is_rand(L:=L) N γ -∗ *)
rand_tapes (L:=L) α (tb, ns) -∗
↯ ε -∗
state_update E (∃ n, ↯ (ε2 n) ∗ rand_tapes (L:=L) α (tb, ns ++ [fin_to_nat n]));
state_update E E (∃ n, ↯ (ε2 n) ∗ rand_tapes (L:=L) α (tb, ns ++ [fin_to_nat n]));


(** * Program specs *)
Expand Down
Loading

0 comments on commit 7fca095

Please sign in to comment.