File size: 4,028 Bytes
1d3f990 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 | % 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).
|