Basics

P4-SpecTec specifications are written in .watsup files using the P4-SpecTec language. The examples here come from the SpecTecX tutorial, which specifies Typed Imp, a small typed imperative language. Where Typed Imp does not cover a construct, examples from the nano-p4 specification are used.

Comments

Single-line comments start with ;;. Additional semicolons (;;;, ;;;;, …) are used by convention to indicate heading levels in the document structure, but have no semantic difference.

;;--------------------
;; Syntax

;;--- Contexts ---

Primitive Data Types

P4-SpecTec has the following primitive types:

These are the types used in metavariable declarations and function signatures, and are distinct from the types of the object language being specified. For example, INT in the Typed Imp spec is a syntax constructor defined with syntax, not the primitive int of the DSL itself.

Options and Lists

Option types are written by appending ? to a type. The absent case is eps, and a present value is written directly:

dec $lookup<K, V>(map<K, V>, K) : V?

def $lookup<K, V>(eps, K_query) = eps    ;; absent: key not found
def $lookup<K, V>((K_h -> V_h)::_, K_query) = V_h
  -- if K_h = K_query                    ;; present: return the value

An if premise can match on an option result:

rule Check_expr/id:
  tenv |- x : t
  -- if $lookup<id, type>(tenv, x) = t   ;; binds t if present, fails if eps

List types are written by appending * to a type. The empty list is eps, and :: is the cons operator:

syntax map<K,V> = (pair<K,V>)*

Pattern matching on lists follows the same :: notation in def cases:

def $lookup<K, V>(eps, K_query) = eps
def $lookup<K, V>((K_h -> V_h)::(K_t -> V_t)*, K_query) = V_h
  -- if K_h = K_query

A single-element list is written [ x ], and lists are concatenated with ++. Here’s one example from the Nano-P4 spec:

def $flatten_parameterList(parameter) = [ parameter ]
def $flatten_parameterList(nonEmptyParameterList ',' parameter)
  = $flatten_parameterList(nonEmptyParameterList) ++ [ parameter ]

A multi-element list literal [ a, b, c ] is also valid.

Lists also appear in rule conclusions and premises to prepend an entry to a context:

rule Check_command/decl:
  tenv |- (t x '=' e) -| (x -> t)::tenv
  -- Check_expr: tenv |- e : t

Here, (x -> t)::tenv constructs a new typing context with the binding x -> t prepended to tenv.

Tuples

A tuple is an anonymous product of two or more values, written with parentheses and commas: (A, B). Tuples do not need to be declared as a named syntax; they can appear inline wherever a type or value is expected.

The most common use is as the element type of a list. For example, $assoc_ in the stdlib takes a list of pairs as its second argument:

builtin dec $assoc_<X, Y>(X, (X, Y)*) : Y?

Here (X, Y)* is a list of (X, Y) tuples.

Tuples also appear as values constructed on the fly in premises. The member access rules in the Nano-P4 spec build a list of (id, typeIR) pairs to pass to $assoc_:

-- if typeIR = $assoc_<id, typeIR>(id_member, (id_field, typeIR_field)*)

The iteration (id_field, typeIR_field)* zips two parallel lists into a list of pairs.

Records

A record is a product type with named, labeled fields. It is declared with braces and comma-separated LABEL value pairs:

syntax globalTypingLayer =
  { TYPE     typeDefEnv,
    CALLABLE callableTypeDefEnv,
    FRAME    typeFrame }

Record values are constructed with the same brace notation:

-- if globalTypingLayer
    = { TYPE $empty_typeDefEnv,
        CALLABLE $empty_callableTypeDefEnv,
        FRAME $empty_typeFrame }

Fields are accessed with dot notation:

-- if typeFrame = TC.GLOBAL.FRAME

Paths can be chained (TC.GLOBAL.FRAME) to reach fields of nested records.

Records are updated functionally with bracket notation. x[.FIELD = v] produces a copy of x with the named field replaced:

def $enter_t(TC)
  = TC[ .LOCAL.FRAMES = $empty_typeFrame :: TC.LOCAL.FRAMES ]

Nested fields can be updated in a single expression as well:

-- if TC' = TC[.GLOBAL.FRAME = typeFrame']

Variant Definitions

The syntax keyword defines a named type. The most common use is to define a grammar production as a set of variants, which forms the abstract syntax of the language being specified. It can also alias an existing type or name a record type.

syntax type =
  | INT
  | BOOL
  | type '->' type

syntax literal =
  | _NUM int
  | _BOOL bool

syntax expr =
  | literal
  | id
  | '!' expr
  | expr '+' expr
  | expr '<=' expr

Each alternative is prefixed with |. Names starting with a lowercase letter refer to built-in types or non-terminals, which are built-in or previously declared syntax types. Everything else is a terminal, an atom of the object language. Atoms come in a few kinds, each with its own marker:

• Keywords are bare uppercase words, like INT and BOOL. They are written without any marker.
• Silent tags are prefixed with an underscore, like _NUM and _BOOL. These are constructor labels that disambiguate alternatives but do not render in the generated output.
• Operators are glyphs wrapped in single quotes, like '->', '+', and '<='. These are the concrete symbols of the object language.
• Target brackets are backtick-paired and symmetric: `( … `), `{ … `}, and `< … `>. These are the object language’s own brackets. Note that the closing bracket also carries a backtick.

Metavariables

The var keyword declares metavariables and their types. These act as shorthands: wherever e appears unbound in a rule, it is implicitly typed as expr.

var i : int
var b : bool
var x : id
var e : expr
var c : command
var t : type

A variable’s type is inferred from its name by stripping a trailing suffix that begins at the first _ or ' character. For example, given var e : expr, the following names are all valid expr variables:

rule Check_expr/add:
  tenv |- e_l '+' e_r : INT   ;; e_l, e_r -> strip at '_' -> e : expr
  -- Check_expr: tenv |- e_l : INT
  -- Check_expr: tenv |- e_r : INT

rule Check_expr/not:
  tenv |- '!' e' : BOOL        ;; e' -> strip at '\'' -> e : expr
  -- Check_expr: tenv |- e' : BOOL

A suffix of only underscores (e__) or a purely alphanumeric suffix without a separator (eLeft) does not strip, so those would not be recognized as expr variables and would cause an error:

rule Check_expr/not:
  tenv |- '!' eLeft : BOOL     ;; ERROR: eLeft does not resolve to a known variable
  -- Check_expr: tenv |- eLeft : BOOL

Meta-level Operators

P4-SpecTec provides a set of operators that work on meta-level values (the bool, int, and nat primitives), distinct from the operators of the target language being specified.

Boolean operators work on bool meta-values:

These appear in function bodies and if premises:

def $bin_op('&&', _B b_l, _B b_r) = _B (b_l /\ b_r)
def $bin_op('||', _B b_l, _B b_r) = _B (b_l \/ b_r)
def $bin_op('!=', value_l, value_r) = _B (~$bin_eq(value_l, value_r))

-- if direction = OUT \/ direction = INOUT

Note the distinction: '&&' and '||' are target-language terminals (P4 operators in the syntax tree), while /\ and \/ are meta-level boolean operators used to write the spec itself.

Arithmetic expressions on int and nat meta-values are written inside $( ... ):

-- if i' = $($pow2(w) - i - 1)
-- if n'  = $(n - 1)

The $( ... ) delimiter signals that the expression inside uses meta-level arithmetic rather than the target language’s expression grammar.

List length is written with | ... |:

-- if |fieldValue_a*| = |fieldValue_b*|

Set membership is tested with the <- premise, which succeeds if a value matches any element of a list used as a set:

rule Expr_ok/integer:
  scope TC |- unop expression : integerTypeIR
  -- if unop <- [ '~', '-', '+' ]
  -- Expr_ok: scope TC |- expression : integerTypeIR

Function Declarations and Definitions

Functions are declared with dec and defined with def. The declaration gives the name, argument types, and return type. Definitions provide pattern-matched cases. Each of those cases are called clauses.

dec $lookup<K, V>(map<K, V>, K) : V?

;; If map is empty, return empty
def $lookup<K, V>(eps, K_query) = eps

;; If head entry's key matches query, return its value
def $lookup<K, V>((K_h -> V_h)::(K_t -> V_t)*, K_query) = V_h
  -- if K_h = K_query

;; If head entry's key does not match query, recursively call on the rest
def $lookup<K, V>((K_h -> V_h)::(K_t -> V_t)*, K_query)
  = $lookup<K, V>((K_t -> V_t)*, K_query)
  -- otherwise

Key points about function definitions:

• Function names are prefixed with $.
• Angle brackets introduce type parameters (e.g. <K, V>). They must be made explicit in function calls.
• The return type V? means an optional value (eps represents the absent case).
• Each def case can have side conditions introduced with if, or a catch-all otherwise.
• When a function is called, clauses are tried from top to bottom. If pattern match fails or if premises are not satisfied, the clause fails and the next clause is tried.

The builtin modifier marks functions whose implementation is provided by the toolchain rather than defined in the spec:

builtin dec $sum_nat(nat*) : nat

Relations and Rules

A relation defines the signature for a set of rules.

;; Type-check `expr` under context `tenv`
relation Check_expr:
  tenv |- expr : type
  hint(input %0 %1)
  hint(prose_in "typechecking" %1 "under context" %0)

This declares a judgment tenv |- expr : type, meaning “expression expr has type type under typing context tenv.” The |- symbol (turnstile) is conventional notation borrowed from inference rules. In P4-SpecTec, it is just a separator between the context and the subject.

%0, %1, etc. refer to the positional components of the judgment. hint(input ...) specifies which components are inputs to the relation. Here, %0 (tenv) and %1 (expr) are inputs, and %2 (type) is the output.

Rules define when a relation holds. Each rule has a conclusion (the judgment being established) and zero or more premises (the conditions that must hold), introduced with --:

;; If expression is integer literal, it has type INT
rule Check_expr/num:
  tenv |- (_NUM i) : INT

;; If expression is logical not,
;;   Check if the operand is BOOL, then it has type BOOL
rule Check_expr/not:
  tenv |- '!' e : BOOL
  -- Check_expr: tenv |- e : BOOL

;; If expression is binary addition,
;;   Check if both operands are INT, then it has type INT
rule Check_expr/add:
  tenv |- e_l '+' e_r : INT
  -- Check_expr: tenv |- e_l : INT
  -- Check_expr: tenv |- e_r : INT

The first rule has no premises; integer literals always have type INT. The second and third rules invoke Check_expr recursively as premises.

Unlike traditional declarative inference rules where premises are unordered and existential witnesses may be guessed non-deterministically, P4-SpecTec rules are algorithmic: premises are executed in order, from top to bottom, and every value must be computed from already-known inputs. This makes rules directly executable as a type checker or interpreter.

An if premise introduces a boolean-valued side condition:

rule Check_expr/id:
  tenv |- x : t
  -- if $lookup<id, type>(tenv, x) = t

The = in an if premise is overloaded: if the right-hand side is already known, it is a check; if it is an unbound metavariable, it becomes a binding that computes the value from the left-hand side. Here, t is unbound, so $lookup is called and its result is bound to t, which is then used in the conclusion tenv |- x : t. If $lookup returns eps (absent), the rule fails and the next rule is tried.

Rules can mix if and relation premises freely:

rule Check_command/assign:
  tenv |- (x '=' e) -| tenv
  -- Check_expr: tenv |- e : t
  -- if $lookup<id, type>(tenv, x) = t

Here the relation premise Check_expr runs first and binds t, then the if premise checks that x is already declared with that same type.

How Rules are Executed

When the inputs to a relation arrive, the interpreter works through the candidate rules one by one until one succeeds. Understanding this dispatch process matters for writing correct specs and for debugging when something goes wrong:

• Rules are tried in declaration order. When a relation or function has multiple rules or clauses, P4-SpecTec tries them from top to bottom. The first one whose premises all hold wins. This means that the order of clauses in the spec matters.
• A failed premise aborts the current clause. If a pattern match fails or an if condition is not satisfied, that clause is abandoned immediately and the interpreter moves on to the next one. No error is reported at this point; the failure is silent.
• If no clause matches, the relation fails. When every candidate clause has been tried and none succeeded, the interpreter reports a runtime error. A missing rule and a wrong pattern produce the same symptom, which is why the debugging techniques in Chapter 6 focus on narrowing down which clause was the last to be attempted.

Rule Groups

When several rules share the same conclusion shape but differ only in their premises, they can be grouped under a single rulegroup heading. This is purely organizational: the toolchain treats each case inside a rulegroup as an independent rule.

For example, the typing rules for unary expressions in the nano-p4 spec are written as a rule group:

rulegroup Expr_ok/unaryExpression {

  rule Expr_ok/boolean:
    scope TC |- '!' expression : BOOL
    -- Expr_ok: scope TC |- expression : BOOL

  rule Expr_ok/integer:
    scope TC |- unop expression : integerTypeIR
    -- if unop <- [ '~', '-', '+' ]
    -- Expr_ok: scope TC |- expression : integerTypeIR

}

The outer rulegroup Expr_ok/unaryExpression { ... } names the group but adds no semantics. Each rule inside is a full, independent rule with its own name and premises.

Iteration

The (pattern)* syntax applies a pattern element-wise over a list.

For example, the following clause (from the Nano-P4 spec) extracts the third component of every element in parameterIR* into a new list nameIR*:

def $distinct_params(parameterIR*)
  = $distinct_<nameIR>(nameIR*)
  -- if (_ _ nameIR = parameterIR)*

The if premise runs the pattern _ _ nameIR = parameterIR once per element, binding nameIR at each position and collecting the results into nameIR*.

More advanced usages of iteration are to be demonstrated further into the tutorial.

Prose Hints

Prose hints are metadata annotations that guide the prose backend when generating human-readable documentation.

relation Eval_expr:
  env |- expr ==> value
  hint(input %0 %1)
  hint(prose_in "evaluating" %1 "in environment" %0)

hint(prose_in ...) controls the generated prose description.

Individual rules can also carry hints:

syntax literal =
  | _NUM int   hint(prose "the integer" %0)
  | _BOOL bool hint(prose "the boolean" %0)

The prose backend is covered in more detail in Generating Prose Specification.

Exercise

For a more hands-on introduction, we strongly recommend the SpecTecX tutorial.