fix(p1): VCLTypeChecker ArgumentError + null-byte sanitisation in VCLBridge

VCLTypeChecker (P1a):
- do_normalize/1: rescue ArgumentError from String.to_existing_atom/1 so
  unknown proof type strings degrade to :unknown instead of crashing the
  process. Existing "rejects unknown proof type" test now passes cleanly.

VCLBridge built-in parser (P1b):
- tokenize/1: reject queries containing null bytes with {:error, msg}.
  Null bytes in entity IDs truncate C strings silently at the Rust FFI
  boundary, enabling entity ID forgery via truncation.
- Add 3 tests in vcl_test.exs covering: null byte in entity ID, null byte
  in WHERE clause, clean query accepted.

STATE updated: both P1 blockers removed, mix-test-failures count corrected.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: hyperpolymath

.machine_readable/6a2/STATE.a2ml

@@ -17,7 +17,7 @@ phase = "Phase 5 — Tropical Consonance + KRL Integration"
 [current-position]
 milestone = "verisim-modular-experiment tropical bridge v0.2 + bellman_ford proved"
 last-session = "2026-04-11"
-last-action = "Closed bellman_ford OFFICIAL SORRY 2 — full min-plus Bellman-Ford proof in Tropical_Matrices_Full.thy. All Isabelle sorries gone (0 remaining)."
+last-action = "VQL→VCL rename (303 files); P1 hardening: VCLTypeChecker ArgumentError fixed, null-byte sanitisation added to VCLBridge tokenizer"
 
 [tropical-bridge]
 status = "v0.2 — RI + RII live, RIII stub (KnotTheory.jl r3_simplify is no-op)"
@@ -42,24 +42,20 @@ benchmarks = "2 Rust files (modality_benchmarks.rs + throughput_benchmarks.rs)"
 total-new-tests = "43 new tests + 5 properties (2026-04-04)"
 
 [test-status]
-mix-test-failures = "6 pre-existing (VCLTypeChecker binary_to_existing_atom crash, KRaft remove_server timeout)"
+mix-test-failures = "1 pre-existing (KRaft remove_server timeout)"
 new-test-failures = "0"
 cargo-bench-compile = "PASS (throughput_benchmarks.rs — no errors, no warnings in bench file)"
 gleam-smoke = "Written; requires compiled lith_nif.so to run connection/lifecycle tests"
 
 [blockers]
-- "VCLTypeChecker calls :erlang.binary_to_existing_atom for unknown proof types → ArgumentError (P1 hardening gap)"
-- "VCL parser does not strip null bytes from entity IDs (C-string truncation risk at FFI, P1)"
 - "Integration test (tests/integration_test.rs) uses old API — does not compile (pre-existing)"
 - "modality_benchmarks.rs uses old API — does not compile (pre-existing)"
 
 [route-to-mvp]
 next = "Add Tropical_Determinants.thy + ProofOptimalAssignment VCL clause"
-then = "Fix VCLTypeChecker binary_to_existing_atom crash (P1 hardening)"
-then = "Fix null-byte entity ID sanitisation in VCL parser"
 then = "Update integration_test.rs to current API"
+then = "Update modality_benchmarks.rs to current API"
 
 [critical-next-actions]
 1 = "Tropical_Determinants.thy new file — permanent = optimal assignment"
-2 = "Fix VCLTypeChecker to use String.to_existing_atom with rescue guard (P1)"
-3 = "Add null-byte sanitisation in VCLBridge built-in parser (P1)"
+2 = "Update integration_test.rs to current API"

verisimdb/elixir-orchestration/lib/verisim/query/vcl_bridge.ex

@@ -347,13 +347,19 @@ defmodule VeriSim.Query.VCLBridge do
   end
 
   defp tokenize(input) do
-    # Simple whitespace-aware tokenizer
-    tokens =
-      input
-      |> String.replace(~r/\s+/, " ")
-      |> String.split(" ", trim: true)
+    # Reject null bytes before tokenising: they truncate C strings silently at the
+    # Rust FFI boundary, allowing entity IDs to be forged via truncation.
+    if String.contains?(input, "\0") do
+      {:error, "VCL query contains null bytes"}
+    else
+      # Simple whitespace-aware tokenizer
+      tokens =
+        input
+        |> String.replace(~r/\s+/, " ")
+        |> String.split(" ", trim: true)
 
-    {:ok, tokens}
+      {:ok, tokens}
+    end
   end
 
   defp parse_tokens(tokens) do

verisimdb/elixir-orchestration/lib/verisim/query/vcl_type_checker.ex

@@ -308,8 +308,16 @@ defmodule VeriSim.Query.VCLTypeChecker do
   defp normalize_proof_type(_), do: :unknown
 
   defp do_normalize(str) when is_binary(str) do
-    atom = str |> String.downcase() |> String.to_existing_atom()
+    # String.to_existing_atom/1 raises ArgumentError for atoms not yet interned.
+    # Rescue it so unknown proof type names degrade to :unknown instead of crashing.
+    atom =
+      str
+      |> String.downcase()
+      |> String.to_existing_atom()
+
     if atom in @known_proof_types, do: atom, else: :unknown
+  rescue
+    ArgumentError -> :unknown
   end
   defp do_normalize(atom) when is_atom(atom) do
     if atom in @known_proof_types, do: atom, else: :unknown

verisimdb/elixir-orchestration/test/verisim/query/vcl_test.exs

@@ -246,4 +246,28 @@ defmodule VeriSim.Query.VCLTest do
       assert is_map(ast)
     end
   end
+
+  # ===========================================================================
+  # Security: null-byte sanitisation (P1 hardening)
+  # ===========================================================================
+
+  describe "null-byte sanitisation" do
+    test "rejects query containing a null byte" do
+      # Null bytes in entity IDs truncate C strings at the Rust FFI boundary,
+      # allowing forged IDs. The built-in parser must reject them.
+      assert {:error, msg} = VCLBridge.parse("SELECT GRAPH FROM HEXAD abc\0evil")
+      assert msg =~ "null"
+    end
+
+    test "rejects query with null byte in WHERE clause" do
+      assert {:error, msg} =
+               VCLBridge.parse("SELECT GRAPH FROM HEXAD abc-123 WHERE GRAPH.id = 'ok\0bad'")
+
+      assert msg =~ "null"
+    end
+
+    test "clean query without null bytes is accepted" do
+      assert {:ok, _ast} = VCLBridge.parse("SELECT GRAPH FROM HEXAD abc-123")
+    end
+  end
 end