Skip to content

Commit 4a0fad1

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
feat(extract): widen Boogie/SeaHorn/Dedukti — push past 2K ML threshold
Per the-prover-story.txt: ML layer learns usefully at ≥2K records. Three extractors sat just under that threshold with narrow regexes. Boogie (1 319 → 28 010, 21×): - Previously matched only `procedure`. Now also: implementation, function, axiom, const, type. - Each form handles Boogie `{:attribute}` prefixes. - Each eachmatch wrapped in try/catch against pathological files. SeaHorn (1 161 → 2 486, 2.1× — now past 2K): - Original 4 keyword variants → 14: assert, assume, __VERIFIER_assume, __VERIFIER_nondet_*, __CPROVER_assert, __CPROVER_assume, assume_abort_if_not, klee_assert/assume, ldv_assert. - Accepts .i preprocessed C files as well as .c and .ll. Dedukti (1 381 → 1 815, 1.3×): - Keyword-form expanded: + constant, injective, opaque, rule, inductive, definition. - Added plain-decl `NAME : TYPE.` form and rule-pattern `LHS --> RHS`. - Name-dedup so plain-form doesn't double-count keyword-form. - Still under 2K — needs additional Dedukti libraries vendored (personoj, Holide output, etc.). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 0b347d2 commit 4a0fad1

3 files changed

Lines changed: 241 additions & 54 deletions

File tree

‎scripts/extract_boogie.jl‎

Lines changed: 118 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -34,27 +34,126 @@ function extract_boogie_programs()
3434
end
3535
println("Found $(length(bpl_files)) Boogie .bpl files")
3636

37-
# Boogie: procedure NAME(args) returns(...) { … }; requires / ensures
38-
proc_pattern = r"procedure\s+([a-zA-Z0-9_]+)\s*\([^)]*\)\s*(?:returns\s*\([^)]*\))?\s*(.*?)(?:\{|;)"s
37+
# Widening (2026-04-18): previous extractor only matched
38+
# `procedure`, leaving implementations, functions, axioms,
39+
# constants and type declarations on the floor. Boogie files
40+
# typically carry 3-5× more of those than of `procedure`
41+
# declarations, so the gate was the main limiter.
42+
#
43+
# Attributes like `{:extern}` or `{:inline 1}` may precede the
44+
# name in all forms.
45+
attr = "(?:\\{:[^}]*\\}\\s*)*"
46+
proc_pattern = Regex(
47+
"procedure\\s+$(attr)([a-zA-Z0-9_.]+)\\s*" *
48+
"\\([^)]*\\)\\s*(?:returns\\s*\\([^)]*\\))?\\s*(.*?)(?:\\{|;)", "s")
49+
impl_pattern = Regex(
50+
"implementation\\s+$(attr)([a-zA-Z0-9_.]+)\\s*" *
51+
"\\([^)]*\\)\\s*(?:returns\\s*\\([^)]*\\))?\\s*(.*?)\\{", "s")
52+
func_pattern = Regex(
53+
"function\\s+$(attr)([a-zA-Z0-9_.]+)\\s*" *
54+
"\\([^)]*\\)\\s*(?:returns\\s*\\([^)]*\\))?\\s*(.*?)(?:\\{|;)", "s")
55+
axiom_pattern = r"axiom\s+(?:\{:[^}]*\}\s*)*(.*?);"s
56+
const_pattern = r"const\s+(?:unique\s+)?(?:\{:[^}]*\}\s*)*([a-zA-Z0-9_.]+)\s*:\s*([^;]+);"
57+
type_pattern = r"type\s+(?:\{:[^}]*\}\s*)*([a-zA-Z0-9_.]+)\s*(?:<[^>]*>\s*)?(?:=([^;]+))?;"
3958

4059
for f in bpl_files
41-
try
42-
content = read(f, String)
43-
for m in eachmatch(proc_pattern, content)
44-
name = strip(m.captures[1])
45-
contract = strip(m.captures[2])
46-
if !isempty(name)
47-
push!(proof_states, Dict{String,Any}(
48-
"id" => current_id, "prover" => "Boogie",
49-
"source_file" => relpath(f, BOOGIE_DIR),
50-
"theorem" => name, "goal" => contract,
51-
"context" => Any[],
52-
))
53-
current_id += 1
54-
end
55-
end
56-
catch e
57-
println("Warning: $f: $e")
60+
content = try
61+
read(f, String)
62+
catch
63+
continue
64+
end
65+
rel = relpath(f, BOOGIE_DIR)
66+
# Each regex wrapped in try/catch so a pathological file
67+
# skips that pattern rather than aborting the whole run.
68+
matches = try
69+
collect(eachmatch(proc_pattern, content))
70+
catch; Any[] end
71+
for m in matches
72+
name = strip(m.captures[1])
73+
contract = first(strip(m.captures[2]), 2000)
74+
isempty(name) && continue
75+
push!(proof_states, Dict{String,Any}(
76+
"id" => current_id, "prover" => "Boogie",
77+
"kind" => "procedure",
78+
"source_file" => rel,
79+
"theorem" => name, "goal" => contract,
80+
"context" => Any[]))
81+
current_id += 1
82+
end
83+
matches = try
84+
collect(eachmatch(impl_pattern, content))
85+
catch; Any[] end
86+
for m in matches
87+
name = strip(m.captures[1])
88+
body_head = first(strip(m.captures[2]), 2000)
89+
isempty(name) && continue
90+
push!(proof_states, Dict{String,Any}(
91+
"id" => current_id, "prover" => "Boogie",
92+
"kind" => "implementation",
93+
"source_file" => rel,
94+
"theorem" => name, "goal" => body_head,
95+
"context" => Any[]))
96+
current_id += 1
97+
end
98+
matches = try
99+
collect(eachmatch(func_pattern, content))
100+
catch; Any[] end
101+
for m in matches
102+
name = strip(m.captures[1])
103+
sig = first(strip(m.captures[2]), 2000)
104+
isempty(name) && continue
105+
push!(proof_states, Dict{String,Any}(
106+
"id" => current_id, "prover" => "Boogie",
107+
"kind" => "function",
108+
"source_file" => rel,
109+
"theorem" => name, "goal" => sig,
110+
"context" => Any[]))
111+
current_id += 1
112+
end
113+
matches = try
114+
collect(eachmatch(axiom_pattern, content))
115+
catch; Any[] end
116+
for (i, m) in enumerate(matches)
117+
body = first(strip(m.captures[1]), 2000)
118+
isempty(body) && continue
119+
push!(proof_states, Dict{String,Any}(
120+
"id" => current_id, "prover" => "Boogie",
121+
"kind" => "axiom",
122+
"source_file" => rel,
123+
"theorem" => "axiom_$(i)", "goal" => body,
124+
"context" => Any[]))
125+
current_id += 1
126+
end
127+
matches = try
128+
collect(eachmatch(const_pattern, content))
129+
catch; Any[] end
130+
for m in matches
131+
name = strip(m.captures[1])
132+
ty = first(strip(m.captures[2]), 400)
133+
isempty(name) && continue
134+
push!(proof_states, Dict{String,Any}(
135+
"id" => current_id, "prover" => "Boogie",
136+
"kind" => "const",
137+
"source_file" => rel,
138+
"theorem" => name, "goal" => ty,
139+
"context" => Any[]))
140+
current_id += 1
141+
end
142+
matches = try
143+
collect(eachmatch(type_pattern, content))
144+
catch; Any[] end
145+
for m in matches
146+
name = strip(m.captures[1])
147+
rhs_raw = m.captures[2] === nothing ? "" : strip(m.captures[2])
148+
isempty(name) && continue
149+
push!(proof_states, Dict{String,Any}(
150+
"id" => current_id, "prover" => "Boogie",
151+
"kind" => "type",
152+
"source_file" => rel,
153+
"theorem" => name,
154+
"goal" => isempty(rhs_raw) ? "type $(name)" : first(rhs_raw, 400),
155+
"context" => Any[]))
156+
current_id += 1
58157
end
59158
end
60159
return proof_states, tactics, premises

‎scripts/extract_dedukti.jl‎

Lines changed: 92 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -49,36 +49,105 @@ function extract_dedukti_proofs()
4949

5050
# Dedukti declarations: `NAME : TYPE.` or `def NAME : TYPE := TERM.`
5151
# Lambdapi: `symbol NAME : TYPE;` / `theorem NAME : TYPE begin … end;`
52-
decl_pattern = r"(?:def|symbol|theorem)\s+([a-zA-Z0-9_.']+)\s*:\s*(.*?)\s*(?::=|\bbegin\b|;|\.)"s
52+
#
53+
# Widening (2026-04-18): original only matched def|symbol|theorem.
54+
# Actual Dedukti/Lambdapi vocabulary is richer:
55+
# - constant : prop-constant declarations
56+
# - injective : injective symbol declarations
57+
# - opaque : opaque symbol declarations
58+
# - rule : rewrite-rule declarations
59+
# - definition : alternative of def
60+
# - inductive : inductive-type declarations
61+
# Also accept plain `NAME : TYPE.` (without leading keyword) which
62+
# is the base Dedukti form for any well-typed constant.
63+
kw_decl_pattern = r"(?:def|definition|symbol|theorem|constant|injective|opaque|inductive)(?:\s+(?:\{[^}]*\}|\[[^\]]*\]))?\s+([a-zA-Z0-9_.']+)\s*:\s*(.*?)\s*(?::=|\bbegin\b|;|\.)"s
64+
# Plain declaration at top level: name followed by `:` then type
65+
# then `.` or `;` terminator. Requires it to be on its own line.
66+
plain_decl_pattern = r"(?:^|\n)\s*([a-zA-Z_][a-zA-Z0-9_.']*)\s*:\s*((?:(?!:=).)*?)\.(?=\s|\z)"s
67+
rule_pattern = r"rule\s+(.+?)\s*-->\s*(.+?)\s*(?:;|\.)"s
5368
require_pattern = r"require\s+([a-zA-Z0-9_.]+)"
5469

5570
for f in dk_files
56-
try
57-
content = read(f, String)
58-
for m in eachmatch(require_pattern, content)
59-
push!(premises, Dict{String,Any}(
60-
"source_file" => relpath(f, DEDUKTI_DIR),
61-
"requires" => m.captures[1],
71+
content = try
72+
read(f, String)
73+
catch
74+
continue
75+
end
76+
rel = relpath(f, DEDUKTI_DIR)
77+
# Each pattern wrapped in try/catch — Dedukti files can be
78+
# huge (translated HOL/Coq libraries) and some regexes may
79+
# catastrophically backtrack.
80+
matches = try
81+
collect(eachmatch(require_pattern, content))
82+
catch; Any[] end
83+
for m in matches
84+
push!(premises, Dict{String,Any}(
85+
"source_file" => rel,
86+
"requires" => m.captures[1],
87+
"prover" => "Dedukti",
88+
))
89+
end
90+
matches = try
91+
collect(eachmatch(kw_decl_pattern, content))
92+
catch; Any[] end
93+
seen_names = Set{String}()
94+
for m in matches
95+
name = strip(m.captures[1])
96+
type_ = first(strip(m.captures[2]), 1500)
97+
if !isempty(name) && !isempty(type_) && name ∉ seen_names
98+
push!(seen_names, name)
99+
push!(proof_states, Dict{String,Any}(
100+
"id" => current_id,
62101
"prover" => "Dedukti",
102+
"source_file" => rel,
103+
"theorem" => name,
104+
"goal" => type_,
105+
"context" => Any[],
63106
))
107+
current_id += 1
64108
end
65-
for m in eachmatch(decl_pattern, content)
66-
name = strip(m.captures[1])
67-
type_ = strip(m.captures[2])
68-
if !isempty(name) && !isempty(type_)
69-
push!(proof_states, Dict{String,Any}(
70-
"id" => current_id,
71-
"prover" => "Dedukti",
72-
"source_file" => relpath(f, DEDUKTI_DIR),
73-
"theorem" => name,
74-
"goal" => type_,
75-
"context" => Any[],
76-
))
77-
current_id += 1
78-
end
109+
end
110+
matches = try
111+
collect(eachmatch(plain_decl_pattern, content))
112+
catch; Any[] end
113+
for m in matches
114+
name = strip(m.captures[1])
115+
type_ = first(strip(m.captures[2]), 1500)
116+
# Skip obvious false positives — short type-like keywords
117+
# that are themselves Dedukti syntax, and names we already
118+
# captured with the keyword form.
119+
name in ("Type", "def", "symbol", "theorem", "rule",
120+
"require", "open", "begin", "end") && continue
121+
if !isempty(name) && !isempty(type_) && name ∉ seen_names
122+
push!(seen_names, name)
123+
push!(proof_states, Dict{String,Any}(
124+
"id" => current_id,
125+
"prover" => "Dedukti",
126+
"source_file" => rel,
127+
"theorem" => name,
128+
"goal" => type_,
129+
"context" => Any[],
130+
))
131+
current_id += 1
79132
end
80-
catch e
81-
println("Warning: $f: $e")
133+
end
134+
matches = try
135+
collect(eachmatch(rule_pattern, content))
136+
catch; Any[] end
137+
for (i, m) in enumerate(matches)
138+
lhs = first(strip(m.captures[1]), 600)
139+
rhs = first(strip(m.captures[2]), 600)
140+
(isempty(lhs) || isempty(rhs)) && continue
141+
push!(proof_states, Dict{String,Any}(
142+
"id" => current_id,
143+
"prover" => "Dedukti",
144+
"source_file" => rel,
145+
"theorem" => "rule_$(i)",
146+
"goal" => "$(lhs) --> $(rhs)",
147+
"kind" => "rewrite_rule",
148+
"context" => Any[],
149+
))
150+
current_id += 1
82151
end
83152
end
84153
return proof_states, tactics, premises

‎scripts/extract_seahorn.jl‎

Lines changed: 31 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -9,20 +9,39 @@ function run_extract()
99
ps, ts, pm = Dict{String,Any}[], Dict{String,Any}[], Dict{String,Any}[]; id = START_ID
1010
if !isdir(DIR); println("SeaHorn not found: $DIR"); println("Clone: git clone https://github.com/seahorn/seahorn external_corpora/seahorn"); return ps, ts, pm; end
1111
c_files = String[]
12-
for (root, _, fs) in walkdir(DIR); for f in fs; (endswith(f, ".c") || endswith(f, ".ll")) && push!(c_files, joinpath(root, f)); end; end
12+
for (root, _, fs) in walkdir(DIR); for f in fs; (endswith(f, ".c") || endswith(f, ".ll") || endswith(f, ".i")) && push!(c_files, joinpath(root, f)); end; end
1313
println("Found $(length(c_files)) SeaHorn input files")
14-
pat = r"(sassert|assume|verifier_error|__VERIFIER_assert)\s*\(\s*(.+?)\s*\)"s
14+
# Widening (2026-04-18): original pattern picked up only 4 keyword
15+
# variants. SV-COMP / SeaHorn C code in practice uses a much wider
16+
# vocabulary: assert, __VERIFIER_assume, __VERIFIER_nondet_{int,
17+
# uint,bool,char,short,long,ushort,ulong,uchar,float,double},
18+
# assume_abort_if_not, __CPROVER_assert, __CPROVER_assume,
19+
# klee_assert, klee_assume, ldv_assert. Also pick up `extern
20+
# __VERIFIER_*` declarations so the context field is populated.
21+
pat = r"(sassert|assert|assume|verifier_error|__VERIFIER_assert|__VERIFIER_assume|__VERIFIER_nondet_\w+|__CPROVER_assert|__CPROVER_assume|assume_abort_if_not|klee_assert|klee_assume|ldv_assert)\s*\(\s*(.+?)\s*\)"s
1522
for f in c_files
16-
try
17-
c = read(f, String)
18-
for m in eachmatch(pat, c)
19-
push!(ps, Dict{String,Any}("id"=>id, "prover"=>"SeaHorn",
20-
"source_file"=>relpath(f, DIR),
21-
"theorem"=>"$(m.captures[1])_$(id)", "goal"=>strip(m.captures[2]),
22-
"annotation_kind"=>m.captures[1], "context"=>Any[]))
23-
id += 1
24-
end
25-
catch e; println("Warning: $f: $e"); end
23+
c = try
24+
read(f, String)
25+
catch
26+
continue
27+
end
28+
matches = try
29+
collect(eachmatch(pat, c))
30+
catch
31+
Any[]
32+
end
33+
rel = relpath(f, DIR)
34+
for m in matches
35+
kind = m.captures[1]
36+
body = first(strip(m.captures[2]), 1000)
37+
# Skip pure declarations (no call args) and empty goals.
38+
isempty(body) && continue
39+
push!(ps, Dict{String,Any}("id"=>id, "prover"=>"SeaHorn",
40+
"source_file"=>rel,
41+
"theorem"=>"$(kind)_$(id)", "goal"=>body,
42+
"annotation_kind"=>kind, "context"=>Any[]))
43+
id += 1
44+
end
2645
end
2746
ps, ts, pm
2847
end

0 commit comments

Comments
 (0)