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"
ICP170 Q
ICP171 ;
ICP172 TEST ;
ICP173 D BUILD
ICP174 D VERIFY
ICP175 D FINAL
ICP176 Q
ICP177 ;
ICP178 INVARIANT ;
ICP179 ; I1: EVERY EDGE HAS TWO EXISTING ENDPOINTS.
ICP180 ; I2: NO SELF-EDGES.
ICP181 ; I3: UNKNOWN CLAIMS CANNOT BE AUTHORIZED.
ICP182 ; I4: CONTRADICTED CLAIMS CANNOT BE AUTHORIZED.
ICP183 ; I5: EXECUTION REQUIRES AUTHORIZED DECISION.
ICP184 ; I6: PROOF MUST REFERENCE A CLAIM.
ICP185 ; I7: POLICY MUST REFERENCE A CONSTRAINT.
ICP186 ; I8: CONSTRAINT FAILURE PROPAGATES TO GOVERNANCE FAILURE.
ICP187 ; I9: GOVERNANCE FAILURE PREVENTS EXECUTION.
ICP188 ; I10: ASP UNSAT => ICP HALT.
ICP189 Q
ICP190 ;
ICP191 GRAPH ;
ICP192 ; AUTHORITATIVE DAG:
ICP193 ;
ICP194 ; POLICY
ICP195 ;    |
ICP196 ;    v
ICP197 ; CONSTRAINT
ICP198 ;    ^
ICP199 ;    |
ICP200 ; EVIDENCE --> CLAIM --> PROOF
ICP201 ;                    |
ICP202 ;                    v
ICP203 ;                 DECISION
ICP204 ;                    |
ICP205 ;                    v
ICP206 ;              AUTHORIZATION
ICP207 ;                    |
ICP208 ;                    v
ICP209 ;                EXECUTION
ICP210 ;                    |
ICP211 ;                    v
ICP212 ;                  AUDIT
ICP213 ;
ICP214 ; REJECTION PATH:
ICP215 ; UNKNOWN --> REJECT
ICP216 ; CONTRADICTED --> REJECT
ICP217 ; MISSING EVIDENCE --> REJECT
ICP218 ; MISSING PROOF --> REJECT
ICP219 ; ASP UNSAT --> HALT
ICP220 Q
ICP221 ;
ICP222 SECURITY ;
ICP223 ; NO SECRET MODEL-INTERNAL ACCESS
ICP224 ; NO SANDBOX ESCAPE
ICP225 ; NO FABRICATED EVIDENCE
ICP226 ; NO UNSOURCED CLAIM PROMOTION
ICP227 ; NO SILENT CONSTRAINT BYPASS
ICP228 ; NO AUTHORITY ESCALATION
ICP229 ; NO EXECUTION AFTER GOVERNANCE FAILURE
ICP230 Q
ICP231 ;
ICP232 SEAL ;
ICP233 I $G(^ICP("STATUS"))'="VERIFIED" Q $$FAIL("UNVERIFIED-DAG")
ICP234 S ^ICP("SEAL","STATE")="SEALED"
ICP235 S ^ICP("SEAL","NODES")=$G(^ICP("NODES"))
ICP236 S ^ICP("SEAL","EDGES")=$G(^ICP("EDGES"))
ICP237 Q 1
ICP238 ;
ICP239 REPORT ;
ICP240 W !,"ICP-DAG"
ICP241 W !,"VERSION: ",$G(^ICP("VERSION"))
ICP242 W !,"LEVEL: ",$G(^ICP("LEVEL"))
ICP243 W !,"STATUS: ",$G(^ICP("STATUS"))
ICP244 W !,"NODES: ",$G(^ICP("NODES"))
ICP245 W !,"EDGES: ",$G(^ICP("EDGES"))
ICP246 W !,"FAILURES: ",$G(^ICP("FAILURES"))
ICP247 Q
ICP248 ;
ICP249 COMMIT ;
ICP250 D FINAL
ICP251 I $G(^ICP("STATUS"))="HALTED" Q
ICP252 D SEAL
ICP253 I $G(^ICP("STATUS"))="VERIFIED" W !,"ICP-DAG COMMIT: ACCEPTED"
ICP254 Q
ICP255 ;
ICP256 END ;
ICP257 ; END INTEGRITY CONSTRAINT DAG