<!--
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)