Skip to content

Regular Languages

A text rule is a precise set of strings. Every check is a single pass over the input.

  1. 001Union, concatenation, intersection, and exclusion are computed exactly by the compiler's own verified set arithmetic, with no outside solver.exact compositionSource: Scope-Forge compiler
  2. 002Every text check runs in a single pass over the input, against a precompiled, verified pattern matcher.single-pass checksSource: Scope-Forge compiler

01Languages

A text rule is a set of strings

Every value either matches the whole format or is rejected. An identifier format, a permitted command, or a callsign pattern is a set of strings, and a value is admitted when it belongs to the set. A rule is built from literals, inclusive character ranges, union, concatenation, intersection, exclusion, and the repetitions optional, any number, and one or more. Concatenation binds tighter than union and intersection, and parentheses group. Every rule built this way is a regular language, so it compiles to one finite matching machine and is checked in a single pass. Small rules compose into larger ones, and the result is exact.

callsign-format.sf

letter: str where in "a".."z" || "A".."Z"
digit: str where in "0".."9"
flight_number: str where in "1".."9" ++ digit? ++ digit? ++ digit?
callsign: str where in letter ++ letter ++ letter ++ flight_number ++ letter?
squawk: str where in ("0".."7") ++ ("0".."7") ++ ("0".."7") ++ ("0".."7")
manifest: str where in (callsign ++ ",")* ++ callsign

accepted: 6 declarations, 0 contradictions

A callsign format built from ranges, concatenation, and repetition.

02Automata

Composing text rules

The compiler turns each text rule into a small matching machine and combines machines the way it combines sets, exactly and with no outside solver. The storyboard follows five declarations, from one set to a byte with one value excluded; the callsign format above is built the same way.

hex-byte-machine.sf

storyboard

digit: str where in "0".."9"
hex_digit: str where in digit || "a".."f" || "A".."F"
hex_byte: str where in hex_digit ++ hex_digit
lower_hex: str where in hex_digit && ("0".."9" || "a".."f")
safe_byte: str where in hex_byte && != "00"

1 of 9 digit

digitdigit compiles to one transition carrying one interval class."0".."9"digit: one class, one transition
Five declarations: each operator takes the machines of its operands and builds the machine of the result.

03Exclusion

Exclusion is exact

Excluding a value, or a whole pattern, is a set operation, and the compiler computes it exactly with its own verified arithmetic, never by approximation; no solver runs when a policy is checked (what is trusted). There are no solver time-outs and no machine-dependent limits, so the same rule means the same thing on every machine.

No solver when a policy is checked. The same answer on every machine.

Exclusion is exact

04Runtime

One pass over the input

Text checks run in a single pass over the input. Everything decided at compile time is gone from the running system, and what remains for a text check is one linear pass against a precompiled, verified pattern matcher. The matcher is built at compile time by the regex engine in the verified core libraries, whose UTF-8 validation is proven equal to its specification, including the accelerated paths; what runs is the precompiled matcher inside the compiled policy.

regex-identifier.sf

identifier_start: str where in "a".."z" || "A".."Z" || "_"
identifier_char: str where in identifier_start || "0".."9"
identifier: str where in identifier_start ++ identifier_char*

accepted: 3 declarations, 0 contradictions

An identifier format: a start character, then any number of identifier characters.

A text rule that means exactly what it says.