% Rules: Release Readiness Determination
% Source-of-truth query for system readiness

:- module(release, [
    release_ready/1,
    readiness_check/2,
    all_proofs_satisfied/1,
    receipt_chain_sealed/1,
    no_revoked_capabilities/1,
    all_cells_complete/1,
    dispatch_gated/5
]).

:- use_module(authorization).
:- use_module(transitions).
:- use_module(proofs).
:- use_module(provenance).
:- use_module(receipts).
:- use_module(agents).
:- use_module(notebook_cells).

% release_ready(IsReady)
% Master query: system is release-ready if all conditions are met

release_ready(true) :-
    all_proofs_satisfied(true),
    receipt_chain_sealed(true),
    no_revoked_capabilities(true),
    all_cells_complete(true),
    receipt_chain_valid(true).

release_ready(false).

% readiness_check(CheckName, PassedBoolean)
% Individual readiness checks

readiness_check('proofs_satisfied', Result) :- all_proofs_satisfied(Result).
readiness_check('receipt_chain_sealed', Result) :- receipt_chain_sealed(Result).
readiness_check('no_revoked_capabilities', Result) :- no_revoked_capabilities(Result).
readiness_check('all_cells_complete', Result) :- all_cells_complete(Result).
readiness_check('receipt_chain_integrity', Result) :- receipt_chain_valid(Result).

% all_proofs_satisfied(IsSatisfied)
% All proof obligations must be verified

all_proofs_satisfied(true) :-
    proof_satisfied('proof_borrow_step_sound', true),
    proof_satisfied('proof_cons_cell_model', true),
    proof_satisfied('proof_dispatch_safe', true),
    proof_satisfied('proof_receipt_chain_integrity', true).

all_proofs_satisfied(false).

% receipt_chain_sealed(IsSealed)
% Receipt chain must have reached its head (final seal)

receipt_chain_sealed(true) :-
    receipt_chain_head(HeadID),
    receipt_issued(HeadID, _Seq, metatron, _Cap, _Instr, finalize, _InHash, _OutHash, _TS),
    receipt_valid(HeadID, true).

receipt_chain_sealed(false).

% no_revoked_capabilities(IsClean)
% Verify that no active agent capabilities have been revoked

no_revoked_capabilities(true) :-
    \+ (agent_active(Agent, true),
        capability_issued(_CapID, _Issuer, Agent, _Runtime, _Perms, _Issued, _Expires),
        capability_revoked(_CapID, _)).

no_revoked_capabilities(false).

% all_cells_complete(IsComplete)
% All cells must be either sealed or passed execution

all_cells_complete(true) :-
    \+ (cell_exists(CellID, _Type, _Kernel, _Visibility, _SourceHash, _OutputHash),
        \+ (cell_sealed(CellID, true) ; cell_metadata(CellID, _Class, _DepCount, passed))).

all_cells_complete(false).

% Detailed readiness report (for logging)

readiness_report(Report) :-
    findall(check(Name, Result), readiness_check(Name, Result), Checks),
    Report = Checks.

% dispatch_gated(AgentID, CapabilityID, TargetRuntime, Permission, IsPermitted)
% SEALED authorization gate: all external dispatch MUST pass through this predicate.
% This is the only entry point for runtime authorization decisions.
% Directly querying capability_active/2 or dispatch_permitted/5 is not allowed.

dispatch_gated(AgentID, CapID, TargetRuntime, Permission, true) :-
    % Step 1: Verify agent exists and is active
    agent_active(AgentID, true),
    % Step 2: Verify agent trust tier is not observer (tier_2)
    agent_trust_level(AgentID, TrustLevel),
    TrustLevel \= tier_2,
    % Step 3: Verify capability is held by agent for this runtime
    capability_issued(CapID, _IssuerID, AgentID, TargetRuntime, _Perms, _IssuedAt, _ExpiresAt),
    % Step 4: Verify capability is active (not revoked, not expired)
    \+ capability_revoked(CapID, _),
    get_time(Now),
    Timestamp is floor(Now),
    ExpiresAt_val is _ExpiresAt,
    Timestamp < ExpiresAt_val,
    % Step 5: Verify permission is in capability
    member(Permission, _Perms),
    % Step 6: Verify target runtime is active
    runtime_active(TargetRuntime, true).

dispatch_gated(_, _, _, _, false).