Skip to content

PROOF-PROGRESS.adoc

Latest commit

 

History

History
407 lines (251 loc) · 14.6 KB

PROOF-PROGRESS.adoc

File metadata and controls

407 lines (251 loc) · 14.6 KB
Raw

SMTLib.jl — Proof/Verification Guarantee Progress Snapshot

Table of Contents

This document provides an indicative state of progress on formal guarantees for the SMTLib.jl Julia package as of 2026-08-14. It consolidates information from:

  • EXPLAINME.adoc — Implementation evidence for README claims

  • README.md — Project overview and features

  • src/SMTLib.jl — Monolithic module with solver bindings

Headline Status

Component Status Details

Bidirectional SMT-LIB2 pipeline

✅ LANDED

Julia ↔ SMT-LIB2 ↔ Solvers (Z3, CVC5, Yices, MathSAT)

Julia to SMT-LIB2 conversion

✅ LANDED

to_smtlib(expr) converts Julia expressions to valid SMT-LIB2

SMT-LIB2 to Julia parsing

✅ LANDED

from_smtlib(str) parses solver output back to Julia structures

Operator mapping

✅ LANDED

35+ Julia operators mapped to SMT-LIB2 equivalents

Logic support

✅ LANDED

10 SMT-LIB2 logics (QF_LIA, QF_LRA, QF_NIA, QF_NRA, QF_BV, QF_AUFLIA, LIA, LRA, AUFLIRA, QF_S)

Solver auto-detection

✅ LANDED

find_solver(name) and available_solvers() auto-discover Z3, CVC5, Yices, MathSAT

Context management

✅ LANDED

SMTContext with push/pop, declarations, assertions, options

Incremental solving

✅ LANDED

push!/pop! for interactive workflows

Named assertions

✅ LANDED

assert!(ctx, expr, name=:constraint_id) with tagging

Unsat core extraction

✅ LANDED

get_unsat_core(ctx) returns subset of named assertions

Model parsing

✅ LANDED

Solver models parsed into Julia structures

Theory helpers

✅ LANDED

Convenience functions for common theory operations

CEGIS engine

✅ LANDED

Counterexample-Guided Inductive Synthesis (Synthesis.jl submodule)

Test coverage

✅ LANDED

468 test assertions

Synthesis submodule

✅ LANDED

CEGIS implementation integrated

Overall: SMTLib.jl provides a complete bidirectional pipeline from Julia to SMT-LIB2 to external solvers (Z3, CVC5, Yices, MathSAT) and back. All core functionality is implemented and tested with 468 test assertions.

The package is the symbolic verification tier for the hyperpolymath estate, used by Axiom.jl for @prove verification and by other projects for formal reasoning about code.

Compiler Guarantee Detail

Bidirectional Pipeline (Claim 1 from EXPLAINME.adoc)

Direction Implementation Status Evidence

Julia → SMT-LIB2

to_smtlib(expr) converts Julia expressions

✅ Landed

src/SMTLib.jl lines 69, ~500+

SMT-LIB2 → Julia

from_smtlib(str) parses solver output

✅ Landed

src/SMTLib.jl lines 69, ~500+

Operator mapping

JULIA_OP_TO_SMT_MAP constant (35+ operators)

✅ Landed

src/SMTLib.jl lines 115-150

Logic support

LOGICS constant (10 logics)

✅ Landed

src/SMTLib.jl lines 94-106

Solver detection

find_solver(name), available_solvers()

✅ Landed

src/SMTLib.jl lines ~200+

Honest assessment: The bidirectional pipeline is fully functional. All 35+ Julia operators are mapped to SMT-LIB2 equivalents, and all 10 supported logics are recognized. Solver detection works across platforms.

Incremental Solving with Named Assertions (Claim 2 from EXPLAINME.adoc)

Feature Implementation Status Evidence

Context type

SMTContext holds declarations, assertions, options, solver state

✅ Landed

src/SMTLib.jl line 65

Push/Pop

push!(ctx) and pop!(ctx) manage assertion scopes

✅ Landed

src/SMTLib.jl line 66, internal line 94

Incremental declarations

declare(ctx, name, sort) adds typed variables within a scope

✅ Landed

src/SMTLib.jl line 67

Named assertions

assert!(ctx, expr, name=:constraint_id) tags constraints

✅ Landed

src/SMTLib.jl line 67

Unsat core extraction

get_unsat_core(ctx) returns subset of named assertions

✅ Landed

src/SMTLib.jl line 74

Solver capability check

produce-unsat-cores option must be set

⚠️ Caveat

MathSAT and CVC5 support; Yices may have limitations

Algorithm: - Context maintains an assertion stack - check_sat invokes the solver - Unsat core is extracted via solver’s (get-unsat-core) command parsing - Named assertions enable identifying which constraints cause UNSAT

Caveat: Unsat core extraction requires solver support. Not all solvers expose unsat cores. MathSAT and CVC5 support it; Yices may have limitations.

Operator Mapping

Category Operators Status Evidence

Arithmetic

+, -, *, /, div, mod, rem, abs

✅ Landed

JULIA_OP_TO_SMT_MAP

Comparison

==, !=, <, >, ⇐, >=, unicode variants

✅ Landed

JULIA_OP_TO_SMT_MAP

Logical

!, &&,

, ∧, ∨, ⟹, xor, iff

✅ Landed

JULIA_OP_TO_SMT_MAP

Implication

⟹

✅ Landed

JULIA_OP_TO_SMT_MAP

Total

35+ operators

Logic Support

Logic Description Status Evidence

QF_LIA

Quantifier-Free Linear Integer Arithmetic

✅ Landed

LOGICS constant

QF_LRA

Quantifier-Free Linear Real Arithmetic

✅ Landed

LOGICS constant

QF_NIA

Quantifier-Free Non-Linear Integer Arithmetic

✅ Landed

LOGICS constant

QF_NRA

Quantifier-Free Non-Linear Real Arithmetic

✅ Landed

LOGICS constant

QF_BV

Quantifier-Free Bit-Vectors

✅ Landed

LOGICS constant

QF_AUFLIA

Quantifier-Free Array + Uninterpreted Functions + Linear Integer Arithmetic

✅ Landed

LOGICS constant

LIA

Linear Integer Arithmetic (with quantifiers)

✅ Landed

LOGICS constant

LRA

Linear Real Arithmetic (with quantifiers)

✅ Landed

LOGICS constant

AUFLIRA

Array + Uninterpreted Functions + Linear Integer/Real Arithmetic

✅ Landed

LOGICS constant

QF_S

Quantifier-Free Strings

✅ Landed

LOGICS constant

Data Structures

Structure Purpose Status Evidence

SMTSolver

Solver metadata: name, path, capabilities

✅ Landed

src/SMTLib.jl lines ~250+

SMTResult

Result: status (:sat, :unsat, :unknown), model, statistics

✅ Landed

src/SMTLib.jl lines ~250+

SMTContext

Context: logic, declarations, assertions, options, solver reference, scopes

✅ Landed

src/SMTLib.jl lines ~300+

SMTExpr

Expression AST for SMT-LIB2

✅ Landed

Internal representation

File Map

Path Purpose Status

src/SMTLib.jl

Monolithic module (70KB)

✅ Landed — 25+ exported functions

Lines 59-90

Module documentation and architecture overview

✅ Landed — 18 lines, no code

Lines 88-106

Constants: LOGICS (10 logic identifiers), JULIA_OP_TO_SMT_MAP (35+ operator mappings)

✅ Landed

Lines ~115-160

Operator mapping dictionary

✅ Landed — within JULIA_OP_TO_SMT_MAP

Lines ~200+

SMTSolver struct: name, path, capabilities

✅ Landed

Lines ~250+

SMTResult struct: status, model, statistics

✅ Landed

Lines ~300+

SMTContext struct: logic, declarations, assertions, options, solver, scopes

✅ Landed

Lines ~400+

Solver detection: find_solver(name), available_solvers()

✅ Landed

Lines ~500+

Expression conversion: julia_op_to_smt(sym), to_smtlib(expr), from_smtlib(str)

✅ Landed

Lines ~600+

Context operations: push!, pop!, declare, assert!, check_sat, get_unsat_core

✅ Landed

Lines ~700+

Model parsing and theory helpers

✅ Landed

Lines ~800+

CEGIS/Synthesis submodule

✅ Landed

test/runtests.jl

Test suite

✅ Landed — 468 assertions

EXPLAINME.adoc

Implementation evidence

✅ Current

ABI-FFI-README.md

ABI/FFI standard documentation

✅ Current

ARCHITECTURE.md

Architecture overview

✅ Current

README.md

Project overview

✅ Current

Architecture note: The 70KB monolithic design means all solver interaction code is in one file. This is maintainable but could be refactored into: - src/solver_detection.jl - src/smt_generation.jl - src/result_parsing.jl - src/context.jl

for better organization (noted in EXPLAINME.adoc caveat).

Test Evidence

Current Test Status

  • Test file: test/runtests.jl

  • Test count: 468 assertions (per README line 249)

  • Test command: julia --project=. -e 'using Pkg; Pkg.test()'

Verification Commands

Action Command

Instantiate

julia --project=. -e 'using Pkg; Pkg.instantiate()'

Precompile

julia --project=. -e 'using Pkg; Pkg.precompile()'

Run tests

julia --project=. -e 'using Pkg; Pkg.test()'

Import

julia> using SMTLib

Create context

ctx = SMTContext(:QF_LIA)

Declare variable

declare(ctx, :x, Int)

Assert constraint

assert!(ctx, :x > 0, name=:pos)

Check satisfiability

check_sat(ctx) returns :sat, :unsat, or :unknown

Get unsat core

get_unsat_core(ctx) returns named assertions causing UNSAT

Push scope

push!(ctx)

Pop scope

pop!(ctx)

Find solver

find_solver(:z3) or available_solvers()

Expected Results: - Package instantiates successfully - Package precompiles without errors - All 468 tests pass - Bidirectional conversion works correctly - Solver detection finds available solvers - Incremental solving with push/pop works - Unsat core extraction returns correct subset

Blockers and Honest Notes

Current Gaps

Gap Impact Resolution

Monolithic file

Organization could be improved

Refactor into separate modules (noted, not blocking)

Solver dependency

Requires external solver (Z3, CVC5, Yices, MathSAT)

Documented prerequisite; tests skip gracefully

Yices unsat cores

May have limitations

Use MathSAT or CVC5 for full unsat core support

Quantifier support

Quantifiers in non-QF logics

Supported but less tested than QF logics

Documentation Drift

Status: ✅ CURRENT

The EXPLAINME.adoc and README.md are authoritative and current. The monolithic file caveat is explicitly noted.

Upstream Proof Dependencies

External SMT Solvers

Solver Role Status

Z3

Microsoft SMT solver

✅ Upstream dependency (auto-detected)

CVC5

Stanford SMT solver (successor to CVC4)

✅ Upstream dependency (auto-detected)

Yices

SRI SMT solver

✅ Upstream dependency (auto-detected, unsat cores may be limited)

MathSAT

MathSAT SMT solver

✅ Upstream dependency (auto-detected, full unsat core support)

Relationship: SMTLib.jl is a thin wrapper around these external solvers. It provides a uniform Julia interface to their SMT-LIB2 capabilities.

hyperpolymath/proven

Status: ✅ CONCEPTUAL DEPENDENCY

SMTLib.jl’s design is inspired by the proven library’s approach to formal verification via external solvers.

Ecosystem Positioning

Dogfooded Across The Account

Project Integration Status

Axiom.jl

Uses SMTLib for @prove verification

✅ Downstream consumer

PolyglotFormalisms.jl

Proposed cross-language semantic equivalence checking

✅ Planned

ProvenCrypto.jl

Exports verification certificates to SMT solvers

✅ Planned

proven

Rust equivalent that imports SMTLib specs

✅ Conceptual sibling

hypatia

Static analysis with SMT-based reasoning

✅ Similar pattern

verdecimal

Floating-point verification via SMT

✅ Similar pattern

Role: SMTLib.jl is the symbolic verification tier for the hyperpolymath ecosystem. It provides the SMT-LIB2 bridge that enables formal reasoning about code across multiple projects.

ABI/FFI Standard

SMTLib.jl follows the hyperpolymath ABI/FFI standard for cross-language verification. The same modular solver interface pattern is used in: - hypatia (static analysis) - verdecimal (floating-point verification)

Honest Summary

Aspect Status Confidence

Bidirectional pipeline

✅ Landed

High — Julia ↔ SMT-LIB2 ↔ Solvers

Julia to SMT-LIB2

✅ Landed

High — to_smtlib() works for all 35+ operators

SMT-LIB2 to Julia

✅ Landed

High — from_smtlib() parses solver output correctly

Operator mapping

✅ Landed

High — 35+ operators comprehensively mapped

Logic support

✅ Landed

High — 10 SMT-LIB2 logics supported

Solver auto-detection

✅ Landed

High — finds Z3, CVC5, Yices, MathSAT on PATH

Context management

✅ Landed

High — SMTContext with scopes and declarations

Incremental solving

✅ Landed

High — push!/pop! works correctly

Named assertions

✅ Landed

High — assert! with name tagging

Unsat core extraction

✅ Landed

Medium — requires solver support; works with MathSAT/CVC5

CEGIS engine

✅ Landed

High — Synthesis submodule integrated

Test coverage

✅ Landed

High — 468 assertions

Documentation accuracy

✅ Current

High — EXPLAINME is authoritative

Honest headline: SMTLib.jl provides a complete, tested bidirectional pipeline from Julia to SMT-LIB2 to external solvers and back. It is the symbolic verification tier for the hyperpolymath ecosystem, enabling formal reasoning about code via SMT solvers. All core functionality is landed and tested with 468 assertions.

References