Theorem Catalog
33 proved · 0 sorry · 33 total
Condition Key Evaluation (IamExplainer.Condition)
| Status | Name | Description |
|---|---|---|
| 🟢 proved | evalCond_noContext_T_imp | |
| 🟢 proved | evalCond_noContext_tu |
SCPs, Permission Boundaries, and RCPs (IamExplainer.Layers)
| Status | Name | Description |
|---|---|---|
| 🟢 proved | evalLayers_blocked_noContext_empty | |
| 🟢 proved | evalLayers_noLayers_blocked |
End-to-End IAM Authorization Proofs (IamExplainer.Proofs)
| Status | Name | Description |
|---|---|---|
| 🟢 proved | allows_nocontext_conservative | |
| 🟢 proved | allows_replaceAllow_mono | |
| 🟢 proved | allows_replace_stmt_mono | Generalized statement replacement mono |
| 🟢 proved | emitFixed_narrows | |
| 🟢 proved | grants_complete | Grants completeness and no-context conservatism |
| 🟢 proved | layer_add_monotone | |
| 🟢 proved | layered_nocontext_conservative | |
| 🟢 proved | layers_narrow | Layer theorems: layered evaluation only narrows access. |
| 🟢 proved | matchPattern_ci_congr | |
| 🟢 proved | narrowActions_narrows | |
| 🟢 proved | narrowResources_narrows | NEW: narrowResources_narrows (T3) |
| 🟢 proved | removeAllow_narrows | |
| 🟢 proved | stmtGrantsAction_ci_congr | |
| 🟢 proved | stmtGrantsAction_narrow |
Policy Evaluation Semantics (Seclib.Domain.PolicySem)
| Status | Name | Description |
|---|---|---|
| 🟢 proved | filterMap_narrows | |
| 🟢 proved | grants_complete | grants_complete: if allowed, an Allow statement exists that matches |
| 🟢 proved | narrow_narrows | narrow_narrows: replacing a statement with one that matches fewer requests narro |
| 🟢 proved | nocontext_conservative | nocontext_conservative: if allowed under any context, allowed under noCtx |
| 🟢 proved | removeAllow | removeAllow: removing an Allow statement narrows access |
Action and Resource Pattern Matching (Seclib.Prim.Glob)
| Status | Name | Description |
|---|---|---|
| 🟢 proved | ciEq_toLowerStr | |
| 🟢 proved | matchPatternGo_literal_eq | |
| 🟢 proved | matchPattern_cs_literal_eq | |
| 🟢 proved | matchPattern_literal_mp | |
| 🟢 proved | toLower_eq_question | |
| 🟢 proved | toLower_eq_star |
Statement Combining — Deny Overrides (Seclib.Prim.Rule)
| Status | Name | Description |
|---|---|---|
| 🟢 proved | appliesOf_unknown_conservative | Lemma 4: Unknown applicability is conservative |
| 🟢 proved | conj_narrows | Lemma 3: Conjunction of evaluation gates never widens access |
| 🟢 proved | denyOverrides_add_deny_narrows | Lemma 2: Adding a deny narrows |
| 🟢 proved | denyOverrides_remove_allow_narrows | Lemma 1: Removing an allow rule narrows access |