Crate rucc_rules 

The rule DSL compiler.

Design: spec/09-optimizer.md and spec/10-backend.md. Outside the layer stack: this is a build dependency, never a runtime one.

Middle-end rewrites and instruction selection patterns are written once, in one language, and this crate compiles them into the matching code the compiler runs. The same rule text is what rucc-verify discharges against an SMT solver, which is the point: a rule that is verified and a rule that is applied cannot drift apart if they are the same text.

The language

A rule names what to match, what to put in its place, and why that is sound:

(rule (lower (add.i64 (value x) (mul.i64 (value y) (iconst 4))))
      (x64.lea (amode_base_index_scale x y 4))
      (spec (= (bvadd x (bvmul y 4)) (result))))

A rule that only holds under a condition says so between the two, where it can be read as part of deciding whether the rule fires rather than as part of what firing produces:

(rule (lower (shl.i64 (value x) (iconst k)))
      (if (and (>= k 0) (< k 64)))
      (x64.shl x k)
      (spec (= (bvshl x k) (result))))

Everything is a term, and a term is a name, a number, or a head applied to arguments. A bare name is a variable and a parenthesised one is an application, which is the whole of the distinction and is why a constructor taking nothing is still written (result). Variables are bound by the pattern and used everywhere else, (result) stands for what the replacement computes and so appears only in a specification, and a name may not be bound twice in one pattern, because that would be asking the matcher for an equality test it does not have.

The spec clause is required rather than optional. spec/17-milestones.md asks that a rule the solver cannot discharge never enter the rule set, and making the claim part of the grammar is what gives that somewhere to stand: a rule without one is not an unverified rule, it is a syntax error.

One rule in a hundred has a claim no solver will settle in the time anybody will wait, which is usually a multiplication of two unknowns at full width. Such a rule may carry a last clause saying why a proof at narrower widths would be enough:

(rule (lower (mul.i64 (value x) (value y)))
      (x64.imul x y)
      (spec (= (bvmul x y) (result)))
      (bounded "multiplication of two unknowns at 64 bits is out of reach"))

The clause excuses nothing on its own. The rule is still asked at its own width first, and all the clause does is say what a person is willing to sign for if the answer comes back as a shrug. rucc-verify is what acts on it, and what counts how often it had to.

The matcher

A rule set compiles into a trie over its patterns rather than into a conditional per rule. Every pattern is flattened into the steps that match it, read in pre-order, and patterns that begin the same way share the steps they agree on, so testing that a term is an add.i64 happens once however many rules begin with one. Specificity is the shape rather than a sort: the concrete tests at a node are tried before the wildcard, so a rule that names an operand is tried before a rule that takes anything there.

Status

The language, its reader and the matcher are here, and rucc-verify discharges the specifications. Emitting the matcher as Rust for the compiler to link against is the piece that follows. All of it lands in M3 because spec/10-backend.md says retrofitting verification onto an existing rule set is the thing not to do.

Structs

Error

A place in a rule file and what is wrong there.

Match

What a successful match found.

Matcher

The automaton a rule set compiles into.

Rule

One rule: what it matches, what it produces, and what makes that sound.

Term

A term: the pattern a rule matches, the replacement it produces, and the two clauses that constrain it are all one shape.

Enums

TermKind

The three kinds of term.

Constants

MILESTONE

The milestone in spec/17-milestones.md that fills this crate in.

Functions

parse

Read every rule in one file.

parse_terms

Read a file of bare terms rather than of rules.