Module symexec 

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

The executor walks the AST and produces a SymSummary: the ordered sequence of Show outputs and a sticky “an observable error occurred” condition, each expressed as a VerifyExpr over the program’s free inputs. Two summaries can then be compared for observable equivalence by the SMT backend (crate::equiv).

Verifiable Core (this phase)

Straight-line Int/Bool programs: integer literals, booleans, + - *, signed comparisons, == !=, and/or (logical on Bool, bitwise on Int), not, Let, Set, and Show … to show. Int is modeled as a 64-bit bitvector so wrapping/overflow matches the interpreter’s native i64. Anything outside the fragment yields Unsupported — never a silent or wrong result.

Structs

SymSummary

The observable summary of a program: the ordered Show outputs plus the condition under which the program raised an observable error.

Unsupported

A construct outside the currently-supported Verifiable Core. Carries a human reason so the validator can report Unverified(reason) rather than ever guessing.

Enums

SymValue

A symbolic LOGOS value: an integer (64-bit bitvector), a boolean, or a channel handle.

Constants

INT_WIDTH

Bit width used to model LOGOS Int (native i64).

Functions

execute

Symbolically execute a program (a sequence of statements) into a SymSummary.

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.