PROTOCOL.md

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