src/Certificate.bend
ber-core-store@0.1.1.0 · 150 lines · 0 definitions
1import Base
2import ber-core-store@0.1.1.0/src/Reading.bend as Reading
3import ber-core-store@0.1.1.0/src/StateTree.bend as StateTree
4import ber-core-store@0.1.1.0/src/History.bend as History
5import ber-core-store@0.1.1.0/src/Merging.bend as Merging
6import ber-core-store@0.1.1.0/src/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.
16def 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.
24def 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.
32def 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.
40def 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.
48def 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.
52def 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.
60def 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.
68def 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.
76def 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.
84def 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.
92def 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.
100def 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.
108def 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.
112def 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.
120def 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.
128def 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.
136def 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.
144def 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)