mutgen

Documentation

Overview

Command mutgen enumerates and applies single-site WEAKENING mutations to the Go verification rail, so that what the conformance corpus FORCES can be measured instead of asserted.

A vector count is an upper bound on forcing and never a measurement of it. The question a relying party actually has is: if a rule vanished from a verifier, would this corpus notice? That is answered by removing exactly one rule and replaying the whole corpus. Every operator below makes the rail strictly MORE PERMISSIVE at one syntactic site, which is the direction the question asks about:

IF_OFF      if COND {...}          -> if false && (COND) {...}   whole guard off
IF_DISJ     if A || B {...}        -> if (false && (A)) || B     one disjunct off
IF_CONJ     if A && B {...}        -> if (true || (A)) && B      one conjunct off
CASE_OFF    switch { case C: }     -> case false && (C):         tagless switch arm off
CASE_DISJ   as IF_DISJ, in a tagless switch arm
CASE_CONJ   as IF_CONJ, in a tagless switch arm
CASE_DEL    switch T { case V: }   -> the arm is deleted         tagged/type switch arm off
RET_TRUE    return <boolexpr>      -> return true || (<expr>)    bool predicate arm
RET_FALSE   return <boolexpr>      -> return false && (<expr>)
CODE_OFF    appendCode(cs, CodeX)  -> cs                         one emission off
VALID_TRUE  ev.valid = <expr>      -> ev.valid = true || (<expr>)

This command is measurement tooling, not part of the consumer surface: nothing a relying party runs imports it, and it never touches a tree outside the one named by -pkg. scripts/forcing-gate.py drives it.

Usage:

mutgen -pkg <dir> -list               # JSON-lines catalogue of every site
mutgen -pkg <dir> -apply <KEY>        # print the mutated file
mutgen -pkg <dir> -apply <KEY> -write # rewrite the one file in place