Semantic.CC.Safety

Convert a capture set in a platform context to a concrete capability set. Platform contexts have N capabilities arranged as pairs (C, x) at levels (0,1), (2,3), ..., (2N-2, 2N-1), where capability i corresponds to variables at levels 2i and 2i+1. Bound variables map via level / 2, while free variables directly reference heap locations.

Equations

Instances For

source

def CC.TypeEnv.platform_of (N : ℕ) :

TypeEnv (Sig.platform_of N)

Type environment for a platform with N ground capabilities. Maps each pair (C, x) to capability i at heap location i: capture variable C maps to singleton ground capture set {i}, term variable x maps to heap location i.

Equations

CC.TypeEnv.platform_of 0 = CC.TypeEnv.empty
CC.TypeEnv.platform_of n.succ = ((CC.TypeEnv.platform_of n).extend_cvar (CC.CaptureSet.var (CC.Var.free n))).extend_var n

Instances For

source

theorem CC.Heap.platform_of_wf (N : ℕ) :

(platform_of N).WfHeap

The platform heap is well-formed: it contains only capabilities, no values.

source

theorem CC.Heap.platform_of_has_fin_dom (N : ℕ) :

(platform_of N).HasFinDom (Finset.range N)

The platform heap has finite domain {0, 1, ..., N-1}.

source

def CC.Memory.platform_of (N : ℕ) :

Memory

Platform memory with N ground capabilities.

Equations

CC.Memory.platform_of N = { heap := CC.Heap.platform_of N, wf := ⋯, findom := ⋯ }

Instances For

source

theorem CC.platform_memory_subsumes {N M : ℕ} (hNM : N ≤ M) :

(Memory.platform_of M).subsumes (Memory.platform_of N)

Platform memory M subsumes platform memory N when M ≥ N.

source

theorem CC.env_typing_platform_monotonic {s : Sig} {Γ : Ctx s} {env : TypeEnv s} {N M : ℕ} (hNM : N ≤ M) (ht : EnvTyping Γ env (Memory.platform_of N)) :

EnvTyping Γ env (Memory.platform_of M)

EnvTyping for platform is monotonic: platform N types in platform M memory when M ≥ N.

source

theorem CC.env_typing_of_platform {N : ℕ} :

EnvTyping (Ctx.platform_of N) (TypeEnv.platform_of N) (Memory.platform_of N)

source

def CC.Exp.SafeWithPlatform (e : Exp ∅) (N : ℕ) (P : CapabilitySet) :

Prop

An expression e is safe with a platform environment of N ground capabilities under permission P iff for any possible reduction state starting from e on the platform, it is progressive.

Equations

e.SafeWithPlatform N P = ∀ (M1 : CC.Memory) (e1 : CC.Exp ∅), CC.Reduce P (CC.Memory.platform_of N) e M1 e1 → CC.IsProgressive P M1 e1

Instances For

source

theorem CC.reachability_of_loc_platform {N l : ℕ} (hl : l < N) :

reachability_of_loc (Heap.platform_of N) l = {l}

Reachability of a location in platform heap is just the singleton set.

source

theorem CC.Sig.platform_of_length {N : ℕ} :

List.length (platform_of N) = 2 * N

The length of a platform signature is 2*N.

source

theorem CC.TypeEnv.lookup_var_platform {N : ℕ} {x : BVar (Sig.platform_of N) Kind.var} :

(platform_of N).lookup_var x = x.level / 2

Lookup of term variable in platform environment.

source

theorem CC.TypeEnv.lookup_cvar_platform {N : ℕ} {c : BVar (Sig.platform_of N) Kind.cvar} :

(platform_of N).lookup_cvar c = CaptureSet.var (Var.free (c.level / 2))

Lookup of capture variable in platform environment.

source

theorem CC.BVar.level_var_bound {N : ℕ} {b : BVar (Sig.platform_of N) Kind.var} :

b.level / 2 < N

For any bound term variable in a platform signature, its level divided by 2 is less than N.

source

theorem CC.BVar.level_cvar_bound {N : ℕ} {c : BVar (Sig.platform_of N) Kind.cvar} :

c.level / 2 < N

For any bound capture variable in a platform signature, its level divided by 2 is less than N.

source

theorem CC.capture_set_denot_eq_platform {N : ℕ} {C : CaptureSet (Sig.platform_of N)} (hwf : C.WfInHeap (Heap.platform_of N)) :

CaptureSet.denot (TypeEnv.platform_of N) C (Memory.platform_of N) = C.to_platform_capability_set

The denotation of a capture set in the platform environment equals its direct capability set translation, provided the capture set is well-formed.

source

theorem CC.adequacy_platform {N : ℕ} {C : CaptureSet (Sig.platform_of N)} {E : Ty TySort.exi (Sig.platform_of N)} {e : Exp (Sig.platform_of N)} (ht : C # Ctx.platform_of N ⊨ e : E) (hclosed : C.IsClosed) :

(e.subst (Subst.from_TypeEnv (TypeEnv.platform_of N))).SafeWithPlatform N C.to_platform_capability_set

Adequacy of semantic typing on platform contexts. Requires that the capture set is closed (contains no free variables).