Skip to content

Commit 4f6b1f8

Browse files
hyperpolymathclaude
andcommitted
chore: add K9 Kennel-level metadata guard
Proof system invariants: 0 Admitted max, forbidden proof bypass patterns, multi-prover support declared. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
1 parent c52df41 commit 4f6b1f8

1 file changed

Lines changed: 91 additions & 0 deletions

File tree

Lines changed: 91 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,91 @@
1+
K9!
2+
# SPDX-License-Identifier: PMPL-1.0-or-later
3+
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
4+
# K9 Kennel-level guard: echidna project metadata and proof-system invariants
5+
# Security Level: Kennel (data-only, no execution)
6+
# No signature required
7+
8+
{
9+
pedigree = {
10+
schema_version = "1.0.0",
11+
component_type = "proof-tool-metadata",
12+
security = {
13+
leash = 'Kennel,
14+
trust_level = "data-only",
15+
allow_network = false,
16+
allow_filesystem_write = false,
17+
allow_subprocess = false,
18+
},
19+
metadata = {
20+
name = "echidna-metadata",
21+
version = "2.1.0",
22+
description = "Echidna: neurosymbolic theorem proving platform — project invariants",
23+
author = "Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>",
24+
},
25+
},
26+
27+
# Project configuration
28+
config = {
29+
# Proof system invariants (CRITICAL)
30+
proof_system = {
31+
# Dangerous proof bypasses that must NEVER appear in proofs
32+
forbidden_proof_patterns = [
33+
"believe_me",
34+
"assert_total",
35+
"Admitted",
36+
"sorry",
37+
"unsafeCoerce",
38+
"Obj.magic",
39+
"postulate",
40+
],
41+
# All proofs must be complete (no Admitted/sorry)
42+
admitted_count_max = 0,
43+
},
44+
45+
# Multi-prover support requirements
46+
supported_provers = [
47+
"coq",
48+
"lean4",
49+
"idris2",
50+
"agda",
51+
],
52+
53+
# Safety invariants
54+
safety = {
55+
forbidden_patterns = [
56+
"unwrap()",
57+
"expect()",
58+
"todo!()",
59+
"unimplemented!()",
60+
],
61+
},
62+
63+
# Test requirements
64+
tests = {
65+
min_unit_tests = 50,
66+
integration_tests_required = true,
67+
proof_verification_required = true,
68+
},
69+
70+
# Build configuration
71+
build = {
72+
edition = "2021",
73+
msrv = "1.75",
74+
},
75+
76+
# Language policy
77+
banned_files = ["Makefile", "Dockerfile"],
78+
banned_languages = ["python", "typescript", "javascript", "go"],
79+
},
80+
81+
# RSR compliance
82+
rsr = {
83+
explainme = true,
84+
ai_manifest = true,
85+
machine_readable = true,
86+
spdx_headers_required = true,
87+
security_md_required = true,
88+
idris2_abi = true,
89+
zig_ffi = true,
90+
},
91+
}

0 commit comments

Comments
 (0)