Research-Stack/audit/integration_audit.md

Integration Audit: Research-Stack Cross-Language Boundaries

Summary

Category	Count	Severity
Integration points identified	18	—
Critical type mismatches	3	CRITICAL
Error handling gaps	7	HIGH
Broken CLI contracts	2	HIGH
Workflow gaps / missing handoffs	5	MEDIUM
Race conditions	2	MEDIUM
Duplicate divergent Q16_16 libraries	2	HIGH
Generated files not properly managed	3	MEDIUM
sorry in proofs unchecked by CI	1	HIGH

---

Critical Issues

C1: Q16_16 Conversion Mismatch — Lean vs. Python vs. C [CRITICAL]

Files:

• 0-Core-Formalism/lean/Semantics/Semantics/FixedPoint.lean (lines 270-290)
• 0-Core-Formalism/lean/Semantics/BindServer.lean (lines 33-44)
• 4-Infrastructure/lib/q16.py
• 4-Infrastructure/auto/lib/q16.py
• 0-Core-Formalism/core/include/manifold_binary.h (lines 52-60)

Issue: Three different Q16_16 float conversion algorithms exist across the boundary:

1. Lean FixedPoint.lean: Uses (f * 65536.0).floor — rounds down (truncates toward zero)
2. Lean BindServer.lean: Uses (f * 65536.0).floor.toUInt32 — same floor, but goes through UInt32 with saturation at 0xFFFFFFFF/0x80000000
3. Python q16.py: Uses int(round(value * 65536)) — rounds to nearest (banker's rounding for .5)
4. C manifold_binary.h: Uses (q16_16_t)(f * (1 << 16)) — C cast truncates toward zero

Impact: Values near half-LSB boundaries (e.g., 1.00001) will diverge. A value of 1.5 / 65536.0 = 0.000022888... will be:

• Lean (floor): 1 (raw 65536)
• Python (round): 2 (raw 131072)
• C (truncation): 1 (raw 65536)

This affects all data flowing through the pipeline: spectral profiles, Sidon addresses, QUBO coefficients, and braid parameters.

Recommendation: Unify on a single conversion spec. The Lean floor approach is the most conservative and is formally specified; Python and C should match it.

---

C2: Duplicate Divergent Q16_16 Python Libraries [CRITICAL]

Files:

• 4-Infrastructure/lib/q16.py (1494 bytes, has q16_add, q16_sub, q16_mul, q16_div)
• 4-Infrastructure/auto/lib/q16.py (910 bytes, MISSING arithmetic ops)

Issue: Two copies of the Q16_16 Python library exist. The auto/ version is a strict subset — it lacks q16_add, q16_sub, q16_mul, q16_div, q16_gt, q16_ge. Scripts importing from auto/lib/ will fail at runtime if they call any arithmetic function.

Both use the same module name q16, creating import ambiguity depending on sys.path ordering.

Impact: Runtime AttributeError when arithmetic is attempted via the auto/ copy. The qaoa_adapter.py imports from ../lib but other shims may import from auto/lib.

Recommendation: Delete the auto/lib/q16.py stub or make it a re-export of the canonical lib/q16.py.

---

C3: Lean BindServer JSON Parsing Lacks Error Handling on Float Overflow [CRITICAL]

File: 0-Core-Formalism/lean/Semantics/BindServer.lean (lines 33-44)

@[inline]
def q16_16_of_float (f : Float) : UInt32 :=
  if f.isNaN || f >= 32768.0 then 0xFFFFFFFF
  else if f <= -32768.0 then 0x80000000
  else (f * 65536.0).floor.toUInt32

Issue: The 0xFFFFFFFF sentinel for NaN/overflow is indistinguishable from the bit pattern for -1/65536.0 in two's complement. When this UInt32 flows to C via JSON, manifold_binary.h's q16_16_from_float does NOT check for this sentinel — it will interpret 0xFFFFFFFF as (float)0xFFFFFFFF / 65536.0 = 65535.999985 instead of signaling an error.

Impact: Silent data corruption on NaN/overflow inputs. The C side has no way to detect that a sentinel value was transmitted.

Recommendation: Use an explicit JSON error field instead of a bit-pattern sentinel. Or, have the C side validate against 0xFFFFFFFF and return an error code.

---

C4: sorry in Generated Lean Theorems Never Checked by CI [HIGH]

Files:

• 4-Infrastructure/shim/eigensolid_pipeline.py (lines 270-310, Lean generation code)
• .github/workflows/math-check.yml

Issue: The eigensolid_pipeline.py generates Lean theorems where every proof body is sorry:

theorem symmetry_violation_0 : Prop := by
  sorry

The CI math-check.yml validates JSON schemas, DeepSeek receipts, and claims registries — but does NOT attempt to build or lint the generated .lean files. The sorry axioms accumulate unverified claims into the codebase.

Impact: Generated theorems provide false confidence. A downstream proof that depends on these sorry theorems will silently accept any conclusion.

Recommendation: Add a CI step that runs lake build on generated Lean files and rejects files containing sorry in theorem bodies.

---

Warnings

W1: lean_trace_bridge.py — No Exit Code Check from Proof Worker [HIGH]

File: 4-Infrastructure/shim/lean_trace_bridge.py (lines 118-140)

def prove_step(code: str, timeout_s: int = 120) -> dict:
    result = subprocess.run(
        ["curl", "-s", "--connect-timeout", "10", "-X", "POST", ...],
        capture_output=True, text=True, timeout=timeout_s,
    )
    if result.returncode != 0:
        return {"ok": False, "error": f"curl: {result.stderr[:200]}", ...}

Issue: Only checks curl's exit code, NOT the HTTP status code from the proof worker. A 500/404 from the worker would produce returncode == 0 from curl but with non-JSON body, leading to a JSONDecodeError that IS caught — but an HTTP 200 with {"ok": false, ...} is silently recorded as a failed step without raising any alarm.

Impact: Network errors and worker failures are silently logged as "failure" steps with no alerting mechanism.

Recommendation: Check the HTTP response status code explicitly and surface non-2xx responses as distinct error categories.

---

W2: eigensolid_pipeline.py — No Schema Version Validation on Input JSON [HIGH]

File: 4-Infrastructure/shim/eigensolid_pipeline.py (lines 456-460)

extraction = json.loads(extraction_path.read_text())

Issue: The extraction JSON is loaded without any schema validation. If the upstream CERN data format changes (e.g., renames conservation_laws to conservationLaws), the pipeline will silently produce empty outputs rather than fail.

Impact: Silent data loss on upstream format changes.

Recommendation: Add a JSON schema validation step and version check before processing.

---

W3: load_dependency_graph.py — Hardcoded Gremlin Credentials from .env [HIGH]

File: scripts/load_dependency_graph.py (lines 43-48)

ENV_FILE = ROOT / ".env.gremlin"
load_dotenv(ENV_FILE)
ENDPOINT = os.environ["GREMLIN_ENDPOINT"]
USERNAME = os.environ["GREMLIN_USERNAME"]
PASSWORD = os.environ["GREMLIN_PASSWORD"]

Issue: Requires .env.gremlin to exist with plaintext credentials. If the file is missing, the script crashes with KeyError. The credentials file is gitignored in most setups but may be accidentally committed.

Impact: Deployment fragility + potential credential leak.

Recommendation: Add graceful fallback when env vars are missing, and warn about the credential file in .gitignore.

---

W4: build_static.sh — Executable List May Be Stale [MEDIUM]

File: 0-Core-Formalism/lean/Semantics/build-static/build_static.sh (lines 26-28)

EXECUTABLES=(bindserver searchserver SemanticsCli openworm_benchmark \
    ExtremeParameterTestEval NominalParameterTestEval moim_benchmark \
    generate_sparkle_phi_s3c tangnano9k_emitter)

Issue: The list of executables is hardcoded. If the Lean lakefile.lean changes and adds/removes executables, this list will silently fail to build the new targets or crash trying to build removed ones.

Impact: Build inconsistency between lake build and the static compilation script.

Recommendation: Parse the executable list from lakefile.lean or use lake exe --list if available.

---

W5: pist_neuromorphic.c — Stats Export Destructively Modifies Frequency Data [MEDIUM]

File: 6-Kernel-Shim/pist_neuromorphic.c (lines 433-445)

for (i = 0; i < 10 && pos < PAGE_SIZE - 64; i++) {
    int max_idx = 0;
    // ...find max...
    pos += sprintf(buf + pos, " %02x=%llu", max_idx, st->byte_freq[max_idx]);
    st->byte_freq[max_idx] = 0; /* zero out for next iter (destructive!) */
}

Issue: The stats_show sysfs handler zeroes out byte frequencies while formatting the output. A concurrent read will see corrupted (partially zeroed) data. This is a race condition within a single show call, not even requiring concurrent readers.

Impact: Frequency data is corrupted after the first read. Subsequent reads show only zeros for the top-10 frequencies.

Recommendation: Copy the frequency array before formatting, or use a non-destructive selection algorithm (e.g., min-heap for top-k).

---

W6: qaoa_adapter.py — Optional Backend Imports Fail Silently [MEDIUM]

File: 4-Infrastructure/shim/qaoa_adapter.py (lines 40-52)

try:
    import cirq
    _HAS_CIRQ = True
except ImportError:
    _HAS_CIRQ = False

Issue: All three quantum backends (cirq, qiskit, numpy) are optional. If none are installed, many functions will fail at call time rather than import time. The qaoa_solve_qubo function references _HAS_CIRQ and _HAS_QISKIT but may still proceed to use numpy-dependent code that expects np to exist.

Impact: Late failure with confusing error messages when quantum backends are missing.

Recommendation: Add a runtime check at module load that at least numpy is available, and raise a clear ImportError if not.

---

W7: batch_compute.yml — Uses actions/checkout@v4 (Outdated) [LOW]

File: .github/workflows/batch_compute.yml (line 31)

uses: actions/checkout@v4

Issue: Other workflows in the same repo use actions/checkout@v6 (e.g., math-check.yml). Version mismatch may lead to different behavior around LFS handling, fetch-depth, etc.

Impact: Inconsistent CI behavior between workflows.

Recommendation: Standardize on actions/checkout@v6 across all workflows.

---

W8: manifold_binary.c — Deserialization Does Not Validate Array Bounds [MEDIUM]

File: 0-Core-Formalism/core/src/manifold_binary.c (lines 71-130)

Issue: manifold_binary_deserialize validates the header magic and version, but does NOT validate that num_shells * sizeof(PistShell) etc. won't overflow a size_t. On a maliciously crafted input with very large num_shells, the malloc() call may succeed (returning NULL or a wrapped size) and the subsequent memcpy will write out of bounds.

Impact: Potential buffer overflow on untrusted binary input.

Recommendation: Add bounds checks: if (num_shells > MAX_SHELLS) return -5; before allocation.

---

W9: eigensolid_pipeline.py Generated Lean File Missing end Namespace Check [MEDIUM]

File: 4-Infrastructure/shim/eigensolid_pipeline.py (lines 265-275)

lines.append("end Semantics.CERNEigensolidData")
return "\n".join(lines)

Issue: The generated Lean code is always wrapped in namespace Semantics.CERNEigensolidData / end Semantics.CERNEigensolidData. However, the generated content may contain syntax errors (e.g., malformed identifiers from lean_ident) that cause lake build to fail on the entire file, blocking all other modules.

Impact: A single malformed theorem name can break the entire Lean build.

Recommendation: Run lake build on generated files before they are checked in, and isolate generated files into a separate lake package.

---

W10: load_dependency_graph.py — Theorem Body Parsing Is Fragile [MEDIUM]

File: scripts/load_dependency_graph.py (lines 108-140)

Issue: The theorem body extraction uses a heuristic that walks lines until the next theorem , lemma , or def . This will fail for:

• Nested def inside a where clause
• theorem mentioned in a comment string inside a proof
• Tactics that output these keywords in error messages

Impact: Incorrect theorem body extraction leads to wrong dependency edges in the Gremlin graph.

Recommendation: Use Lean's server protocol (lean --server) for accurate AST-based parsing, or at minimum add a TODO acknowledging the heuristic nature.

---

Per-Pipeline Breakdown

Pipeline A: Equation → Eigensolid → Lean Theorems

Files: eigensolid_pipeline.py → CERNEigensolidData.lean → lake build

Step	Output	Handoff Risk
CERN parquet → DataFrame	pd.DataFrame	Medium — column names hardcoded
Extraction JSON → dict	dict	High — no schema validation
Spectral profile → Sidon address	SidonAddress	Medium — threshold hardcoded
Sidon address → Lean code	str (Lean text)	High — sorry in every proof
Lean text → file	.lean file	Medium — no build verification

Gap: The generated Lean file is written to disk but never compiled or checked by CI. The sorry placeholder means no mathematical validation occurs.

Race Condition: If the pipeline is run concurrently with different --alpha values, the output .lean file will be overwritten without version tracking.

---

Pipeline B: Lean Proof → Trace Capture → Gremlin Graph

Files: lean_trace_bridge.py → trace.json → load_dependency_graph.py → Gremlin

Step	Output	Handoff Risk
Lean code → proof worker	HTTP POST	High — no HTTP status check
Proof worker → JSON response	dict	Medium — malformed responses ignored
Trace → JSON file	trace.json	Low
All files → Gremlin	Gremlin vertices/edges	High — credential file dependency

Gap: Phase 7 verification queries run after loading but do NOT check that theorem bodies contain valid Lean syntax — only that the graph structure is connected.

---

Pipeline C: Q16_16 ↔ QUBO ↔ QAOA Circuit ↔ Receipt

Files: qaoa_adapter.py → qubo_highs.py → receipt JSON

Step	Languages	Handoff Risk
Lean QUBOFormulation → Python QUBO	Lean ↔ Python	Critical — Q16_16 conversion mismatch
Python QUBO → HiGHS MIP	Python ↔ C++	Medium — optional dependency
HiGHS solution → receipt	Python → JSON	Low

Gap: The qaoa_adapter.py imports from braid_search which may not be available, and the fallback _fallback_bracket_qubo uses different coefficients than the original. This means QUBO results depend on which modules are importable, not just the input data.

---

Pipeline D: C Kernel → Sysfs → Userspace Daemon

Files: pist_compress.c / pist_neuromorphic.c → /sys/kernel/pist*/ → (daemon implied)

Step	Output	Handoff Risk
Kernel module → sysfs	text/binary	Medium — stats_show is destructive
sysfs → userspace	(not implemented)	High — no daemon in repo

Gap: There is NO userspace daemon in the repository that reads from /sys/kernel/pist_neuromorphic/dag_dump. The dag_generation counter increments but nothing consumes it. The DAG export functionality is incomplete.

---

Pipeline E: Lean Static Build → FPGA Bitstream

Files: build_static.sh → lake exe tangnano9k_emitter → Verilog → FPGA

Step	Output	Handoff Risk
Lean → C → static binary	ELF	Medium — hardcoded executable list
Static binary → Verilog	.v files	Medium — lake exe may fail silently
Verilog → FPGA bitstream	.bit	High — no CI for this path

Gap: The build_static.sh script references 5-Applications/out/verilog/build_tangnano9k.sh which may not exist in all environments. The FPGA synthesis path has no CI coverage.

---

Type Mismatch Matrix

Type	Lean Definition	Python Implementation	C Implementation	Consistent?
Q16_16 scale	65536 (q16Scale)	65536 (Q16_SCALE)	1 << 16 = 65536	YES
Q16_16 float→raw	(f * 65536.0).floor	int(round(v * 65536))	(int32_t)(f * 65536)	NO
Q16_16 raw→float	Float.ofInt q.toInt / 65536.0	value / 65536	(float)q / 65536	YES
Q16_16 NaN sentinel	infinity = q16MaxRaw	None	None	NO
Q16_16 overflow	Saturates to maxVal/minVal	No saturation check	No saturation check	NO
Sidon set	[1, 2, 4, 8, 16, 32, 64, 128]	Same (Python)	Not in C	N/A
JSON Q16_16	{"val": <int>}	Raw int	Not used	NO

---

Generated Files Status

File	Generated By	Checked In?	Should Be?
CERNEigensolidData.lean	eigensolid_pipeline.py	Likely NO	NO (regenerate in CI)
eigensolid_analysis.json	eigensolid_pipeline.py	Likely NO	NO (CI artifact)
shared-data/data/stack_solidification/*.json	Various shims	Partially YES	YES (receipts)
4-Infrastructure/shim/burgers_chaos_game_receipt.json	burgers_chaos_game.py	YES	YES (example receipt)
4-Infrastructure/shim/eigensolid_analysis/	eigensolid_pipeline.py	Unknown	NO (CI output)
.lake/build/bin/*	lake build	NO (gitignored)	NO (build output)

Note: The repository contains some checked-in receipts (shared-data/data/stack_solidification/*.json) but the generation pipeline for these is not documented in CI. This creates a risk that checked-in receipts are stale relative to the generating code.

---

CI Workflow Gaps

Workflow	Tests Lean Build?	Tests Q16_16 Roundtrip?	Tests Kernel Module?	Tests Receipt Integrity?
math-check.yml	NO	NO	NO	YES (SHA-256)
wolfram-verification.yml	NO (only comments)	NO	NO	NO
batch_compute.yml	NO	NO	NO	NO
lean_action_ci.yml	YES (OTOM subproject)	NO	NO	NO

Gap: No CI workflow tests the full roundtrip: Lean Q16_16 → JSON → Python → C → back to Lean. A dedicated integration test should:

1. Generate Q16_16 values in Lean
2. Export via BindServer JSON
3. Parse in Python with q16.py
4. Serialize via manifold_binary.h format
5. Deserialize in C
6. Roundtrip back to Lean
7. Verify bit-exact equality

---

Recommendations (Priority Order)

1. Unify Q16_16 conversion: Standardize on floor semantics across all three languages. Add a conformance test.
2. Deduplicate q16.py: Remove the auto/lib/ copy or make it re-export from lib/.
3. Add NaN/error propagation: Use JSON {"error": "overflow"} instead of 0xFFFFFFFF sentinel.
4. Build generated Lean in CI: Add lake build step for all generated .lean files. Reject sorry.
5. Fix destructive stats_show: Copy frequency array before formatting in pist_neuromorphic.c.
6. Add schema validation: Validate extraction JSON against a schema before processing.
7. Complete the kernel userspace bridge: Implement or document the DAG consumer daemon.
8. Add roundtrip integration test: Test the full Lean→Python→C→Lean data flow in CI.