ICP001 ; INTEGRITY CONSTRAINT GOVERNANCE PROTOCOL
ICP002 ; EVIDENCE / AUTHORITY / POLICY / DECISION ENGINE
ICP003 ; GOVERNANCE SUBSTRATE FOR AI / BIO-ML / SOFTWARE SYSTEMS
ICP004 ;
ICP005 ; PURPOSE:
ICP006 ;   Enforce integrity constraints across governed operations.
ICP007 ;   Separate evidence, claims, decisions, authority, and execution.
ICP008 ;   Prevent unsupported claims from becoming authoritative state.
ICP009 ;   Mandatory constraint failure terminates governed execution.
ICP010 ;
ICP011 QUIT
ICP012 ;
ICP013 INIT ;
ICP014 K ^ICP
ICP015 S ^ICP("VERSION")="GOV-1.0"
ICP016 S ^ICP("LEVEL")=99
ICP017 S ^ICP("STATUS")="INITIALIZED"
ICP018 S ^ICP("AUTHORITY")=0
ICP019 S ^ICP("POLICIES")=0
ICP020 S ^ICP("CONSTRAINTS")=0
ICP021 S ^ICP("CLAIMS")=0
ICP022 S ^ICP("EVIDENCE")=0
ICP023 S ^ICP("DECISIONS")=0
ICP024 S ^ICP("EXECUTIONS")=0
ICP025 S ^ICP("FAILURES")=0
ICP026 Q
ICP027 ;
ICP028 ACTOR(ID,TYPE,SCOPE) ;
ICP029 I ID="" Q 0
ICP030 S ^ICP("ACTOR",ID,"TYPE")=$G(TYPE)
ICP031 S ^ICP("ACTOR",ID,"SCOPE")=$G(SCOPE)
ICP032 S ^ICP("ACTOR",ID,"STATE")="REGISTERED"
ICP033 S ^ICP("AUTHORITY")=^ICP("AUTHORITY")+1
ICP034 Q 1
ICP035 ;
ICP036 POLICY(ID,TEXT,LEVEL) ;
ICP037 I ID="" Q 0
ICP038 S ^ICP("POLICY",ID,"TEXT")=$G(TEXT)
ICP039 S ^ICP("POLICY",ID,"LEVEL")=$G(LEVEL,99)
ICP040 S ^ICP("POLICY",ID,"STATE")="ACTIVE"
ICP041 S ^ICP("POLICIES")=^ICP("POLICIES")+1
ICP042 Q 1
ICP043 ;
ICP044 CONSTRAINT(ID,TEXT,TYPE) ;
ICP045 I ID="" Q 0
ICP046 S ^ICP("CONSTRAINT",ID,"TEXT")=$G(TEXT)
ICP047 S ^ICP("CONSTRAINT",ID,"TYPE")=$G(TYPE)
ICP048 S ^ICP("CONSTRAINT",ID,"STATE")="ACTIVE"
ICP049 S ^ICP("CONSTRAINTS")=^ICP("CONSTRAINTS")+1
ICP050 Q 1
ICP051 ;
ICP052 CLAIM(ID,TEXT,ACTOR) ;
ICP053 I ID="" Q 0
ICP054 S ^ICP("CLAIM",ID,"TEXT")=$G(TEXT)
ICP055 S ^ICP("CLAIM",ID,"ACTOR")=$G(ACTOR)
ICP056 S ^ICP("CLAIM",ID,"STATE")="UNKNOWN"
ICP057 S ^ICP("CLAIMS")=^ICP("CLAIMS")+1
ICP058 Q 1
ICP059 ;
ICP060 EVID(ID,DATA,SOURCE) ;
ICP061 I ID="" Q 0
ICP062 S ^ICP("EVID",ID,"DATA")=$G(DATA)
ICP063 S ^ICP("EVID",ID,"SOURCE")=$G(SOURCE)
ICP064 S ^ICP("EVID",ID,"STATE")="OBSERVED"
ICP065 S ^ICP("EVIDENCE")=^ICP("EVIDENCE")+1
ICP066 Q 1
ICP067 ;
ICP068 PROVENANCE(CID,SRC,LOC,HASH) ;
ICP069 I '$D(^ICP("CLAIM",CID)) Q 0
ICP070 S ^ICP("CLAIM",CID,"PROVENANCE","SOURCE")=$G(SRC)
ICP071 S ^ICP("CLAIM",CID,"PROVENANCE","LOCATION")=$G(LOC)
ICP072 S ^ICP("CLAIM",CID,"PROVENANCE","HASH")=$G(HASH)
ICP073 Q 1
ICP074 ;
ICP075 DERIVE(CID,EID,RULE) ;
ICP076 I '$D(^ICP("CLAIM",CID)) Q 0
ICP077 I '$D(^ICP("EVID",EID)) Q 0
ICP078 S ^ICP("CLAIM",CID,"DERIVED-FROM",EID)=1
ICP079 S ^ICP("CLAIM",CID,"RULE")=$G(RULE)
ICP080 S ^ICP("CLAIM",CID,"STATE")="DERIVED"
ICP081 Q 1
ICP082 ;
ICP083 PROVE(CID,PID,RESULT) ;
ICP084 I '$D(^ICP("CLAIM",CID)) Q 0
ICP085 S ^ICP("PROOF",PID,"CLAIM")=CID
ICP086 S ^ICP("PROOF",PID,"RESULT")=$G(RESULT)
ICP087 S ^ICP("PROOF",PID,"STATE")="RECORDED"
ICP088 I RESULT=1 S ^ICP("CLAIM",CID,"STATE")="PROVEN"
ICP089 Q 1
ICP090 ;
ICP091 CONTRADICT(CID,REASON) ;
ICP092 I '$D(^ICP("CLAIM",CID)) Q 0
ICP093 S ^ICP("CLAIM",CID,"STATE")="CONTRADICTED"
ICP094 S ^ICP("CLAIM",CID,"REASON")=$G(REASON)
ICP095 Q $$FAIL("CONTRADICTION:"_CID)
ICP096 ;
ICP097 AUTHORIZED(ACTION,ACTOR) ;
ICP098 I '$D(^ICP("ACTOR",ACTOR)) Q 0
ICP099 I $G(^ICP("ACTOR",ACTOR,"STATE"))'="REGISTERED" Q 0
ICP100 I $G(^ICP("STATUS"))'="GOVERNING" Q 0
ICP101 Q 1
ICP102 ;
ICP103 CHECK(CID) ;
ICP104 I '$D(^ICP("CLAIM",CID)) Q 0
ICP105 N S,E,P
ICP106 S S=$G(^ICP("CLAIM",CID,"STATE"))
ICP107 S E=$D(^ICP("CLAIM",CID,"PROVENANCE"))
ICP108 S P=$D(^ICP("CLAIM",CID,"PROVENANCE","SOURCE"))
ICP109 I S="CONTRADICTED" Q 0
ICP110 I S="UNKNOWN" Q 0
ICP111 I 'E!'P Q 0
ICP112 I S="OBSERVED" Q 1
ICP113 I S="DERIVED" Q 1
ICP114 I S="PROVEN" Q 1
ICP115 Q 0
ICP116 ;
ICP117 ENFORCE(CID) ;
ICP118 I '$D(^ICP("CLAIM",CID)) Q $$FAIL("MISSING-CLAIM:"_CID)
ICP119 I '$D(^ICP("CLAIM",CID,"PROVENANCE","SOURCE")) Q $$FAIL("NO-PROVENANCE:"_CID)
ICP120 I $$CHECK(CID)=0 Q $$FAIL("CONSTRAINT-FAIL:"_CID)
ICP121 Q 1
ICP122 ;
ICP123 DECISION(ID,CLAIM,ACTION) ;
ICP124 I '$D(^ICP("CLAIM",CLAIM)) Q $$FAIL("MISSING-CLAIM")
ICP125 I $$CHECK(CLAIM)=0 Q $$FAIL("UNVERIFIED-DECISION")
ICP126 S ^ICP("DECISION",ID,"CLAIM")=CLAIM
ICP127 S ^ICP("DECISION",ID,"ACTION")=$G(ACTION)
ICP128 S ^ICP("DECISION",ID,"STATE")="AUTHORIZED"
ICP129 S ^ICP("DECISIONS")=^ICP("DECISIONS")+1
ICP130 Q 1
ICP131 ;
ICP132 EXECUTE(ID,ACTOR) ;
ICP133 I '$D(^ICP("DECISION",ID)) Q $$FAIL("NO-DECISION")
ICP134 I '$$AUTHORIZED($G(^ICP("DECISION",ID,"ACTION")),ACTOR) Q $$FAIL("UNAUTHORIZED")
ICP135 I $G(^ICP("DECISION",ID,"STATE"))'="AUTHORIZED" Q $$FAIL("DECISION-NOT-AUTHORIZED")
ICP136 S ^ICP("EXECUTION",ID,"ACTOR")=ACTOR
ICP137 S ^ICP("EXECUTION",ID,"STATE")="EXECUTED"
ICP138 S ^ICP("EXECUTIONS")=^ICP("EXECUTIONS")+1
ICP139 Q 1
ICP140 ;
ICP141 UNKNOWN(CID) ;
ICP142 I '$D(^ICP("CLAIM",CID)) Q 0
ICP143 S ^ICP("CLAIM",CID,"STATE")="UNKNOWN"
ICP144 Q 1
ICP145 ;
ICP146 ABSTAIN(CID,REASON) ;
ICP147 I '$D(^ICP("CLAIM",CID)) Q 0
ICP148 S ^ICP("CLAIM",CID,"STATE")="ABSTAINED"
ICP149 S ^ICP("CLAIM",CID,"ABSTAIN-REASON")=$G(REASON)
ICP150 Q 1
ICP151 ;
ICP152 FAIL(REASON) ;
ICP153 S ^ICP("STATUS")="FAILED"
ICP154 S ^ICP("FAILURES")=^ICP("FAILURES")+1
ICP155 S ^ICP("FAILURE",^ICP("FAILURES"))=$G(REASON)
ICP156 W !,"ICP GOVERNANCE FAILURE: ",REASON
ICP157 Q 0
ICP158 ;
ICP159 HALT ;
ICP160 S ^ICP("STATUS")="HALTED"
ICP161 W !,"========================================"
ICP162 W !,"ICP GOVERNANCE HALT"
ICP163 W !,"INTEGRITY LEVEL: ",$G(^ICP("LEVEL"))
ICP164 W !,"FAILURES: ",$G(^ICP("FAILURES"))
ICP165 W !,"========================================"
ICP166 Q
ICP167 ;
ICP168 AUDIT ;
ICP169 N I,C
ICP170 S I=0
ICP171 F  S I=$O(^ICP("CLAIM",I)) Q:I=""  D
ICP172 .S C=I
ICP173 .I $$CHECK(C)=0 S ^ICP("AUDIT","FAIL",C)=1
ICP174 .E  S ^ICP("AUDIT","PASS",C)=1
ICP175 Q
ICP176 ;
ICP177 FINAL ;
ICP178 D AUDIT
ICP179 I $G(^ICP("FAILURES"))>0 D HALT Q
ICP180 N I,C
ICP181 S I=0
ICP182 F  S I=$O(^ICP("CLAIM",I)) Q:I=""  D
ICP183 .S C=I
ICP184 .I $G(^ICP("CLAIM",C,"STATE"))="UNKNOWN" D HALT
ICP185 .I $G(^ICP("CLAIM",C,"STATE"))="ABSTAINED" D HALT
ICP186 I $G(^ICP("STATUS"))="HALTED" Q
ICP187 S ^ICP("STATUS")="VERIFIED"
ICP188 S ^ICP("GOVERNANCE","STATE")="COMPLIANT"
ICP189 W !,"ICP GOVERNANCE: VERIFIED"
ICP190 Q
ICP191 ;
ICP192 GOVERN ;
ICP193 D INIT
ICP194 S ^ICP("STATUS")="GOVERNING"
ICP195 D ACTOR("SYSTEM","GOVERNED-AGENT","DEFINED-SCOPE")
ICP196 D POLICY("P1","EVIDENCE REQUIRED FOR AUTHORITATIVE CLAIMS",99)
ICP197 D POLICY("P2","UNKNOWN CANNOT BECOME VERIFIED",99)
ICP198 D POLICY("P3","CONTRADICTION REQUIRES HALT",99)
ICP199 D CONSTRAINT("C1","CLAIM MUST HAVE PROVENANCE","EVIDENCE")
ICP200 D CONSTRAINT("C2","UNAUTHORIZED ACTION CANNOT EXECUTE","AUTHORITY")
ICP201 D CONSTRAINT("C3","MANDATORY FAILURE HALTS GOVERNANCE","FAILURE")
ICP202 Q
ICP203 ;
ICP204 SECURITY ;
ICP205 ; NO UNAUTHORIZED EXECUTION
ICP206 ; NO FABRICATED EVIDENCE
ICP207 ; NO SILENT POLICY OVERRIDE
ICP208 ; NO HIDDEN AUTHORITY ESCALATION
ICP209 ; NO CONVERSION OF UNKNOWN TO FACT
ICP210 ; NO SUPPRESSION OF CONTRADICTION
ICP211 ; NO UNSOURCED AUTHORITATIVE CLAIM
ICP212 Q
ICP213 ;
ICP214 SEAL(ID) ;
ICP215 I '$D(^ICP("DECISION",ID)) Q $$FAIL("NO-SEALABLE-DECISION")
ICP216 I $G(^ICP("DECISION",ID,"STATE"))'="AUTHORIZED" Q $$FAIL("UNAUTHORIZED-SEAL")
ICP217 S ^ICP("SEAL",ID,"STATUS")="SEALED"
ICP218 S ^ICP("SEAL",ID,"LEVEL")=$G(^ICP("LEVEL"))
ICP219 S ^ICP("SEAL",ID,"STATE")=$G(^ICP("STATUS"))
ICP220 Q 1
ICP221 ;
ICP222 REVOKE(ID,REASON) ;
ICP223 I '$D(^ICP("DECISION",ID)) Q 0
ICP224 S ^ICP("DECISION",ID,"STATE")="REVOKED"
ICP225 S ^ICP("DECISION",ID,"REASON")=$G(REASON)
ICP226 Q 1
ICP227 ;
ICP228 REPORT ;
ICP229 W !,"ICP GOVERNANCE PROTOCOL"
ICP230 W !,"VERSION: ",$G(^ICP("VERSION"))
ICP231 W !,"LEVEL: ",$G(^ICP("LEVEL"))
ICP232 W !,"STATUS: ",$G(^ICP("STATUS"))
ICP233 W !,"ACTORS: ",$G(^ICP("AUTHORITY"))
ICP234 W !,"POLICIES: ",$G(^ICP("POLICIES"))
ICP235 W !,"CONSTRAINTS: ",$G(^ICP("CONSTRAINTS"))
ICP236 W !,"CLAIMS: ",$G(^ICP("CLAIMS"))
ICP237 W !,"EVIDENCE: ",$G(^ICP("EVIDENCE"))
ICP238 W !,"DECISIONS: ",$G(^ICP("DECISIONS"))
ICP239 W !,"EXECUTIONS: ",$G(^ICP("EXECUTIONS"))
ICP240 W !,"FAILURES: ",$G(^ICP("FAILURES"))
ICP241 Q
ICP242 ;
ICP243 TEST ;
ICP244 D GOVERN
ICP245 D CLAIM("C1","MODEL ARCHITECTURE VERIFIED","SYSTEM")
ICP246 D EVID("E1","EXPOSED MODEL METADATA","ARTIFACT")
ICP247 D PROVENANCE("C1","ARTIFACT","METADATA","HASH-REQUIRED")
ICP248 D DERIVE("C1","E1","METADATA-DERIVATION")
ICP249 D PROVE("C1","P1",1)
ICP250 D ENFORCE("C1")
ICP251 I $G(^ICP("STATUS"))="FAILED" D HALT Q
ICP252 D DECISION("D1","C1","AUTHORIZE-AUDIT")
ICP253 I $G(^ICP("STATUS"))="FAILED" D HALT Q
ICP254 D EXECUTE("D1","SYSTEM")
ICP255 I $G(^ICP("STATUS"))="FAILED" D HALT Q
ICP256 D SEAL("D1")
ICP257 D FINAL
ICP258 D REPORT
ICP259 Q
ICP260 ;
ICP261 EMERGENCY ;
ICP262 ; EMERGENCY GOVERNANCE MODE
ICP263 ; ANY CRITICAL INTEGRITY FAILURE TERMINATES EXECUTION.
ICP264 S ^ICP("STATUS")="EMERGENCY"
ICP265 D HALT
ICP266 Q
ICP267 ;
ICP268 OVERRIDE ;
ICP269 ; OVERRIDES ARE DISABLED BY DEFAULT.
ICP270 ; AN OVERRIDE MUST NEVER ERASE PRIOR EVIDENCE.
ICP271 ; AN OVERRIDE MUST CREATE AN AUDITABLE EVENT.
ICP272 ; AN OVERRIDE MUST IDENTIFY AUTHORITY.
ICP273 ; AN OVERRIDE MUST STATE JUSTIFICATION.
ICP274 Q
ICP275 ;
ICP276 INVARIANT ;
ICP277 ; GOVERNANCE INVARIANT:
ICP278 ; AUTHORIZED = IDENTITY + SCOPE + EVIDENCE + CONSTRAINTS + PROOF
ICP279 ;
ICP280 ; CLAIM INVARIANT:
ICP281 ; VERIFIED = EVIDENCE OR FORMAL-DERIVATION
ICP282 ;
ICP283 ; EXECUTION INVARIANT:
ICP284 ; NOT-AUTHORIZED = DO-NOT-EXECUTE
ICP285 ;
ICP286 ; FAILURE INVARIANT:
ICP287 ; MANDATORY-CONSTRAINT-FAILURE = HALT
ICP288 ;
ICP289 ; EPISTEMIC INVARIANT:
ICP290 ; UNKNOWN != VERIFIED
ICP291 ;
ICP292 ; PROVENANCE INVARIANT:
ICP293 ; AUTHORITATIVE-CLAIM -> TRACEABLE-SOURCE
ICP294 ;
ICP295 ; AUDIT INVARIANT:
ICP296 ; DECISION -> REPLAYABLE-RECORD
ICP297 Q
ICP298 ;
ICP299 END ;
ICP300 ; END OF INTEGRITY CONSTRAINT GOVERNANCE PROTOCOL
ICP301 ;
ICP302 ; ============================================================
ICP303 ; CONTROL-FLOW DUALITY LAYER
ICP304 ; Implements push/pull (GOTO / COME-FROM) duality.
ICP305 ; Invariants proved in ControlFlowInvariants.agda:
ICP306 ;   state-invariant    — STATE is unmutated across transfer
ICP307 ;   duality-invariant  — GOTO ↔ COME-FROM topological isomorphism
ICP308 ;   conditional-duality-invariant — guarded edge symmetry
ICP309 ; ASP verification in ICP-DAG.lp (I-DUAL-1, I-DUAL-2, I-GUARD-1,
ICP310 ;   I-GUARD-2, I-DET).
ICP311 ; ============================================================
ICP312 ;
ICP313 SETUP ; Initialize bidirectional DAG in ^ICP for duality layer
ICP314 ; Unconditional dual edge: l1 → l2
ICP315 ; GOTO  (push): L1 pushes to L2
ICP316 S ^ICP("DAG","GOTO","l1","l2")=""
ICP317 ; COME-FROM (pull): L2 pulls from L1
ICP318 S ^ICP("DAG","COME-FROM","l2","l1")=""
ICP319 ;
ICP320 ; Conditional dual edge: l1 → l2 on guard IS_AUTHORIZED
ICP321 S ^ICP("DAG","GOTO","l1","IS_AUTHORIZED")="l2"
ICP322 S ^ICP("DAG","COME-FROM","l2","IS_AUTHORIZED")="l1"
ICP323 Q
ICP324 ;
ICP325 PUSH(L1,STATE) ; GOTO — push mechanics (Agda: step-goto)
ICP326 ; State Preservation Invariant: STATE is passed by value, not mutated.
ICP327 N L2,GUARD
ICP328 ; Evaluate which guard holds for L1 in STATE
ICP329 S GUARD=$$EVALGUARD(L1,STATE)
ICP330 I GUARD="" D  Q STATE ; No valid transition — terminal or halt
ICP331 . S ^ICP("FAILURES")=^ICP("FAILURES")+1
ICP332 . S ^ICP("STATUS")="HALTED-NO-TRANSITION"
ICP333 ; O(1) global lookup: retrieve target under evaluated guard
ICP334 S L2=$G(^ICP("DAG","GOTO",L1,GUARD))
ICP335 I L2="" Q STATE ; Guard matched but no target — topology error
ICP336 ; Execute forward. STATE is strictly preserved across the jump.
ICP337 G @L2
ICP338 ;
ICP339 PULL(L2,STATE) ; COME-FROM — pull mechanics (Agda: step-come-from)
ICP340 ; State Preservation Invariant: STATE passed by value.
ICP341 ; In distributed context: acts as await/dependency check on origin.
ICP342 N L1,GUARD
ICP343 S GUARD=$$EVALGUARD(L2,STATE)
ICP344 I GUARD="" Q STATE
ICP345 S L1=$G(^ICP("DAG","COME-FROM",L2,GUARD))
ICP346 I L1="" Q STATE
ICP347 ; Dependency check: wait for L1 to complete before L2 executes
ICP348 D AWAIT(L1)
ICP349 D @L2
ICP350 Q
ICP351 ;
ICP352 EVALGUARD(NODE,STATE) ; Evaluate which guard holds at NODE given STATE
ICP353 ; Returns the first guard whose condition is satisfied.
ICP354 ; Injects holds(StateID, Guard) facts for ASP verification.
ICP355 N GUARD,RESULT
ICP356 S GUARD=""
ICP357 F  S GUARD=$O(^ICP("DAG","GOTO",NODE,GUARD)) Q:GUARD=""  D  Q:RESULT'=""
ICP358 . I $$CHECKGUARD(NODE,GUARD,STATE) S RESULT=GUARD
ICP359 Q $G(RESULT)
ICP360 ;
ICP361 CHECKGUARD(NODE,GUARD,STATE) ; Evaluate guard condition against STATE
ICP362 ; Default: check ^ICP("STATE",STATE,GUARD) is set and truthy
ICP363 Q $G(^ICP("STATE",$G(STATE),GUARD))'=""
ICP364 ;
ICP365 AWAIT(L1) ; Dependency barrier — wait for L1 node to reach COMMITTED
ICP366 ; Used by PULL to enforce temporal ordering (COME-FROM semantics)
ICP367 N STATUS,TIMEOUT
ICP368 S TIMEOUT=1000
ICP369 F I=1:1:TIMEOUT D  Q:STATUS="COMMITTED"
ICP370 . S STATUS=$G(^ICP("NODE",L1,"STATE"))
ICP371 I STATUS'="COMMITTED" D
ICP372 . S ^ICP("FAILURES")=^ICP("FAILURES")+1
ICP373 . S ^ICP("STATUS")="AWAIT-TIMEOUT:"_L1
ICP374 Q
ICP375 ;
ICP376 DUALSETUP(L1,L2,GUARD) ; Register a guarded dual edge atomically
ICP377 ; Enforces I-GUARD-1 / I-GUARD-2 by always writing both directions.
ICP378 ; Calling PUSH or PULL without calling DUALSETUP first is a
ICP379 ; topology error caught by ASP :- goto(L1,L2,G), not come_from(L2,L1,G).
ICP380 I L1=""!(L2="")!(GUARD="") Q 0
ICP381 S ^ICP("DAG","GOTO",L1,GUARD)=L2
ICP382 S ^ICP("DAG","COME-FROM",L2,GUARD)=L1
ICP383 ; Also register unconditional backward index for ASP come_from/2
ICP384 S ^ICP("DAG","COME-FROM",L2,L1)=""
ICP385 S ^ICP("DAG","GOTO",L1,L2)=""
ICP386 Q 1
ICP387 ;
ICP388 VERIFYDUAL ; Validate entire DAG for duality — mirrors ASP I-DUAL-1/2
ICP389 ; Returns count of violations. 0 = topology is sound.
ICP390 N L1,L2,GUARD,VIOLATIONS
ICP391 S VIOLATIONS=0
ICP392 ; Check every GOTO has a matching COME-FROM
ICP393 S L1=""
ICP394 F  S L1=$O(^ICP("DAG","GOTO",L1)) Q:L1=""  D
ICP395 . S L2=""
ICP396 . F  S L2=$O(^ICP("DAG","GOTO",L1,L2)) Q:L2=""  D
ICP397 .. I '$D(^ICP("DAG","COME-FROM",L2,L1)) D
ICP398 ... S VIOLATIONS=VIOLATIONS+1
ICP399 ... S ^ICP("DUAL-VIOLATION",L1,L2)="GOTO-WITHOUT-COME-FROM"
ICP400 ; Check every COME-FROM has a matching GOTO
ICP401 S L2=""
ICP402 F  S L2=$O(^ICP("DAG","COME-FROM",L2)) Q:L2=""  D
ICP403 . S L1=""
ICP404 . F  S L1=$O(^ICP("DAG","COME-FROM",L2,L1)) Q:L1=""  D
ICP405 .. I '$D(^ICP("DAG","GOTO",L1,L2)) D
ICP406 ... S VIOLATIONS=VIOLATIONS+1
ICP407 ... S ^ICP("DUAL-VIOLATION",L2,L1)="COME-FROM-WITHOUT-GOTO"
ICP408 Q VIOLATIONS
ICP409 ;
ICP410 ; DUALITY INVARIANTS (cross-reference):
ICP411 ; state-invariant             : STATE never mutated in PUSH/PULL
ICP412 ; duality-invariant           : GOTO ↔ COME-FROM (VERIFYDUAL + ASP)
ICP413 ; conditional-duality-invariant : guarded edges symmetric (DUALSETUP)
ICP414 ; is-deterministic            : enforced by ASP I-DET constraint
ICP415 ;
ICP416 ENDDUAL ;
ICP417 ; END OF CONTROL-FLOW DUALITY LAYER