| <!-- | |
| Copyright 2026 Bel Esprit D'Accord Irrevocable Trust (EIN: 42-697643) | |
| Licensed under the Apache License, Version 2.0 (the "License"); | |
| you may not use this file except in compliance with the License. | |
| You may obtain a copy of the License at | |
| http://www.apache.org/licenses/LICENSE-2.0 | |
| OR | |
| Licensed under the GNU Affero General Public License, Version 3.0 | |
| (the "AGPL"); you may not use this file except in compliance with the AGPL. | |
| You may obtain a copy of the AGPL at | |
| https://www.gnu.org/licenses/agpl-3.0.html | |
| OR | |
| Licensed under the Business Source License 1.1 (BSL-1.1); | |
| converts to Apache-2.0 after 4 years. See LICENSE-BSL for terms. | |
| --> | |
| # ICP-DAG-1.0 Protocol Specification | |
| ## Integrity Constraint Protocol — Governance DAG | |
| **Version**: 1.0 | |
| **Author**: Ahmad Ali Parr / SnapKitty Collective | |
| **Trust**: Bel Esprit D'Accord Irrevocable Trust (EIN: 42-697643) | |
| **Prior Art**: PAR-001 through PAR-018 | |
| --- | |
| ## Overview | |
| The ICP-DAG (Integrity Constraint Protocol — Directed Acyclic Graph) is a formal governance framework that enforces which claims may be published/acted upon based on their evidence type. It implements a deterministic state machine with cryptographic verification at each transition. | |
| ### Governance Flow (DAG Contract) | |
| ``` | |
| EVIDENCE → CLAIM → CONSTRAINT → PROOF → DECISION → AUTHORIZATION → EXECUTION → AUDIT | |
| ``` | |
| Each edge MUST reference existing nodes. The DAG is sealed with a SHA3-512 commitment. | |
| --- | |
| ## Node Types | |
| | Type | State Values | Description | | |
| |------|--------------|-------------| | |
| | EVIDENCE | OBSERVED | Raw artifact (code, proof, measurement) | | |
| | CLAIM | UNKNOWN, PROVEN, CONTRADICTED | Assertion requiring verification | | |
| | CONSTRAINT | ACTIVE, CONTRADICTED | System invariant that must hold | | |
| | PROOF | PROVEN | Verification artifact linking CLAIM → CONSTRAINT | | |
| | DECISION | PROPOSED, AUTHORIZED, REJECTED | Governance decision on a CLAIM | | |
| | EXECUTION | PENDING, EXECUTED, BLOCKED | Action taken on AUTHORIZED decision | | |
| | POLICY | ACTIVE | Governance rule enforcing CONSTRAINTs | | |
| | AUDIT | SEALED | Immutable record of governance events | | |
| --- | |
| ## Edge Types | |
| | Type | From → To | Semantics | | |
| |------|-----------|-----------| | |
| | SUPPORTS | EVIDENCE → CLAIM | Evidence backs claim | | |
| | PROVEN_BY | CLAIM → PROOF | Claim verified by proof | | |
| | SATISFIES | PROOF → CONSTRAINT | Proof discharges constraint | | |
| | DECIDES | CLAIM → DECISION | Decision governs claim | | |
| | EXECUTES | DECISION → EXECUTION | Execution implements decision | | |
| | ENFORCES | POLICY → CONSTRAINT | Policy mandates constraint | | |
| --- | |
| ## Invariant Enforcement (ICP178–ICP188) | |
| ### I1: Edge Endpoint Existence | |
| Every edge MUST reference two existing nodes. Violation → HALT. | |
| ### I2: No Self-Edges | |
| No node may have an edge to itself. Violation → HALT. | |
| ### I3: UNKNOWN Claims Cannot Authorize | |
| `node(C, claim, unknown) ∧ edge(C, D, decides) ⇒ ¬authorized(D)` | |
| ### I4: CONTRADICTED Claims Cannot Authorize | |
| `node(C, claim, contradicted) ∧ edge(C, D, decides) ⇒ ¬authorized(D)` | |
| ### I5: Execution Requires AUTHORIZED Decision | |
| `node(E, execution, _) ∧ edge(D, E, executes) ⇒ state(D) = authorized` | |
| ### I6: PROOF Must Reference CLAIM | |
| `node(P, proof, _) ⇒ ∃C: node(C, claim, _) ∧ edge(C, P, proven-by)` | |
| ### I7: POLICY Must Reference CONSTRAINT | |
| `node(P, policy, _) ⇒ ∃C: node(C, constraint, _) ∧ edge(P, C, enforces)` | |
| ### I8: Constraint Failure → Governance Failure | |
| `node(C, constraint, contradicted) ⇒ governance_failed` | |
| ### I9: Governance Failure → Execution Blocked | |
| `governance_failed ⇒ ¬node(E, execution, executed)` | |
| ### I10: ASP UNSAT → HALT | |
| If Answer Set Programming encoding is unsatisfiable, governance HALTs. | |
| --- | |
| ## Evidence Types & Execution Policy | |
| | Evidence Type | Description | Can Execute | | |
| |---------------|-------------|-------------| | |
| | MACHINE-CHECKED | Zero-sorry Lean 4 / Coq proof (`native_decide`, `rfl`, `norm_num`) | ✅ Yes | | |
| | VERIFIED-COMPUTATIONAL | Exhaustive computational check over all inputs | ✅ Yes | | |
| | VERIFIED-FORMAL | Axiom-free proof in EasyCrypt / F* / Q# | ✅ Yes | | |
| | AXIOM | Asserted with `axiom` keyword; proof obligation open | ⚠️ Deps must be VERIFIED | | |
| | CLAIMED | Stated in docstring/comment; not verified | ❌ No | | |
| | OPEN | Proof obligation identified; work not started | ❌ No | | |
| --- | |
| ## MUMPS Reference Implementation | |
| ```mumps | |
| ; ICP-DAG Core Routines (MUMPS) | |
| ICP001 ; INTEGRITY CONSTRAINT DAG | |
| ICP002 ; MUMPS + ANSWER SET PROGRAMMING GOVERNANCE GRAPH | |
| ICP003 ; EVIDENCE / CLAIM / PROOF / POLICY / DECISION / EXECUTION | |
| ICP004 ; | |
| ICP005 ; DAG CONTRACT: | |
| ICP006 ; NODE -> EVIDENCE -> CLAIM -> CONSTRAINT -> PROOF | |
| ICP007 ; PROOF -> DECISION -> AUTHORIZATION -> EXECUTION -> AUDIT | |
| ICP008 ; EVERY EDGE MUST REFERENCE EXISTING NODES. | |
| ICP009 ; UNKNOWN CANNOT REACH VERIFIED. | |
| ICP010 ; FAILED CONSTRAINT CANNOT REACH EXECUTION. | |
| ICP011 ; | |
| ICP012 QUIT | |
| ICP013 ; | |
| ICP014 INIT ; | |
| ICP015 K ^ICP | |
| ICP016 S ^ICP("VERSION")="ICP-DAG-1.0" | |
| ICP017 S ^ICP("STATUS")="INITIALIZED" | |
| ICP018 S ^ICP("LEVEL")=99 | |
| ICP019 S ^ICP("NODES")=0 | |
| ICP020 S ^ICP("EDGES")=0 | |
| ICP021 S ^ICP("FAILURES")=0 | |
| ICP022 Q | |
| ICP023 ; | |
| ICP024 NODE(ID,TYPE,STATE) ; | |
| ICP025 I ID="" Q 0 | |
| ICP026 S ^ICP("NODE",ID,"TYPE")=$G(TYPE) | |
| ICP027 S ^ICP("NODE",ID,"STATE")=$G(STATE) | |
| ICP028 S ^ICP("NODES")=^ICP("NODES")+1 | |
| ICP029 Q 1 | |
| ICP030 ; | |
| ICP031 EDGE(FROM,TO,TYPE) ; | |
| ICP032 I '$D(^ICP("NODE",FROM)) Q 0 | |
| ICP033 I '$D(^ICP("NODE",TO)) Q 0 | |
| ICP034 S ^ICP("EDGE",FROM,TO)=TYPE | |
| ICP035 S ^ICP("EDGES")=^ICP("EDGES")+1 | |
| ICP036 Q 1 | |
| ICP037 ; | |
| ICP038 CLAIM(ID,TEXT) ; | |
| ICP039 D NODE(ID,"CLAIM","UNKNOWN") | |
| ICP040 S ^ICP("NODE",ID,"TEXT")=$G(TEXT) | |
| ICP041 Q | |
| ICP042 ; | |
| ICP043 EVIDENCE(ID,SOURCE) ; | |
| ICP044 D NODE(ID,"EVIDENCE","OBSERVED") | |
| ICP045 S ^ICP("NODE",ID,"SOURCE")=$G(SOURCE) | |
| ICP046 Q | |
| ICP047 ; | |
| ICP048 CONSTRAINT(ID,TEXT) ; | |
| ICP049 D NODE(ID,"CONSTRAINT","ACTIVE") | |
| ICP050 S ^ICP("NODE",ID,"TEXT")=$G(TEXT) | |
| ICP051 Q | |
| ICP052 ; | |
| ICP053 PROOF(ID,CLAIM,RESULT) ; | |
| ICP054 D NODE(ID,"PROOF","PROVEN") | |
| ICP055 S ^ICP("NODE",ID,"RESULT")=$G(RESULT) | |
| ICP056 D EDGE(CLAIM,ID,"PROVEN-BY") | |
| ICP057 Q | |
| ICP058 ; | |
| ICP059 DECISION(ID,CLAIM,STATE) ; | |
| ICP060 D NODE(ID,"DECISION",STATE) | |
| ICP061 D EDGE(CLAIM,ID,"DECIDES") | |
| ICP062 Q | |
| ICP063 ; | |
| ICP064 EXECUTION(ID,DECISION) ; | |
| ICP065 D NODE(ID,"EXECUTION","PENDING") | |
| ICP066 D EDGE(DECISION,ID,"EXECUTES") | |
| ICP067 Q | |
| ICP068 ; | |
| ICP069 POLICY(ID,TEXT) ; | |
| ICP070 D NODE(ID,"POLICY","ACTIVE") | |
| ICP071 S ^ICP("NODE",ID,"TEXT")=$G(TEXT) | |
| ICP072 Q | |
| ICP073 ; | |
| ICP074 APPLY(POLICY,CONSTRAINT) ; | |
| ICP075 D EDGE(POLICY,CONSTRAINT,"ENFORCES") | |
| ICP076 Q | |
| ICP077 ; | |
| ICP078 CHECK(CID) ; | |
| ICP079 I '$D(^ICP("NODE",CID)) Q 0 | |
| ICP080 N S S S=$G(^ICP("NODE",CID,"STATE")) | |
| ICP081 I S="UNKNOWN" Q 0 | |
| ICP082 I S="CONTRADICTED" Q 0 | |
| ICP083 Q 1 | |
| ICP084 ; | |
| ICP085 AUTHORIZE(DID) ; | |
| ICP086 I '$D(^ICP("NODE",DID)) Q 0 | |
| ICP087 N C S C=$O(^ICP("EDGE",DID,"")) | |
| ICP088 I C="" Q 0 | |
| ICP089 I '$$CHECK(C) Q 0 | |
| ICP090 S ^ICP("NODE",DID,"STATE")="AUTHORIZED" | |
| ICP091 Q 1 | |
| ICP092 ; | |
| ICP093 FAIL(REASON) ; | |
| ICP094 S ^ICP("STATUS")="FAILED" | |
| ICP095 S ^ICP("FAILURES")=^ICP("FAILURES")+1 | |
| ICP096 S ^ICP("FAILURE",^ICP("FAILURES"))=REASON | |
| ICP097 Q 0 | |
| ICP098 ; | |
| ICP099 DAGCHECK ; | |
| ICP100 N A,B | |
| ICP101 S A="" | |
| ICP102 F S A=$O(^ICP("EDGE",A)) Q:A="" D | |
| ICP103 .S B="" | |
| ICP104 .F S B=$O(^ICP("EDGE",A,B)) Q:B="" D | |
| ICP105 ..I A=B D FAIL("SELF-EDGE:"_A) | |
| ICP106 Q | |
| ICP107 ; | |
| ICP108 GOVERN ; | |
| ICP109 D DAGCHECK | |
| ICP110 I $G(^ICP("FAILURES"))>0 Q | |
| ICP111 S ^ICP("STATUS")="GOVERNING" | |
| ICP112 Q | |
| ICP113 ; | |
| ICP114 ASP ; | |
| ICP115 ; ASP REPRESENTATION OF THE SAME DAG CONTRACT | |
| ICP116 ; node(N,Type,State). | |
| ICP117 ; edge(From,To,Type). | |
| ICP118 ; | |
| ICP119 ; CONSTRAINTS: | |
| ICP120 ; :- node(C,claim,unknown), node(D,decision,_), edge(C,D,decides). | |
| ICP121 ; :- node(C,claim,contradicted), node(D,decision,_), edge(C,D,decides). | |
| ICP122 ; :- node(D,decision,S), S=authorized, | |
| ICP123 ; node(C,claim,_), edge(C,D,decides), not proven(C). | |
| ICP124 ; :- node(E,execution,_), edge(D,E,executes), | |
| ICP125 ; node(D,decision,S), S != authorized. | |
| ICP126 ; :- node(C,claim,unknown), node(C,claim,verified). | |
| ICP127 ; :- node(N,_,_), edge(N,N,_). | |
| ICP128 ; | |
| ICP129 ; ASP RESULT: | |
| ICP130 ; SAT = DAG satisfies governance constraints. | |
| ICP131 ; UNSAT = DAG violates governance constraints. | |
| ICP132 Q | |
| ICP133 ; | |
| ICP134 BUILD ; | |
| ICP135 D INIT | |
| ICP136 D NODE("P1","POLICY","ACTIVE") | |
| ICP137 D NODE("C1","CONSTRAINT","ACTIVE") | |
| ICP138 D APPLY("P1","C1") | |
| ICP139 D EVIDENCE("E1","MODEL-ARTIFACT") | |
| ICP140 D CLAIM("CL1","ARCHITECTURE CLAIM") | |
| ICP141 D EDGE("E1","CL1","SUPPORTS") | |
| ICP142 D PROOF("PR1","CL1",1) | |
| ICP143 D EDGE("PR1","C1","SATISFIES") | |
| ICP144 D DECISION("D1","CL1","PROPOSED") | |
| ICP145 D EXECUTION("X1","D1") | |
| ICP146 D GOVERN | |
| ICP147 Q | |
| ICP148 ; | |
| ICP149 VERIFY ; | |
| ICP150 N I,J,T | |
| ICP151 S I="" | |
| ICP152 F S I=$O(^ICP("EDGE",I)) Q:I="" D | |
| ICP153 .S J="" | |
| ICP154 .F S J=$O(^ICP("EDGE",I,J)) Q:J="" D | |
| ICP155 ..S T=$G(^ICP("EDGE",I,J)) | |
| ICP156 ..W !,I," --",T,"--> ",J | |
| ICP157 Q | |
| ICP158 ; | |
| ICP159 HALT ; | |
| ICP160 S ^ICP("STATUS")="HALTED" | |
| ICP161 W !,"ICP-DAG HALT" | |
| ICP162 W !,"FAILURES: ",$G(^ICP("FAILURES")) | |
| ICP163 Q | |
| ICP164 ; | |
| ICP165 FINAL ; | |
| ICP166 D DAGCHECK | |
| ICP167 I $G(^ICP("FAILURES"))>0 D HALT Q | |
| ICP168 S ^ICP("STATUS")="VERIFIED" | |
| ICP169 W !,"ICP-DAG STATUS: VERIFIED" | |
| ICP169 Q | |
| ICP170 ; | |
| ICP171 INVARIANT ; | |
| ICP172 ; I1: EVERY EDGE HAS TWO EXISTING ENDPOINTS. | |
| ICP173 ; I2: NO SELF-EDGES. | |
| ICP174 ; I3: UNKNOWN CLAIMS CANNOT BE AUTHORIZED. | |
| ICP175 ; I4: CONTRADICTED CLAIMS CANNOT BE AUTHORIZED. | |
| ICP176 ; I5: EXECUTION REQUIRES AUTHORIZED DECISION. | |
| ICP177 ; I6: PROOF MUST REFERENCE A CLAIM. | |
| ICP178 ; I7: POLICY MUST REFERENCE A CONSTRAINT. | |
| ICP179 ; I8: CONSTRAINT FAILURE PROPAGATES TO GOVERNANCE FAILURE. | |
| ICP180 ; I9: GOVERNANCE FAILURE PREVENTS EXECUTION. | |
| ICP181 ; I10: ASP UNSAT => ICP HALT. | |
| ICP182 Q | |
| ICP183 ; | |
| ICP184 GRAPH ; | |
| ICP185 ; AUTHORITATIVE DAG: | |
| ICP186 ; | |
| ICP187 ; POLICY | |
| ICP188 ; | | |
| ICP189 ; v | |
| ICP190 ; CONSTRAINT | |
| ICP191 ; ^ | |
| ICP192 ; | | |
| ICP193 ; EVIDENCE --> CLAIM --> PROOF | |
| ICP194 ; | | |
| ICP195 ; v | |
| ICP196 ; DECISION | |
| ICP197 ; | | |
| ICP198 ; v | |
| ICP199 ; AUTHORIZATION | |
| ICP200 ; | | |
| ICP201 ; v | |
| ICP202 ; EXECUTION | |
| ICP203 ; | | |
| ICP204 ; v | |
| ICP205 ; AUDIT | |
| ICP206 ; | |
| ICP207 ; REJECTION PATH: | |
| ICP208 ; UNKNOWN --> REJECT | |
| ICP209 ; CONTRADICTED --> REJECT | |
| ICP210 ; MISSING EVIDENCE --> REJECT | |
| ICP211 ; MISSING PROOF --> REJECT | |
| ICP212 ; ASP UNSAT --> HALT | |
| ICP213 Q | |
| ICP214 ; | |
| ICP215 SECURITY ; | |
| ICP216 ; NO SECRET MODEL-INTERNAL ACCESS | |
| ICP217 ; NO SANDBOX ESCAPE | |
| ICP218 ; NO FABRICATED EVIDENCE | |
| ICP219 ; NO UNSOURCED CLAIM PROMOTION | |
| ICP220 ; NO SILENT CONSTRAINT BYPASS | |
| ICP221 ; NO AUTHORITY ESCALATION | |
| ICP222 ; NO EXECUTION AFTER GOVERNANCE FAILURE | |
| ICP223 Q | |
| ICP224 ; | |
| ICP225 SEAL ; | |
| ICP226 I $G(^ICP("STATUS"))'="VERIFIED" Q $$FAIL("UNVERIFIED-DAG") | |
| ICP227 S ^ICP("SEAL","STATE")="SEALED" | |
| ICP228 S ^ICP("SEAL","NODES")=$G(^ICP("NODES")) | |
| ICP229 S ^ICP("SEAL","EDGES")=$G(^ICP("EDGES")) | |
| ICP230 Q 1 | |
| ICP226 ; | |
| ICP227 REPORT ; | |
| ICP228 W !,"ICP-DAG" | |
| ICP229 W !,"VERSION: ",$G(^ICP("VERSION")) | |
| ICP230 W !,"LEVEL: ",$G(^ICP("LEVEL")) | |
| ICP231 W !,"STATUS: ",$G(^ICP("STATUS")) | |
| ICP232 W !,"NODES: ",$G(^ICP("NODES")) | |
| ICP233 W !,"EDGES: ",$G(^ICP("EDGES")) | |
| ICP234 W !,"FAILURES: ",$G(^ICP("FAILURES")) | |
| ICP235 Q | |
| ICP236 ; | |
| ICP237 COMMIT ; | |
| ICP238 D FINAL | |
| ICP239 I $G(^ICP("STATUS"))="HALTED" Q | |
| ICP240 D SEAL | |
| ICP241 I $G(^ICP("STATUS"))="VERIFIED" W !,"ICP-DAG COMMIT: ACCEPTED" | |
| ICP242 Q | |
| ICP243 ; | |
| ICP244 END ; | |
| ``` | |
| --- | |
| ## ASP Encoding (for clingo/DLV) | |
| ```prolog | |
| % ICP-DAG ASP Encoding | |
| % node(N, Type, State). | |
| % edge(From, To, Type). | |
| % Types: evidence, claim, constraint, proof, decision, execution, policy, audit | |
| % States: unknown, observed, active, proven, contradicted, proposed, authorized, | |
| % pending, executed, blocked, rejected, sealed | |
| % Governance Constraints (Hard) | |
| :- node(C, claim, unknown), node(D, decision, _), edge(C, D, decides). | |
| :- node(C, claim, contradicted), node(D, decision, _), edge(C, D, decides). | |
| :- node(D, decision, S), S = authorized, | |
| node(C, claim, _), edge(C, D, decides), not proven(C). | |
| :- node(E, execution, _), edge(D, E, executes), | |
| node(D, decision, S), S != authorized. | |
| :- node(C, claim, unknown), node(C, claim, verified). | |
| :- node(N, _, _), edge(N, N, _). | |
| % Derived | |
| proven(C) :- node(P, proof, proven), edge(C, P, proven-by). | |
| supported(C) :- node(C, claim, _), node(E, evidence, observed), edge(E, C, supports). | |
| authorized(D) :- node(D, decision, proposed), node(C, claim, _), edge(C, D, decides), | |
| proven(C), not node(C, claim, contradicted). | |
| ready(E) :- node(E, execution, pending), node(D, decision, authorized), edge(D, E, executes). | |
| execute(P) :- node(P, execution, pending), ready(P), not governance_failed. | |
| governance_failed :- node(C, constraint, contradicted). | |
| governance_failed :- node(C, constraint, active), not satisfied(C). | |
| satisfied(C) :- node(P, proof, proven), edge(C, P, satisfies). | |
| #show node/3. | |
| #show edge/3. | |
| #show execute/1. | |
| #show governance_failed/0. | |
| #show authorized/1. | |
| #show ready/1. | |
| ``` | |
| --- | |
| ## Circom ZK Circuit: Cognitive Strain Verifier (ICP001) | |
| ```circom | |
| // ICP001: Cognitive Strain Verifier | |
| // ZK Proof that hidden mental strain scalar ≤ max_strain_threshold | |
| // during active governance epoch. | |
| pragma circom 2.1.6; | |
| include "circomlib/circuits/comparators.circom"; | |
| template CognitiveStrainCheck(max_strain_threshold, n_bits) { | |
| signal private input neuron_id; | |
| signal private input hidden_strain_scalar; | |
| signal input epoch_id; | |
| signal input proposal_id; | |
| signal input max_strain_threshold_pub; | |
| signal output valid_strain; | |
| component range_check = LessThan(n_bits); | |
| range_check.in[0] <== hidden_strain_scalar; | |
| range_check.in[1] <== 1 << n_bits; | |
| range_check.out === 1; | |
| component le_check = LessEqThan(n_bits); | |
| le_check.in[0] <== hidden_strain_scalar; | |
| le_check.in[1] <== max_strain_threshold_pub; | |
| valid_strain <== le_check.out; | |
| valid_strain === 1; | |
| } | |
| template ICP001_Governance(num_neurons, n_bits) { | |
| signal private input neuron_ids[num_neurons]; | |
| signal private input hidden_strain_scalars[num_neurons]; | |
| signal input max_strain_threshold; | |
| signal input epoch_id; | |
| signal input proposal_id; | |
| signal output governance_valid; | |
| for (var i = 0; i < num_neurons; i++) { | |
| component strain_check = CognitiveStrainCheck(max_strain_threshold, n_bits); | |
| strain_check.neuron_id <== neuron_ids[i]; | |
| strain_check.hidden_strain_scalar <== hidden_strain_scalars[i]; | |
| strain_check.epoch_id <== epoch_id; | |
| strain_check.proposal_id <== proposal_id; | |
| strain_check.max_strain_threshold_pub <== max_strain_threshold; | |
| } | |
| governance_valid <== 1; | |
| } | |
| component main = ICP001_Governance(4, 8); | |
| ``` | |
| --- | |
| ## AutomatedOperator Integration | |
| The AutomatedOperator implements the ICP-DAG as a deterministic automaton: | |
| ``` | |
| AutomatedOperator = (Σ, Q, q₀, δ, F, Γ) | |
| Σ = ObjectiveSpace | |
| Q = OperatorState | |
| q₀ = (∅, ⊥, 0.20, TrustAnchor) | |
| δ: Q × Σ → Q | |
| F ⊆ Q | |
| Γ: Q → Objective | |
| ``` | |
| ### Invariant Mapping | |
| | ICP Invariant | AutomatedOperator Enforcement | | |
| |---------------|------------------------------| | |
| | I1 (Edge endpoints) | FFI bridge validates all inputs exist | | |
| | I2 (No self-edges) | State machine prevents self-transition | | |
| | I3/I4 (UNKNOWN/CONTRADICTED) | Only MACHINE-CHECKED/VERIFIED claims reach `next_objective()` | | |
| | I5 (Auth required) | `receive_result()` only after valid `next_objective()` | | |
| | I6 (Proof→Claim) | ZK proof binds to objective via Poseidon hash | | |
| | I7 (Policy→Constraint) | ScoreWeights enforce entropy/sovereign constraints | | |
| | I8/I9 (Constraint failure) | `valid_objective()` gates all transitions | | |
| | I10 (ASP UNSAT) | Lean 4 proofs verify ASP encoding SAT | | |
| --- | |
| ## Seal & Commit | |
| Upon successful governance, the DAG is sealed: | |
| ```json | |
| { | |
| "state": "SEALED", | |
| "nodes": 107, | |
| "edges": 92, | |
| "timestamp": 1788131137, | |
| "hash": "4d507f078930bfbb88be5761357b0937e124f55fa35f686ceba1c31400a42bc8" | |
| } | |
| ``` | |
| Seal hash = SHA3-512(canonical JSON of all nodes + edges). | |
| --- | |
| ## Protocol Versioning | |
| | Version | Date | Changes | | |
| |---------|------|---------| | |
| | 1.0 | 2026-08-30 | Initial release: ICP-DAG, AutomatedOperator, ICP001 | | |
| --- | |
| ## References | |
| 1. [ICP-DAG MUMPS Reference](icp_dag.m) | |
| 2. [ASP Encoding](icp_dag.lp) | |
| 3. [Circom ZK Circuit](cognitive_strain_verifier.circom) | |
| 4. [AutomatedOperator Rust](src/lib.rs) | |
| 5. [Lean 4 Proofs](lean/Invariants.lean) | |
| 5. [Coq P5 Progress](docs/P5_Progress.v) |