File size: 5,404 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 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 | % 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).
|