Skip to content

PROOF-STATUS.adoc

Latest commit

 

History

History
131 lines (95 loc) · 4.22 KB

PROOF-STATUS.adoc

File metadata and controls

131 lines (95 loc) · 4.22 KB
Raw

Proof Status — KRL

Requirements: PROOF-NEEDS.md. Single coherent story: PROOF-NARRATIVE.md. Assumption registry: ASSUMPTIONS.md.

This file tracks the per-obligation status. Updated 2026-06-01.

Summary

Category Total Done In Progress Partial Blocked Not Started

Typing (TP)

2

0

0

0

0

2

Invariant (INV)

3

0

0

2

0

1

Algorithm (ALG)

1

0

0

1

0

0

ABI (ABI)

1

0

0

0

0

1 (decision pending)

Domain (DOM)

1

0

0

0

0

1

Total

8

0

0

3

0

5

Overall: 0% proven, 37.5% partial (KR-3, KR-6, KR-7).

The partial entries (KR-3 simplification across compose() and KR-7 generator index validity) have implementations or smoke coverage but no property test or formal proof.

Proofs done

ID Proof Prover File Date Verified by

—

none yet at the KRL surface level

—

—

—

—

The Tangle core proofs (Progress, Preservation, Determinism, Type Safety + 12 lemmas, 16 results total) in hyperpolymath/tangle/proofs/Tangle.lean are foundational for KRL because KRL lowers into Tangle. They are tracked in tangle’s PROOF-STATUS, not here.

Proofs in progress

ID Proof Prover Assignee Started Blocker

—

—

—

—

—

—

Proofs partial

ID Proof Form Notes

KR-3

simplify semantics-preserving

Property test in KRLAdapter.jl/test/

R1 + R2 (within a single sigma sequence) covered. R2 across compose() not covered. R3 implementation gap. See quandledb/PROOF-NARRATIVE.md QD-2.

KR-6

Fragment grammar and actual parser must agree

Conformance corpus tests/conformance/retrieval_fragment.jl (11 checks) + differential_test.jl (canonical projection determinism)

Two-parser equivalence VOID (KRLAdapter gone). Re-scoped to fragment conformance per PROOF-NARRATIVE. See docs/v0.1.0-subset.md for historical two-parser design.

KR-7

sigma N accepted iff N ≥ 1

Parser error path

Not property-tested. Lexical check in grammar_smoke.sh only.

Proofs blocked

ID Proof Blocked by

KR-2

Lowering preserves port arity

Typechecker not yet implemented (see READINESS.md)

KR-3c

R3 invariance

KnotTheory.jl has no R3 simplifier (see quandledb QD-2)

Proofs remaining

ID Proof Category Prover Priority Effort

KR-1

lower total on parseable programs

TP

Idris2 + property test

P1

1d

KR-2

lower preserves port arity

TP

Idris2 + impl

P1

3d

KR-3

simplify semantics-preserving

ALG

Lean4 / property

P1

5d

KR-4

Pretty/parse round-trip

INV

Property

P1

4h

KR-5

ABI primitives load-bearing

ABI

Decision

P3

2h

KR-6

Fragment grammar and actual parser must agree (was two-parser equivalence)

INV

Conformance corpus tests/conformance/retrieval_fragment.jl + differential_test.jl (canonical projection design in docs/v0.1.0-subset.md)

P1

2d (1d subset doc + 1d harness)

KR-7

Generator index validity

INV

Property test

P2

1h

KR-8

equivalent? sound

DOM

Lean4 (via QuandleDB QD-3)

P1

5d

Verification commands

# Check all Idris2 proofs
just proof-check-idris2

# Check all Lean4 proofs
just proof-check-lean4

# Run all proof checks
just proof-check-all

# Scan for dangerous patterns
panic-attack assail --proofs-only

Changelog

Date Change By

2026-04-04

Initial proof status tracking

Template (rsr-template-repo)

2026-06-01

Replaced template-content scaffold with KRL-specific obligations KR-1..KR-8. Deleted template-content proof files (Coq/Lean/Idris) that had zero KRL content.

Audit

2026-09-20

KR-6 re-scoped: two-parser equivalence VOID (KRLAdapter gone), now fragment grammar vs actual parser agreement. Added docs/v0.1.0-subset.md with canonical projection design, added tests/conformance/differential_test.jl with determinism checks and skipped two-parser test. Updated partial count 2→3.

Agent