Crate logicaffeine_tv 

logicaffeine-tv

tv = translation validation: per compile, prove the Rust the logicaffeine compiler emits is observationally equivalent to its LOGOS source by symbolically executing into the shared logicaffeine-verify semantic domain (bitvectors / booleans) and discharging the equivalence with Z3.

Part of the Logicaffeine workspace. Excluded from default-members (Z3-backed); depends on logicaffeine_compile and logicaffeine_verify.

Role in the workspace

This is rung 3–4 (translation validation), not rung 5 (machine-checked proof) — the trust boundary is the encoders + Z3 + rustc, not a mechanized meta-theorem. See proof-and-verification.md for how the verification rungs fit together.

Today only the LOGOS source side has a symbolic executor; there is no Rust-emitter-side executor yet, so the full source↔emitted-Rust equivalence is not closed in code. What runs is the source encoder plus its meta-soundness oracle: check_encoder_sound runs a program through the tree-walking interpreter (interpret_program, the independent ground truth) and the symbolic encoder, then proves with Z3 that they agree on the full observable behavior — the ordered Show outputs (each slot equality validated) and whether an error was raised. A buggy encoder is caught here, not masked by a downstream equivalence that “proves” two wrong things equal. Out-of-fragment programs are soundly excluded (Unsupported), never reported as agreement.

Verifiable Core

Straight-line Int/Bool programs; anything outside yields Unsupported(reason). Int is a 64-bit bitvector (INT_WIDTH = 64), so wrapping/overflow matches the interpreter’s native i64.

• + - * → wrapping Add/Sub/Mul.
• / % → SDiv/SRem; divisor == 0 is OR’d into a sticky errored condition (div-by-zero is an observable error; outputs are compared only when neither side errored).
• Comparisons: < → SLt, > → swapped SLt; <=/>= → SLe (swapped for >=).
• == != — Int via bitvector Eq, Bool via iff.
• and/or — logical on Bool, bitwise (And/Or) on Int; not — boolean on Bool, bitwise ~ (XOR u64::MAX) on Int.
• Statements: Let, Set (target must be in scope), Show <expr> to show.
• Punted: If/While/Repeat/Return/functions/calls, indexing, lists, interpolated strings, non-Int/Bool literals.

Public API

// crate root
pub fn summarize_logos(source: &str) -> Result<SymSummary, TvError>;
pub fn check_encoder_sound(source: &str) -> SoundnessReport;
pub use symexec::{SymSummary, SymValue};
pub use verdict::{SoundnessReport, TvError};

• summarize_logos — parse and symbolically execute the source side into a summary (no optimizer).
• check_encoder_sound — the encoder/interpreter cross-check described above.
• SymSummary { outputs: Vec<SymValue>, errored: VerifyExpr }; SymValue is Int(VerifyExpr) (width-64 bitvector) or Bool(VerifyExpr).
• SoundnessReport = Agrees | Disagrees { detail } | Unsupported { reason } | ParseFailed { detail }; TvError = Parse(ParseError) | Unsupported(String).

Public submodules — symexec (big-step symbolic execution of the Verifiable Core into VerifyExpr), parse (arena-lifetime-safe parsing via a callback), equiv (Z3 validity), and verdict (the SoundnessReport / TvError result types):

// symexec — big-step symbolic execution of the Verifiable Core into VerifyExpr
pub const INT_WIDTH: u32 = 64;
pub fn execute(stmts: &[Stmt], interner: &Interner) -> Result<SymSummary, Unsupported>;

// parse — arena lifetimes can't escape, so the AST is handed back via callback
pub fn with_program<R>(source: &str, optimize: bool, f: impl FnOnce(&[Stmt], &Interner) -> R)
    -> Result<R, ParseError>;

// equiv — validity via check_equivalence(pred, true): Unsat ⇒ valid, Sat ⇒ counterexample
pub fn prove_valid(pred: &VerifyExpr) -> EquivalenceResult;
pub fn is_valid(pred: &VerifyExpr) -> bool;

with_program(.., optimize = true, ..) runs the production optimize_program pipeline — the hook for validating optimizer output against the source.

Example

use logicaffeine_tv::{check_encoder_sound, summarize_logos, SoundnessReport};

let src = "## Main\nLet x be 2 + 3 * 4.\nShow x.";
assert_eq!(check_encoder_sound(src), SoundnessReport::Agrees);

let summary = summarize_logos(src).unwrap();
assert_eq!(summary.outputs.len(), 1);

Dependencies

• logicaffeine_compile — parser, interner, arena AST, tree-walking interpreter (interpret_program), optimizer (optimize_program).
• logicaffeine_verify — VerifyExpr, BitVecOp, EquivalenceResult, check_equivalence; pulls in Z3 (z3 = "0.12") transitively, which is why this crate is excluded from default-members (plain cargo build/cargo test need no Z3).

The crate declares no feature flags and no binary. The encoder-soundness suite lives in crates/logicaffeine_tests/tests/phase_tv_encoder_sound.rs, gated on that crate’s verification feature:

cargo test -p logicaffeine-tests --features verification phase_tv_encoder_sound

License

Business Source License 1.1 — see LICENSE.md.

---

Docs index · Root README · Changelog

Re-exports

pub use symexec::SymSummary;

pub use symexec::SymValue;

pub use verdict::SoundnessReport;

pub use verdict::TvError;

Modules

equiv

The SMT equivalence primitive, built on logicaffeine_verify::check_equivalence.

parse

Parse a LOGOS source string into the arena-allocated AST and hand it to a callback, mirroring the front-end of compile::compile_program_full.

symexec

Big-step symbolic execution of the LOGOS Verifiable Core into VerifyExpr.

verdict

Result types for the translation validator.

Functions

check_encoder_sound

Cross-validate the LOGOS encoder against the tree-walking interpreter on one program.

summarize_logos

Parse source and symbolically execute it into a SymSummary over the LOGOS semantics. Does not run the optimizer (the source-of-truth side).