IamExplainer.Layers

Layers — ⚪ definition

structure · source

structure Layers where

LayerVerdict — ⚪ definition

structure · source

structure LayerVerdict where

LayerResult — ⚪ definition

structure · source

structure LayerResult where

evalLayers — ⚪ definition

def · source

def evalLayers (req : Request) (ctx : CondContext) (layers : Layers)
    (rcpServices : List String) (kind : DocKind) : LayerResult

noLayers — ⚪ definition

def · source

def noLayers : Layers

validateScp — ⚪ definition

def · source

def validateScp (p : Policy) : Option String

validateRcp — ⚪ definition

def · source

def validateRcp (p : Policy) : Option String

evalLayers_noLayers_blocked — 🟢 proved

theorem · source

theorem evalLayers_noLayers_blocked (req : Request) (ctx : CondContext)
    (rcpSvcs : List String) (kind : DocKind) :
    (evalLayers req ctx noLayers rcpSvcs kind).blocked = []

evalLayers_blocked_noContext_empty — 🟢 proved

theorem · source

theorem evalLayers_blocked_noContext_empty (req : Request) (ctx : CondContext)
    (layers : Layers) (rcpSvcs : List String) (kind : DocKind)
    (h : (evalLayers req ctx layers rcpSvcs kind).blocked = []) :
    (evalLayers req noContext layers rcpSvcs kind).blocked = []