IamExplainer.Proofs

Policy.removeStmt — ⚪ definition

def · source

Soundness theorems: policy transforms (T1-T3) and emitFixed can only narrow access, never grant new permissions. All theorems are universally quantified over the condition context.

def Policy.removeStmt (p : Policy) (i : Nat) : Policy

iamSem — ⚪ definition

def · source

def iamSem : PolicySem Statement Request CondContext where

removeAllow_narrows — 🟢 proved

theorem · source

theorem removeAllow_narrows (p : Policy) (i : Nat)
    (hi : i < p.statements.length)
    (heff : (p.statements[i]'hi).effect = .allow)
    (req : Request) (ctx : CondContext)
    (h : allows (p.removeStmt i) req ctx = true) :

matchPattern_ci_congr — 🟢 proved

theorem · source

theorem matchPattern_ci_congr (p s s' : String)
    (h : matchActionPattern p s = true) (heq : ciEq s s' = true) :
    matchActionPattern p s' = true

stmtGrantsAction_ci_congr — 🟢 proved

theorem · source

theorem stmtGrantsAction_ci_congr (st : Statement) (ℓ a : String)
    (h : stmtGrantsAction st ℓ = true) (heq : ciEq ℓ a = true) :
    stmtGrantsAction st a = true

stmtGrantsAction_narrow — 🟢 proved

theorem · source

theorem stmtGrantsAction_narrow (s new_stmt : Statement)
    (hnew_notactions : new_stmt.notActions = none)
    (hnew_actions : ∃ acts, new_stmt.actions = some acts ∧

allows_replaceAllow_mono — 🟢 proved

theorem · source

theorem allows_replaceAllow_mono (p : Policy) (i : Nat) (hi : i < p.statements.length)
    (heff : (p.statements[i]).effect = .allow)
    (new_stmt : Statement) (hnew_eff : new_stmt.effect = .allow)
    (hnew_res : new_stmt.resources = (p.statements[i]).resources)
    (hnew_notres : new_stmt.notResources = (p.statements[i]).notResources)
    (hnew_cond : new_stmt.condition = (p.statements[i]).condition)
    (hgrants : ∀ a, stmtGrantsAction new_stmt a = true → stmtGrantsAction (p.statements[i]) a = true)
    (req : Request) (ctx : CondContext)
    (h : allows { p with statements

narrowActions_narrows — 🟢 proved

theorem · source

theorem narrowActions_narrows
    (p : Policy) (i : Nat)
    (hi : i < p.statements.length)
    (heff : (p.statements[i]).effect = .allow)
    (new_stmt : Statement)
    (hnew : new_stmt.effect = .allow)
    (hnew_notactions : new_stmt.notActions = none)
    (hnew_actions : ∃ acts, new_stmt.actions = some acts ∧

allows_replace_stmt_mono — 🟢 proved

theorem · source

Generalized statement replacement mono

theorem allows_replace_stmt_mono (p : Policy) (i : Nat) (hi : i < p.statements.length)
    (heff : (p.statements[i]).effect = .allow)
    (new_stmt : Statement) (hnew_eff : new_stmt.effect = .allow)
    (hnew_cond : new_stmt.condition = (p.statements[i]).condition)
    (hmono : ∀ req, stmtMatches new_stmt req = true → stmtMatches (p.statements[i]) req = true)
    (req : Request) (ctx : CondContext)
    (h : allows { p with statements

narrowResources_narrows — 🟢 proved

theorem · source

NEW: narrowResources_narrows (T3)

theorem narrowResources_narrows
    (p : Policy) (i : Nat)
    (hi : i < p.statements.length)
    (heff : (p.statements[i]).effect = .allow)
    (new_stmt : Statement) (hnew_eff : new_stmt.effect = .allow)
    (hnew_act : new_stmt.actions = (p.statements[i]).actions)
    (hnew_notact : new_stmt.notActions = (p.statements[i]).notActions)
    (hnew_cond : new_stmt.condition = (p.statements[i]).condition)
    (hnew_notres : new_stmt.notResources = none)
    (hnew_res : ∃ rlist, new_stmt.resources = some rlist ∧

emitFixed_narrows — 🟢 proved

theorem · source

theorem emitFixed_narrows (p : Policy) (ns : Needs)
    (hns : ∀ n ∈ ns.needs, '?' ∉ n.action.toList ∧ '*' ∉ n.action.toList)
    (req : Request) (ctx : CondContext)
    (h : allows (emitFixed p ns).1 req ctx = true) :
    allows p req ctx = true

grants_complete — 🟢 proved

theorem · source

Grants completeness and no-context conservatism

theorem grants_complete (p : Policy) (req : Request) (ctx : CondContext)
    (h : allows p req ctx = true) :

allows_nocontext_conservative — 🟢 proved

theorem · source

theorem allows_nocontext_conservative (p : Policy) (req : Request) (ctx : CondContext)
    (h : allows p req ctx = true) :

layers_narrow — 🟢 proved

theorem · source

Layer theorems: layered evaluation only narrows access.

theorem layers_narrow (p : Policy) (req : Request) (ctx : CondContext)
    (layers : Layers) (rcpSvcs : List String) (kind : DocKind)
    (h : (allowsLayered p req ctx layers rcpSvcs kind).allowed = true) :
    allows p req ctx = true

layer_add_monotone — 🟢 proved

theorem · source

theorem layer_add_monotone (p : Policy) (req : Request) (ctx : CondContext)
    (rcpSvcs : List String) (kind : DocKind)
    (h : allows p req ctx = true) :
    (allowsLayered p req ctx noLayers rcpSvcs kind).allowed = true

layered_nocontext_conservative — 🟢 proved

theorem · source

theorem layered_nocontext_conservative (p : Policy) (req : Request) (ctx : CondContext)
    (layers : Layers) (rcpSvcs : List String) (kind : DocKind)
    (h : (allowsLayered p req ctx layers rcpSvcs kind).allowed = true) :
    (allowsLayered p req noContext layers rcpSvcs kind).allowed = true