pytact.graph_sanity_check

  1import argparse
  2from multiprocessing import Pool
  3from pathlib import Path
  4from functools import partial
  5from collections import Counter
  6import math
  7from pytact.data_reader import GlobalContextSets, lowlevel_data_reader, lowlevel_to_highlevel, Definition, Node, Original, Substituted, Discharged, node_dependencies, definition_dependencies
  8import pytact.graph_api_capnp_cython as apic
  9import capnp
 10import pytact.graph_api_capnp as graph_api_capnp
 11
 12def open_dataset(dataset_path: Path):
 13    global ctx
 14    ctx = lowlevel_data_reader(dataset_path)
 15    global data
 16    data = ctx.__enter__()
 17    global node_counts
 18    node_counts = [len(data[i].graph.nodes) for i in range(0, len(data.graph_files))]
 19    global hdata
 20    hdata = lowlevel_to_highlevel(data)
 21    global global_contexts
 22    global_contexts = GlobalContextSets.new_context().__enter__()
 23
 24# def node_dependencies(n: Node, deps: set[Definition] | None = None) -> set[Definition]:
 25#     if deps is None:
 26#         deps = set()
 27#     seen: set[Node] = set()
 28#     stack = [n]
 29#     while stack:
 30#         node = stack.pop()
 31#         if node in seen:
 32#             continue
 33#         seen.add(node)
 34#         if d := node.definition:
 35#             deps.add(d)
 36#             continue
 37#         for _, child in node.children:
 38#             stack.append(child)
 39#     return deps
 40
 41# def definition_dependencies(d: Definition):
 42#     deps = set()
 43#     for _, c in d.node.children:
 44#         node_dependencies(c, deps)
 45#     return deps
 46
 47def process1(args, fname: Path):
 48    file_errors = []
 49    file_definitions = 0
 50    file_original_definitions = 0
 51    file_base_tactics_text = set()
 52    file_base_tactics_intermtext = set()
 53    file_tactics = Counter()
 54    file_original_tactics = Counter()
 55    file_tactic_arguments = {}
 56    file_tactic_ident_to_base = {}
 57    proof_steps = 0
 58    original_proof_steps = 0
 59    original_proof_steps_faithful = 0
 60    outcomes = 0
 61    original_outcomes = 0
 62    proofs = 0
 63    original_proofs = 0
 64    original_proofs_faithful = 0
 65    unresolvable = 0
 66    file_disappearing_proof_states = 0
 67    graphid = data.graphid_by_filename[fname]
 68    freader = data[graphid]
 69    graph = freader.graph
 70    nodes_count = node_counts[graphid]
 71    edges_count = len(graph.edges)
 72    dependency_count = len(freader.dependencies)
 73    print(f"Checking file {fname}: {nodes_count} nodes and {edges_count} edges")
 74
 75    # Check correctness of Graph struct
 76    for n in graph.nodes:
 77        if not (n.children_index + n.children_count <= edges_count):
 78            file_errors.append(f"{fname}: Children of node {n} are not valid indices of Graph.edges")
 79        if n.label.is_definition:
 80            file_definitions += 1
 81
 82    for t in graph.edges:
 83        target = t.target
 84        dep_index = target.dep_index
 85        if dep_index >= dependency_count:
 86            file_errors.append(f"{fname}: target.depIndex {t.target.dep_index} "
 87                  f"but len(g.dependencies) is {dependency_count} "
 88                  f"and g.dependencies = {freader.dependencies}")
 89        if target.node_index >= node_counts[data.local_to_global(graphid, dep_index)]:
 90            file_errors.append(f"{fname}: Reference for target {t} is out of bounds")
 91
 92    # Check correctness of Dataset struct
 93    if file_definitions != len(freader.definitions):
 94        file_errors.append(f"{fname}: Counted {file_definitions} definitions in the file, "
 95                        f"but Dataset.definitions has size {len(freader.definitions)}")
 96
 97    hreader = hdata[fname]
 98    with global_contexts.sub_context(lambda d: d.is_file_representative) as sub_global_contexts:
 99        for d in hreader.definitions():
100            if not d.node.definition:
101                file_errors.append(f"{fname}: Node {d.node} should be a definition but is not")
102
103            # Check correctness of Definition struct
104            if isinstance(d.status, Original):
105                file_original_definitions += 1
106            elif isinstance(d.status, Discharged):
107                if not d.status.original.node.definition:
108                    file_errors.append(f"{fname}: Discharged node of definition {d.name} "
109                                       f"is not a definition")
110            elif isinstance(d.status, Substituted):
111                if not d.status.original.node.definition:
112                    file_errors.append(f"{fname}: Substituted node of definition {d.name} "
113                                       f"is not a definition")
114
115            def check_in_global_context(s):
116                global_context = sub_global_contexts.global_context_set(d)
117                for dd in s:
118                    if dd not in global_context:
119                        file_errors.append(f"{fname}: Definition {d.name} has dependency {dd.name} "
120                                        f"which is not part of its global context")
121
122            if not args.quick:
123                check_in_global_context(definition_dependencies(d))
124
125            crepr = d.cluster_representative
126            if d not in d.cluster:
127                file_errors.append(f"{fname}: Cluster represented by {crepr.name}"
128                                f"does not contain {d.name}")
129            for cd in d.cluster:
130                if crepr != cd.cluster_representative:
131                    file_errors.append(f"{fname}: Cluster represented by {crepr.name} contains unrelated "
132                                    f"definition {cd.name}")
133            if prev := d.previous:
134                if not prev.node.definition:
135                    file_errors.append(f"{fname}: Previous node of definition {d.name} is not a definition")
136            for ep in d.external_previous:
137                if not ep.node.definition:
138                    file_errors.append(f"{fname}: External dependency of definition {d.name} is "
139                                    f"not a definition")
140            if ps := d.proof:
141                proofs += 1
142                faithful = True
143                before_states = set()
144                for p in ps:
145                    for outcome in p.outcomes:
146                        before_states.add(outcome.before.id)
147                for p in ps:
148                    proof_steps += 1
149                    if t := p.tactic:
150                        ident = t.ident
151                        file_base_tactics_text.add(t.base_text)
152                        file_base_tactics_intermtext.add(t.interm_text)
153                    else:
154                        ident = 0
155                    file_tactics[ident] += 1
156                    if isinstance(d.status, Original):
157                        file_original_tactics[ident] += 1
158                        original_proof_steps += 1
159                        if (t := p.tactic) and t.text == t.interm_text:
160                                original_proof_steps_faithful += 1
161                        else:
162                            faithful = False
163                    for outcome in p.outcomes:
164                        for after in outcome.after:
165                            if after.id not in before_states:
166                                file_disappearing_proof_states += 1
167
168                        if not args.quick:
169                            check_in_global_context(node_dependencies(outcome.term))
170                        for state in [outcome.before] + list(outcome.after):
171                            root_label = state.root.label
172                            if not root_label.is_proof_state:
173                                file_errors.append(f"{fname}: root is proof state {state} is {root_label}")
174
175                            if not args.quick:
176                                check_in_global_context(node_dependencies(state.root))
177                            if len(state.context) != len(state.context_names):
178                                file_errors.append(f"{fname}: Length of context is different from length of"
179                                                f"context_names in proof state {state}")
180                            if len(state.context) != len(state.context_text):
181                                file_errors.append(f"{fname}: Length of context is different from length of"
182                                                f"context_text in proof state {state}")
183                            root_children = [child for _, child in state.root.children]
184                            for c in state.context:
185                                if c not in root_children:
186                                    file_errors.append(
187                                        f"{fname}: hyp {c} of state {state} in def {d.name} is not "
188                                        f"reachable from the root")
189                                if not (c.label.is_context_def or c.label.is_context_assum):
190                                    file_errors.append(
191                                        f"{fname}: ctx {state.context} of a state {state} "
192                                        f"has the wrong node classification {c.label}")
193
194                        file_tactic_arguments.setdefault(ident, len(outcome.tactic_arguments))
195                        if t := p.tactic:
196                            file_tactic_ident_to_base.setdefault(ident, t.base_text)
197                        if file_tactic_arguments[ident] != len(outcome.tactic_arguments):
198                            file_errors.append(f"{fname}: Tactic with two different argument lengths detected. : Original: {file_tactic_arguments[ident]} : {file_tactic_ident_to_base[ident]}. New {len(outcome.tactic_arguments)} : {t.text} : {t.base_text}")
199                        outcomes += 1
200                        if isinstance(d.status, Original):
201                            original_outcomes += 1
202                        for a in outcome.tactic_arguments:
203                            if not a:
204                                unresolvable += 1
205                            else:
206                                if not args.quick:
207                                    check_in_global_context(node_dependencies(a))
208                if isinstance(d.status, Original):
209                    original_proofs += 1
210                    if faithful:
211                        original_proofs_faithful += 1
212    if freader.representative != len(graph.nodes):
213        if not graph.nodes[freader.representative].label.is_definition:
214            file_errors.append(f"{fname}: Representative {freader.representative} is not a definition")
215    for dep in freader.dependencies:
216        if Path(dep) not in data.graphid_by_filename:
217            file_errors.append(f"{fname}: Dependency {dep} could not be found")
218
219
220    return (fname, nodes_count, edges_count,
221            file_definitions, file_original_definitions, file_base_tactics_text,
222            file_base_tactics_intermtext, file_tactics, file_original_tactics, file_tactic_arguments,
223            proof_steps, original_proof_steps, original_proof_steps_faithful,
224            outcomes, original_outcomes, proofs, original_proofs,
225            original_proofs_faithful, unresolvable, file_errors, file_disappearing_proof_states)
226
227def entropy(d):
228    n = sum(d.values())
229    return -sum([(c / n) * math.log(c / n, 2) for c in d.values()])
230
231def main2():
232    parser = argparse.ArgumentParser(
233        description = 'Run sanity checks on a dataset and print some statistics.',
234        formatter_class=argparse.ArgumentDefaultsHelpFormatter)
235
236    parser.add_argument('dataset',
237                        type=str,
238                        help=('The location of the dataset to check. ' +
239                              'Either a dataset directory, or a SquashFS image, ' +
240                              'which will be automatically mounted.'))
241    parser.add_argument('--jobs',
242                        type=int,
243                        default=None,
244                        help='number of parallel multiprocessing jobs to run')
245    parser.add_argument('--quick',
246                        action='store_true',
247                        help='skip the more expensive checks')
248    parser.add_argument('--verbose',
249                       type = int,
250                       default = 0,
251                       help='level of being verbose 0,1..')
252
253    args = parser.parse_args()
254
255    import sys
256    sys.setrecursionlimit(10000)
257
258    dataset_path = Path(args.dataset).resolve()
259
260    errors = []
261    tactics = Counter()
262    original_tactics = Counter()
263    tactic_arguments = {}
264    base_tactics_text = set()
265    base_tactics_intermtext = set()
266    definitions = 0
267    original_definitions = 0
268    nodes_total = 0
269    edges_total = 0
270    proof_steps_total = 0
271    original_proof_steps_total = 0
272    original_proof_steps_faithful_total = 0
273    outcomes_total = 0
274    original_outcomes_total = 0
275    proofs_total = 0
276    original_proofs_total = 0
277    original_proofs_faithful_total = 0
278    unresolvable_total = 0
279    disappearing_proof_states = 0
280
281    with lowlevel_data_reader(dataset_path) as data:
282        file_list = data.graph_files
283
284    process1_partial = partial(process1, args)
285    with Pool(args.jobs, open_dataset, [dataset_path]) as pool:
286        results = pool.map(process1_partial, file_list, chunksize=1)
287    # file_list = file_list[280:360]
288    # print(file_list)
289    # open_dataset(dataset_path)
290    # results = [process1(args, f) for f in file_list]
291
292    for res in results:
293        (fname, nodes_count, edges_count,
294         file_definitions, file_original_definitions, file_base_tactics_text,
295         file_base_tactics_intermtext, file_tactics, file_original_tactics, file_tactic_arguments,
296         proof_steps, original_proof_steps, original_proof_steps_faithful,
297         outcomes, original_outcomes, proofs, original_proofs,
298         original_proofs_faithful, unresolvable, file_errors, file_disappearing_proof_states) = res
299        nodes_total += nodes_count
300        edges_total += edges_count
301        proof_steps_total += proof_steps
302        original_proof_steps_total += original_proof_steps
303        original_proof_steps_faithful_total += original_proof_steps_faithful
304        outcomes_total += outcomes
305        original_outcomes_total += original_outcomes
306        proofs_total += proofs
307        original_proofs_total += original_proofs
308        original_proofs_faithful_total += original_proofs_faithful
309        definitions +=  file_definitions
310        original_definitions += file_original_definitions
311        base_tactics_text.update(file_base_tactics_text)
312        base_tactics_intermtext.update(file_base_tactics_intermtext)
313        tactics += file_tactics
314        original_tactics += file_original_tactics
315        disappearing_proof_states += file_disappearing_proof_states
316        errors += file_errors
317        for tac, length in file_tactic_arguments.items():
318            tactic_arguments.setdefault(tac, length)
319            if tactic_arguments[tac] != length:
320                errors.append(f'{fname}: Tactic with two different argument lengths detected: {tac}')
321
322        unresolvable_total += unresolvable
323
324    for error in errors:
325        print(error)
326
327    print(f"Errors encountered {len(errors)}")
328    print(f"Nodes total {nodes_total}")
329    print(f"Edges total {edges_total}")
330    print(f"Tactics total {len(tactics)}")
331    print(f"Original tactics total {len(original_tactics)}")
332    print(f"Tactics entropy (bits) {entropy(tactics)}")
333    print(f"Original tactics entropy (bits) {entropy(original_tactics)}")
334    print(f"Tactics base text total {len(base_tactics_text)}")
335    print(f"Tactics base intermtext total {len(base_tactics_intermtext)}")
336    print(f"Definitions total {definitions}")
337    print(f"Original definitions total {original_definitions}")
338    print(f"Proof steps total {proof_steps_total}")
339    print(f"Original proof steps total {original_proof_steps_total}")
340    print(f"Faithfully represented original proof steps total {original_proof_steps_faithful_total}")
341    print(f"Outcomes total {outcomes_total}")
342    print(f"Original outcomes total {original_outcomes_total}")
343    print(f"Proofs total {proofs_total}")
344    print(f"Original proofs total {original_proofs_total}")
345    print(f"Faithful original proofs total {original_proofs_faithful_total}")
346    print(f"Unresolvable tactic arguments {unresolvable_total}")
347    print(f"Disappearing proof states (spooky action at a distance) {disappearing_proof_states}")
348
349    if (args.verbose >= 1):
350        print("Tactics base text:")
351        for t in base_tactics_text:
352            print(t)
353        print("Tactics intermtext text:")
354        for t in base_tactics_intermtext:
355            print(t)
356
357    if len(errors) > 0:
358        raise Exception("Errors occurred")
359
360def main():
361    # import pstats, cProfile
362    # cProfile.runctx("main2()", globals(), locals(), "Profile.prof")
363    # s = pstats.Stats("Profile.prof")
364    # s.strip_dirs().sort_stats("time").print_stats()
365    main2()
366
367if __name__ == '__main__':
368    main()