Karpal v0.5.0

0.5.0 Release

New crates

• karpal-diagram — monoidal categories, string-diagram DSL, coherence witnesses, verification integration (Phase 13, complete)
• karpal-schubert-types — Schubert intersection type system (Phase 14 A–C)

Phase 12 — karpal-verify extensions

• Kani verification backend with harness generation
• GPU compute obligation builders for Metal/MSL kernel contracts
• karpal-verify-derive companion proc-macro crate (#[export_obligations])
• karpal-proof bridge (ProofBridge, ProofEvidence) for proof-derived certificates
• Continuous verification CI workflow

Phase 13 — karpal-diagram (complete)

• Monoidal category traits: Tensor, Braiding, Symmetry, Trace
• String-diagram DSL with Identity, Box, Sequence, Parallel, Swap, Cup, Cap nodes
• Runtime diagram normalization with NormalizationTrace and 6 rewrite rules
• Compact-closed cup/cap yanking normalization
• Text and SVG renderers
• Type-level coherence witnesses: PentagonIdentity, TriangleIdentity, HexagonIdentity
• Diagrammatic rewriting bridge: ByNormalization, ByYanking, equivalent_proved(), prove_yanking()
• Verification integration: CoherenceCertificate, coherence_certificates()

Phase 14 — karpal-schubert-types (A–C, 0.5.0 scope)

• SchubertType — Schubert classes in Grassmannians via amari-enumerative
• Intersection / IntersectionKind — LR coefficient intersection with structured zero classification
• SchubertTyped trait + SchubertProven<M, T> proof-carrying values
• compose_checks() — chained type-check composition via LR rule
• External verification: schubert_bundle() + verify_schubert() with 3 obligation types

Licensing

All 0.5.0+ crates use AGPL-3.0-or-later. The 0.4.x support line remains available under MIT OR Apache-2.0.