Numeric Sets | IronVelo

A numeric rule is one exact set. A rule can relate one field to another.

001A range, an exclusion from it, or a combination of several is one exact set, computed by the compiler's own verified set arithmetic.exact rangesSource: Scope-Forge compiler
002A policy can say the approver must not be the requester, or that the request time must be before the credential's expiry, across nested records.rules across fieldsSource: Scope-Forge compiler
003A range that no request could ever satisfy is a compile error that says exactly why and where.broken policies do not buildSource: Scope-Forge compiler

01Ranges

Ranges are exact sets

The policy admits precisely the values its author wrote, nothing more and nothing less. A clearance band, a time window, or a limit on a count is a set of numbers; combining ranges, or excluding values from them, is set arithmetic, and the compiler performs it with its own verified operations. There is no ambiguity about what a range means, and the compiler can reason about it completely.

restricted-altitude.sf

flight_level: num where in 10..600
restricted_block: num where in 280..300
assignable_level: flight_level where not in restricted_block && != 450

accepted: 3 declarations, 0 contradictions

assignable_level: 10..279, 301..449, 451..600

An altitude range with a restricted block and one level carved out exactly.

not in restricted_block and != 450 cut two holes out of the flight-level range, leaving three exact ranges: 10 to 279, 301 to 449, and 451 to 600. The compiler keeps that set exact; nothing rounds the holes away.

02Relations

Rules that relate one field to another

Separation of duties and time limits are part of the policy itself, not bolted-on code. A policy can say the approver must not be the requester, the request time must be before the credential's expiry, or break-glass access applies only under stated conditions. A rule relates a field to another field of the same record by a comparison (before, after, at most, at least, equal, not equal) against that field's resolved value, and it reaches across nested records, such as a request that contains a user that contains a clearance. Numeric values are whole numbers, so every numeric rule is an exact set of whole numbers. Below, the expiry rule, with an assertion that a stale request is never a live one.

live-request.sf

PositiveTime: num where > 0

Request requires {
    expires: PositiveTime
    now: PositiveTime
}

Live requires Request && {
    now: PositiveTime where < resolved This.expires
}

Stale requires Request && {
    now: PositiveTime where >= resolved This.expires
}

assert Stale never in Live
    because "a request made at or after its credential's expiry is never live"

accepted: 4 declarations, 1 assertion, 0 contradictions

The request time must be before the credential's expiry: one field compared with another field of the same record.

This names the record being described, and resolved reads the value of that field in the same record. Live and Stale are both Request, narrowed by a comparison of now with expires. The assertion says no record is in both, and the compiler proves it for every record: before and at-or-after contradict each other on every record.

A field can also be defined by what another scope's field admits, so one band governs every rule that depends on it.

shared-clearance.sf

use ops::Mission

Escort requires {
    clearance: Mission.clearance
    sector: Mission.sector
    speed_kts: num where in 120..450
}

pub relay_clearance: num where in Mission.clearance && != 5

accepted: 1 import, 2 declarations, 0 contradictions

A field defined in terms of another scope's field.

Escort reuses the mission's clearance and sector as its own types, imported through use ops::Mission. The public relay_clearance is defined by what Mission.clearance admits, minus the top level, so a change to the mission's band flows through to it and is re-checked at compile time.

The approver is never the requester, and a request never outlives the credential: written in the policy, not around it.

Separation of duties in the policy

03Empty set

A rule no request could satisfy does not build

A numeric rule that contradicts itself, or that no request could ever satisfy, is a compile error: the compiler refuses to build the policy and says exactly why and where. A later edit that breaks a written security rule stops the build the same way, with a concrete example of a record that breaks the rule. The mistake is caught on the author's desk, not in production.

A policy that contradicts itself does not build.

Caught on the author's desk

04Reproducibility

The same answer on every machine

When a policy is checked, Scope-Forge's own verified set arithmetic decides every numeric question and no solver runs (what is trusted). There are no solver time-outs and no machine-dependent limits, so a policy's meaning never depends on how fast a computer is, and anyone can re-run the check and get the identical result. Two spellings of the same set reduce to the same set.

same-set-two-spellings.sf

hour: num where in 0..23
off_shift: hour where not in 6..18
off_shift_spelled_out: hour where < 6 || > 18

accepted: 3 declarations, 0 contradictions

off_shift, off_shift_spelled_out: one set, 0..5 and 19..23

Two spellings of the same off-shift window, one policy.

not in 6..18 and < 6 || > 18 are two spellings of the same set of hours, 0 to 5 and 19 to 23. The compiler reduces both to the same set, so the author picks the clearer spelling and the answer does not change.

Ranges are exact sets

Rules that relate one field to another

Separation of duties in the policy

A rule no request could satisfy does not build

Caught on the author's desk

The same answer on every machine

A numeric rule that means exactly what it says.