concretize hint

Concept

The concretize hint is a performance hint supported by rtlv/shiva that determines, via a solver query, whether a named field in a circuit state can only evaluate to a single concrete value, and if so replaces the field's symbolic term with that concrete value. It enables aggressive symbolic-state reduction in push-button software-on-hardware verification while guaranteeing soundness through the underlying solver.

First seen 6/9/2026

Last seen 6/9/2026

Evidence 2 chunks

Wiki v1

WIKI

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].

READ FULL ARTICLE →

NEIGHBORHOOD

2 nodes · 1 edges

graph · concretize hint · depth=1

RELATIONSHIPS

1 connections

rtlv/shiva ← implements 100% 2e

rtlv/shiva implements the concretize performance hint.

LINKED ENTITIES

1 links

rtlv/shiva IMPLEMENTS Extracted graph relationship

CITATIONS

6 sources

6 citations — click to expand

[1] The concretize hint takes a field name, uses a solver query to check whether the field can only evaluate to a single concrete value, and replaces the symbolic term with that concrete value if so. rtlv: push-button verification of software on hardware

[2] The solver query ensures the concretize hint cannot be misused to transform the circuit state in an incorrect way, making it more powerful than Rosette's syntactic rewrite rules (e.g., it collapses `(ite a 0 a)` to `0`, for which Rosette has no built-in rewrite rule). rtlv: push-button verification of software on hardware

[3] In the MicroTitan case study, concretize is applied on cycle 150 to the SPI RX FIFO state-machine control register, which is provably idle by that cycle, allowing the register to remain concrete for the rest of the execution. rtlv: push-button verification of software on hardware

[4] Without performance hints such as concretize, verification of MicroTitan would time out; with them, output-determinism verification completes in under 100 minutes on an Intel Core i7-5930K in single-threaded verification code. rtlv: push-button verification of software on hardware

[5] Concretize is one of several rtlv/shiva performance hints listed in Table 1 alongside abstract, abstract-or-overapproximate-vector, collect-garbage, run-and-replace, and unsafe-custom-hint. rtlv: push-button verification of software on hardware

[6] Performance hints such as concretize can take advantage of the specific property being verified and are therefore more specific than general optimizations such as Rosette's rewrite rules. rtlv: push-button verification of software on hardware