Concurrent hash

theories/approxis/primitive_laws.v

@@ -76,7 +76,7 @@ Definition nat_tape `{approxisGS Σ} l (N : nat) (ns : list nat) : iProp Σ :=
   ∃ (fs : list (fin (S N))), ⌜fin_to_nat <$> fs = ns⌝ ∗ l ↪ (N; fs).
 
 Notation "l ↪N ( M ; ns )" := (nat_tape l M ns)%I
-                                (at level 20, format "l ↪N ( M ; ns )") : bi_scope.
+  (at level 20, format "l  ↪N  ( M ;  ns )") : bi_scope.
 
 (*
 Definition nat_spec_tape `{approxisGS Σ} l (N : nat) (ns : list nat) : iProp Σ :=

theories/base_logic/error_credits.v

@@ -12,7 +12,8 @@ Canonical Structure nonnegrealO : ofe := leibnizO nonnegreal.
 
 (** ** RA for the reals in the interval [0, 1) with addition as the operation. *)
 Section nonnegreal.
-
+
+  Global Instance R_inhabited : Inhabited R := populate (1%R).
   Global Instance nonnegreal_inhabited : Inhabited nonnegreal := populate (nnreal_one).
 
   #[local] Open Scope R.
@@ -291,6 +292,14 @@ Section error_credit_theory.
     lra.
   Qed.
 
+  Lemma ec_valid (ε : R) : ↯ ε -∗ ⌜(0<=ε<1)%R⌝.
+  Proof.
+    iIntros "(%&<-&H)".
+    rewrite ec_unseal /ec_def.
+    iDestruct (own_valid with "H") as %?%auth_frag_valid_1.
+    destruct x. compute in H. simpl in *. iPureIntro. lra.
+  Qed. 
+
   #[local] Lemma err_amp_power ε k :
     0 < ε →
     1 < k →
@@ -372,3 +381,5 @@ Proof.
   - pose (C := EcGS _ _ γEC).
     iModIntro. iExists C. by iFrame.
 Qed.
+
+#[global] Hint Resolve cond_nonneg : core.

theories/con_prob_lang/erasure.v

@@ -540,40 +540,7 @@ Lemma limprim_coupl_step_limprim_aux
   (state_step σ1 α ≫= (λ σ2, sch_lim_exec sch (ζ, (e1, σ2)))) v.
 Proof.
   intro Hsome.
-   rewrite sch_lim_exec_unfold/=.
-   rewrite {2}/pmf/=/dbind_pmf.
-   setoid_rewrite sch_lim_exec_unfold.
-   simpl in *.
-   assert
-     (SeriesC (λ a: state, state_step σ1 α a * Sup_seq (λ n : nat, sch_exec sch n (ζ, (e1, a)) v)) =
-     SeriesC (λ a: state, Sup_seq (λ n : nat, state_step σ1 α a * sch_exec sch n (ζ, (e1, a)) v))) as Haux.
-   { apply SeriesC_ext; intro v'.
-     apply eq_rbar_finite.
-     rewrite rmult_finite.
-     rewrite (rbar_finite_real_eq (Sup_seq (λ n : nat, sch_exec sch n (ζ, (e1, v')) v))); auto.
-     - rewrite <- (Sup_seq_scal_l (state_step σ1 α v') (λ n : nat, sch_exec sch n (ζ, (e1, v')) v)); auto.
-     - apply (Rbar_le_sandwich 0 1).
-       + apply (Sup_seq_minor_le _ _ 0%nat); simpl; auto.
-       + apply upper_bound_ge_sup; intro; simpl; auto.
-   }
-   rewrite Haux.
-   rewrite (MCT_seriesC _ (λ n, sch_exec sch n (ζ, (e1,σ1)) v) (sch_lim_exec sch (ζ, (e1,σ1)) v)); auto.
-   - real_solver.
-   - intros. apply Rmult_le_compat; auto; [done|apply sch_exec_mono].
-   - intro. exists (state_step σ1 α a)=>?. real_solver.
-   - intro n.
-     rewrite (Rcoupl_eq_elim _ _ (prim_coupl_step_prim n e1 σ1 α bs _ Hsome)); auto.
-     rewrite {3}/pmf/=/dbind_pmf.
-     apply SeriesC_correct; auto.
-     apply (ex_seriesC_le _ (state_step σ1 α)); auto.
-     real_solver.
-   - rewrite sch_lim_exec_unfold.
-     rewrite rbar_finite_real_eq; [apply Sup_seq_correct |].
-     rewrite mon_sup_succ.
-     + apply (Rbar_le_sandwich 0 1); auto.
-       * apply (Sup_seq_minor_le _ _ 0%nat); simpl; auto.
-       * apply upper_bound_ge_sup; intro; simpl; auto.
-     + intros. eapply sch_exec_mono.
+  erewrite <-sch_erasable_sch_lim_exec; [done|by eapply state_step_sch_erasable|done].
 Qed.
 
 Lemma sch_limprim_coupl_step_sch_limprim
@@ -679,27 +646,42 @@ Proof.
   rewrite -insert_app_l.
   - by rewrite app_comm_cons.
   - by eapply lookup_lt_Some.
-Qed. 
+Qed.
 
-Lemma prim_coupl_step_prim' `{Hcountable:Countable sch_int_σ} e n es1 σ1 α bs ζ e1 (num:nat) `{HTO: TapeOblivious sch_int_σ sch} :
-  σ1.(tapes) !! α = Some bs →
+
+Lemma prim_coupl_step_prim_sch_erasable `{Hcountable:Countable sch_int_σ} e n es1 σ1 ζ e1 (num:nat) μ `{HTO: TapeOblivious sch_int_σ sch} :
+  sch_erasable (λ t _ _ sch, TapeOblivious t sch) μ σ1 ->
   (e::es1)!!num=Some e1 ->
   to_val e = None ->
   to_val e1 = None ->
   Rcoupl
     (prim_step e1 σ1 ≫= λ '(e', s, l), sch_exec sch n (ζ, (<[num:=e']> (e::es1 ++ l), s)))
-    (state_step σ1 α ≫= (λ σ2, prim_step e1 σ2 ≫= λ '(e', s, l), sch_exec sch n (ζ, (<[num:=e']> (e::es1 ++ l), s))))
+    (μ ≫= (λ σ2, prim_step e1 σ2 ≫= λ '(e', s, l), sch_exec sch n (ζ, (<[num:=e']> (e::es1 ++ l), s))))
     eq.
 Proof.
   intros H1 H2 H3 H4.
   erewrite force_first_thread_scheduler_lemma'; try done.
   eapply Rcoupl_eq_trans.
-  - eapply prim_coupl_step_prim; last done.
-    apply force_first_thread_scheduler_tape_oblivious.
+  - erewrite <-H1; last apply force_first_thread_scheduler_tape_oblivious.
+    apply Rcoupl_eq.
   - eapply Rcoupl_dbind; last apply Rcoupl_eq.
     intros ??->.
     apply Rcoupl_eq_sym.
     rewrite force_first_thread_scheduler_lemma'; try done.
     apply Rcoupl_eq.
 Qed. 
 
+Lemma prim_coupl_step_prim' `{Hcountable:Countable sch_int_σ} e n es1 σ1 α bs ζ e1 (num:nat) `{HTO: TapeOblivious sch_int_σ sch} :
+  σ1.(tapes) !! α = Some bs →
+  (e::es1)!!num=Some e1 ->
+  to_val e = None ->
+  to_val e1 = None ->
+  Rcoupl
+    (prim_step e1 σ1 ≫= λ '(e', s, l), sch_exec sch n (ζ, (<[num:=e']> (e::es1 ++ l), s)))
+    (state_step σ1 α ≫= (λ σ2, prim_step e1 σ2 ≫= λ '(e', s, l), sch_exec sch n (ζ, (<[num:=e']> (e::es1 ++ l), s))))
+    eq.
+Proof.
+  intros H1 H2 H3 H4.
+  apply prim_coupl_step_prim_sch_erasable; try done.
+  by eapply state_step_sch_erasable.
+Qed. 

theories/con_prob_lang/lang.v

@@ -832,6 +832,168 @@ Proof.
   by rewrite (lookup_total_correct (tapes σ) α (N; ns)); last done.
 Qed.
 
+Lemma iterM_state_step_unfold σ (N p:nat) α xs :
+  σ.(tapes) !! α = Some (N%nat; xs) ->
+  (iterM p (λ σ1', state_step σ1' α) σ) =
+  dmap (λ v, state_upd_tapes <[α := (N%nat; xs ++ v)]> σ)
+    (dunifv N p).
+Proof.
+  revert σ N α xs.
+  induction p as [|p' IH].
+  { (* base case *)
+    intros. simpl.
+    apply distr_ext.
+    intros. rewrite /dret/dret_pmf{1}/pmf/=.
+    rewrite dmap_unfold_pmf.
+
+    (** Why doesnt this work?? *)
+    (* rewrite (@SeriesC_subset _ _ _ (λ x, x= (nil:list (fin (S N)))) _ _). *)
+    (* - rewrite (SeriesC_singleton_dependent nil). *)
+
+    erewrite (SeriesC_ext ).
+    - erewrite (SeriesC_singleton_dependent [] (λ a0:list (fin (S N)), dunifv N 0 a0 * (if bool_decide (a = state_upd_tapes <[α:=(N; xs ++ a0)]> σ) then 1 else 0))).
+      rewrite dunifv_pmf. simpl.
+      case_bool_decide.
+      + rewrite bool_decide_eq_true_2; [lra|]. rewrite app_nil_r.
+        rewrite state_upd_tapes_no_change; done.
+      + rewrite bool_decide_eq_false_2; [lra|]. rewrite app_nil_r.
+        rewrite state_upd_tapes_no_change; done.
+    - intros. simpl.
+      symmetry.
+      case_bool_decide; first done.
+      rewrite dunifv_pmf.
+      rewrite bool_decide_eq_false_2; first lra.
+      intros ?%nil_length_inv. done.
+  }
+  (* inductive case *)
+  intros σ N α xs Ht.
+  replace (S p') with (p'+1)%nat; last lia.
+  rewrite iterM_plus; simpl.
+  erewrite IH; last done.
+  erewrite dbind_ext_right; last first.
+  { intros. apply dret_id_right. }
+  apply distr_ext. intros σ'. rewrite dmap_unfold_pmf.
+  replace (p'+1)%nat with (S p') by lia.
+  assert (Decision (∃ v: list (fin (S N)), length v = S p' /\ σ' = state_upd_tapes <[α:=(N; xs ++ v)]> σ)) as Hdec.
+  { (* can be improved *)
+    apply make_decision. }
+  destruct (decide (∃ v: list (fin (S N)), length v = S p' /\ σ' = state_upd_tapes <[α:=(N; xs ++ v)]> σ)) as [K|K].
+  - (* σ' is reachable *)
+    destruct K as [v [Hlen ->]].
+    rewrite (SeriesC_subset (λ a, a = v)); last first.
+    { intros a Ha.
+      rewrite bool_decide_eq_false_2; first lra.
+      move => /state_upd_tapes_same. intros L. simplify_eq.
+    }
+    rewrite SeriesC_singleton_dependent. rewrite bool_decide_eq_true_2; last done.
+    rewrite dunifv_pmf. rewrite Rmult_1_r.
+    remember (/ (S N ^ S p')%nat) as val eqn:Hval.
+    rewrite /dbind/dbind_pmf{1}/pmf/=.
+    rewrite (SeriesC_subset (λ a, a = state_upd_tapes <[α := (N; xs ++ take p' v)]> σ)).
+    + rewrite SeriesC_singleton_dependent. erewrite state_step_unfold; last first.
+      { simpl. rewrite lookup_insert. done. }
+      rewrite !dmap_unfold_pmf.
+      rewrite (SeriesC_subset (λ a, a = take p' v)); last first.
+      { intros. rewrite bool_decide_eq_false_2; first lra.
+        move => /state_upd_tapes_same. intros L. simplify_eq.
+      }
+      rewrite SeriesC_singleton_dependent.
+      rewrite bool_decide_eq_true_2; last done.
+      rewrite dunifv_pmf.
+      rewrite bool_decide_eq_true_2; last first.
+      { rewrite firstn_length_le; lia. }
+      assert (is_Some (last v)) as [x Hsome].
+      { rewrite last_is_Some. intros ?. subst. done. }
+      rewrite (SeriesC_subset (λ a, a = x)); last first.
+      { intros a H'. rewrite bool_decide_eq_false_2; first lra.
+        rewrite state_upd_tapes_twice. move => /state_upd_tapes_same.
+        rewrite <-app_assoc. intros K.
+        simplify_eq. apply H'.
+        rewrite -K in Hsome.
+        rewrite last_snoc in Hsome. by simplify_eq.
+      }
+      rewrite SeriesC_singleton_dependent.
+      rewrite /dunifP dunif_pmf. rewrite bool_decide_eq_true_2; last rewrite state_upd_tapes_twice.
+      * rewrite bool_decide_eq_true_2; last done.
+        rewrite Hval.
+        cut ( / INR (S N ^ p') * (/ INR (S N)) = / INR (S N ^ S p')); first lra.
+        rewrite -Rinv_mult.
+        f_equal. rewrite -mult_INR. f_equal. simpl. lia.
+      * rewrite -app_assoc. repeat f_equal.
+        rewrite <-(firstn_all v) at 1.
+        rewrite Hlen. erewrite take_S_r; first done.
+        rewrite -Hsome last_lookup.
+        f_equal. rewrite Hlen. done.
+    + (* prove that σ' is not an intermediate step*)
+      intros σ'.
+      intros Hσ.
+      assert (dmap (λ v0, state_upd_tapes <[α:=(N; xs ++ v0)]> σ) (dunifv N p') σ' *  state_step σ' α (state_upd_tapes <[α:=(N; xs ++ v)]> σ) >= 0) as [H|H]; last done.
+      { apply Rle_ge. apply Rmult_le_pos; auto. }
+      exfalso.
+      apply Rmult_pos_cases in H as [[H1 H2]|[? H]]; last first.
+      { pose proof pmf_pos (state_step σ' α)  (state_upd_tapes <[α:=(N; xs ++ v)]> σ). lra. }
+      rewrite dmap_pos in H1.
+      destruct H1 as [v' [-> H1]].
+      apply Hσ. repeat f_equal.
+      erewrite state_step_unfold in H2; last first.
+      { simpl. apply lookup_insert. }
+      apply dmap_pos in H2.
+      destruct H2 as [a [H2?]].
+      rewrite state_upd_tapes_twice in H2.
+      apply state_upd_tapes_same in H2. rewrite -app_assoc in H2. simplify_eq.
+      rewrite take_app_length'; first done.
+      rewrite app_length in Hlen. simpl in *; lia.
+  - (* σ' is not reachable, i.e. both sides are zero *)
+    rewrite SeriesC_0; last first.
+    { intros x.
+      assert (0<=dunifv N (S p') x) as [H|<-] by auto; last lra.
+      apply Rlt_gt in H.
+      rewrite -dunifv_pos in H.
+      rewrite bool_decide_eq_false_2; [lra|naive_solver].
+    }
+    rewrite /dbind/dbind_pmf{1}/pmf/=.
+    apply SeriesC_0.
+    intros σ''.
+    rewrite /dmap/dbind/dbind_pmf{1}/pmf/=.
+    setoid_rewrite dunifv_pmf.
+    assert (SeriesC
+    (λ a : list (fin (S N)),
+       (if bool_decide (length a = p') then / (S N ^ p')%nat else 0) *
+         dret (state_upd_tapes <[α:=(N; xs ++ a)]> σ) σ'') * state_step σ'' α σ' >= 0) as [H|H]; last done.
+    { apply Rle_ge. apply Rmult_le_pos; auto. apply SeriesC_ge_0'.
+      intros. apply Rmult_le_pos; auto. case_bool_decide; try lra.
+      rewrite -Rdiv_1_l. apply Rcomplements.Rdiv_le_0_compat; first lra.
+      apply lt_0_INR.
+      epose proof Nat.pow_le_mono_r (S N) 0 p' _ _ as H0; simpl in H0; lia.
+      Unshelve.
+      all: lia.
+    }
+    apply Rmult_pos_cases in H as [[H1 H2]|[? H]]; last first.
+    { pose proof pmf_pos (state_step σ'' α) σ'. lra. }
+    epose proof SeriesC_gtz_ex _ _ H1. simpl in *.
+    destruct H as [v H].
+    apply Rmult_pos_cases in H as [[? H]|[]]; last first.
+    { epose proof pmf_pos (dret (state_upd_tapes <[α:=(N; xs ++ v)]> σ)) σ''. lra. }
+    apply dret_pos in H; subst.
+    case_bool_decide; last lra.
+    erewrite state_step_unfold in H2; last first.
+    { simpl. rewrite lookup_insert. done. }
+    exfalso.
+    apply K. rewrite dmap_pos in H2. destruct H2 as [x[-> H2]]. subst.
+    setoid_rewrite state_upd_tapes_twice.
+    rewrite -app_assoc.
+    exists (v++[x]); rewrite app_length; simpl; split; first lia. done.
+    Unshelve.
+    simpl.
+    intros. case_bool_decide; last real_solver.
+    apply Rmult_le_pos; last auto.
+    rewrite -Rdiv_1_l. apply Rcomplements.Rdiv_le_0_compat; first lra.
+    apply lt_0_INR.
+    epose proof Nat.pow_le_mono_r (S N) 0 p' _ _ as H0; simpl in H0; lia.
+    Unshelve.
+    all: lia.
+Qed.
+
 (** Basic properties about the language *)
 Global Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
 Proof. induction Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.