Specification · v1

Canonical forms

A valid contract has three canonical forms:

Two sources that differ only in layout, comments, number spelling, the case of the mode or boolean words, or FORBID x() against FORBID x have the same canonical text, and so the same digest. Any change that can affect a decision changes the digest, and so do some changes that cannot, such as the order of TRIGGER entries or a LOG line.

Canonical forms are defined for contracts that pass validation.

1. Canonical text

Rules, applied in order:

1. CONTRACT <name> {, then the sections in grammar order, then } and a line feed.
2. Indentation is two spaces per level. There is one item per line, and lines end with LF.
3. Comments are dropped.
4. ENFORCEMENT_MODE: <mode>, with the mode in lower case.
5. ENTITIES <name> {, then one name: type per line.
6. The CONSTANTS block is printed only if it has constants. Each constant is name: type == value [SOURCE:id].
7. TRIGGER events are printed as action().
8. ENSURE action() WHEN … [SOURCE:id] and FORBID action WHEN … [SOURCE:id], with no parentheses after a FORBID action.
9. An empty PROHIBITION and an empty OBSERVABILITY are omitted.
10. Each LOG is LOG "<message>" ON <event>, with the message verbatim.
11. Source ids are written trimmed, directly after SOURCE:. (A constant's tag written with a space after [ is kept verbatim; that is errata E1.)

Literals:

Conditions are printed with the fewest parentheses that preserve the tree. Comparisons are left op right with single spaces. AND binds tighter than OR and both associate to the left, so:

• the right operand of an OR is parenthesised if it is an OR;
• the left operand of an AND is parenthesised if it is an OR;
• the right operand of an AND is parenthesised if it is an AND or an OR.

The canonical text re-parses to itself, with one known exception in ulang-lite 0.1.0: a constant whose source tag is written [ SOURCE:id] (see errata E1).

# layout, comments and spelling do not matter to the digest
CONTRACT   Thermostat{ENFORCEMENT_MODE:ENFORCED
  CONTEXT { ENTITIES Reading { celsius: float
      sensor_ok: bool  retries: int }
    CONSTANTS { ceiling_c: float == 1.2e2 [SOURCE:  SPEC-7 ]
      max_retries: int == 003 [SOURCE:SPEC-9] } }
  TRIGGER { accept_reading( ) }
  GUARANTEE { ENSURE accept_reading() WHEN (Reading.sensor_ok == TRUE) [SOURCE:sensor_healthy] }
  PROHIBITION {
    // over range, or retried too often while unhealthy
    FORBID accept_reading() WHEN Reading.celsius > ceiling_c OR (Reading.retries >= max_retries AND (Reading.sensor_ok == FALSE)) [SOURCE:reject_reading]
  }
}

CONTRACT Thermostat {
  ENFORCEMENT_MODE: enforced
  CONTEXT {
    ENTITIES Reading {
      celsius: float
      sensor_ok: bool
      retries: int
    }
    CONSTANTS {
      ceiling_c: float == 120.0 [SOURCE:SPEC-7]
      max_retries: int == 3 [SOURCE:SPEC-9]
    }
  }
  TRIGGER {
    accept_reading()
  }
  GUARANTEE {
    ENSURE accept_reading() WHEN Reading.sensor_ok == true [SOURCE:sensor_healthy]
  }
  PROHIBITION {
    FORBID accept_reading WHEN Reading.celsius > ceiling_c OR Reading.retries >= max_retries AND Reading.sensor_ok == false [SOURCE:reject_reading]
  }
}

2. Digest

digest = lowercase_hex( SHA-256( UTF-8( canonical text ) ) )

A file's contracts are digested one at a time. The command line prints each contract's digest (check) and attaches it to every decision (eval, as contract_sha256).

ulang-lite includes a synchronous FIPS 180-4 SHA-256 (sha256Hex), so a digest is computed identically in Workers, Node and browsers.

3. Canonical JSON

canonicalJson is the contract as JSON with keys sorted at every level and no white space:

{
  contract:      name,
  mode:          "enforced" | "advisory" | "audit" | null,
  entities:      [ { name, fields: [ { name, type } … ] } … ] | null,
  constants:     [ { name, type, hard, value, source } … ],
  trigger:       [ { action, args, when } … ] | null,
  guarantee:     [ { action, args, when, source } … ],
  prohibition:   [ { action, args, when, source } … ],
  observability: [ { message, on } … ]
}

Values are tagged: {"int":"7"} (a decimal string), {"float":"0.25"} (canonical spelling), {"string":"…"}, {"bool":true}, {"name":"zero"}, {"path":["Entity","field"]}. Conditions are {"and":[l,r]}, {"or":[l,r]} and {"compare":[l,"op",r]}. args is null when no parentheses were written, and [] for (). The digest is computed over the canonical text, not the JSON.

4. Rule-set hash (µLang Git profile)

An application that decides with a set of contracts needs one identity for the set. The µLang Git forge uses:

rule_set_hash = SHA-256( "governed-forge-c8-source-v1" ‖ 0x00 ‖
                         for each contract, sorted by name:
                           u64be(len(name)) ‖ name ‖ u64be(len(source)) ‖ source )

Here name and source are UTF-8 bytes, and source is the contract's exact source text. The forge's decisions are { verdict, clause_id, rule_set_hash }. This profile belongs to the forge, not to v1. Other applications may define their own set identity.