Specification · v1

Syntax

1. Source text

A v1 source is Unicode text. Its size is measured in UTF-8 bytes (65,536 by default, see Limits). A source holds zero or more contracts. An empty source is rejected (limit[source-size]).

2. Reading in context

v1 has no separate tokenizer pass. The parser asks for the kind of token it can accept at the current position: a keyword, a name, a word, a number, a string or a source tag. Three consequences follow.

Keywords are matched as prefixes, and only where the grammar expects them. At a position where CONTRACT may appear, any text that begins with CONTRACT is read as the keyword: CONTRACTX { is CONTRACT followed by the name X. Elsewhere a keyword is not reserved. A field may be called WHEN, and an entity may be called CONTEXT.

Names and words are read greedily. x == 1 ANDROID == 2 reads as x == 1 AND ROID == 2, and integer reads as the type int followed by the name eger. trueAND is a single word.

Write a space after every keyword.

3. White space and comments

There are no block comments.

3.1 A comment can become part of a word (sharp edge)

An operand word or a type extends over any trivia that follows it, including a comment. In

    FORBID grant WHEN Request.count <= zero // must be non-empty
      [SOURCE:claim_nonempty]

the constant is named zero // must be non-empty, which does not resolve (unsupported[unknown-name]). Put comments on their own line, or after the source tag.

CONTRACT Claim {
  ENFORCEMENT_MODE: enforced
  CONTEXT {
    ENTITIES Request {
      count: int
      region: string
      ready: bool
      ratio: float
    }
    CONSTANTS {
      zero: int == 0 [SOURCE:POLICY]
      cap: int == 25 [SOURCE:POLICY]
    }
  }
  TRIGGER {
    grant()
  }
  PROHIBITION {
    FORBID grant WHEN Request.count <= zero // must be non-empty
      [SOURCE:claim_nonempty]
  }
}

A comment after a field's type does the same to the type, which is then no longer primitive:

CONTRACT Claim {
  ENFORCEMENT_MODE: enforced
  CONTEXT {
    ENTITIES Request {
      count: int // paths requested
      region: string
      ready: bool
      ratio: float
    }
    CONSTANTS {
      zero: int == 0 [SOURCE:POLICY]
      cap: int == 25 [SOURCE:POLICY]
    }
  }
  TRIGGER {
    grant()
  }
  GUARANTEE {
    ENSURE grant() WHEN Request.ready == true [SOURCE:must_be_ready]
  }
  PROHIBITION {
    FORBID grant WHEN Request.count > cap [SOURCE:over_cap]
  }
}

4. Lexical elements

A minus sign is part of a number only when a digit follows it directly. -1 is a negative literal. - 1 is arithmetic, and arithmetic is refused (§7).

5. Grammar

The grammar in EBNF. It is also available as a file: ulang-v1.ebnf.

file          = { contract } ;
contract      = "CONTRACT" name "{"
                  [ mode ] [ context ] [ trigger ]
                  [ guarantee ] [ prohibition ] [ observability ]
                "}" ;
mode          = "ENFORCEMENT_MODE" ":"
                ( "enforced" | "ENFORCED" | "advisory" | "ADVISORY" | "audit" | "AUDIT" ) ;

context       = "CONTEXT" "{" { entities } [ constants ] "}" ;
entities      = "ENTITIES" [ name ] "{" field { field } "}" ;
field         = name ":" type ;
type          = "int" | "float" | "bool" | "string"
              | name [ "<" type { "," type } ">" ] ;
constants     = "CONSTANTS" [ name ] "{" { constant } "}" ;
constant      = name ":" type ( "==" | "=" ) literal [ source ] ;

trigger       = "TRIGGER" "{" event { event } "}" ;
event         = name [ "(" [ args ] ")" ] [ "WHEN" condition ] ;

guarantee     = "GUARANTEE" "{" { "ENSURE" clause } "}" ;
prohibition   = "PROHIBITION" "{" { "FORBID" clause } "}" ;
clause        = name [ "(" [ args ] ")" ] [ "WHEN" condition ] [ source ] ;

observability = "OBSERVABILITY" "{" { "LOG" string "ON" word } "}" ;

source        = "[" "SOURCE:" text "]" ;

condition     = conjunction { "OR" conjunction } ;
conjunction   = primary { "AND" primary } ;
primary       = "(" condition ")"
              | value [ op value ]
              | word "=" value ;                  (* assignment: outside the subset *)
op            = "==" | "!=" | "<=" | ">=" | "<" | ">" ;
value         = term { "-" integer } ;            (* subtraction: outside the subset *)
term          = integer | float | string | boolean
              | word [ "(" [ args ] ")" ]         (* a call: outside the subset *)
              | "(" value ")" ;                   (* right-hand side only *)
args          = value { "," value } ;
literal       = integer | float | string | boolean ;

5.1 Reading the grammar

• Sections appear in the order shown, each at most once. A section out of order is a syntax error at the point where it begins: the parser expected the contract's closing } there.
• Inside CONTEXT, every ENTITIES block comes before the CONSTANTS block.
• Fields and constants are separated by white space, not commas.
• An ENTITIES block has at least one field. A TRIGGER has at least one event.
• AND binds tighter than OR, and both associate to the left. Parentheses group conditions and are not nodes: (a == 1) is the same tree as a == 1.
• A parenthesised value is allowed only on the right of a comparison, in an argument, or on the right of =. At the start of a primary, ( always opens a condition.
• A single = after a name, path or boolean word parses as an assignment, which validation refuses (unsupported[condition-form]). After any other operand a single = is a syntax error. Write == to compare.

6. Comparisons

7. Refused before parsing

A linear bounds scan runs before the parser. It skips strings, comments and source tags, and refuses:

• the text NOT, anywhere it occurs, including inside a name such as CANNOT_MERGE or ANNOTATION (unsupported[not-operator]);
• +, *, / (other than //), ^, and - not directly followed by a digit (unsupported[arithmetic]).

CONTRACT Claim {
  ENFORCEMENT_MODE: enforced
  CONTEXT {
    ENTITIES Request {
      CANNOT_MERGE: bool
    }
    CONSTANTS {
      zero: int == 0 [SOURCE:POLICY]
      cap: int == 25 [SOURCE:POLICY]
    }
  }
  TRIGGER {
    grant()
  }
  GUARANTEE {
    ENSURE grant() WHEN Request.CANNOT_MERGE == false [SOURCE:mergeable]
  }
}

Use lower-case names for fields that would otherwise contain NOT, and compare with == false instead of negating.

8. Multiple contracts

A source may hold several contracts. Each is validated independently, in order, and two contracts in one source may not share a name (semantic[duplicate-contract]). Anything between contracts other than white space and comments is a syntax error.