Post 12 — Final Model and Invariants

The Problem: When "Reasonable" Implementations Diverge

Over the past 11 posts, we've built a complete authorization model: relationship-based access control (Posts 1-4), attribute-based conditions (Posts 5-7), schema-level safety (Post 8), determinism (Post 9), fail-safe defaults (Post 10), and snapshot isolation (Post 11).

But there's one final critical requirement: semantic precision.

Here's the problem: Two engineers can read the same model and build different implementations that both seem correct—but produce different results.

Real-world examples where this matters:

Google Zanzibar: Published a formal semantics paper so other teams could build compatible systems
OAuth 2.0: RFC 6749 defines exact token lifecycle semantics—before this, providers diverged on expiration behavior
Kubernetes RBAC: API specification with conformance tests ensures GKE and EKS behave identically
OpenID Connect: Specification enables interoperability across hundreds of identity providers

What we need:

❝

"Two independent implementations of Enma, given the same tuples, schema, caveats, revision, and context, must return the same result—always, everywhere, forever."

This post freezes Enma's semantics with 16 core invariants that define exact behavior for every edge case.

Human Rule

❝

"Same inputs, same outputs—always, everywhere, forever."

This is the golden rule of authorization: deterministic, reproducible, verifiable evaluation.

Why do we need this?

Let's examine what happens without a formal specification.

Scenario: Two Teams Implement Enma

Team A (Backend Engineers):

// Their interpretation: Evaluate UNION left-to-right, short-circuit on TRUE
func evaluateUnion(children []Node) Result {
    for _, child := range children {
        result := evaluate(child)
        if result == TRUE {
            return TRUE  // Short-circuit
        }
    }
    return FALSE
}

Team B (Security Engineers):

// Their interpretation: Evaluate all children, pick best result
func evaluateUnion(children []Node) Result {
    results := []Result{}
    for _, child := range children {
        results = append(results, evaluate(child))
    }
    return pickBestResult(results)  // TRUE > REQUIRES_CONTEXT > FALSE
}

Problem: Both interpretations seem reasonable, but they produce different results when caveats are involved:

// Schema: viewer = direct ∪ computed(editor)
// Tuple 1: document:1#viewer → user:alice [business_hours]
// Tuple 2: document:1#editor → user:alice [no caveat]

// Check(document:1#viewer, user:alice) with NO context:

// Team A (short-circuit):
// 1. Evaluate direct → REQUIRES_CONTEXT (missing business_hours)
// 2. Evaluate computed(editor) → TRUE
// 3. Short-circuit on TRUE
// Result: TRUE ✅

// Team B (evaluate all):
// 1. Evaluate direct → REQUIRES_CONTEXT (missing business_hours)
// 2. Evaluate computed(editor) → TRUE
// 3. Pick best: TRUE > REQUIRES_CONTEXT
// Result: TRUE ✅

// Both agree here, but...

Now reverse the schema order:

// Schema: viewer = computed(editor) ∪ direct
// Same tuples, same query

// Team A (short-circuit):
// 1. Evaluate computed(editor) → TRUE
// 2. Short-circuit immediately
// Result: TRUE ✅

// Team B (evaluate all):
// 1. Evaluate computed(editor) → TRUE
// 2. Evaluate direct → REQUIRES_CONTEXT
// 3. Pick best: TRUE > REQUIRES_CONTEXT
// Result: TRUE ✅

// Still agree, but what about this case...

Note: Both teams agree in the above cases because TRUE dominates REQUIRES_CONTEXT. The real divergence happens when all children return REQUIRES_CONTEXT—then we need to decide which missing parameters to return.

Edge case: Multiple REQUIRES_CONTEXT results:

// Schema: viewer = direct ∪ computed(editor) ∪ computed(owner)
// Tuple 1: document:1#viewer → user:alice [business_hours]
// Tuple 2: document:1#editor → user:alice [ip_restriction]
// Tuple 3: document:1#owner → user:alice [mfa_verified]

// Check(document:1#viewer, user:alice) with NO context:

// Team A (short-circuit):
// 1. Evaluate direct → REQUIRES_CONTEXT([business_hours])
// 2. Evaluate computed(editor) → REQUIRES_CONTEXT([ip_restriction])
// 3. Evaluate computed(owner) → REQUIRES_CONTEXT([mfa_verified])
// 4. No TRUE found, return... which REQUIRES_CONTEXT?
// Result: ??? (undefined behavior)

// Team B (evaluate all):
// 1. Collect all results: [REQUIRES_CONTEXT, REQUIRES_CONTEXT, REQUIRES_CONTEXT]
// 2. Pick minimal missing params: [business_hours] (1 param)
// Result: REQUIRES_CONTEXT([business_hours]) ✅

// Now they DISAGREE!

The problem: Without a formal specification, reasonable interpretations diverge.

Design Intention: Frozen Semantics

We need a specification that:

Defines exact evaluation rules — No ambiguity in edge cases
Enumerates all invariants — Complete list of guarantees
Specifies minimal interface — What implementations must provide
Documents algebraic laws — Safe optimizations and transformations

Key insight: The specification is separate from implementation. Multiple implementations can exist (in-memory, distributed, optimized), but all must satisfy the same semantics.

Architectural Decision: Core Semantics Document

We formalize the model in a Core Semantics Specification that serves as the single source of truth.

Design Principles

Deterministic — Same inputs always produce same outputs
Bounded — All operations have finite cost
Snapshot-isolated — Entire evaluation at one revision
Type-safe — Compile-time schema validation
Fail-safe — Invalid data is ignored, not errored

These principles guide every design decision and ensure production-readiness.

Model Design: The 16 Core Invariants

Here's the complete list of invariants that define Enma's semantics. These are non-negotiable guarantees that every implementation must uphold.

Phase I: Schema & Type System (INV-1 to INV-4)

INV-1: Relation Identity

Relation identity is (namespace, relation). Renames create new identities; no aliasing at runtime.

Why: Ensures stable indices and Expand results across schema evolution.

Example:

// Renaming a relation creates a NEW relation
// Old: document#viewer
// New: document#reader
// These are DIFFERENT relations, not aliases

INV-2: No Resource Wildcards

Wildcards are ONLY for subjects, never resources.

Why: Keeps Check decidable and bounded. To grant access to "all documents," use hierarchical relationships (folders, organizations) with OP_EDGE.

Example:

// ❌ INVALID: document:*#viewer → user:alice
// ✅ VALID: folder:shared#viewer → user:alice
//           document:1#viewer = edge(parent → folder#viewer)

INV-3: Schema Closure

Every OP_COMPUTED_SUBJECTS(rel) and OP_EDGE(EdgeFrom, EdgeTo) must reference existing relations. Verified at compile time.

Why: Prevents runtime errors from dangling references.

Example:

// ❌ INVALID: viewer = computed(nonexistent_relation)
// ✅ VALID: viewer = computed(editor)  // editor exists in schema

INV-4: Allowed Kinds Mask

Each relation explicitly lists which subject types are admissible: {DirectSubject, SubjectSet, WildcardSubject}. Tuples with other kinds are ignored at evaluation time (not errored).

Why: Graceful handling of invalid data after schema changes.

Example:

// Schema: document#viewer allows only DirectSubject{user}
// Tuple: document:1#viewer → role:admin#member  // SubjectSet
// Behavior: IGNORED during evaluation (not errored)

Phase II: Evaluation Semantics (INV-5 to INV-8)

INV-5: Single Snapshot Evaluation

Check evaluates an entire proof at ONE revision (single snapshot). All node reads and caveat evaluations in that Check share the same revision.

Why: Prevents time-of-check-time-of-use (TOCTOU) anomalies, especially in OP_EXCLUSION.

Example:

// Check(document:1#viewer, user:alice) at revision 100
// ALL tuple reads happen at revision 100
// Even if writes occur during evaluation, they're invisible

INV-6: Non-Monotonicity

OP_EXCLUSION makes the algebra non-monotonic. Adding tuples can remove access.

Why: Exclusion is inherently non-monotonic. Child subtrees of exclusion are evaluated at the same revision (see INV-5).

Example:

// viewer = direct − computed(blocked)
// Adding tuple to blocked REMOVES access

INV-7: No SubjectSet Expansion During Check

Direct query does NOT match a SubjectSet candidate. Check does not implicitly expand SubjectSets.

Why: Keeps Check bounded and predictable. Use OP_EDGE for indirection.

Example:

// Tuple: document:1#viewer → role:admin#member
// Check(document:1#viewer, user:alice) → FALSE
// (Does NOT expand role:admin#member to see if alice is a member)

// Correct modeling:
// viewer = direct ∪ edge(admin_role → role:admin#member)

INV-8: Invalid Tuples Are Ignored

When a tuple's subject violates SubjectConstraints for the current relation, IGNORE that tuple (treat as absent).

Why: Ensures old tuples don't break evaluation after schema changes. Evaluation is deterministic (no partial failures).

Example:

// Schema: document#viewer allows only DirectSubject{user}
// Tuple: document:1#viewer → role:admin#member  // Violates constraints
// Behavior: IGNORED (not errored)

Phase III: Caveat Semantics (INV-9 to INV-11)

INV-9: Parameter Naming Convention

Establish naming conventions to avoid collisions and clarify authoring:

Prefix	Purpose	Example
`{namespace}.*`	Attributes of that namespace	`user.department`, `document.classification`
`env.*`	Environment context	`env.current_hour`, `env.user_ip`
`request.*`	Request metadata	`request.method`, `request.path`

Why: Makes caveats self-documenting and prevents parameter name collisions.

Note: This is a design convention, not a technical requirement. The system doesn't interpret parameter names.

INV-10: Function Registry

Caveat functions are:

Pure — No side effects
Deterministic — Same inputs → same outputs
Total — Must return T/F/R, never throw/panic
Bounded — Finite execution time

Why: Ensures deterministic, reproducible evaluation.

Invalid functions: Network calls, database queries, random number generation, current time (use env.current_time parameter instead).

INV-11: RequiredCaveat Composition

Effective caveat = RequiredCaveat AND TupleCaveat.

Rules:

If RequiredCaveat is present and tuple has NO caveat: EffectiveCaveat = RequiredCaveat
If both exist and both produce REQUIRES_CONTEXT: MissingParams = RequiredMissing ∪ TupleMissing

Why: Enforces mandatory policies at schema level while allowing tuple-specific conditions.

Phase IV: Determinism (INV-12 to INV-13)

INV-12: UNION Tie-Breaking

If multiple REQUIRES_CONTEXT children have the same cardinality of missing params, pick first in schema order.

Why: Ensures deterministic results across all evaluators.

Example:

// viewer = direct ∪ computed(editor) ∪ computed(owner)
// All return REQUIRES_CONTEXT with 1 missing param
// Result: Pick first in schema order (direct)

INV-13: INTERSECTION Tie-Breaking

If multiple intersection paths exist with different missing sets, pick the minimal-cardinality result. If tie, pick first in schema order.

Why: Ensures deterministic results and minimal context requirements.

Invariant Dependencies

Some invariants build on others. Understanding these dependencies helps with implementation order:

Invariant	Depends On	Why
INV-5 (Snapshot)	INV-1 (Identity)	Needs stable relation IDs across evaluation
INV-6 (Non-monotonic)	INV-5 (Snapshot)	Exclusion requires snapshot isolation to be safe
INV-8 (Ignore invalid)	INV-4 (Allowed kinds)	Needs constraints to determine what's invalid
INV-11 (RequiredCaveat)	INV-10 (Function registry)	Composition requires deterministic functions
INV-12 (UNION tie-break)	INV-9 (Naming)	Needs to compare parameter sets by name
INV-13 (INTERSECTION tie-break)	INV-12	Same tie-breaking strategy, minimal cardinality
INV-15 (Canonical signature)	INV-5 (Snapshot)	Cycle detection at one revision, no revision in key
INV-16 (Unknown caveat)	INV-10 (Function registry)	Needs registry to detect missing caveats

Implementation order: Start with Phase I (Schema), then Phase II (Evaluation), then add Phases III-VI incrementally.

Phase V: Wildcard & Cycle Detection (INV-14 to INV-15)

INV-14: Per-Candidate Wildcard Evaluation

Wildcard subject caveats evaluate PER matched candidate.

Why: Same tuple, different query subjects → different caveat evaluations.

Example:

// Tuple: document:1#viewer → user:* [department_match]
// Caveat: user.department == document.department

// Check(document:1#viewer, user:alice):
// - Evaluate caveat with alice's department
// - Result: TRUE if alice.department == document.department

// Check(document:1#viewer, user:bob):
// - Evaluate caveat with bob's department
// - Result: TRUE if bob.department == document.department

INV-15: Canonical Subject Signature

Use canonical form that collapses equivalent representations:

Subject Type	Canonical Signature
DirectSubject	`direct:{namespace}:{objectID}`
SubjectSet	`set:{namespace}:{objectID}#{relation}`
WildcardSubject	`wildcard:{namespace}`

Why: Ensures cycle detection works correctly across equivalent representations.

Note: Do NOT include revision—all evaluation is at one snapshot (INV-5).

Phase VI: Fail-Safe Defaults (INV-16)

INV-16: Unknown Caveat Handling

If a tuple references a caveat that doesn't exist in the schema, treat the tuple as if it had CAVEAT_FALSE.

Why: Fail-safe default. Schema evolution (removing caveats) doesn't accidentally grant access.

Example:

// Tuple: document:1#viewer → user:alice [old_caveat]
// Schema: old_caveat no longer exists
// Behavior: Treat as CAVEAT_FALSE (deny access)

Implementation: Minimal Interface Surface

To implement Enma, you need to provide these four interfaces:

1. TupleReader

type TupleReader interface {
    // Read tuples matching (resource, *, *) at given revision
    ReadTuples(
        resource *ObjectAndRelation,
        revision *Revision,
    ) ([]*RelationTuple, error)
}

Purpose: Provide tuple storage abstraction.

Implementations: In-memory map, SQL database, distributed KV store.

2. SchemaRepo

type SchemaRepo interface {
    // Get compiled schema at given revision
    GetSchema(revision *Revision) (*CompiledSchema, error)
}

Purpose: Provide schema storage abstraction.

Implementations: In-memory cache, versioned storage, schema registry.

3. CaveatRegistry

type CaveatRegistry interface {
    // Evaluate caveat with given context
    Evaluate(
        caveatName string,
        context *CaveatContext,
    ) (CaveatEvalResult, error)
}

Purpose: Provide caveat evaluation abstraction.

Implementations: Expression evaluator, compiled bytecode, JIT compiler.

4. RevisionSource

type RevisionSource interface {
    // Get current revision
    GetCurrentRevision() (*Revision, error)

    // Get revision at or after given revision
    GetRevisionAtLeast(minRevision *Revision) (*Revision, error)
}

Purpose: Provide revision tracking abstraction.

Implementations: Hybrid Logical Clock, Lamport timestamp, database sequence.

Happy Path Example: Complete Evaluation

Let's trace a complete Check evaluation through all invariants:

Scenario: Document Access with Hierarchies and Caveats

Schema:

namespace document {
    relation parent: folder
    relation owner: user
    relation editor: user
    relation viewer: user | user:*

    permission view = viewer ∪ computed(editor) ∪ edge(parent → folder#view)
}

namespace folder {
    relation owner: user
    relation viewer: user

    permission view = viewer ∪ computed(owner)
}

caveat business_hours {
    expression: env.current_hour >= 9 && env.current_hour < 17
}

caveat department_match {
    expression: user.department == document.department
}

Tuples (at revision 100):

// Document ownership
document:1#owner → user:alice

// Folder hierarchy
document:1#parent → folder:shared
folder:shared#viewer → user:bob

// Wildcard with caveat
document:1#viewer → user:* [department_match]

Query:

Check(document:1#view, user:charlie) at revision 100
Context: {
    "env.current_hour": 14,
    "user.department": "engineering",
    "document.department": "engineering",
}

Evaluation Trace:

1. Start: Check(document:1#view, user:charlie) at revision 100
   VisitKey: {document, 1, view, direct:user:charlie}
   Budget: {MaxDepth: 50, MaxNodes: 1000, MaxTuples: 10000}

2. Evaluate: document#view = viewer ∪ computed(editor) ∪ edge(parent → folder#view)
   Operation: OP_UNION (3 children)

3. Evaluate child 1: viewer
   Operation: OP_DIRECT
   Query tuples: document:1#viewer at revision 100
   Found: [document:1#viewer → user:* [department_match]]

   3.1. Match subject: user:charlie vs user:*
        Result: MATCH (wildcard matches namespace)

   3.2. Evaluate caveat: department_match (INV-14: per-candidate)
        Expression: user.department == document.department
        Context: {"user.department": "engineering", "document.department": "engineering"}
        Result: CAVEAT_TRUE ✅

   3.3. Child 1 result: TRUE

4. UNION aggregation (INV-12: short-circuit on TRUE)
   Child 1: TRUE
   Result: TRUE (short-circuit, don't evaluate other children)

5. Final result: TRUE ✅

Invariants Applied:

✅ INV-5: All reads at revision 100
✅ INV-14: Wildcard caveat evaluated per-candidate (charlie)
✅ INV-12: UNION short-circuits on TRUE
✅ INV-15: Canonical signature for cycle detection

Edge Cases: Invariants in Action

Edge Case 1: Schema Evolution (INV-4, INV-8, INV-16)

Scenario: Schema changes, old tuples remain.

Old Schema (revision 50):

namespace document {
    relation viewer: user | role#member  // Allows SubjectSet
}

New Schema (revision 100):

namespace document {
    relation viewer: user  // Only allows DirectSubject
}

Tuples:

// Old tuple (created at revision 50)
document:1#viewer → role:admin#member  // SubjectSet

// New tuple (created at revision 100)
document:1#viewer → user:alice  // DirectSubject

Query:

Check(document:1#viewer, user:alice) at revision 100

Evaluation:

1. Read tuples at revision 100:
   - document:1#viewer → role:admin#member
   - document:1#viewer → user:alice

2. Check SubjectConstraints (INV-4):
   - role:admin#member: SubjectSet NOT in allowed types
   - Action: IGNORE (INV-8)

3. Check user:alice:
   - DirectSubject IS in allowed types
   - Match: user:alice == user:alice
   - Result: TRUE ✅

4. Final result: TRUE (old tuple ignored gracefully)

Takeaway: Old tuples don't break evaluation after schema changes.

Edge Case 2: Cycle Detection (INV-15)

Scenario: Misconfigured schema creates cycle.

Schema:

namespace document {
    relation viewer: user
    relation editor: user

    permission view = viewer ∪ computed(edit)
    permission edit = editor ∪ computed(view)  // CYCLE!
}

Tuples:

document:1#editor → user:alice

Query:

Check(document:1#view, user:alice)

Evaluation:

1. Start: Check(document:1#view, user:alice)
   VisitKey: {document, 1, view, direct:user:alice}
   Visited: [{document, 1, view, direct:user:alice}]

2. Evaluate: view = viewer ∪ computed(edit)

   2.1. Evaluate child 1: viewer (OP_DIRECT)
        No tuples found
        Result: FALSE

   2.2. Evaluate child 2: computed(edit)
        Recurse: Check(document:1#edit, user:alice)
        VisitKey: {document, 1, edit, direct:user:alice}
        Visited: [{document, 1, view, direct:user:alice}, {document, 1, edit, direct:user:alice}]

        2.2.1. Evaluate: edit = editor ∪ computed(view)

               2.2.1.1. Evaluate child 1: editor (OP_DIRECT)
                        Found: document:1#editor → user:alice
                        Match: user:alice == user:alice
                        Result: TRUE ✅

               2.2.1.2. UNION short-circuits on TRUE
                        Result: TRUE

        2.2.2. Backtrack: Remove {document, 1, edit, direct:user:alice} from visited
               Result: TRUE

3. UNION aggregation:
   Child 1: FALSE
   Child 2: TRUE
   Result: TRUE ✅

4. Final result: TRUE (cycle avoided by backtracking)

Takeaway: Cycle detection with backtracking allows same node in different branches.

Edge Case 3: Deterministic Tie-Breaking (INV-12)

Scenario: Multiple REQUIRES_CONTEXT results with same cardinality.

Schema:

namespace document {
    relation viewer: user
    relation editor: user
    relation owner: user

    permission view = viewer ∪ computed(editor) ∪ computed(owner)
}

Tuples:

document:1#viewer → user:alice [business_hours]
document:1#editor → user:alice [ip_restriction]
document:1#owner → user:alice [mfa_verified]

Query:

Check(document:1#view, user:alice) with NO context

Evaluation:

1. Evaluate: view = viewer ∪ computed(editor) ∪ computed(owner)

2. Evaluate child 1: viewer
   Found: document:1#viewer → user:alice [business_hours]
   Caveat: business_hours
   Context: {} (empty)
   Result: REQUIRES_CONTEXT([business_hours])

3. Evaluate child 2: computed(editor)
   Found: document:1#editor → user:alice [ip_restriction]
   Caveat: ip_restriction
   Context: {} (empty)
   Result: REQUIRES_CONTEXT([ip_restriction])

4. Evaluate child 3: computed(owner)
   Found: document:1#owner → user:alice [mfa_verified]
   Caveat: mfa_verified
   Context: {} (empty)
   Result: REQUIRES_CONTEXT([mfa_verified])

5. UNION aggregation (INV-12):
   All children: REQUIRES_CONTEXT with cardinality 1
   Tie-break: Pick first in schema order
   Result: REQUIRES_CONTEXT([business_hours]) ✅

6. Final result: REQUIRES_CONTEXT([business_hours])

Takeaway: Schema order ensures deterministic tie-breaking.

Why INV-12 matters:

Without INV-12, different implementations would return different results:

// WITHOUT INV-12 (non-deterministic):
// Implementation A might return: REQUIRES_CONTEXT([business_hours])
// Implementation B might return: REQUIRES_CONTEXT([ip_restriction])
// Implementation C might return: REQUIRES_CONTEXT([mfa_verified])
// Result: DIFFERENT RESULTS for same query! ❌

// WITH INV-12 (deterministic):
// All implementations return: REQUIRES_CONTEXT([business_hours])
// Result: IDENTICAL RESULTS across all implementations ✅

This is exactly the divergence problem we saw in "Why Current Models Don't Work"—without frozen semantics, reasonable implementations produce different results.

Edge Case 4: INTERSECTION Tie-Breaking (INV-13)

Scenario: Multiple intersection paths with different missing sets.

Schema:

namespace document {
    relation viewer: user
    relation employee: user

    permission restricted_view = viewer ∩ employee
}

Tuples:

document:1#viewer → user:alice [business_hours]
document:1#employee → user:alice [ip_restriction, mfa_verified]

Query:

Check(document:1#restricted_view, user:alice) with NO context

Evaluation:

1. Evaluate: restricted_view = viewer ∩ employee

2. Evaluate child 1: viewer
   Found: document:1#viewer → user:alice [business_hours]
   Caveat: business_hours
   Context: {} (empty)
   Result: REQUIRES_CONTEXT([business_hours])  // Cardinality: 1

3. Evaluate child 2: employee
   Found: document:1#employee → user:alice [ip_restriction, mfa_verified]
   Caveat: ip_restriction AND mfa_verified
   Context: {} (empty)
   Result: REQUIRES_CONTEXT([ip_restriction, mfa_verified])  // Cardinality: 2

4. INTERSECTION aggregation (INV-13):
   Both children: REQUIRES_CONTEXT
   Pick minimal cardinality: [business_hours] (1 < 2)
   Result: REQUIRES_CONTEXT([business_hours]) ✅

5. Final result: REQUIRES_CONTEXT([business_hours])

Takeaway: INTERSECTION picks the path with fewest missing parameters, minimizing context requirements for the caller.

Implementation Notes

Performance Optimization

1. Short-Circuit Evaluation

// UNION: Stop on first TRUE
for _, child := range unionChildren {
    result := evaluate(child)
    if result == TRUE {
        return TRUE  // Short-circuit
    }
}

// INTERSECTION: Stop on first FALSE
for _, child := range intersectionChildren {
    result := evaluate(child)
    if result == FALSE {
        return FALSE  // Short-circuit
    }
}

2. Tuple Batching

// Read all tuples for a resource in one query
tuples := storage.ReadTuples(resource, revision)

// Group by subject type for efficient matching
directSubjects := filterDirectSubjects(tuples)
subjectSets := filterSubjectSets(tuples)
wildcards := filterWildcards(tuples)

3. Caveat Caching

// Cache caveat evaluation results per (caveat, context) pair
cacheKey := hash(caveatName, context)
if cached, ok := caveatCache.Get(cacheKey); ok {
    return cached
}
result := evaluateCaveat(caveatName, context)
caveatCache.Set(cacheKey, result)
return result

Testing Strategies

1. Conformance Tests

// Golden test suite that all implementations must pass
func TestConformance(t *testing.T) {
    tests := LoadGoldenTests("testdata/conformance/*.yaml")
    for _, test := range tests {
        result := enma.Check(test.Resource, test.Subject, test.Context)
        assert.Equal(t, test.Expected, result)
    }
}

2. Property-Based Tests

// Test invariants with random inputs
func TestDeterminism(t *testing.T) {
    quick.Check(func(schema Schema, tuples []Tuple, query Query) bool {
        result1 := enma.Check(query)
        result2 := enma.Check(query)  // Same query
        return result1 == result2  // Must be identical
    }, nil)
}

3. Chaos Tests

// Test fail-safe defaults
func TestChaos(t *testing.T) {
    // Inject failures
    storage.InjectError(errors.New("network timeout"))

    // Evaluation should not panic
    result := enma.Check(resource, subject, context)

    // Should fail safely (deny access)
    assert.Equal(t, FALSE, result)
}

Algebraic Laws (Informational)

These laws are relied upon during planning/normalization:

Idempotence

A ∪ A = A
A ∩ A = A

Use case: Simplify redundant schema definitions.

Identity

A ∪ ∅ = A
A ∩ U = A  (where U = universe of eligible subjects)

Use case: Optimize empty branches.

Commutativity

A ∪ B = B ∪ A
A ∩ B = B ∩ A

Use case: Reorder operations for optimization.

Note: Commutativity is semantic, but evaluation order matters for determinism (INV-12, INV-13).

Non-Distributivity with Exclusion

A ∩ (B − C) ≠ (A ∩ B) − (A ∩ C)  // NOT EQUAL!

Reason: Exclusion breaks distributivity. Keep exclusion operations isolated.

Use case: Prevent incorrect query rewrites.

Example: Query Optimization Using Algebraic Laws

Original query:

permission view = viewer ∪ viewer ∪ computed(editor)

Problem: Redundant evaluation of viewer (appears twice).

Optimization using Idempotence (A ∪ A = A):

permission view = viewer ∪ computed(editor)  // Deduplicated

Why it matters: Reduces evaluation cost by 33% (2 children instead of 3).

Another example using Commutativity:

// Original: expensive operation first
permission view = computed(owner) ∪ direct

// Optimized: cheap operation first (short-circuit potential)
permission view = direct ∪ computed(owner)

Why it matters: If direct returns TRUE, we skip the expensive computed(owner) evaluation entirely.

Note: These optimizations preserve semantics because the algebraic laws guarantee equivalence. However, evaluation order still matters for determinism (INV-12, INV-13) when multiple paths return REQUIRES_CONTEXT.

Takeaways

Frozen semantics enable convergence — A formal specification with 16 invariants ensures that independent implementations produce identical results, enabling multi-vendor ecosystems, conformance testing, and correctness proofs.
Minimal interface surface reduces complexity — Four interfaces (TupleReader, SchemaRepo, CaveatRegistry, RevisionSource) provide the minimal abstraction needed for any implementation, whether in-memory, distributed, or optimized.
Algebraic laws enable safe optimization — Idempotence, identity, and commutativity laws allow query rewrites and optimizations while preserving semantics, but exclusion's non-distributivity requires careful handling.

Why it matters: After 11 posts building the authorization model piece by piece, we now have a complete, frozen specification that defines exact semantics for every edge case. This transforms Enma from a design document into a verifiable standard that multiple teams can implement independently with confidence that their systems will interoperate. The 16 invariants serve as both implementation guide and conformance test suite, ensuring that whether you build an in-memory prototype or a globally distributed production system, the core semantics remain identical. This is how authorization systems scale from proof-of-concept to industry standard—by freezing the semantics so that innovation can happen in implementation while correctness remains guaranteed.

What We've Built: The Complete Journey

Over 12 posts, we've built a complete authorization system from first principles:

Phase I: Groundwork (Posts 1-2)

Post 1: Why traditional authorization breaks at scale
Post 2: Modeling roles and memberships (RBAC v1)

Key concepts: Direct permissions, role-based access control, tuple storage.

Phase II: Graph Logic (Posts 3-4)

Post 3: From roles to relationships (ReBAC v1)
Post 4: Hierarchies and inheritance (ReBAC v2)

Key concepts: Boolean algebra (UNION, INTERSECTION, EXCLUSION), computed subjects, edge traversal, cross-object inheritance.

Phase III: Attributes & Conditions (Posts 5-7)

Post 5: Conditional access (ABAC v1)
Post 6: Organization-scoped conditions
Post 7: Complex boolean logic (ABAC v2)

Key concepts: Tri-state logic, caveats, wildcard subjects, scoped parameters, multi-predicate conditions, function calls.

Phase IV: Determinism & Safety (Posts 8-10)

Post 8: Schema-level safety nets
Post 9: Determinism and tie-breaks
Post 10: Unknowns, duplicates, and fail-safe defaults

Key concepts: Required caveats, subject constraints, canonical signatures, tie-breaking rules, budget limits, cycle detection, fail-safe defaults.

Phase V: Consistency & Finalization (Posts 11-12)

Post 11: Consistency and revisions
Post 12: Final model and invariants

Key concepts: Snapshot isolation, revision tracking, consistency levels, 16 core invariants, minimal interface surface, algebraic laws.

The Final Model: Enma Core Semantics

What is Enma?

Enma is a Zanzibar-style authorization system that combines:

ReBAC (Relationship-Based Access Control) for flexible permission modeling
ABAC (Attribute-Based Access Control) for context-aware conditions
Snapshot isolation for distributed consistency
Fail-safe defaults for production safety
Deterministic evaluation for reproducible results

Core guarantees (16 invariants):

INV-1: Relation identity is (namespace, relation)
INV-2: No resource wildcards
INV-3: Schema closure (all references exist)
INV-4: Allowed kinds mask
INV-5: Single snapshot evaluation
INV-6: Non-monotonicity (exclusion)
INV-7: No SubjectSet expansion during Check
INV-8: Invalid tuples are ignored
INV-9: Parameter naming convention
INV-10: Function registry (pure, deterministic, total, bounded)
INV-11: RequiredCaveat composition
INV-12: UNION tie-breaking (schema order)
INV-13: INTERSECTION tie-breaking (minimal cardinality)
INV-14: Per-candidate wildcard evaluation
INV-15: Canonical subject signature
INV-16: Unknown caveat handling (fail-safe)

Minimal interface:

TupleReader: Tuple storage abstraction
SchemaRepo: Schema storage abstraction
CaveatRegistry: Caveat evaluation abstraction
RevisionSource: Revision tracking abstraction

Design principles:

Deterministic — Same inputs always produce same outputs
Bounded — All operations have finite cost
Snapshot-isolated — Entire evaluation at one revision
Type-safe — Compile-time schema validation
Fail-safe — Invalid data is ignored, not errored

Conclusion

We started with a simple question: Why does traditional authorization break at scale?

Over 12 posts, we've built a complete answer:

Traditional models collapse because they can't handle relationships, hierarchies, and conditions simultaneously.
Relationship-based access control (ReBAC) models permissions as tuples, enabling flexible graph-based authorization.
Attribute-based conditions (ABAC) add context-awareness with tri-state logic and scoped parameters.
Schema-level safety enforces mandatory policies and constraints at compile time.
Determinism and fail-safe defaults ensure production safety even when things go wrong.
Snapshot isolation provides consistency across distributed storage.
Frozen semantics (16 invariants) enable independent implementations to converge.

The result: A production-ready authorization system that handles real-world complexity while maintaining correctness guarantees.

This is how you build authorization at scale. Not with ad-hoc rules and SQL queries, but with a formal model that's deterministic, bounded, snapshot-isolated, type-safe, and fail-safe.

Thank you for following this journey. I hope these 12 posts have given you the tools to build authorization systems that scale from prototype to production, from startup to global enterprise.

Now go build something amazing. 🚀

Post 12 — Final Model and Invariants

The Problem: When "Reasonable" Implementations Diverge

Human Rule

Why do we need this?

Scenario: Two Teams Implement Enma

Design Intention: Frozen Semantics

Architectural Decision: Core Semantics Document

Design Principles

Model Design: The 16 Core Invariants

Phase I: Schema & Type System (INV-1 to INV-4)

INV-1: Relation Identity

INV-2: No Resource Wildcards

INV-3: Schema Closure

INV-4: Allowed Kinds Mask

Phase II: Evaluation Semantics (INV-5 to INV-8)

INV-5: Single Snapshot Evaluation

INV-6: Non-Monotonicity

INV-7: No SubjectSet Expansion During Check

INV-8: Invalid Tuples Are Ignored

Phase III: Caveat Semantics (INV-9 to INV-11)

INV-9: Parameter Naming Convention

INV-10: Function Registry

INV-11: RequiredCaveat Composition

Phase IV: Determinism (INV-12 to INV-13)

INV-12: UNION Tie-Breaking

INV-13: INTERSECTION Tie-Breaking

Invariant Dependencies

Phase V: Wildcard & Cycle Detection (INV-14 to INV-15)

INV-14: Per-Candidate Wildcard Evaluation

INV-15: Canonical Subject Signature

Phase VI: Fail-Safe Defaults (INV-16)

INV-16: Unknown Caveat Handling

Implementation: Minimal Interface Surface

1. TupleReader

2. SchemaRepo

3. CaveatRegistry

4. RevisionSource

Happy Path Example: Complete Evaluation

Scenario: Document Access with Hierarchies and Caveats

Edge Cases: Invariants in Action

Edge Case 1: Schema Evolution (INV-4, INV-8, INV-16)

Edge Case 2: Cycle Detection (INV-15)

Edge Case 3: Deterministic Tie-Breaking (INV-12)

Edge Case 4: INTERSECTION Tie-Breaking (INV-13)

Implementation Notes

Performance Optimization

Testing Strategies

Algebraic Laws (Informational)

Idempotence

Identity

Commutativity

Non-Distributivity with Exclusion

Example: Query Optimization Using Algebraic Laws

Takeaways

What We've Built: The Complete Journey

Phase I: Groundwork (Posts 1-2)

Phase II: Graph Logic (Posts 3-4)

Phase III: Attributes & Conditions (Posts 5-7)

Phase IV: Determinism & Safety (Posts 8-10)

Phase V: Consistency & Finalization (Posts 11-12)

The Final Model: Enma Core Semantics

Conclusion

Keep Reading

Sub-Microseconds

Home