Skip to content

M20: Idris2 → Zig SNIF parser port + verify/ differential-test rig [hypatia#294 unlock] #367

@hyperpolymath

Description

@hyperpolymath

Context

hypatia#294 ruled Option A (split) on 2026-05-27. VCL parse + typecheck runs inside a wasm32-freestanding Zig SNIF (zero imports, no I/O, no clock, no network). The Idris2 reference parser in vcl-ut is canonical; this port differential-tests against it. The VCL → DB hop is host-side via verisim-nif (verisimdb#61).

References:

  • hypatia#294 (boundary ruling, A — split)
  • hypatia#273 (parent architecture-reconciliation epic, Gap 2)
  • docs/architecture/boundary-design-options.adoc (design memo)
  • docs/operations/issue-294-boundary-recommendation.adoc (recommendation memo, committed 2026-05-24)
  • vcl-ut (Idris2 reference parser — canonical)

Scope

  • Port Idris2 VCL parser core to Zig (wasm32-freestanding target — no I/O, no clock, no network, zero imports)
  • Build into a wasm artifact suitable for the existing hypatia SNIF runner
  • Add verify/ differential-test rig: corpus of VCL queries fed to both the Idris2/ReScript reference and the new Zig SNIF; AST equality assertion
  • Wire into lib/verisim_connector.ex once M19 lands — VCL query string → SNIF parse + typecheck → host-side verisim-nif call
  • CI: differential-test rig runs on every PR touching the parser

Estimated effort

~2–3 person-weeks (per the recommendation memo).

Dependencies

  • Blocked by verisimdb#61 (real verisim-nif) for the final verisim_connector.ex retarget step.
  • The parser port + verify/ rig itself can start in parallel; only the connector wire-up waits on M19.

Companion

verisimdb#61 tracks the real verisim-nif implementation; together M19 + M20 close hypatia#294 + hypatia#273 Gap 2.

Metadata

Metadata

Assignees

No one assigned

    Labels

    enhancementNew feature or request

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions