Skip to content

Type Algebra

A policy is a precise set. If it contradicts itself, it does not build.

  1. 001A policy that contradicts itself, or that no request could satisfy, is a compile error that says exactly why and where, with a suggested fix.broken policies do not buildSource: Scope-Forge compiler
  2. 002A security rule written into the policy is checked against every possible record; if a later change breaks it, the build stops with a concrete counterexample.rules the build cannot skipSource: Scope-Forge compiler

01Algebra

Everything is a set, scopes included

Scope-Forge treats a policy as mathematics, and everything in it is a set. A scope is a named product type, a set of records. A number field admits a set of values, and a text field admits a set of strings. One algebra composes them all, so a rule describes exactly which requests it admits, there is no ambiguity about what it means, and every question about the policy is answered exactly, at build time, by a compiler whose own code is machine-checked with Verus.

scope-product.sf

DayShift requires {
    hour: num where in 6..18
    clearance: num where in 1..4
}

Mission requires {
    hour: num where in 10..22
    clearance: num where in 2..5
}

MissionDay requires DayShift && Mission

accepted: 3 declarations, 0 contradictions

MissionDay: hour 10..18, clearance 2..4

Two scopes over the same two fields, composed into the region both admit.

02Composition

Composing policy by composing sets

Groups are described by what their members are, their attributes, and combined freely, so a person in several groups is natural. Roles build on any number of parents and can refer to one another. A cycle with a well-defined meaning resolves to its fixpoint, so every question stays decidable; a meaningless cycle, or one that makes the policy hard to reason about, is rejected at compile time with the exact cycle and a suggested fix.

mission-operator.sf

Operator requires {
    station: str where in ("A".."Z")+ ++ ("0".."9")+
    clearance: num where in 1..5
    action: str where in "read" || "task" || "release"
}

MissionOperator requires Operator && {
    clearance: num where in 3..4
    mission_window: num where in 1400..2200
    action: str where in "read" || "task"
}

accepted: 2 declarations, 0 contradictions

MissionOperator is a subset of Operator

Base operator access, narrowed to a clearance band and a mission window.

03Empty set

The empty set is the error

If the policy is wrong, it does not build. A policy that contradicts itself, or that no request could satisfy, describes the empty set; Scope-Forge refuses to build it, says exactly why and where, and suggests a fix. The mistake is caught on the author's desk, not in production.

empty set: compile error
Two rules that no request can satisfy together: their sets share nothing, the intersection is empty, and the build fails.

The compile error says why, where, and what to change; a broken security rule adds the author's reason and a concrete record that breaks it.

What the compile error contains

contradictory-policy.sf

Cleared requires {
    clearance: num where in 4..5
}

Probationary requires {
    clearance: num where in 1..2
}

ProbationaryRelease requires Cleared && Probationary

rejected: 3 declarations, 1 contradiction

A contradictory policy and the diagnostic it produces.

contradictory-policy.sf

error: cannot admit `ProbationaryRelease.clearance`: no value satisfies the policy

  Cleared.clearance
    admits 4..5
  Probationary.clearance
    admits 1..2
  the intersection is empty
  help: widen one range until 4..5 and 1..2 overlap, or do not compose them

04Assertions

Security rules the build cannot skip

Write "contractors can never hold a clearance that permits restricted reads" into the policy once, and no later change can break it without the build failing, showing your reason, and producing the exact record that would have slipped through. Authors write the guarantees they need directly into the policy, each with a plain-language reason, and the compiler checks every such rule against every possible record, never a sample. The rule cannot quietly erode. Below, that sentence as an assertion: two sets, the relation between them, and the reason. The relations an assertion can state are in (a subset), not in, never in (no record in both), equal and not equal.

contractor-clearance.sf

Principal requires {
    employment: str where in "employee" || "contractor"
    clearance: str where in "none" || "confidential" || "secret"
}

Contractor requires Principal && {
    employment: str where == "contractor"
    clearance: str where == "none"
}

RestrictedRead requires Principal && {
    clearance: str where in "confidential" || "secret"
}

assert Contractor never in RestrictedRead
    because "contractors never hold a clearance that permits restricted reads"

accepted: 3 declarations, 1 assertion, 0 contradictions

The proof point, written as policy: contractors are never inside the set that permits restricted reads.

05Subsets

Narrower by construction

The same algebra settles relations between whole scopes at compile time. A scope built by intersecting its parent with tighter bounds is a subset of that parent by construction. IronIdP relies on the same check: a delegated token's authority is always strictly narrower than its parent's, checked by Scope-Forge.

delegated-agent.sf

Operator requires {
    clearance: num where in 1..5
    action: str where in "read" || "task" || "release"
    ttl_seconds: num where in 1..86400
}

Agent requires Operator && {
    clearance: num where <= 3
    action: str where in "read" || "task"
    ttl_seconds: num where <= 900
}

accepted: 2 declarations, 0 contradictions

Agent is a subset of Operator

A delegated agent scope that is a subset of its operator by construction.

If the policy is wrong, it does not build.