# logicaffeine_tv

> Translation validation for LOGOS: a symbolic encoder of the source, checked with Z3 against the tree-walking interpreter per program

Every public module and item of `logicaffeine_tv`, module by module, each with its one-line summary and its address. Item pages hold the full signature, documentation, trait implementations and a link to the source.

- Crate page: [logicaffeine_tv](https://docs.logicaffeine.com/logicaffeine_tv/)
- All items on one page: [logicaffeine_tv/all](https://docs.logicaffeine.com/logicaffeine_tv/all)
- Source: [src/logicaffeine_tv/lib.rs](https://docs.logicaffeine.com/src/logicaffeine_tv/lib.rs)
- Every crate: [llms.txt](https://docs.logicaffeine.com/llms.txt)

## logicaffeine_tv

- [mod equiv](https://docs.logicaffeine.com/logicaffeine_tv/equiv/): The SMT equivalence primitive, built on `logicaffeine_verify::check_equivalence`.
- [mod parse](https://docs.logicaffeine.com/logicaffeine_tv/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`.
- [mod symexec](https://docs.logicaffeine.com/logicaffeine_tv/symexec/): Big-step symbolic execution of the LOGOS Verifiable Core into `VerifyExpr`.
- [mod tensor](https://docs.logicaffeine.com/logicaffeine_tv/tensor/): A rewrite of the one IR, proven: the obligation `tensor_graph::smt` prints for two graphs, discharged by Z3.
- [mod verdict](https://docs.logicaffeine.com/logicaffeine_tv/verdict/): Result types for the translation validator.
- [fn check_encoder_sound](https://docs.logicaffeine.com/logicaffeine_tv/fn.check_encoder_sound): Cross-validate the LOGOS encoder against the tree-walking interpreter on one program.
- [fn summarize_logos](https://docs.logicaffeine.com/logicaffeine_tv/fn.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).

## logicaffeine_tv::equiv
The SMT equivalence primitive, built on `logicaffeine_verify::check_equivalence`.

- [fn is_valid](https://docs.logicaffeine.com/logicaffeine_tv/equiv/fn.is_valid): True iff `prove_valid` proves the predicate.
- [fn prove_valid](https://docs.logicaffeine.com/logicaffeine_tv/equiv/fn.prove_valid): Prove that a `Bool`-sorted `VerifyExpr` is valid (true under every assignment of its free variables).

## logicaffeine_tv::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`.

- [fn with_program](https://docs.logicaffeine.com/logicaffeine_tv/parse/fn.with_program): Parse `source`, optionally run the production optimizer, and invoke `f` with the resulting statements and the interner used to intern their symbols.

## logicaffeine_tv::symexec
Big-step symbolic execution of the LOGOS Verifiable Core into `VerifyExpr`.

- [struct SymSummary](https://docs.logicaffeine.com/logicaffeine_tv/symexec/struct.SymSummary): The observable summary of a program: the ordered `Show` outputs plus the condition under which the program raised an observable error.
- [struct Unsupported](https://docs.logicaffeine.com/logicaffeine_tv/symexec/struct.Unsupported): A construct outside the currently-supported Verifiable Core. Carries a human reason so the validator can report `Unverified(reason)` rather than ever guessing.
- [enum SymValue](https://docs.logicaffeine.com/logicaffeine_tv/symexec/enum.SymValue): A symbolic LOGOS value: an integer (64-bit bitvector), a boolean, or a channel handle.
- [const INT_WIDTH](https://docs.logicaffeine.com/logicaffeine_tv/symexec/constant.INT_WIDTH): Bit width used to model LOGOS `Int` (native `i64`).
- [fn execute](https://docs.logicaffeine.com/logicaffeine_tv/symexec/fn.execute): Symbolically execute a program (a sequence of statements) into a `SymSummary`.
- [fn execute_seeded](https://docs.logicaffeine.com/logicaffeine_tv/symexec/fn.execute_seeded): Symbolically execute a nondeterministic program under a fixed `seed`, resolving every `Select` winner from a SplitMix64 mirror of the scheduler’s choice function. The result is cross-checked per-seed against `run_treewalker_concurrent_seeded` at the same seed, so a misaligned encoding surfaces as a disagreement — never a false proof.

## logicaffeine_tv::tensor
A rewrite of the one IR, proven: the obligation `tensor_graph::smt` prints for two graphs, discharged by Z3.

- [enum Verdict](https://docs.logicaffeine.com/logicaffeine_tv/tensor/enum.Verdict): What Z3 says of one obligation.
- [fn discharge](https://docs.logicaffeine.com/logicaffeine_tv/tensor/fn.discharge): Discharge `o`: every lemma, each given up to `timeout_ms` for each of its two checks. The first lemma that is not proven gives the verdict.

## logicaffeine_tv::verdict
Result types for the translation validator.

- [enum SoundnessReport](https://docs.logicaffeine.com/logicaffeine_tv/verdict/enum.SoundnessReport): Outcome of cross-validating the LOGOS encoder against the tree-walking interpreter on one program (the meta-soundness check).
- [enum TvError](https://docs.logicaffeine.com/logicaffeine_tv/verdict/enum.TvError): Why building a symbolic summary failed.