Skip to content

Commit 854d606

Browse files
levineuwirthlevineuwirth
authored
specialize ℕ→ℤ end to end — real refinement witnesses, the first lifting (R3-M1) (#91)
R3-M1: ℕ is the first specialized carrier. The reifiers (both bridges) emit the ℤ image of a ℕ goal — `Int.ofNat` cast shells, folded literals (closed `^`, so 2^24-scale numerals ride through), `_pb_nonneg_*` hypotheses, and a `primitive`-kind metadata entry whose `embedding_witness:` tags name the actual embedding lemmas, each with a content-hashed `library_provenance` entry. `Refinement.run` stops fabricating its witness: `soundness_witness` is the joined tag payloads, and no witness means no specialization (fail closed; method specs likewise need a target-level witness — additive-optional schema field, v1.1-bound). The first lifting code: term mode casts every witness-named hypothesis to ℤ by term construction (decidable-byContra wrappers; Lean rides kernel defeq, Rocq uses explicit constructive push lemmas — its ℕ term-mode footprint is EMPTY) and runs the shared Int Farkas fold; the walker gets a cast layer + atom-override context in front of `walkProof`. Cert-consuming closers gate on the recorded specializations being exactly the invertible set. Nonlinear ℕ products atomize to spec-§4.4 `Opaque` payload atoms (the R4-D1 shape, first live `Opaque` producer); ℕ subtraction/division/modulo and nested ℕ quantifiers fail fast. 7 new corpus goals (2^24, ∀ℕ, D1 included) close live-strict via `proof_broker_walker` on both bridges — live-mintable 24/24. check.py/validate.py cross-check every specialization witness against `library_provenance` (IR tags and paired certs). Decision record: delta.md §5.4. This is the C3a mid-phase checkpoint; M2 (polymorphic α) and M3 (def-unfold) follow in-phase. Fourteen commits, reviewable one at a time: `4514cc1` (refinement witnesses, fail closed), `3d6bc32` (SDK cast transparency + Opaque), `449c60c` (content_hash FFI), `e3f91db` (Lean reifier), `c126d58` (Lean lift), `243e920` (Lean tests), `6fb0087` (Rocq port), `d439547` (corpus), `f62d370` (fixtures), `d89d122` (delta §5.4); C3a ROUND 1 fixes: `fbc99ac` (coverage/status honest about static-vs-live replay), `e84799d` (spec gate pinned by synthetic-cert tests, both bridges), `800f98a` (gate covers case-split + plain-path walker attempts), `d727b0f` (atomization refuses hidden ℕ sub/div/mod); C3a ROUND 2 fix: `2ab86bd` (atom scan covers spelled core names + Nat.pred). Validation (local, verbatim CI commands, 2026-09-01, tree `2ab86bd`; tails in `R3-REVIEW.local.md`, Gate status + the ROUND records; review CONVERGED after 2 rounds): schemas all 17 steps exit 0; sdk 29 suites + cross-tool 3/3 + FFI T1–T6; lean pipefail 880 jobs, "OK: all 135 allowlisted theorem(s) within their axiom ceiling", roundtrip 37 OK; rocq from `dune clean` "OK: all 176 within ceiling", corpus drift-free. Rocq `pb_nat_term*_axiom_free` print "Closed under the global context"; Lean `pb_nat_term*` pinned at `[propext, Quot.sound]`; the specialization gate's throw branches are test-pinned on both bridges. Base: `21f07be`. Allowlist: additions only (Lean +15, Rocq +35), no ceiling raised on any existing theorem. Scoped follow-ups (not in this PR): M2/M3; Tier-1 rescue for goals whose cvc5 traces lack `la_generic`; a cast-layer `walker_test` for the static CorpusReplay (ℕ goals carry `static_replay_skip`); reifier accumulator state threading (parallel-elaboration hygiene).
1 parent 21f07be commit 854d606

75 files changed

Lines changed: 6633 additions & 232 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎README.md‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -34,10 +34,10 @@ refreshes it). It is the only place this README states a count.
3434
<!-- status-table:begin (generated by tools/status_table.py; do not edit by hand) -->
3535
| surface | value | source |
3636
|---|---|---|
37-
| Trust gate (Lean) | 120 allowlisted theorems; 3 distinct axioms: `Classical.choice`, `Quot.sound`, `propext` | `tools/axiom_allowlist.json` (gated by `check_axioms.py` in the lean-bridge job) |
38-
| Trust gate (Rocq) | 134 allowlisted theorems; 4 distinct axioms: `ClassicalDedekindReals.sig_forall_dec`, `FunctionalExtensionality.functional_extensionality_dep`, `classic`, `propositional_extensionality` | `tools/axiom_allowlist.json` (gated by `check_axioms.py` in the rocq-bridge job) |
37+
| Trust gate (Lean) | 135 allowlisted theorems; 3 distinct axioms: `Classical.choice`, `Quot.sound`, `propext` | `tools/axiom_allowlist.json` (gated by `check_axioms.py` in the lean-bridge job) |
38+
| Trust gate (Rocq) | 176 allowlisted theorems; 4 distinct axioms: `ClassicalDedekindReals.sig_forall_dec`, `FunctionalExtensionality.functional_extensionality_dep`, `classic`, `propositional_extensionality` | `tools/axiom_allowlist.json` (gated by `check_axioms.py` in the rocq-bridge job) |
3939
| Alethe walker rules | Lean 31, Rocq 31 (at parity) | dispatch arms between `PARITY:walker-rules` markers (`check_walker_parity.py`) |
40-
| Walker corpus | 17 goals, 1138 proof steps; statically walkable 17/17; in the generated `CorpusReplay.v` 17/17 (the coqc ground truth is that file compiling in the rocq-bridge job); live-mintable 17/17 | `corpus/index.json`, `corpus/coverage.json` (`check_walker_coverage.py --check`, `gen_corpus_replay.py --check`) |
40+
| Walker corpus | 24 goals, 1541 proof steps; statically walkable 24/24; in the generated `CorpusReplay.v` 17/24 (the coqc ground truth for those is that file compiling in the rocq-bridge job) + 7/24 live-strict only (`CorpusWalkerLive_*` on both bridges — their coqc/kernel ground truth; the static replay has no ℕ→ℤ cast layer); live-mintable 24/24 | `corpus/index.json`, `corpus/coverage.json` (`check_walker_coverage.py --check`, `gen_corpus_replay.py --check`) |
4141
| Backends (adapter manifests) | cvc4 1.8 (tiers 0,1); cvc5 1.3.0 (tiers 0,1,2,3; alethe-2024); llm 0 (tiers 3; lean-tactic-script); vampire 5.1.0 (tiers 0,3; tstp-fof,tstp-thf); z3 4.16.0 (tiers 0,1) | `examples/manifest-*.json` |
4242
| Toolchain pins | Lean `leanprover/lean4:v4.32.0`; OCaml `5.4`; dune `>= 3.21 & < 3.24`; rocq-runtime `>= 9.0 & < 9.2`; cvc5 `1.3.0`; Vampire `v5.1.0`; elan `v4.2.4` | `lean-bridge/lean-toolchain`, `proof_broker_rocq.opam`, `validate.yml` env pins |
4343
| CI jobs (timeout) | schemas (10 min); sdk (20 min); sdk-cross-platform (20 min); lean-bridge (40 min); rocq-bridge (30 min); ci-status (5 min); weekly cron `17 6 * * 1` | `.github/workflows/validate.yml` |

‎corpus/coverage.json‎

Lines changed: 78 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,13 @@
11
{
22
"supported_rule_count": 31,
3-
"mintable": 17,
3+
"mintable": 24,
44
"summary": {
5-
"walkable": 17,
5+
"walkable": 24,
66
"replayed": 17,
77
"shape_gapped": 0,
8-
"unsat": 17,
9-
"total": 17,
8+
"live_only": 7,
9+
"unsat": 24,
10+
"total": 24,
1011
"non_unsat": []
1112
},
1213
"backlog": {},
@@ -16,118 +17,191 @@
1617
"walkable": true,
1718
"missing": [],
1819
"replay_skip": null,
20+
"static_replay_skip": null,
1921
"mintable": true
2022
},
2123
"lia_eq_from_bounds": {
2224
"result": "unsat",
2325
"walkable": true,
2426
"missing": [],
2527
"replay_skip": null,
28+
"static_replay_skip": null,
2629
"mintable": true
2730
},
2831
"lia_false_from_bounds": {
2932
"result": "unsat",
3033
"walkable": true,
3134
"missing": [],
3235
"replay_skip": null,
36+
"static_replay_skip": null,
3337
"mintable": true
3438
},
3539
"lia_irrefl": {
3640
"result": "unsat",
3741
"walkable": true,
3842
"missing": [],
3943
"replay_skip": null,
44+
"static_replay_skip": null,
4045
"mintable": true
4146
},
4247
"lia_pigeonhole3": {
4348
"result": "unsat",
4449
"walkable": true,
4550
"missing": [],
4651
"replay_skip": null,
52+
"static_replay_skip": null,
4753
"mintable": true
4854
},
4955
"lia_strict_trans": {
5056
"result": "unsat",
5157
"walkable": true,
5258
"missing": [],
5359
"replay_skip": null,
60+
"static_replay_skip": null,
5461
"mintable": true
5562
},
5663
"lia_sum_bound": {
5764
"result": "unsat",
5865
"walkable": true,
5966
"missing": [],
6067
"replay_skip": null,
68+
"static_replay_skip": null,
6169
"mintable": true
6270
},
6371
"lia_weaken_bound": {
6472
"result": "unsat",
6573
"walkable": true,
6674
"missing": [],
6775
"replay_skip": null,
76+
"static_replay_skip": null,
77+
"mintable": true
78+
},
79+
"nat_d1_bracket": {
80+
"result": "unsat",
81+
"walkable": true,
82+
"missing": [],
83+
"replay_skip": null,
84+
"static_replay_skip": "\u2115 goal: the static CorpusReplay walker has no \u2115\u2192\u2124 cast layer (atoms resolve to nat vars); the LIVE-strict suites on both bridges are the kernel ground truth for these goals",
85+
"mintable": true
86+
},
87+
"nat_eq_from_bounds": {
88+
"result": "unsat",
89+
"walkable": true,
90+
"missing": [],
91+
"replay_skip": null,
92+
"static_replay_skip": "\u2115 goal: the static CorpusReplay walker has no \u2115\u2192\u2124 cast layer (atoms resolve to nat vars); the LIVE-strict suites on both bridges are the kernel ground truth for these goals",
93+
"mintable": true
94+
},
95+
"nat_false_from_bounds": {
96+
"result": "unsat",
97+
"walkable": true,
98+
"missing": [],
99+
"replay_skip": null,
100+
"static_replay_skip": "\u2115 goal: the static CorpusReplay walker has no \u2115\u2192\u2124 cast layer (atoms resolve to nat vars); the LIVE-strict suites on both bridges are the kernel ground truth for these goals",
101+
"mintable": true
102+
},
103+
"nat_forall_instance": {
104+
"result": "unsat",
105+
"walkable": true,
106+
"missing": [],
107+
"replay_skip": null,
108+
"static_replay_skip": "\u2115 goal: the static CorpusReplay walker has no \u2115\u2192\u2124 cast layer (atoms resolve to nat vars); the LIVE-strict suites on both bridges are the kernel ground truth for these goals",
109+
"mintable": true
110+
},
111+
"nat_pow_bound": {
112+
"result": "unsat",
113+
"walkable": true,
114+
"missing": [],
115+
"replay_skip": null,
116+
"static_replay_skip": "\u2115 goal: the static CorpusReplay walker has no \u2115\u2192\u2124 cast layer (atoms resolve to nat vars); the LIVE-strict suites on both bridges are the kernel ground truth for these goals",
117+
"mintable": true
118+
},
119+
"nat_strict_trans": {
120+
"result": "unsat",
121+
"walkable": true,
122+
"missing": [],
123+
"replay_skip": null,
124+
"static_replay_skip": "\u2115 goal: the static CorpusReplay walker has no \u2115\u2192\u2124 cast layer (atoms resolve to nat vars); the LIVE-strict suites on both bridges are the kernel ground truth for these goals",
125+
"mintable": true
126+
},
127+
"nat_sum_bound": {
128+
"result": "unsat",
129+
"walkable": true,
130+
"missing": [],
131+
"replay_skip": null,
132+
"static_replay_skip": "\u2115 goal: the static CorpusReplay walker has no \u2115\u2192\u2124 cast layer (atoms resolve to nat vars); the LIVE-strict suites on both bridges are the kernel ground truth for these goals",
68133
"mintable": true
69134
},
70135
"prop_demorgan": {
71136
"result": "unsat",
72137
"walkable": true,
73138
"missing": [],
74139
"replay_skip": null,
140+
"static_replay_skip": null,
75141
"mintable": true
76142
},
77143
"prop_eq_trans": {
78144
"result": "unsat",
79145
"walkable": true,
80146
"missing": [],
81147
"replay_skip": null,
148+
"static_replay_skip": null,
82149
"mintable": true
83150
},
84151
"prop_excluded_middle": {
85152
"result": "unsat",
86153
"walkable": true,
87154
"missing": [],
88155
"replay_skip": null,
156+
"static_replay_skip": null,
89157
"mintable": true
90158
},
91159
"uf_cong": {
92160
"result": "unsat",
93161
"walkable": true,
94162
"missing": [],
95163
"replay_skip": null,
164+
"static_replay_skip": null,
96165
"mintable": true
97166
},
98167
"uf_exists_witness": {
99168
"result": "unsat",
100169
"walkable": true,
101170
"missing": [],
102171
"replay_skip": null,
172+
"static_replay_skip": null,
103173
"mintable": true
104174
},
105175
"uf_forall_inst": {
106176
"result": "unsat",
107177
"walkable": true,
108178
"missing": [],
109179
"replay_skip": null,
180+
"static_replay_skip": null,
110181
"mintable": true
111182
},
112183
"uf_lia_mix": {
113184
"result": "unsat",
114185
"walkable": true,
115186
"missing": [],
116187
"replay_skip": null,
188+
"static_replay_skip": null,
117189
"mintable": true
118190
},
119191
"uf_lia_threshold": {
120192
"result": "unsat",
121193
"walkable": true,
122194
"missing": [],
123195
"replay_skip": null,
196+
"static_replay_skip": null,
124197
"mintable": true
125198
},
126199
"uf_trans": {
127200
"result": "unsat",
128201
"walkable": true,
129202
"missing": [],
130203
"replay_skip": null,
204+
"static_replay_skip": null,
131205
"mintable": true
132206
}
133207
}

0 commit comments

Comments
 (0)