Skip to content

Commit b21e56d

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
feat: add extraction scripts for HOL4, HOL Light, SMT-LIB, and TPTP
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 59b598b commit b21e56d

7 files changed

Lines changed: 2295 additions & 0 deletions

File tree

‎scripts/extract_acl2.py‎

Lines changed: 301 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,301 @@
1+
#!/usr/bin/env python3
2+
# SPDX-FileCopyrightText: 2026 ECHIDNA Project Team
3+
# SPDX-License-Identifier: PMPL-1.0-or-later
4+
5+
"""
6+
Extract proofs from ACL2 community books and convert to ECHIDNA training format.
7+
8+
Attempts to download from the ACL2 GitHub repository (books/ directory).
9+
Falls back to generating high-quality synthetic ACL2 proofs from standard
10+
patterns (defthm, defun, verify-guards).
11+
12+
ACL2 (A Computational Logic for Applicative Common Lisp) is an industrial-
13+
strength theorem prover used for hardware and software verification (e.g.
14+
AMD floating-point division, JVM bytecode verification).
15+
16+
Output: training_data/proof_states_acl2.jsonl
17+
ID range: 92000+
18+
"""
19+
20+
import json
21+
import os
22+
import re
23+
import urllib.request
24+
import urllib.error
25+
from typing import Dict, List, Any, Tuple
26+
27+
REPO_ROOT = os.path.dirname(os.path.dirname(os.path.abspath(__file__)))
28+
EXTERNAL_DIR = os.path.join(REPO_ROOT, "external_corpora", "acl2")
29+
OUTPUT_DIR = os.path.join(REPO_ROOT, "training_data")
30+
OUTPUT_FILE = os.path.join(OUTPUT_DIR, "proof_states_acl2.jsonl")
31+
STATS_FILE = os.path.join(OUTPUT_DIR, "stats_acl2.json")
32+
START_ID = 92000
33+
34+
ACL2_RAW_BASE = "https://raw.githubusercontent.com/acl2/acl2/master"
35+
ACL2_FILES = [
36+
"books/arithmetic/top.lisp",
37+
"books/arithmetic-5/top.lisp",
38+
"books/std/lists/top.lisp",
39+
"books/std/lists/append.lisp",
40+
"books/std/lists/rev.lisp",
41+
"books/std/lists/nth.lisp",
42+
"books/std/lists/len.lisp",
43+
"books/std/alists/top.lisp",
44+
"books/ihs/ihs-definitions.lisp",
45+
"books/ihs/logops-lemmas.lisp",
46+
"books/data-structures/list-theory.lisp",
47+
"books/sorting/msort.lisp",
48+
"books/sorting/isort.lisp",
49+
"books/arithmetic/natp-posp.lisp",
50+
]
51+
52+
53+
def parse_acl2_file(filepath: str) -> List[Dict[str, Any]]:
54+
"""
55+
Parse an ACL2 .lisp file and extract defthm and defun forms.
56+
57+
ACL2 proofs look like:
58+
(defthm theorem-name
59+
body
60+
:hints (("Goal" :in-theory (enable ...))))
61+
"""
62+
results = []
63+
try:
64+
with open(filepath, "r", encoding="utf-8", errors="replace") as fh:
65+
content = fh.read()
66+
except OSError:
67+
return results
68+
69+
# Extract defthm forms
70+
# Match balanced parens is hard; use a simpler heuristic
71+
pattern_thm = re.compile(
72+
r'\(defthm\s+(\S+)\s+(.*?)(?=\n\s*\(def|\n\s*\(in-theory|\n\s*\(include-book|\Z)',
73+
re.DOTALL
74+
)
75+
for m in pattern_thm.finditer(content):
76+
name = m.group(1).strip()
77+
body = m.group(2).strip()
78+
# Clean up body
79+
body_clean = re.sub(r'\s+', ' ', body)[:300]
80+
81+
# Extract hints
82+
hints_match = re.search(r':hints\s*\((.*?)\)', body, re.DOTALL)
83+
hints = []
84+
if hints_match:
85+
hint_text = hints_match.group(1)
86+
hints = re.findall(r':(\w+)', hint_text)
87+
88+
# Extract rule classes
89+
rules_match = re.search(r':rule-classes\s+(\S+)', body)
90+
rule_class = rules_match.group(1) if rules_match else "rewrite"
91+
92+
results.append({
93+
"theorem": name,
94+
"goal": body_clean,
95+
"hints": hints,
96+
"rule_class": rule_class,
97+
"source": f"acl2/{os.path.basename(filepath)}",
98+
})
99+
100+
return results
101+
102+
103+
def download_acl2_files() -> int:
104+
"""Attempt to download ACL2 community book files."""
105+
downloaded = 0
106+
for rel_path in ACL2_FILES:
107+
url = f"{ACL2_RAW_BASE}/{rel_path}"
108+
local_path = os.path.join(EXTERNAL_DIR, os.path.basename(rel_path))
109+
if os.path.exists(local_path):
110+
downloaded += 1
111+
continue
112+
try:
113+
req = urllib.request.Request(url, headers={"User-Agent": "ECHIDNA/1.5"})
114+
with urllib.request.urlopen(req, timeout=15) as resp:
115+
data = resp.read()
116+
with open(local_path, "wb") as fh:
117+
fh.write(data)
118+
downloaded += 1
119+
print(f" Downloaded: {rel_path}")
120+
except (urllib.error.URLError, OSError, TimeoutError) as exc:
121+
print(f" Skipped {rel_path}: {exc}")
122+
return downloaded
123+
124+
125+
def generate_synthetic_acl2() -> List[Dict[str, Any]]:
126+
"""
127+
Generate high-quality synthetic ACL2 proofs.
128+
129+
ACL2 proofs use a unique waterfall architecture: simplification,
130+
destructor elimination, cross-fertilization, generalization, and
131+
induction. Hints guide the prover.
132+
"""
133+
arithmetic = [
134+
("commutativity-of-+", "(equal (+ x y) (+ y x))", ":rule-classes :rewrite"),
135+
("associativity-of-+", "(equal (+ (+ x y) z) (+ x (+ y z)))", ":rule-classes :rewrite"),
136+
("commutativity-of-*", "(equal (* x y) (* y x))", ":rule-classes :rewrite"),
137+
("associativity-of-*", "(equal (* (* x y) z) (* x (* y z)))", ":rule-classes :rewrite"),
138+
("distributivity-of-*-over-+", "(equal (* x (+ y z)) (+ (* x y) (* x z)))", ":rule-classes :rewrite"),
139+
("right-identity-of-+", "(equal (+ x 0) x)", ":rule-classes :rewrite"),
140+
("left-identity-of-*", "(equal (* 1 x) x)", ":rule-classes :rewrite"),
141+
("right-cancellation-for-+", "(implies (equal (+ a x) (+ b x)) (equal a b))", ':hints (("Goal" :use (:instance cancel-common)))'),
142+
("natp-+", "(implies (and (natp x) (natp y)) (natp (+ x y)))", ':hints (("Goal" :in-theory (enable natp)))'),
143+
("natp-*", "(implies (and (natp x) (natp y)) (natp (* x y)))", ':hints (("Goal" :in-theory (enable natp)))'),
144+
("posp-implies-natp", "(implies (posp x) (natp x))", ':hints (("Goal" :in-theory (enable posp natp)))'),
145+
("<=-reflexive", "(implies (natp x) (<= x x))", ":rule-classes :rewrite"),
146+
("<=-transitive", "(implies (and (<= x y) (<= y z)) (<= x z))", ':hints (("Goal" :use (:instance transitivity-of-<=)))'),
147+
("<=-antisymmetric", "(implies (and (<= x y) (<= y x)) (equal x y))", ':hints (("Goal" :use (:instance antisymmetry-of-<=)))'),
148+
("floor-bounds", "(implies (and (natp x) (posp y)) (and (<= (* y (floor x y)) x) (< x (* y (+ 1 (floor x y))))))", ':hints (("Goal" :in-theory (enable floor)))'),
149+
("mod-bounds", "(implies (and (natp x) (posp y)) (< (mod x y) y))", ':hints (("Goal" :in-theory (enable mod)))'),
150+
("mod-+-cancel", "(implies (and (natp a) (natp b) (posp n)) (equal (mod (+ a (mod b n)) n) (mod (+ a b) n)))", ':hints (("Goal" :in-theory (enable mod)))'),
151+
("expt-+", "(implies (and (natp m) (natp n)) (equal (expt b (+ m n)) (* (expt b m) (expt b n))))", ':hints (("Goal" :induct (expt b m)))'),
152+
("evenp-+-2", "(implies (evenp x) (evenp (+ 2 x)))", ':hints (("Goal" :in-theory (enable evenp)))'),
153+
("oddp-+-2", "(implies (oddp x) (oddp (+ 2 x)))", ':hints (("Goal" :in-theory (enable oddp)))'),
154+
]
155+
156+
lists = [
157+
("true-listp-append", "(implies (true-listp x) (true-listp (append x y)))", ':hints (("Goal" :induct (true-listp x)))'),
158+
("append-nil", "(implies (true-listp x) (equal (append x nil) x))", ':hints (("Goal" :induct (true-listp x)))'),
159+
("associativity-of-append", "(equal (append (append x y) z) (append x (append y z)))", ':hints (("Goal" :induct (true-listp x)))'),
160+
("len-append", "(equal (len (append x y)) (+ (len x) (len y)))", ':hints (("Goal" :induct (true-listp x)))'),
161+
("len-revappend", "(equal (len (revappend x y)) (+ (len x) (len y)))", ':hints (("Goal" :induct (revappend x y)))'),
162+
("revappend-revappend", "(equal (revappend (revappend x y) z) (revappend y (append x z)))", ':hints (("Goal" :induct (revappend x y)))'),
163+
("reverse-reverse", "(implies (true-listp x) (equal (reverse (reverse x)) x))", ':hints (("Goal" :in-theory (enable reverse)))'),
164+
("member-append", "(iff (member a (append x y)) (or (member a x) (member a y)))", ':hints (("Goal" :induct (true-listp x)))'),
165+
("nth-of-append", "(implies (< (nfix n) (len x)) (equal (nth n (append x y)) (nth n x)))", ':hints (("Goal" :induct (nth n x)))'),
166+
("car-cons", "(equal (car (cons x y)) x)", ":rule-classes :rewrite"),
167+
("cdr-cons", "(equal (cdr (cons x y)) y)", ":rule-classes :rewrite"),
168+
("cons-car-cdr", "(implies (consp x) (equal (cons (car x) (cdr x)) x))", ":rule-classes :rewrite"),
169+
("len-nonnegative", "(<= 0 (len x))", ":rule-classes :type-prescription"),
170+
("true-listp-revappend", "(implies (true-listp y) (true-listp (revappend x y)))", ':hints (("Goal" :induct (revappend x y)))'),
171+
("nthcdr-of-append", "(implies (<= (nfix n) (len x)) (equal (nthcdr n (append x y)) (append (nthcdr n x) y)))", ':hints (("Goal" :induct (nthcdr n x)))'),
172+
]
173+
174+
alists = [
175+
("alistp-acons", "(implies (alistp a) (alistp (acons key val a)))", ':hints (("Goal" :in-theory (enable acons alistp)))'),
176+
("assoc-of-acons", "(equal (assoc-equal key (acons key val a)) (cons key val))", ':hints (("Goal" :in-theory (enable acons assoc-equal)))'),
177+
("assoc-of-acons-diff", "(implies (not (equal k1 k2)) (equal (assoc-equal k1 (acons k2 v a)) (assoc-equal k1 a)))", ':hints (("Goal" :in-theory (enable acons assoc-equal)))'),
178+
("strip-cars-acons", "(equal (strip-cars (acons key val a)) (cons key (strip-cars a)))", ':hints (("Goal" :in-theory (enable acons strip-cars)))'),
179+
("strip-cdrs-acons", "(equal (strip-cdrs (acons key val a)) (cons val (strip-cdrs a)))", ':hints (("Goal" :in-theory (enable acons strip-cdrs)))'),
180+
]
181+
182+
bitvectors = [
183+
("logand-self", "(equal (logand x x) x)", ':hints (("Goal" :in-theory (enable logand)))'),
184+
("logand-0", "(equal (logand x 0) 0)", ':hints (("Goal" :in-theory (enable logand)))'),
185+
("logior-self", "(equal (logior x x) x)", ':hints (("Goal" :in-theory (enable logior)))'),
186+
("logior-0", "(equal (logior x 0) x)", ':hints (("Goal" :in-theory (enable logior)))'),
187+
("logxor-self", "(equal (logxor x x) 0)", ':hints (("Goal" :in-theory (enable logxor)))'),
188+
("logxor-0", "(equal (logxor x 0) x)", ':hints (("Goal" :in-theory (enable logxor)))'),
189+
("lognot-lognot", "(implies (integerp x) (equal (lognot (lognot x)) x))", ':hints (("Goal" :in-theory (enable lognot)))'),
190+
("logand-comm", "(equal (logand x y) (logand y x))", ':hints (("Goal" :in-theory (enable logand)))'),
191+
("logior-comm", "(equal (logior x y) (logior y x))", ':hints (("Goal" :in-theory (enable logior)))'),
192+
("logxor-comm", "(equal (logxor x y) (logxor y x))", ':hints (("Goal" :in-theory (enable logxor)))'),
193+
("ash-0", "(equal (ash x 0) (ifix x))", ':hints (("Goal" :in-theory (enable ash)))'),
194+
("logbitp-of-logand", "(equal (logbitp n (logand x y)) (and (logbitp n x) (logbitp n y)))", ':hints (("Goal" :in-theory (enable logbitp logand)))'),
195+
("unsigned-byte-p-of-logand", "(implies (or (unsigned-byte-p n x) (unsigned-byte-p n y)) (unsigned-byte-p n (logand x y)))", ':hints (("Goal" :in-theory (enable unsigned-byte-p logand)))'),
196+
]
197+
198+
sorting_search = [
199+
("orderedp-merge", "(implies (and (orderedp x) (orderedp y)) (orderedp (merge-lists x y)))", ':hints (("Goal" :induct (merge-lists x y)))'),
200+
("perm-merge", "(perm (append x y) (merge-lists x y))", ':hints (("Goal" :induct (merge-lists x y)))'),
201+
("orderedp-msort", "(orderedp (msort x))", ':hints (("Goal" :induct (msort x)))'),
202+
("perm-msort", "(perm x (msort x))", ':hints (("Goal" :induct (msort x)))'),
203+
("orderedp-isort", "(orderedp (isort x))", ':hints (("Goal" :induct (isort x)))'),
204+
("perm-isort", "(perm x (isort x))", ':hints (("Goal" :induct (isort x)))'),
205+
("member-of-sorted", "(implies (and (orderedp x) (member a x) (member b x) (<= a b)) (member b (cdr (member a x))))", ':hints (("Goal" :induct (member a x)))'),
206+
("bsearch-correct", "(implies (and (orderedp arr) (member key arr)) (equal (nth (bsearch key arr) arr) key))", ':hints (("Goal" :in-theory (enable bsearch)))'),
207+
]
208+
209+
all_categories = [
210+
("arithmetic", arithmetic),
211+
("lists", lists),
212+
("alists", alists),
213+
("bitvectors", bitvectors),
214+
("sorting_search", sorting_search),
215+
]
216+
217+
proofs = []
218+
for category, theorems in all_categories:
219+
for name, goal, hints in theorems:
220+
hint_keywords = re.findall(r':(\w+)', hints)
221+
proofs.append({
222+
"theorem": name,
223+
"goal": f"(defthm {name} {goal})",
224+
"tactic_proof": f"(defthm {name} {goal} {hints})",
225+
"tactics": list(dict.fromkeys(hint_keywords))[:20],
226+
"source": f"acl2_synthetic/{category}",
227+
})
228+
return proofs
229+
230+
231+
def run() -> Tuple[int, int]:
232+
"""Run the full extraction pipeline."""
233+
os.makedirs(OUTPUT_DIR, exist_ok=True)
234+
os.makedirs(EXTERNAL_DIR, exist_ok=True)
235+
236+
all_entries: List[Dict[str, Any]] = []
237+
extracted_count = 0
238+
239+
print("[ACL2] Phase 1: Attempting to download from GitHub ...")
240+
downloaded = download_acl2_files()
241+
print(f" Downloaded/cached {downloaded} files")
242+
243+
for fname in os.listdir(EXTERNAL_DIR):
244+
if fname.endswith(".lisp"):
245+
fpath = os.path.join(EXTERNAL_DIR, fname)
246+
parsed = parse_acl2_file(fpath)
247+
for entry in parsed:
248+
all_entries.append(entry)
249+
if parsed:
250+
print(f" Parsed {len(parsed)} theorems from {fname}")
251+
extracted_count = len(all_entries)
252+
253+
print(f"[ACL2] Phase 2: Generating synthetic proofs ...")
254+
synthetic = generate_synthetic_acl2()
255+
existing_names = {e["theorem"] for e in all_entries}
256+
added = 0
257+
for entry in synthetic:
258+
if entry["theorem"] not in existing_names:
259+
all_entries.append(entry)
260+
existing_names.add(entry["theorem"])
261+
added += 1
262+
print(f" Generated {added} unique synthetic proofs")
263+
264+
current_id = START_ID
265+
output_records = []
266+
for entry in all_entries:
267+
record = {
268+
"id": current_id,
269+
"prover": "ACL2",
270+
"theorem": entry["theorem"],
271+
"goal": entry["goal"],
272+
"context": entry.get("tactics", entry.get("hints", [])),
273+
"tactic_proof": entry.get("tactic_proof", ""),
274+
"source": entry.get("source", "acl2"),
275+
}
276+
output_records.append(record)
277+
current_id += 1
278+
279+
with open(OUTPUT_FILE, "w", encoding="utf-8") as fh:
280+
for rec in output_records:
281+
fh.write(json.dumps(rec, ensure_ascii=False) + "\n")
282+
283+
stats = {
284+
"prover": "ACL2",
285+
"total_proofs": len(output_records),
286+
"extracted_from_source": extracted_count,
287+
"synthetic_added": len(output_records) - extracted_count,
288+
"id_range": [START_ID, current_id - 1],
289+
"output_file": OUTPUT_FILE,
290+
}
291+
with open(STATS_FILE, "w", encoding="utf-8") as fh:
292+
json.dump(stats, fh, indent=2)
293+
294+
print(f"\n[ACL2] COMPLETE: {len(output_records)} proofs written to {OUTPUT_FILE}")
295+
print(f" Extracted from source: {extracted_count}")
296+
print(f" Synthetic: {len(output_records) - extracted_count}")
297+
return extracted_count, len(output_records) - extracted_count
298+
299+
300+
if __name__ == "__main__":
301+
run()

0 commit comments

Comments
 (0)