# SemanticVerifier

[![CI](https://github.com/collective-mind/semantic_verifier/actions/workflows/ci.yml/badge.svg)](https://github.com/collective-mind/semantic_verifier/actions/workflows/ci.yml)
[![Hex.pm](https://img.shields.io/hexpm/v/semantic_verifier.svg)](https://hex.pm/packages/semantic_verifier)
[![Hex Docs](https://img.shields.io/badge/hex-docs-purple.svg)](https://hexdocs.pm/semantic_verifier)
[![License](https://img.shields.io/badge/license-Apache%202.0-blue.svg)](https://github.com/collective-mind/semantic_verifier/blob/main/LICENSE)

**SemanticVerifier** is a formal verification engine for FrameNet Semantic IR in Elixir, leveraging the **Z3 SMT Theorem Prover** to eliminate dead branches and enforce safety invariants before AST compilation.

---

## Key Features

* **Two-Phase Verification:** Structural checking with `NimbleOptions`, followed by first-order logic proving via `Z3`.
* **Zero-Disk Session Pool:** In-memory interactive Port pool (`z3 -in -smt2`) eliminating temporary file I/O.
* **Dead Code Detection:** Identifies unreachable branches and shadowed conditions.
* **Counter-Example Extraction:** Parses SMT `(get-model)` outputs into structured Elixir maps.
* **Self-Healing AST Engine:** Automatically prunes dead code and synthesizes missing preconditions.

---

## Demo

The two sessions below were run with `iex -S mix`; the same calls are collected in [`examples/demo_pipeline.exs`](examples/demo_pipeline.exs).

### 1. Happy path — a valid IR verifies cleanly

The frame declares the preconditions its safety constraint needs, so verification returns `{:ok, verified}` with no errors and no recovery candidates. The enriched IR adds a `"branches"` key to every frame and top-level `errors`/`recovery_candidates` alongside their atom-keyed counterparts.

```elixir
iex> ir = %{
...>   "intent" => "sample_pipeline",
...>   "frames" => [
...>     %{
...>       "id" => "f1",
...>       "frame" => "Reading",
...>       "FE" => %{"Source" => "file.txt"},
...>       "Preconditions" => ["Exists(file.txt)", "Readable(file.txt)"]
...>     }
...>   ],
...>   "constraints" => ["Readable(file.txt)"]
...> }
iex> {:ok, verified} = SemanticVerifier.verify(ir)
{:ok,
 %{
   :errors => [],
   "constraints" => ["Readable(file.txt)"],
   "errors" => [],
   "frames" => [
     %{
       "FE" => %{"Source" => "file.txt"},
       "Preconditions" => ["Exists(file.txt)", "Readable(file.txt)"],
       "branches" => [],
       "frame" => "Reading",
       "id" => "f1"
     }
   ],
   "intent" => "sample_pipeline",
   "recovery_candidates" => []
 }}
```

### 2. Violated invariant — counter-example and recovery candidate

The frame reads `protected.txt` but declares no preconditions, so `Readable(protected.txt)` cannot be formally proven. The returned `%SemanticVerifier.Error{}` carries the violated constraint plus a concrete Z3 counter-example model (`Readable -> false`), and the enriched IR proposes adding the missing precondition — exactly what `SemanticVerifier.auto_heal/1` applies.

```elixir
iex> invalid_ir = %{
...>   "intent" => "violation_test",
...>   "frames" => [
...>     %{"id" => "f1", "frame" => "Reading", "FE" => %{"Source" => "protected.txt"}, "Preconditions" => []}
...>   ],
...>   "constraints" => ["Readable(protected.txt)"]
...> }
iex> {:error, [error | _], enriched_ir} = SemanticVerifier.verify(invalid_ir)
{:error,
 [
   %SemanticVerifier.Error{
     id: "err_39536691",
     category: "IOError",
     cause: "SMT_MODEL_COUNTER_EXAMPLE",
     violated_constraint: "Readable(protected.txt)",
     affected_node: "f1",
     target: nil,
     impact: "Safety invariant 'Readable(protected.txt)' cannot be formally proven.",
     smt_status: :sat_violation_found,
     counter_example: %{
       functions: %{
         "Exists" => %{parameters: [["x!0", "Resource"]], return_type: "Bool", interpretation: true},
         "IsFile" => %{parameters: [["x!0", "Resource"]], return_type: "Bool", interpretation: true},
         "Readable" => %{parameters: [["x!0", "Resource"]], return_type: "Bool", interpretation: false},
         "Writable" => %{parameters: [["x!0", "Resource"]], return_type: "Bool", interpretation: true}
       },
       raw_model: "(\n  ;; universe for Resource:\n  ;;   Resource!val!0 \n  ;; -----------\n  ;; definitions for universe elements:\n  (declare-fun Resource!val!0 () Resource)\n  ;; cardinality constraint:\n  (forall ((x Resource)) (= x Resource!val!0))\n  ;; -----------\n  (define-fun protected.txt () Resource\n    Resource!val!0)\n  (define-fun IsFile ((x!0 Resource)) Bool\n    true)\n  (define-fun Exists ((x!0 Resource)) Bool\n    true)\n  (define-fun Readable ((x!0 Resource)) Bool\n    false)\n  (define-fun Writable ((x!0 Resource)) Bool\n    true)\n)",
       constants: %{"protected.txt" => "Resource!val!0"}
     }
   }
 ],
 %{
   :errors => [ ... ],
   :recovery_candidates => [
     %{
       reason: "Explicitly enforce 'Readable(protected.txt)' prior to execution",
       action: "AddPrecondition",
       constraint: "Readable(protected.txt)",
       target: "f1",
       confidence: 0.95,
       risk: "Low"
     }
   ],
   "constraints" => ["Readable(protected.txt)"],
   "errors" => [],
   "frames" => [ ... ],
   "intent" => "violation_test",
   "recovery_candidates" => []
 }}
```

> The error `id` is derived deterministically from the violated constraint. The `raw_model` string is emitted by Z3 and may vary slightly across Z3 versions. For brevity, the enriched IR above elides the repeated error under `:errors`/`"errors"` and the frames (each frame gains `"branches" => []`); `examples/demo_pipeline.exs` prints the complete output.

---

## Requirements

Requires the **Z3 SMT Solver** CLI:

* **macOS:** `brew install z3`
* **Ubuntu/Debian:** `sudo apt-get install -y z3`

---

## Installation

Add `semantic_verifier` to `mix.exs`:

```elixir
def deps do
  [
    {:semantic_verifier, "~> 0.1.0"}
  ]
end
```