% ICP-DAG v1.0 — Answer Set Programming Governance Constraints
% Companion to ICP-DAG.m (MUMPS imperative layer)
% SAT = governance holds. UNSAT = governance violation → HALT.

% --- INTEGRITY CONSTRAINTS (hard rules) ---

% I3: Unknown claims cannot reach decision
:- node(C,claim,unknown), node(D,decision,_), edge(C,D,decides).

% I4: Contradicted claims cannot reach decision
:- node(C,claim,contradicted), node(D,decision,_), edge(C,D,decides).

% I5: Authorization requires proof
:- node(D,decision,authorized),
   node(C,claim,_), edge(C,D,decides), not proven(C).

% I5b: Execution requires authorized decision
:- node(E,execution,_), edge(D,E,executes),
   node(D,decision,S), S != authorized.

% I9: Unknown and verified are mutually exclusive
:- node(C,claim,unknown), node(C,claim,verified).

% I2: No self-edges
:- node(N,_,_), edge(N,N,_).

% I1: Every edge has two existing endpoints
:- edge(A,B,_), not node(A,_,_).
:- edge(A,B,_), not node(B,_,_).

% --- DERIVED PREDICATES ---

proven(C) :- node(P,proof,proven), edge(C,P,"proven-by").

% ============================================================
% CONTROL-FLOW DUALITY LAYER (from ControlFlowInvariants.agda)
% Enforces is-dual and is-guarded-dual at the ASP governance level.
% Facts injected by MUMPS ICP-GOV.m SETUP routine.
% ============================================================

% --- STATIC TOPOLOGY (unconditional duality) ---
% goto(Source, Target).
% come_from(Target, Source).

% I-DUAL-1: Every GOTO must have a matching COME-FROM (push → pull).
:- goto(L1, L2), not come_from(L2, L1).

% I-DUAL-2: Every COME-FROM must have a matching GOTO (pull → push).
:- come_from(L2, L1), not goto(L1, L2).

% Unified edge predicate — traversable by either mechanism.
edge_cf(L1, L2) :- goto(L1, L2).
edge_cf(L1, L2) :- come_from(L2, L1).

% --- CONDITIONAL DUALITY (guarded edges) ---
% goto(Source, Target, Guard).
% come_from(Target, Source, Guard).

% I-GUARD-1: A conditional push must have an identical conditional pull.
:- goto(L1, L2, Guard), not come_from(L2, L1, Guard).

% I-GUARD-2: A conditional pull must have an identical conditional push.
:- come_from(L2, L1, Guard), not goto(L1, L2, Guard).

% --- DYNAMIC EXECUTION STATE ---
% holds(StateID, Guard).  % injected by MUMPS $$EVALUATE^ICP

% An edge is traversable only when its guard holds in the current state.
traversable(StateID, L1, L2) :-
    goto(L1, L2, Guard),
    holds(StateID, Guard).

% I-DET: Determinism — at most one outgoing guarded edge may hold per state.
% (mirrors is-deterministic in ControlFlowInvariants.agda)
:- traversable(StateID, L1, L2),
   traversable(StateID, L1, L3),
   L2 != L3.

% --- STATE PRESERVATION ---
% The operational step relation guarantees state is not mutated by traversal.
% Enforced here by ensuring no edge_cf fact touches node state fields.
% (Proved as state-invariant in ControlFlowInvariants.agda: s₁ ≡ s₂)
:- edge_cf(L1, L2), node(L1, Type, S1), node(L2, Type2, S2),
   S1 != S2, Type = Type2, Type = execution.

% --- SHOW ---
#show node/3.
#show edge/3.
#show proven/1.
#show goto/2.
#show come_from/2.
#show goto/3.
#show come_from/3.
#show traversable/3.