concretize hint

Overview

The concretize hint is a performance hint implemented by rtlv/shiva (relation: IMPLEMENTS). It targets a specific field in the symbolic circuit state and asks the SMT solver whether that field, given current constraints, can only evaluate to one concrete value. If the solver confirms uniqueness, rtlv/shiva rewrites the field's symbolic term to the concrete value, shrinking the symbolic state and speeding up subsequent symbolic execution. The solver query acts as a soundness guard: the transformation is only applied when it is provably safe, so a misuse of the hint cannot silently produce an incorrect circuit state ^[1].

Signature and semantics

Table 1 of the rtlv paper lists the hint as:

concretize [field-name]

• Argument: the name of a field in the circuit state.
• Behavior: issues a solver query to determine whether the field can only evaluate to a single concrete value; if so, replaces the symbolic term representing the field with that concrete term ^[1].
• Soundness: enforced by the solver check rather than by syntactic rewrite rules ^[1].

Why it is more powerful than rewrite rules

Rosette's built-in rewrite rules are syntactic and limited. The paper gives the example of the expression (ite a 0 a), which is always equal to 0 (it returns 0 when a equals 1, and a when a equals 0). Rosette has no built-in rewrite rule for this case, but a solver-driven hint such as concretize can recognize that the value is forced to a single concrete value and collapse it. Without solver-backed reasoning, equivalent collapses must be hand-coded for every shape that appears in the circuit ^[1].

Case study: MicroTitan SPI RX FIFO state machine

The concretize hint was critical for verifying output determinism in MicroTitan. The hardware state machine controlling the SPI peripheral's RX FIFO has a symbolic term for its state register that grows rapidly each cycle if left unchecked. After approximately 150 cycles of boot code execution, however, the state machine deterministically returns to an idle state and remains there for the rest of the run. The verification code applies concretize to the state-machine control register on cycle 150, which forces rtlv/shiva to verify that the register must be idle and then replaces the symbolic term with the concrete idle term. From that point on, the register can stay concrete through the rest of the execution, preventing the symbolic blow-up that would otherwise cause the verification to time out ^[1].

Role in the rtlv/shiva hint set

Concretize is one of several performance hints exposed by rtlv/shiva. Others described in the paper include:

• abstract — replaces a field with a fresh symbolic value when it depends only on allowed dependencies (property-specific; meaningful only in the context of properties such as output determinism) ^[2].
• abstract-or-overapproximate-vector — abstracts each entry of a memory field if it only depends on allowed dependencies, and otherwise overapproximates it ^[1].
• collect-garbage — forces a garbage-collection run ^[1].
• run-and-replace — re-runs verification from the initial state to the current cycle using a provided list of hints, then replaces the named fields in the main execution with the values obtained in the secondary execution ^[1].
• unsafe-custom-hint — a general interface letting user verification code implement circuit-state transformations directly (used for transformations that depend on relationships between registers and are too circuit-specific to generalize) ^[1].

Performance hints in general can exploit the specific property being verified and are therefore typically more targeted than general-purpose optimizations such as Rosette's rewrite rules ^[2].

Impact

Applying concretize (and the other performance hints) to the MicroTitan case study allowed output-determinism verification to finish in under 100 minutes on an Intel Core i7-5930K, on single-threaded verification code. Without these hints, the same verification would time out ^[1].