% PHASE 9: Prolog Verification Tests
% Unit and integration tests for receipt verification and proof obligations

:- use_module(library(plunit)).

:- begin_tests(receipt_verification).

% Test 1: Canonical hash verification
test(receipt_hash_canonical) :-
    receipt_v2(1, 'rcpt-v2-0000000001-loc',
        'a7c4b9e2d1f3c8a5e6b2c9d4e5f6a7b8c9d0e1f2a3b4c5d6e7f8a9b0c1d2e3',
        'loc', _, _, _, _, _, _, _, 'success'),
    verify_receipt_hash(
        'a7c4b9e2d1f3c8a5e6b2c9d4e5f6a7b8c9d0e1f2a3b4c5d6e7f8a9b0c1d2e3',
        'rcpt-v2-0000000001-loc'
    ).

% Test 2: Ed25519 signature verification
test(ed25519_signature_verification) :-
    receipt_v2(1, 'rcpt-v2-0000000001-loc', _, 'loc', _, _, _, _, _, 1, 'sig-001-ed25519', _),
    verify_receipt_signature('rcpt-v2-0000000001-loc', 'sig-001-ed25519', 1).

% Test 3: Chain linkage verification (first receipt)
test(chain_linkage_first_receipt) :-
    receipt_chain_link('a7c4b9e2d1f3c8a5e6b2c9d4e5f6a7b8c9d0e1f2a3b4c5d6e7f8a9b0c1d2e3',
                       '0000000000000000000000000000000000000000000000000000000000000000'),
    verify_chain_linkage('a7c4b9e2d1f3c8a5e6b2c9d4e5f6a7b8c9d0e1f2a3b4c5d6e7f8a9b0c1d2e3',
                         '0000000000000000000000000000000000000000000000000000000000000000').

% Test 4: Chain linkage verification (subsequent receipts)
test(chain_linkage_subsequent) :-
    receipt_chain_link('b8d5c0f3e2g4d9b6f7c3d0e5f6a7b8c9d0e1f2a3b4c5d6e7f8a9b0c1d2e3f4',
                       'a7c4b9e2d1f3c8a5e6b2c9d4e5f6a7b8c9d0e1f2a3b4c5d6e7f8a9b0c1d2e3'),
    verify_chain_linkage('b8d5c0f3e2g4d9b6f7c3d0e5f6a7b8c9d0e1f2a3b4c5d6e7f8a9b0c1d2e3f4',
                         'a7c4b9e2d1f3c8a5e6b2c9d4e5f6a7b8c9d0e1f2a3b4c5d6e7f8a9b0c1d2e3').

% Test 5: Replay protection - first nonce succeeds
test(replay_protection_first) :-
    nonce_record('nonce-loc-001', 'global', 1, _),
    verify_replay_protection('nonce-loc-001', 'global', 2).

% Test 6: Replay protection - increasing counter
test(replay_protection_monotonic) :-
    nonce_record('nonce-loc-001', 'global', 1, _),
    verify_replay_protection('nonce-loc-001', 'global', 3).

% Test 7: Full receipt verification
test(full_receipt_verification) :-
    verify_receipt_complete('rcpt-v2-0000000001-loc', 'loc', 1, 'nonce-loc-001', 'global', 2).

% Test 8: Release gate - all receipts must be verified
test(release_gate_receipts) :-
    release_ready_receipts.

% Test 9: Proof obligation assignment
test(proof_obligation_z3_assignment) :-
    proof_obligation('inv-001', 'invariant_preservation', 'receipt_chain'),
    proof_tool_assignment('invariant_preservation', 'z3').

% Test 10: Proof obligation assignment - Lean 4
test(proof_obligation_lean4_assignment) :-
    proof_obligation('sem-001', 'semantic_preservation', 'subleq_codegen'),
    proof_tool_assignment('semantic_preservation', 'lean4').

% Test 11: Proof obligation assignment - Ada/SPARK
test(proof_obligation_spark_assignment) :-
    proof_obligation('loop-001', 'loop_invariant', 'receipt_append'),
    proof_tool_assignment('loop_invariant', 'spark').

% Test 12: Proof obligation assignment - Agda
test(proof_obligation_agda_assignment) :-
    proof_obligation('chain-001', 'receipt_chain_integrity', 'v2_chain'),
    proof_tool_assignment('receipt_chain_integrity', 'agda').

% Test 13: All proof obligations assigned
test(all_obligations_assigned) :-
    findall(Type, proof_obligation(_, Type, _), Types),
    list_to_set(Types, UniqueTypes),
    forall(
        member(Type, UniqueTypes),
        proof_tool_assignment(Type, _)
    ).

% Test 14: All obligations discharged (release gate)
test(all_obligations_discharged) :-
    all_obligations_discharged.

% Test 15: Receipt status validity
test(receipt_status_success) :-
    receipt_v2(_, 'rcpt-v2-0000000001-loc', _, _, _, _, _, _, _, _, _, 'success'),
    receipt_status_valid('rcpt-v2-0000000001-loc', true).

% Test 16: Canonical form generation
test(receipt_canonical_form) :-
    verify_receipt_canonical('rcpt-v2-0000000001-loc', Canonical),
    atom(Canonical),
    atom_length(Canonical, Length),
    Length > 0.

% Test 17: Receipt chain statistics
test(receipt_chain_stats) :-
    receipt_chain_stats(Total, Signed, Verified),
    Total > 0,
    Signed > 0,
    Verified > 0.

% Test 18: Nonce context isolation
test(nonce_context_isolation) :-
    nonce_record('nonce-loc-001', 'global', 1, _),
    % Different context would allow same nonce with different counter
    \+ nonce_record('nonce-loc-001', 'different-context', 1, _).

% Test 19: Public key exists for all agents
test(public_keys_for_agents) :-
    findall(Agent, receipt_v2(_, _, _, Agent, _, _, _, _, _, _, _, _), Agents),
    list_to_set(Agents, UniqueAgents),
    forall(
        member(Agent, UniqueAgents),
        ed25519_public_key(Agent, _, _)
    ).

% Test 20: Proof obligation type coverage
test(proof_obligation_type_coverage) :-
    findall(Type, proof_tool_assignment(Type, _), ToolTypes),
    findall(Type, proof_obligation(_, Type, _), ObligationTypes),
    list_to_set(ToolTypes, UniqueToolTypes),
    list_to_set(ObligationTypes, UniqueObligationTypes),
    UniqueToolTypes = UniqueObligationTypes.

:- end_tests(receipt_verification).

% Run all tests
run_tests :-
    run_tests(receipt_verification).