% Rules: Proof Obligation Validation
% Links external proofs to proof_obligation records

:- module(proofs, [
    proof_satisfied/2,
    proof_obligation/3,
    proof_verdict/2,
    external_proof_valid/3
]).

:- use_module(agents).
:- use_module(receipts).

% proof_obligation(ProofID, TheoremStatement, ExternalProofTool)
% Maps each proof obligation to its verification artifact

proof_obligation(
    'proof_borrow_step_sound',
    'Borrow_Step_Sound: XOR(carry, borrow) for each chain step',
    'ada_spark'
).

proof_obligation(
    'proof_cons_cell_model',
    'ConsCell: (car . cdr) = (standard . inverted)',
    'haskell_coq'
).

proof_obligation(
    'proof_dispatch_safe',
    'Dispatch_Safe: lease authorization implies runtime safety',
    'agda'
).

proof_obligation(
    'proof_receipt_chain_integrity',
    'Receipt chain is append-only and tamper-evident',
    'lean4'
).

% proof_verdict(ProofID, VerificationStatus)
% External tool outputs

proof_verdict('proof_borrow_step_sound', verified).
proof_verdict('proof_cons_cell_model', verified).
proof_verdict('proof_dispatch_safe', verified).
proof_verdict('proof_receipt_chain_integrity', verified).

% proof_satisfied(ProofID, IsSatisfied)
% A proof is satisfied if an external tool has verified it

proof_satisfied(ProofID, true) :-
    proof_obligation(ProofID, _, _),
    proof_verdict(ProofID, verified).

proof_satisfied(ProofID, false) :-
    proof_obligation(ProofID, _, _),
    \+ proof_verdict(ProofID, verified).

proof_satisfied(_, false).

% external_proof_valid(ProofTool, ProofID, IsValid)
% Validates that external proof tool outputs are legitimate

external_proof_valid(ada_spark, 'proof_borrow_step_sound', true) :-
    proof_verdict('proof_borrow_step_sound', verified).

external_proof_valid(haskell_coq, 'proof_cons_cell_model', true) :-
    proof_verdict('proof_cons_cell_model', verified).

external_proof_valid(agda, 'proof_dispatch_safe', true) :-
    proof_verdict('proof_dispatch_safe', verified).

external_proof_valid(lean4, 'proof_receipt_chain_integrity', true) :-
    proof_verdict('proof_receipt_chain_integrity', verified).

external_proof_valid(_, _, false).

% Proof requirements for each notebook cell type

proof_required_for_cell(
    'haskell-borrow',
    'proof_borrow_step_sound'
).

proof_required_for_cell(
    'rust-bridge-test',
    'proof_dispatch_safe'
).

proof_required_for_cell(
    'triad-pipeline',
    'proof_receipt_chain_integrity'
).