From dfc299f41cbb591288228e2287649fb609210984 Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Mon, 16 Sep 2024 11:58:42 -0400 Subject: [PATCH] add urand and utapes --- theories/meas_lang/lang.v | 74 +++++++++++++++++++++++++++++---------- 1 file changed, 56 insertions(+), 18 deletions(-) diff --git a/theories/meas_lang/lang.v b/theories/meas_lang/lang.v index eaf93f87..6be6ff2b 100644 --- a/theories/meas_lang/lang.v +++ b/theories/meas_lang/lang.v @@ -7,7 +7,7 @@ From clutch.prob Require Export distribution. From clutch.common Require Export language ectx_language ectxi_language locations. From iris.prelude Require Import options. From HB Require Import structures. -From mathcomp Require Import ssrbool all_algebra finmap. +From mathcomp Require Import ssrbool eqtype fintype choice all_algebra finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality fsbigop. From mathcomp.analysis Require Import reals ereal signed normedtype sequences esum numfun measure lebesgue_measure lebesgue_integral. @@ -18,6 +18,8 @@ From clutch.prob_lang Require Import lang. Delimit Scope expr_scope with E. Delimit Scope val_scope with V. +Global Instance classical_eq_dec {T : Type} : EqDecision T. +Proof. intros ? ?; apply ClassicalEpsilon.excluded_middle_informative. Defined. Module meas_lang. @@ -62,9 +64,12 @@ Inductive expr := | AllocN (e1 e2 : expr) (* Array length and initial value *) | Load (e : expr) | Store (e1 : expr) (e2 : expr) - (* Probabilistic choice *) + (* Finite probabilistic choice *) | AllocTape (e : expr) | Rand (e1 e2 : expr) + (* Real probabilistic choice *) + | AllocUTape (e : expr) + | URand (e1 e2 : expr) (* No-op operator used for cost *) | Tick (e : expr) with val := @@ -85,10 +90,12 @@ Definition to_val (e : expr) : option val := | _ => None end. -(* MARKUSDE: This will be the only part of the sigma algebra which is not discrete *) +(* This part of the sigma algebra is not discrete *) (* MARKUSDE: Externalizing the fin bound here also simplifies definitions *) Definition history : Type := nat -> option nat. + +(* Tapes in the computable fragment *) Record tape : Type := { tape_bound : nat; tape_state : nat; @@ -178,20 +185,27 @@ Definition tapeHasEventually (t : tape) (l : list nat) : Prop Global Instance tape_inhabited : Inhabited tape := populate (emptyTape 0). - -Global Instance classical_eq_dec {T : Type} : EqDecision T. -Proof. intros ? ?; apply ClassicalEpsilon.excluded_middle_informative. Defined. - - Global Instance tapes_lookup_total : LookupTotal loc tape (gmap loc tape). Proof. apply map_lookup_total. Defined. Global Instance tapes_insert : Insert loc tape (gmap loc tape). Proof. apply map_insert. Defined. -(** The state: a [loc]-indexed heap of [val]s, and [loc]-indexed tapes of fins. *) + +(* Tapes for the real-valued fragment *) +Definition utape : Type := list R. +Global Instance utape_inhabited : Inhabited utape := populate []. +Global Instance utapes_lookup_total : LookupTotal loc utape (gmap loc utape). +Proof. apply map_lookup_total. Defined. +Global Instance utapes_insert : Insert loc utape (gmap loc utape). +Proof. apply map_insert. Defined. + + + +(** The state: a [loc]-indexed heap of [val]s, and [loc]-indexed tapes, and [loc]-indexed utapes *) Record state : Type := { - heap : gmap loc val; - tapes : gmap loc tape + heap : gmap loc val; + tapes : gmap loc tape; + utapes : gmap loc utape }. (** Equality and other typeclass stuff *) @@ -206,7 +220,7 @@ Proof. intros ??. congruence. Qed. Global Instance state_inhabited : Inhabited state := - populate {| heap := inhabitant; tapes := inhabitant |}. + populate {| heap := inhabitant; tapes := inhabitant; utapes := inhabitant |}. Global Instance val_inhabited : Inhabited val := populate (LitV LitUnit). Global Instance expr_inhabited : Inhabited expr := populate (Val inhabitant). @@ -237,8 +251,11 @@ Inductive ectx_item := | StoreLCtx (v2 : val) | StoreRCtx (e1 : expr) | AllocTapeCtx + | AllocUTapeCtx | RandLCtx (v2 : val) | RandRCtx (e1 : expr) + | URandLCtx (v2 : val) + | URandRCtx (e1 : expr) | TickCtx. Definition fill_item (Ki : ectx_item) (e : expr) : expr := @@ -262,8 +279,11 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr := | StoreLCtx v2 => Store e (Val v2) | StoreRCtx e1 => Store e1 e | AllocTapeCtx => AllocTape e + | AllocUTapeCtx => AllocUTape e | RandLCtx v2 => Rand e (Val v2) | RandRCtx e1 => Rand e1 e + | URandLCtx v2 => URand e (Val v2) + | URandRCtx e1 => URand e1 e | TickCtx => Tick e end. @@ -306,11 +326,17 @@ Definition decomp_item (e : expr) : option (ectx_item * expr) := | _ => Some (StoreRCtx e1, e2) end | AllocTape e => noval e AllocTapeCtx + | AllocUTape e => noval e AllocUTapeCtx | Rand e1 e2 => match e2 with | Val v => noval e1 (RandLCtx v) | _ => Some (RandRCtx e1, e2) end + | URand e1 e2 => + match e2 with + | Val v => noval e1 (URandLCtx v) + | _ => Some (URandRCtx e1, e2) + end | Tick e => noval e TickCtx | _ => None end. @@ -336,14 +362,15 @@ Fixpoint subst (x : string) (v : val) (e : expr) : expr := | Load e => Load (subst x v e) | Store e1 e2 => Store (subst x v e1) (subst x v e2) | AllocTape e => AllocTape (subst x v e) + | AllocUTape e => AllocUTape (subst x v e) | Rand e1 e2 => Rand (subst x v e1) (subst x v e2) + | URand e1 e2 => URand (subst x v e1) (subst x v e2) | Tick e => Tick (subst x v e) end. Definition subst' (mx : binder) (v : val) : expr → expr := match mx with BNamed x => subst x v | BAnon => λ x, x end. - (** The stepping relation *) Definition un_op_eval (op : un_op) (v : val) : option val := match op, v with @@ -421,13 +448,17 @@ Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val := end. Definition state_upd_heap (f : gmap loc val → gmap loc val) (σ : state) : state := - {| heap := f σ.(heap); tapes := σ.(tapes) |}. + {| heap := f σ.(heap); tapes := σ.(tapes); utapes := σ.(utapes) |}. Global Arguments state_upd_heap _ !_ /. Definition state_upd_tapes (f : gmap loc tape → gmap loc tape) (σ : state) : state := - {| heap := σ.(heap); tapes := f σ.(tapes) |}. + {| heap := σ.(heap); tapes := f σ.(tapes); utapes := σ.(utapes) |}. Global Arguments state_upd_tapes _ !_ /. +Definition state_upd_utapes (f : gmap loc utape → gmap loc utape) (σ : state) : state := + {| heap := σ.(heap); tapes := σ.(tapes); utapes := f σ.(utapes) |}. +Global Arguments state_upd_utapes _ !_ /. + Lemma state_upd_tapes_twice σ l xs ys : state_upd_tapes <[ l := ys ]> (state_upd_tapes <[ l := xs ]> σ) = state_upd_tapes <[ l:= ys ]> σ. Proof. rewrite /state_upd_tapes /=. f_equal. apply insert_insert. Qed. @@ -548,7 +579,7 @@ Qed. #[local] Open Scope R. -(* + Section pointed_instances. Local Open Scope classical_set_scope. (** states are pointed *) @@ -641,6 +672,10 @@ Section meas_semantics. | Some v => giryM_ret R ((Val $ LitV LitUnit, state_upd_heap <[l:=w]> σ1) : <>) | None => giryM_zero end + + (* FIXME: Finish implementation for tapes *) + + (* (* Uniform sampling from [0, 1 , ..., N] *) | Rand (Val (LitV (LitInt N))) (Val (LitV LitUnit)) => giryM_map @@ -649,7 +684,8 @@ Section meas_semantics. | AllocTape (Val (LitV (LitInt z))) => let ι := fresh_loc σ1.(tapes) in giryM_ret R ((Val $ LitV $ LitLbl ι, state_upd_tapes <[ι := (fin (Z.to_nat z; [])) ]> σ1) : <>) - (* FIXME: Decide on the representation and semantics of infinite tapes *) + *) + (* (* Labelled sampling, conditional on tape contents *) | Rand (Val (LitV (LitInt N))) (Val (LitV (LitLbl l))) => @@ -685,9 +721,10 @@ Section meas_semantics. Definition head_stepM : measurable_map <> (giryM <>) := m_discr head_stepM_def. - (* Instead, we may consider restructing the semantics to use 'I_m instead of (fin m) *) + (* Instead, we may consider restructing the semantics to use 'I_m instead of (fin m) Definition fin_of_Im (m : nat) : 'I_m -> stdpp.fin.fin m. Admitted. + *) Definition state_stepM_def (c : state * loc) : giryM (<>) := let (σ1, α) := c in @@ -707,6 +744,7 @@ Section meas_semantics. End meas_semantics. +(* (* Lemma state_step_unfold σ α N ns: tapes σ !! α = Some (N; ns) ->