PROOF-NEEDS.adoc

Proof Requirements — KRL

The single coherent story is PROOF-NARRATIVE.adoc. The assumption registry is ASSUMPTIONS.adoc. This file is the per-obligation checklist with status, prover, priority.

Proof Tier

Tier: T2 — High. KRL’s assurance must come from its actual parser, transformation implementations and resolution witnesses. QuandleDB implements the current fragment. Tangle is a separate language and supplies no inherited KRL proof guarantee.

Proof categories

Code	Meaning	Applies?
TP	Typing proofs (port-arity, lowering totality)	Yes
INV	Invariant proofs (round-trip, grammar refinement)	Yes
SEC	Security proofs	No
CONC	Concurrency proofs	No
ALG	Algorithm proofs (simplification correctness)	Yes
ABI	ABI/FFI proofs (Zig FFI boundary, Idris2 layout)	Yes (low priority)
DOM	Domain proofs (quandle equivalence soundness)	Yes

Obligations

#	Statement	Category	Prover	Priority	Effort	Status
KR-1	Accepted fragment operations execute with defined semantics or explicit refusal	TP	Idris2 + Julia property test	P1	1d	PARTIAL (retrieval and assurance-refusal assertions run in the Julia fragment workflow; general proof open)
KR-2	Construction/composition preserve checked port arity	TP	Idris2 + typechecker impl	P1	3d	NOT STARTED (typechecker not implemented)
KR-3	simplify is semantics-preserving (KR-3a: R1; KR-3b: R2; KR-3c: R3)	ALG	Lean4 or property test against quandle iso	P1	5d	OPEN (no KRL transformation implementation claimed)
KR-4	Pretty/parse round-trip: parse(pretty(e)) = e	INV	Julia property test (cheap)	P1	4h	NOT STARTED
KR-5	Idris2 SafePtr / Handle are load-bearing in the Zig FFI surface	ABI	Decision + wiring	P3	2h	DECISION PENDING
KR-6	Declared fragment agrees with quandledb/server/krl/Parser.jl	INV	Acceptance/rejection corpus	P1	—	PARTIAL (syntax, AST and execution/refusal checks; full conformance open)
KR-7	sigma N, cup N, etc. accepted iff N ≥ 1	INV	Grammar smoke test extension	P2	1h	DRAFT (example lexical checks only)
KR-8	equivalent? is sound w.r.t. fundamental-quandle isomorphism	DOM	Lean4 (factored through QuandleDB’s QD-3)	P1	5d	NOT STARTED

For full statements, why valuable, and the assumptions each obligation rests on, see PROOF-NARRATIVE.adoc. For the assumptions themselves, see ASSUMPTIONS.adoc.

Dangerous patterns (BANNED)

CI rejects any PR introducing any of these:

Pattern	Language	Meaning
believe_me	Idris2	Unsafe cast
assert_total	Idris2	Skip totality check
postulate	Idris2 / Agda	Unproven axiom
sorry	Lean4	Incomplete proof
Admitted	Coq	Incomplete proof
unsafeCoerce	Haskell	Unsafe cast
Obj.magic	OCaml / ReScript	Unsafe cast
unsafe (unaudited)	Rust	Unsafe block without safety comment

Enforced by panic-attack assail --proofs-only.

Where proofs go

verification/proofs/
├── idris2/   — ABI / type-level invariants (KR-1, KR-2, KR-5)
├── lean4/    — Semantic claims (KR-3, KR-8)
└── julia/    — Property tests against the declared QuandleDB fragment (KR-4, KR-6, KR-7)

References

• Current narrative and obligation dispositions.

• Surface contracts.

• hyperpolymath/quandledb/PROOF-NARRATIVE.md — database semantic obligations.

• Implementation under test: quandledb/server/krl/.