1	import Base
2	import ./Reading.bend as Reading
3	import ./StateTree.bend as StateTree
4	import ./History.bend as History
5	import ./Merging.bend as Merging
6	import ./Store.bend as Store
7	
8	# Independent merge verification. The pure core re-derives everything from
9	# entry lists: strategy known, result hash matches recomputed hash, merge
10	# recomputation yields the same entry set, every recorded law passed and at
11	# least one law recorded (empty evidence rejects). The shell loads the trees
12	# named by the certificate — a tampered cert names trees whose content
13	# contradicts its claims.
14	
15	# A key/value pair counts as present only when both match.
16	def decide_entry_present(key_matches: Bool, +head_value: String, +target_value: String, tail_result: Bool) -> Bool:
17	  match key_matches:
18	    case True{}:
19	      String.eq(head_value, target_value)
20	    case False{}:
21	      tail_result
22	
23	# Scans entries for an exact key/value pair.
24	def entry_present_in(+target_key: String, +target_value: String, entries: List<&2, Reading.ChainEntry>) -> Bool:
25	  match entries:
26	    case Nil{}:
27	      False{}
28	    case Con{+head_entry, remaining_entries}:
29	      decide_entry_present(String.eq(Reading.entry_key_of(head_entry), target_key), Reading.entry_value_of(head_entry), target_value, entry_present_in(target_key, target_value, remaining_entries))
30	
31	# Conjunction step: a missing head fails the whole check.
32	def decide_all_present(head_present: Bool, tail_result: Bool) -> Bool:
33	  match head_present:
34	    case True{}:
35	      tail_result
36	    case False{}:
37	      False{}
38	
39	# Every source entry must occur in the target list.
40	def all_present_in(source_entries: List<&2, Reading.ChainEntry>, +target_entries: List<&2, Reading.ChainEntry>) -> Bool:
41	  match source_entries:
42	    case Nil{}:
43	      True{}
44	    case Con{+head_entry, remaining_entries}:
45	      decide_all_present(entry_present_in(Reading.entry_key_of(head_entry), Reading.entry_value_of(head_entry), target_entries), all_present_in(remaining_entries, target_entries))
46	
47	# Set equality both directions; exact because lists are unique-keyed.
48	def entries_equal(+first_entries: List<&2, Reading.ChainEntry>, +second_entries: List<&2, Reading.ChainEntry>) -> Bool:
49	  all_present_in(first_entries, second_entries) && all_present_in(second_entries, first_entries)
50	
51	# Conjunction step over law evidence.
52	def decide_law_step(head_passed: Bool, tail_result: Bool) -> Bool:
53	  match head_passed:
54	    case True{}:
55	      tail_result
56	    case False{}:
57	      False{}
58	
59	# Every remaining check must have passed.
60	def all_remaining_pass(remaining_checks: List<&2, Merging.LawCheck>) -> Bool:
61	  match remaining_checks:
62	    case Nil{}:
63	      True{}
64	    case Con{head_check, tail_checks}:
65	      decide_law_step(Merging.law_check_passed(head_check), all_remaining_pass(tail_checks))
66	
67	# Non-empty evidence with every check passed; empty evidence rejects.
68	def verify_laws_step(checked_laws: List<&2, Merging.LawCheck>) -> Bool:
69	  match checked_laws:
70	    case Nil{}:
71	      False{}
72	    case Con{head_check, remaining_checks}:
73	      decide_law_step(Merging.law_check_passed(head_check), all_remaining_pass(remaining_checks))
74	
75	# Matching entries unlock the law-evidence check.
76	def verify_entries_step(entries_match: Bool, +certificate: Merging.MergeCertificate) -> Bool:
77	  match entries_match:
78	    case False{}:
79	      False{}
80	    case True{}:
81	      verify_laws_step(Merging.cert_checked_laws(certificate))
82	
83	# A clean recomputation unlocks the entry-set check; conflicts reject.
84	def verify_recompute_step(recomputed_outcome: Merging.MergeOutcome, +merged_entries: List<&2, Reading.ChainEntry>, +certificate: Merging.MergeCertificate) -> Bool:
85	  match recomputed_outcome:
86	    case Merging.ConflictingKeys{conflicting_keys}:
87	      False{}
88	    case Merging.MergedEntries{recomputed_entries}:
89	      verify_entries_step(entries_equal(recomputed_entries, merged_entries), certificate)
90	
91	# A matching result hash unlocks the merge recomputation; mismatch rejects.
92	def verify_hash_step(hash_matches: Bool, +base_entries: List<&2, Reading.ChainEntry>, +first_entries: List<&2, Reading.ChainEntry>, +second_entries: List<&2, Reading.ChainEntry>, +merged_entries: List<&2, Reading.ChainEntry>, +certificate: Merging.MergeCertificate) -> Bool:
93	  match hash_matches:
94	    case False{}:
95	      False{}
96	    case True{}:
97	      verify_recompute_step(Merging.merge_entry_lists(base_entries, first_entries, second_entries), merged_entries, certificate)
98	
99	# Only the union-disjoint strategy verifies; anything else rejects.
100	def decide_strategy_known(strategy_known: Bool, +base_entries: List<&2, Reading.ChainEntry>, +first_entries: List<&2, Reading.ChainEntry>, +second_entries: List<&2, Reading.ChainEntry>, +merged_entries: List<&2, Reading.ChainEntry>, +certificate: Merging.MergeCertificate) -> Bool:
101	  match strategy_known:
102	    case False{}:
103	      False{}
104	    case True{}:
105	      verify_hash_step(String.eq(Merging.cert_result_tree(certificate), StateTree.compute_tree_hash(merged_entries)), base_entries, first_entries, second_entries, merged_entries, certificate)
106	
107	# Pure verification core: re-derives strategy, hash, merge and law evidence.
108	def verify_merge_certificate_pure(+base_entries: List<&2, Reading.ChainEntry>, +first_entries: List<&2, Reading.ChainEntry>, +second_entries: List<&2, Reading.ChainEntry>, +merged_entries: List<&2, Reading.ChainEntry>, +certificate: Merging.MergeCertificate) -> Bool:
109	  decide_strategy_known(String.eq(Merging.cert_strategy_name(certificate), "union-disjoint"), base_entries, first_entries, second_entries, merged_entries, certificate)
110	
111	# A present result tree unlocks the pure core; a missing one rejects.
112	def decide_verify_result(+certificate: Merging.MergeCertificate, base_tree: StateTree.StateTreeNode, first_tree: StateTree.StateTreeNode, second_tree: StateTree.StateTreeNode, result_maybe: Maybe<&2, StateTree.StateTreeNode>) -> Bool:
113	  match result_maybe:
114	    case None{}:
115	      False{}
116	    case Some{result_tree}:
117	      verify_merge_certificate_pure(StateTree.tree_entries(base_tree), StateTree.tree_entries(first_tree), StateTree.tree_entries(second_tree), StateTree.tree_entries(result_tree), certificate)
118	
119	# Unpacks the second tree or rejects when missing.
120	def decide_verify_second(+certificate: Merging.MergeCertificate, base_tree: StateTree.StateTreeNode, first_tree: StateTree.StateTreeNode, second_maybe: Maybe<&2, StateTree.StateTreeNode>, result_maybe: Maybe<&2, StateTree.StateTreeNode>) -> Bool:
121	  match second_maybe:
122	    case None{}:
123	      False{}
124	    case Some{second_tree}:
125	      decide_verify_result(certificate, base_tree, first_tree, second_tree, result_maybe)
126	
127	# Unpacks the first tree or rejects when missing.
128	def decide_verify_first(+certificate: Merging.MergeCertificate, base_tree: StateTree.StateTreeNode, first_maybe: Maybe<&2, StateTree.StateTreeNode>, second_maybe: Maybe<&2, StateTree.StateTreeNode>, result_maybe: Maybe<&2, StateTree.StateTreeNode>) -> Bool:
129	  match first_maybe:
130	    case None{}:
131	      False{}
132	    case Some{first_tree}:
133	      decide_verify_second(certificate, base_tree, first_tree, second_maybe, result_maybe)
134	
135	# Unpacks the base tree or rejects when missing.
136	def decide_verify_trees(+certificate: Merging.MergeCertificate, base_maybe: Maybe<&2, StateTree.StateTreeNode>, first_maybe: Maybe<&2, StateTree.StateTreeNode>, second_maybe: Maybe<&2, StateTree.StateTreeNode>, result_maybe: Maybe<&2, StateTree.StateTreeNode>) -> Bool:
137	  match base_maybe:
138	    case None{}:
139	      False{}
140	    case Some{base_tree}:
141	      decide_verify_first(certificate, base_tree, first_maybe, second_maybe, result_maybe)
142	
143	# Shell: loads the four trees named by the certificate and runs the core.
144	def verify_certificate(+certificate: Merging.MergeCertificate) -> Store.Op<&2, Bool>:
145	  do Store.Op<&2, Bool>:
146	    base_tree_maybe : Maybe<&2, StateTree.StateTreeNode> <- History.read_tree_at(Merging.cert_base_commit(certificate))
147	    first_tree_maybe : Maybe<&2, StateTree.StateTreeNode> <- History.read_tree_at(Merging.cert_first_parent(certificate))
148	    second_tree_maybe : Maybe<&2, StateTree.StateTreeNode> <- History.read_tree_at(Merging.cert_second_parent(certificate))
149	    result_tree_maybe : Maybe<&2, StateTree.StateTreeNode> <- History.load_tree_text(Merging.cert_result_tree(certificate))
150	    return decide_verify_trees(certificate, base_tree_maybe, first_tree_maybe, second_tree_maybe, result_tree_maybe)