Skip to content

V-L3-D1: verification/ tree is empty scaffolding — populate or strip #15

@hyperpolymath

Description

@hyperpolymath

Context

The top-level README claims:

Idris2 proofs (in src/interface/abi/) verify drift detection correctness, provenance chain integrity, temporal version ordering, sidecar isolation.

The actual verification/ tree contains eight empty subdirectories (benchmarks/, coverage/, fuzzing/, proofs/, safety_case/, simulations/, tests/, traceability/) — each with a ~20-byte README.adoc and an a2ml manifest. Zero proofs, zero benchmarks, zero fuzzing, zero safety case.

A reader who follows the README's claim is misled.

Decision needed

Pick one:

A. Populate — accept that verification/ is part of the product surface, and file follow-up issues (one per subdir) to add at least a stub proof / benchmark / fuzz target. Don't pretend Idris2 proofs exist until they do.

B. Strip — delete the empty verification/ subtree, remove the README's claims about Idris2 verification, and re-add the folder only when there's something to put in it.

Recommendation: B in the short term. Add verification/ back with a single concrete artifact (e.g. a proptest harness) when V-L1-C1 (Tier 1 SQLite piggyback) lands.

Acceptance

  • Decision recorded as docs/decisions/ADR-0002-verification-tree.adoc
  • README and ROADMAP updated to match reality
  • No verification/*/README.adoc shorter than its parent directory's name

Metadata

Metadata

Assignees

No one assigned

    Labels

    documentationImprovements or additions to documentation

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions