Synthesis & equivalence
Protect the shape of important computations while checking that their intended results are preserved.
Reconstruct the computation itself#
Counterexample-Guided Inductive Synthesis, or CEGIS, searches for an alternative computation from behavior and counterexamples. In the engine’s eligible pure scalar regions, candidate expressions are constructed in a different Boolean-arithmetic basis and evaluation structure. This can change the expression graph rather than merely decorate its instructions.
A counterexample improves the next candidate#
A candidate is submitted to regional translation validation. If the validator finds an input on which the candidate diverges, that witness is fed back into synthesis. The next candidate must account for it. This creates a search-and-proof loop with explicit outcomes instead of accepting a formula because it happened to pass a handful of examples.
Only a proved regional rewrite is accepted#
The validator distinguishes PROVED, COUNTEREXAMPLE_FOUND, OUT_OF_SCOPE and UNKNOWN_BUDGET_EXCEEDED. Only PROVED is an acceptance result. Running out of solver budget does not become success, and a region outside the supported semantic model cannot borrow a proof from a different scope.
Explore the validator’s decision rules. This diagram does not run a solver.
R₀(x)R₁(x)Results + traps + entry preconditions
The candidate is accepted within the declared regional model and entry preconditions. The verdict concerns that rewrite, not the entire application.
A concrete input exposes a difference. Reject this candidate and feed the witness back into the synthesis process.
The region violates supported purity, ownership, frame or boundary obligations. It cannot be accepted under this model.
The solver exhausted its budget without a proof. An inconclusive run does not authorize the rewrite and is not cached as a successful proof.
The proof has a precise contract#
The regional model compares exact 32/64-bit results and trap behavior under declared entry preconditions and frame obligations. Signed widths, overflow and division by zero belong to that contract. The implementation has regression cases for missing preconditions, mismatching trap channels and inconclusive solver runs, including proof-cache behavior.
This is a scoped correctness property of an accepted region rewrite. It is not a proof that an entire application is bug-free, or that the protected program cannot be reverse engineered. Application validation and the security model remain separate responsibilities.