Mosaic

The Mosaic CHC Verifier provides facilities for Constrained Horn Clause (CHC) verification with advanced preprocessing and translation techniques.

Location: include/Verification/Mosaic/, lib/Verification/Mosaic/

CLI Tool: tools/verifier/mosaic/ (binary lotus-verify-mosaic)

Overview

Mosaic acts as a verification backend leveraging Z3’s fixed-point engine. Its primary feature is the ability to translate between Bit-Vector (BV) and Integer (Int) arithmetic domains before and during CHC solving, which is critical for performance and decidability in many software verification tasks.

Key Components

  • MosaicFixedpoint: The core CHC verification engine wrapping Z3’s fixed-point solver with custom CHC rule management and solving strategies.

  • Bv2IntTranslator / Int2BvTranslator: Utilities for translating constraints from bit-vector arithmetic to integer arithmetic, and vice versa. This allows the solver to pick the most efficient background theory for the CHC problem at hand.

  • Int2BvPreprocessor / Int2BvOverflowAnalyzer: Analyzes whether integer constraints can be safely encoded into finite-width bit-vectors by checking for potential overflows, applying simplifications and reducing the state space.

  • CHCParser: Parses external CHC problems for verification.

Usage

Mosaic is built into the lotus-verify-mosaic tool:

./build/bin/lotus-verify-mosaic input.smt2

It integrates closely with Lotus’s analysis infrastructure to resolve constraints extracted from LLVM IR.