File size: 18,011 Bytes

6afa130

% ============================================================================
% NOTEBOOK ENGINE v2.0 — Production-Ready Prolog Knowledge Kernel
% ============================================================================
% Purpose: Symbolic reasoning layer for notebook cell verification,
%          receipt chain integrity, and trust policy enforcement.
%
% Architecture:
%   - Cell Facts: Source code + markdown definitions with hashing
%   - Receipt Facts: v2.0 compatible with chain linkage validation
%   - Nonce Records: Replay protection with monotonic counters
%   - Ed25519 Keys: Agent public key registry
%   - Trust Policies: Role-based access control with expiry
%   - Cell Dependencies: DAG verification and cycle detection
%
% Output: Pure logic, no side effects. All queries backtrack for full solutions.
% ============================================================================

% ============================================================================
% SECTION 1: CELL FACTS — Notebook Execution Artifacts
% ============================================================================

% cell(CellIndex, Type, Source, OutputData, OutputHash, ExecutionTime)
% - CellIndex: unique identifier (integer)
% - Type: 'code' or 'markdown'
% - Source: source text or markdown
% - OutputData: computed result (code cells only; nil for markdown)
% - OutputHash: SHA256 hash of output (nil for markdown)
% - ExecutionTime: milliseconds to execute

cell(1, code, 'let x = 42; x * 2', 84, 'a1b2c3d4e5f6g7h8i9j0k1l2m3n4o5p6q7r8s9t0u1v2w3x4y5z6a7b8c9d0e1f2', 125).

cell(2, markdown, '# Computation Results\n\nThis cell documents the computation of doubling.', nil, nil, 0).

cell(3, code, 'const result = 84; console.log(`Result: ${result}`);', 'Result: 84', 'b2c3d4e5f6g7h8i9j0k1l2m3n4o5p6q7r8s9t0u1v2w3x4y5z6a7b8c9d0e1f2g3', 87).

cell(4, code, 'import { verify_receipt } from "./crypto.js";\nverify_receipt();', 'OK', 'c3d4e5f6g7h8i9j0k1l2m3n4o5p6q7r8s9t0u1v2w3x4y5z6a7b8c9d0e1f2g3h4', 203).

% ============================================================================
% SECTION 2: RECEIPT FACTS v2.0 — Chain-Linked Verification Records
% ============================================================================

% receipt(ReceiptID, Hash, Signature, AgentID, Status, Timestamp)
% - ReceiptID: unique receipt identifier
% - Hash: SHA256 of cell execution (links to OutputHash)
% - Signature: Ed25519 signature (64 hex chars)
% - AgentID: executing agent identifier
% - Status: 'success' | 'sealed'
% - Timestamp: Unix milliseconds

receipt(r001, 'a1b2c3d4e5f6g7h8i9j0k1l2m3n4o5p6q7r8s9t0u1v2w3x4y5z6a7b8c9d0e1f2',
        '1a2b3c4d5e6f7a8b9c0d1e2f3a4b5c6d7e8f9a0b1c2d3e4f5a6b7c8d9e0f1a2b3c4d5e6f7a8b9c0d1e2f3a4b5c6d7e8f9a0b1c2d3e4f5',
        'agent_prime', 'success', 1719374400000).

receipt(r002, 'b2c3d4e5f6g7h8i9j0k1l2m3n4o5p6q7r8s9t0u1v2w3x4y5z6a7b8c9d0e1f2g3',
        '2b3c4d5e6f7a8b9c0d1e2f3a4b5c6d7e8f9a0b1c2d3e4f5a6b7c8d9e0f1a2b3c4d5e6f7a8b9c0d1e2f3a4b5c6d7e8f9a0b1c2d3e4f5a6',
        'agent_flux', 'success', 1719374450000).

receipt(r003, 'c3d4e5f6g7h8i9j0k1l2m3n4o5p6q7r8s9t0u1v2w3x4y5z6a7b8c9d0e1f2g3h4',
        '3c4d5e6f7a8b9c0d1e2f3a4b5c6d7e8f9a0b1c2d3e4f5a6b7c8d9e0f1a2b3c4d5e6f7a8b9c0d1e2f3a4b5c6d7e8f9a0b1c2d3e4f5a6b7',
        'agent_cipher', 'sealed', 1719374500000).

% ============================================================================
% SECTION 3: RECEIPT CHAIN LINKAGE — Integrity Verification
% ============================================================================

% receipt_chain_link(Hash, PreviousHash)
% - Establishes chronological ordering and chain integrity
% - Genesis block: previous hash is all zeros
% - Each receipt cryptographically commits to ancestor state

receipt_chain_link('a1b2c3d4e5f6g7h8i9j0k1l2m3n4o5p6q7r8s9t0u1v2w3x4y5z6a7b8c9d0e1f2',
                   '0000000000000000000000000000000000000000000000000000000000000000').

receipt_chain_link('b2c3d4e5f6g7h8i9j0k1l2m3n4o5p6q7r8s9t0u1v2w3x4y5z6a7b8c9d0e1f2g3',
                   'a1b2c3d4e5f6g7h8i9j0k1l2m3n4o5p6q7r8s9t0u1v2w3x4y5z6a7b8c9d0e1f2').

receipt_chain_link('c3d4e5f6g7h8i9j0k1l2m3n4o5p6q7r8s9t0u1v2w3x4y5z6a7b8c9d0e1f2g3h4',
                   'b2c3d4e5f6g7h8i9j0k1l2m3n4o5p6q7r8s9t0u1v2w3x4y5z6a7b8c9d0e1f2g3').

% Genesis block helper
is_genesis_hash('0000000000000000000000000000000000000000000000000000000000000000').

% ============================================================================
% SECTION 4: NONCE RECORDS — Replay Attack Protection
% ============================================================================

% nonce_record(Nonce, Context, MonotonicCounter, Timestamp)
% - Nonce: unique random token (hex string)
% - Context: execution context identifier
% - MonotonicCounter: strictly increasing per context
% - Timestamp: Unix milliseconds (for expiry enforcement)

nonce_record('nonce_7a3f1b9c2d8e4f5a1b2c3d4e5f6a7b8c', 'cell_exec_1', 1, 1719374400000).

nonce_record('nonce_8b4g2c0d3e9f5g6b2c3d4e5f6g7a8b9d', 'cell_exec_1', 2, 1719374410000).

nonce_record('nonce_9c5h3d1e4f0g6h7c3d4e5f6g7h8b9c0e', 'cell_exec_2', 1, 1719374420000).

% Per-context counter tracking
context_max_counter('cell_exec_1', 2).
context_max_counter('cell_exec_2', 1).

% Nonce expiry window: 3600 seconds (1 hour)
nonce_expiry_window(3600000).

% ============================================================================
% SECTION 5: ED25519 PUBLIC KEY REGISTRY
% ============================================================================

% ed25519_public_key(AgentID, KeyVersion, PublicKeyHex)
% - AgentID: unique agent identifier
% - KeyVersion: version of the key (for rotation)
% - PublicKeyHex: 64 hex chars representing the public key

ed25519_public_key('agent_prime', 1, '7f3a9c2d5e1b4f8c9d2e5a1f3c6b9e2d5a7c0f3b6e9a2c5f8b1e4d7a0c3f6').

ed25519_public_key('agent_prime', 2, '8g4b0d3e6f2c5a9d0e3f6b2c5f8a1d4e7b0c3f6a9d2e5f8b1c4f7a0d3e6b9').

ed25519_public_key('agent_flux', 1, '9h5c1e4f7g3d6b0e1f4g7c3d6g9a2e5f8c1d4g7b0e3f6a9d2f5g8b1c4f7d0').

ed25519_public_key('agent_cipher', 1, '0i6d2f5g8h4e7c1f2g5h8d4e7h0b3f6g9c2e5h8d1e4g7b0f3g6a9d2f5g8c1').

% Current active key version per agent
active_key_version('agent_prime', 2).
active_key_version('agent_flux', 1).
active_key_version('agent_cipher', 1).

% ============================================================================
% SECTION 6: TRUST POLICIES — Role-Based Access Control
% ============================================================================

% trust_policy(AgentID, Capability, Tier, ExpiryTimestamp)
% - AgentID: agent identifier
% - Capability: permission name (e.g., 'execute_code', 'seal_receipt')
% - Tier: access level ('read', 'write', 'admin')
% - ExpiryTimestamp: Unix milliseconds (0 = no expiry)

trust_policy('agent_prime', 'execute_code', 'write', 0).
trust_policy('agent_prime', 'seal_receipt', 'admin', 0).
trust_policy('agent_prime', 'verify_chain', 'read', 0).

trust_policy('agent_flux', 'execute_code', 'write', 1719460800000).
trust_policy('agent_flux', 'query_cells', 'read', 0).
trust_policy('agent_flux', 'verify_chain', 'read', 0).

trust_policy('agent_cipher', 'execute_code', 'write', 1719547200000).
trust_policy('agent_cipher', 'seal_receipt', 'write', 1719633600000).
trust_policy('agent_cipher', 'verify_chain', 'read', 0).

% ============================================================================
% SECTION 7: CELL DEPENDENCIES — Execution DAG
% ============================================================================

% cell_depends_on(CellIndex, DependsOnCellIndex)
% - Establishes a directed acyclic graph (DAG) of execution dependencies
% - Used for: cycle detection, provenance chains, topological ordering

cell_depends_on(2, 1).      % Cell 2 (markdown) references Cell 1
cell_depends_on(3, 1).      % Cell 3 (code) depends on Cell 1 output
cell_depends_on(4, 3).      % Cell 4 (code) depends on Cell 3 output
cell_depends_on(4, 2).      % Cell 4 also references Cell 2 documentation

% ============================================================================
% SECTION 8: VERIFICATION PREDICATES — Core Logic
% ============================================================================

% verify_receipt_complete(ID, Agent, KeyVersion, Nonce, Context, Counter)
% Full validation pipeline: receipt exists, signature valid, nonce unique,
% counter monotonic, trust policy active, and chain linked.
%
% Success: All 6 checks pass
% Failure: Unification fails on any check
verify_receipt_complete(ReceiptID, AgentID, KeyVersion, Nonce, Context, Counter) :-
    % Check 1: Receipt exists and is accessible
    receipt(ReceiptID, Hash, _Signature, AgentID, Status, _Timestamp),
    ( Status = 'success' ; Status = 'sealed' ),

    % Check 2: Agent has active key in requested version
    active_key_version(AgentID, ActiveVersion),
    KeyVersion =< ActiveVersion,
    ed25519_public_key(AgentID, KeyVersion, _PublicKey),

    % Check 3: Nonce exists and is valid (not replayed)
    nonce_record(Nonce, Context, RecordedCounter, NonceTimestamp),

    % Check 4: Monotonic counter constraint
    Counter >= RecordedCounter,
    context_max_counter(Context, MaxSoFar),
    Counter > MaxSoFar,

    % Check 5: Trust policy permits this operation
    trust_policy(AgentID, 'seal_receipt', _Tier, ExpiryTime),
    ( ExpiryTime =:= 0 ; get_current_timestamp(CurrentTime), CurrentTime < ExpiryTime ),

    % Check 6: Receipt is chain-linked
    receipt_chain_link(Hash, _PreviousHash).

% all_obligations_discharged()
% Release gate: validates ALL receipts in chain are valid, no nonce replays,
% and all agents have sufficient trust policies. Returns true if system is
% in a verified safe state.
all_obligations_discharged() :-
    % Obligation 1: All receipts must have valid chain links
    forall(receipt(_, Hash, _, _, _, _),
           receipt_chain_link(Hash, _)),

    % Obligation 2: All receipts must have corresponding cells
    forall(receipt(_, Hash, _, _, _, _),
           cell(_, _, _, _, Hash, _)),

    % Obligation 3: No nonce replays in any context
    forall(nonce_record(Nonce, Context, Counter, _),
           \+ replay_attempt(Nonce, Context, Counter)),

    % Obligation 4: All agents with active receipts have valid trust policies
    forall(receipt(_, _, _, AgentID, Status, _),
           ( Status = 'sealed' ->
               (trust_policy(AgentID, 'seal_receipt', _, _),
                active_key_version(AgentID, _))
           ;   true
           )),

    % Obligation 5: All cell dependencies are acyclic (DAG constraint)
    \+ has_circular_dependency(_).

% Helper: Detect replay attempt (same nonce with lower counter)
replay_attempt(Nonce, Context, Counter) :-
    nonce_record(Nonce, Context, RecordedCounter, _),
    Counter < RecordedCounter.

% ============================================================================
% SECTION 9: QUERY PREDICATES — For JIT Execution Box
% ============================================================================

% query_cell_dependencies(CellIndex, DependentCells)
% Find all cells that depend on (or transitively depend on) CellIndex.
% Returns list of cell indices in dependency order.
query_cell_dependencies(CellIndex, DependentCells) :-
    findall(Dep, cell_depends_on(Dep, CellIndex), DirectDeps),
    ( DirectDeps = [] ->
        DependentCells = []
    ;   findall(Cell, (
            member(Dep, DirectDeps),
            (Cell = Dep ; query_cell_dependencies(Dep, SubDeps), member(Cell, SubDeps))
        ), AllDeps),
        sort(AllDeps, DependentCells)
    ).

% query_provenance_chain(CellIndex, Chain)
% Construct full execution history for a cell: its direct dependencies
% and all transitive ancestors in the DAG.
query_provenance_chain(CellIndex, Chain) :-
    findall(Ancestor, cell_ancestor(CellIndex, Ancestor), Ancestors),
    sort([CellIndex | Ancestors], UnsortedChain),
    % Sort by cell execution order (reverse topological sort)
    reverse(UnsortedChain, Chain).

% Helper: Find all ancestors of a cell in the dependency DAG
cell_ancestor(CellIndex, Ancestor) :-
    cell_depends_on(CellIndex, Parent),
    Ancestor = Parent.
cell_ancestor(CellIndex, Ancestor) :-
    cell_depends_on(CellIndex, Parent),
    cell_ancestor(Parent, Ancestor).

% query_trust_rules(AgentID, Rules)
% Return all trust policies for a given agent as a list of policy terms.
query_trust_rules(AgentID, Rules) :-
    findall(trust_policy(AgentID, Cap, Tier, Expiry),
            trust_policy(AgentID, Cap, Tier, Expiry),
            Rules).

% verify_cell_chain_integrity()
% Validate the entire receipt chain: every hash links to previous,
% genesis is properly formed, and no gaps exist.
verify_cell_chain_integrity() :-
    % Every receipt must have a chain link
    forall(receipt(_, Hash, _, _, _, _),
           receipt_chain_link(Hash, _)),

    % Every chain link must originate from genesis
    forall(receipt(_, Hash, _, _, _, _),
           chain_reaches_genesis(Hash)).

% Helper: Verify a hash reaches genesis through the chain
chain_reaches_genesis(Hash) :-
    receipt_chain_link(Hash, PrevHash),
    ( is_genesis_hash(PrevHash) ->
        true
    ;   chain_reaches_genesis(PrevHash)
    ).

% has_circular_dependency(CellIndex)
% Check if CellIndex is part of a cycle in the dependency DAG.
% Returns the cell involved in the cycle.
has_circular_dependency(CellIndex) :-
    cell_depends_on(CellIndex, Dep),
    path_exists(Dep, CellIndex).

% Helper: Check if a path exists from Start to End in the DAG
path_exists(Start, End) :-
    cell_depends_on(Start, End).
path_exists(Start, End) :-
    cell_depends_on(Start, Mid),
    path_exists(Mid, End).

% is_authorized(AgentID, Capability)
% Check if agent has permission for capability and policy is active.
% Returns true only if trust_policy exists and expiry has not passed.
is_authorized(AgentID, Capability) :-
    trust_policy(AgentID, Capability, _Tier, ExpiryTime),
    ( ExpiryTime =:= 0 ->
        true
    ;   get_current_timestamp(CurrentTime),
        CurrentTime < ExpiryTime
    ).

% notebook_summary(Summary)
% High-level overview of notebook state as a structured term.
% Summary: summary(CellCount, ReceiptCount, AgentCount, ChainValid)
notebook_summary(summary(CellCount, ReceiptCount, AgentCount, ChainValid)) :-
    findall(_, cell(_, _, _, _, _, _), Cells),
    length(Cells, CellCount),

    findall(_, receipt(_, _, _, _, _, _), Receipts),
    length(Receipts, ReceiptCount),

    findall(A, (receipt(_, _, _, A, _, _)), AgentsList),
    sort(AgentsList, Agents),
    length(Agents, AgentCount),

    ( verify_cell_chain_integrity() ->
        ChainValid = true
    ;   ChainValid = false
    ).

% ============================================================================
% SECTION 10: HELPER PREDICATES — Utilities
% ============================================================================

% get_current_timestamp(Timestamp)
% Mock timestamp for verification. In production, calls system time.
% For testing, returns a fixed value within the policy validity windows.
get_current_timestamp(1719400000000).  % 2024-06-26 12:00:00 UTC

% hash_length_valid(Hash)
% Verify hash is 64 hex characters (SHA256 representation).
hash_length_valid(Hash) :-
    atom_string(Hash, HexStr),
    string_length(HexStr, 64),
    atom_codes(Hash, Codes),
    forall(member(C, Codes),
           (C >= 48, C =< 57) ;  % 0-9
           (C >= 97, C =< 102) ;  % a-f
           (C >= 65, C =< 70)).   % A-F (uppercase)

% key_length_valid(KeyHex)
% Verify Ed25519 public key is 64 hex characters.
key_length_valid(KeyHex) :-
    atom_string(KeyHex, HexStr),
    string_length(HexStr, 64).

% signature_length_valid(SigHex)
% Verify Ed25519 signature is 128 hex characters (64 bytes → 128 hex).
signature_length_valid(SigHex) :-
    atom_string(SigHex, HexStr),
    string_length(HexStr, 128).

% ============================================================================
% SECTION 11: INTEGRITY ASSERTIONS — Invariant Checks
% ============================================================================

% Assert: No two nonces are identical across any context
assert_nonces_unique :-
    findall(N-C, nonce_record(N, C, _, _), NonceContexts),
    \+ has_duplicate_pairs(NonceContexts).

% Assert: All receipt agents have matching Ed25519 keys
assert_all_agents_have_keys :-
    forall(receipt(_, _, _, AgentID, _, _),
           ed25519_public_key(AgentID, _, _)).

% Assert: No cell has a self-dependency
assert_no_self_loops :-
    \+ cell_depends_on(C, C).

% Helper: Detect duplicate nonce pairs
has_duplicate_pairs(Pairs) :-
    append(Left, [H|Right], Pairs),
    (member(H, Left) ; member(H, Right)).

% ============================================================================
% SECTION 12: EXPORT/PUBLIC INTERFACE
% ============================================================================

% These predicates form the public API for the notebook engine:
%
% Primary verification:
%   - verify_receipt_complete/6
%   - all_obligations_discharged/0
%
% Query interface:
%   - query_cell_dependencies/2
%   - query_provenance_chain/2
%   - query_trust_rules/2
%   - verify_cell_chain_integrity/0
%   - has_circular_dependency/1
%   - is_authorized/2
%   - notebook_summary/1
%
% Assertion (for debug):
%   - assert_nonces_unique/0
%   - assert_all_agents_have_keys/0
%   - assert_no_self_loops/0
%
% ============================================================================
% END OF NOTEBOOK ENGINE
% ============================================================================