automated-operator / PROTOCOL.md
SNAPKITTYWEST's picture
push from SNAPKITTYWEST/automated-operator
0a93d9c verified
|
Raw
History Blame Contribute Delete
17 kB

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

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

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

// 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:

{
  "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
  2. ASP Encoding
  3. Circom ZK Circuit
  4. AutomatedOperator Rust
  5. Lean 4 Proofs
  6. Coq P5 Progress