Metadata-Version: 2.4
Name: shred-lean
Version: 0.2.1
Summary: Profile and eliminate repeated work in batched Lean verification
Author: Memo Ozdincer
Project-URL: Homepage, https://github.com/memo-ozdincer/shred
Project-URL: Repository, https://github.com/memo-ozdincer/shred
Project-URL: Documentation, https://github.com/memo-ozdincer/shred#readme
Project-URL: Issues, https://github.com/memo-ozdincer/shred/issues
Keywords: lean,theorem-proving,verification,profiling,proof-assistants
Classifier: Development Status :: 3 - Alpha
Classifier: Environment :: Console
Classifier: Intended Audience :: Developers
Classifier: Intended Audience :: Science/Research
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Topic :: Scientific/Engineering
Classifier: Typing :: Typed
Requires-Python: >=3.11
Description-Content-Type: text/markdown
Provides-Extra: dev
Requires-Dist: build>=1.2; extra == "dev"

# SHRED

**Reuse repeated work across thousands of Lean proof attempts.**

SHRED is an installable Python package, Lean instrumentation suite, and
evidence-backed workload profiler. It tells you whether a proof workload has
enough cost-weighted repetition to justify caching before you modify a
verifier.

SHRED is a performance research system for batched Lean verification. It finds
computation shared by model-generated proof attempts, executes or generates
that work once, and preserves ordinary Lean as the final correctness authority.

On authentic proof closures from a large theorem-proving rollout, SHRED's
certificate-transfer prototype made repeated `nlinarith` closure up to
**325.6× faster** and repeated `positivity` closure **27.1× faster**, measured
as generation-plus-check versus application-plus-check. The project combines
Lean metaprogramming with a reproducible Python analysis and execution stack.

```text
32 independent proof attempts
            │
            ▼
  Lean-native parsing and telemetry
            │
       ┌────┴────┐
       ▼         ▼
 exact shared   checked closing
 prefixes       certificates
       └────┬────┘
            ▼
 ordinary Lean verdict for every proposal
```

## Why SHRED

Modern proof-generation systems can produce tens or hundreds of candidates for
the same theorem. Verification then treats every candidate as an unrelated
program-even when candidates repeat the same opening tactics or converge on
the same expensive closing calculation.

SHRED explores two conservative ways to remove that duplication:

1. **Exact prefix sharing.** Represent a batch as a tactic trie, execute a
   common rooted prefix once, and fork only when proofs diverge.
2. **Closing-certificate reuse.** Cache a proof produced by an expensive
   closing tactic, match it against an exact elaborated context and target,
   and ask ordinary Lean to type-check it before reuse.

Neither path weakens verification, invents tactics, or substitutes a learned
judge. Unsupported or unmatched attempts take the original execution path.

## Plug-and-play workflow

### 1. Diagnose your corpus

SHRED expects JSONL or JSONL.gz rollout records containing `theorem_name`,
`proof`, and `correct`. Register the files without copying or rewriting them:

```bash
shred init \
  --input /data/rollouts.jsonl.gz \
  --samples-per-theorem 32 \
  --output workload.manifest.json
```

Start with the bounded screening profile. It audits hashes and counts, extracts
Lean-native tactic boundaries, replays unchanged proofs, measures reached CPU
cost, and writes one recommendation:

```bash
shred profile \
  --manifest workload.manifest.json \
  --lean-workspace /path/to/mathlib4 \
  --output-dir shred-profile

cat shred-profile/profile.json
```

The default examines at most 256 proposals and always labels its recommendation
`screening_only`. If the signal is promising, repeat on a representative
immutable workload with `--full`. SHRED counts unsupported syntax, timeouts,
errors, and fallbacks instead of silently dropping them.

### 2. Act on the diagnosis

The report deliberately produces one of three full-workload decisions:

| Decision | Action |
|---|---|
| `prefix_reuse_candidate` | Benchmark an exact prefix executor against warm independent verification before deployment. |
| `do_not_deploy_exact_prefix_reuse` | Do not build prefix caching for this workload; inspect expensive closing-tactic tails. |
| `inconclusive` | Resolve attribution, timeout, fallback, or verdict-agreement failures first. |

### 3. Reuse expensive closing certificates

When profiling identifies repeated expensive closing tactics, add the SHRED
Lean package and wrap only those tactics:

```toml
# lakefile.toml
[[require]]
name = "shred"
path = "../shred/lean"
```

```lean
import SHRED

open LeanPrefix.AutomaticCertificate

example (x : Real) (h : x = 3) : x ^ 2 = 9 := by
  reuse_closing in nlinarith
```

Cache hits remain ordinary Lean proofs. SHRED requires an exact environment,
tactic, elaborated target, and ordered local context; then it infers the reused
proof's type and checks definitional equality with the current goal. A miss or
exception restores state and runs `nlinarith` unchanged.

## Scale and measured highlights

SHRED was developed against a self-contained DeepSeek-Prover rollout corpus:

| Measurement | Result |
|---|---:|
| Theorems | 9,655 |
| Registered proof proposals | 308,960 |
| Lean-correct proposals | 168,029 |
| Proposals eligible for conservative Lean-native splitting | 304,546 |
| Exact duplicate proposal occurrences | 42,815 |
| Eligible proposals sharing their first tactic | 53.71% |
| Lean tactic occurrences analyzed | 888,421 |
| Automatic certificate pairs checked in the representative study | 4,096 |
| Paired Lean-verdict agreement | 4,096 / 4,096 |
| Safe automatic certificate hits | 921 |
| Best measured certificate-transfer acceleration | 325.6× |

The repository includes immutable manifests, aggregate reports, deterministic
selection logic, proposal-level accounting, and hand-reviewed examples. Its
experiments ran on a 192-core Intel node with up to 766 GB RAM, using pinned
Lean, Mathlib, REPL, corpus, and Git revisions.

## Where this can matter most

SHRED's mechanisms are especially promising for workloads that create repeated
or deliberately branching proof computation:

- reinforcement-learning pipelines that verify large rollout groups;
- beam search, best-first search, and tree search with common partial proofs;
- synthetic algebra and arithmetic theorem families with repeated expensive
  closers such as `nlinarith`, `linarith`, `ring`, `omega`, or normalization;
- proof-generation services using best-of-N sampling;
- benchmark and dataset builders that repeatedly revisit related Lean states;
- interactive or hosted Lean systems that can amortize checked certificates
  across a long-running process.

A lightweight corpus profiler can use SHRED's measurements to determine whether
a workload has enough cost-weighted reuse to justify an execution cache before
building or deploying one.

## Architecture

The implementation has three auditable layers:

- **Lean-native instrumentation:** exact tactic boundaries, elaborated target
  and local-context keys, proof capture, type inference, definitional-equality
  checks, and transactional fallback.
- **Python orchestration:** streaming corpus readers, deterministic sampling,
  persistent REPL control, paired baseline/cached execution, timeout and memory
  isolation, and strict result consolidation.
- **Reproducible evidence:** self-contained compressed data shards, SHA-256
  manifests, frozen configurations, structured JSON reports, bootstrap
  intervals, and manual audits of successes and failure modes.

The certificate cache uses hashes only to locate candidate buckets. A hit still
requires exact structural equality, a compatible ordered local context,
successful proof-type inference, definitional equality with the target, and
ordinary Lean checking. Any exception restores the tactic state and runs the
original tactic.

## What the study discovered

The full corpus produced an important performance map. Exact shared prefixes
were common by count but represented only **3.762%** of cost-weighted execution
opportunity. In the representative certificate study, **22.85%** of
instrumented closing tactics hit the cache while total paired CPU fell
**3.2405%**. Many repeated steps were simply too cheap to dominate end-to-end
runtime.

At the same time, selected expensive closures saved tens to more than one
hundred CPU-seconds per reuse. This points to SHRED's strongest next design: a
cost-aware cache of named, shallow certificates for expensive proof tails,
rather than indiscriminate caching of every repeated tactic.

## Development and bundled evidence

```bash
python -m venv .venv
. .venv/bin/activate
python -m pip install -e .
python -m unittest discover -s tests -v

shred audit --manifest data/c0.manifest.json
shred analyze-exact --manifest data/c0.manifest.json
```

The same workflow is available as a typed Python API:

```python
from pathlib import Path
from shred import ProfileConfig, profile_workload

result = profile_workload(ProfileConfig(
    manifest=Path("data/c0.manifest.json"),
    lean_workspace=Path("/path/to/mathlib4"),
    output_dir=Path("artifacts/my-workload-profile"),
))
print(result.report["recommendation"])
```

The historical `lean-prefix` command remains available as a compatibility
alias. The complete C0 corpus is included as four deterministic gzip shards
under `data/c0/proofs/`; the auditor streams them without extraction and checks
both repository hashes and original uncompressed-source hashes.

## Evidence and design notes

- [`reports/c0_certificate_prevalence_d030.json`](reports/c0_certificate_prevalence_d030.json)
  - automatic certificate prevalence and paired CPU measurements
- [`reports/c0_certificate_prevalence_review.md`](reports/c0_certificate_prevalence_review.md)
  - hand audit of representative and expensive-tail cases
- [`docs/DESIGN.md`](docs/DESIGN.md) - execution and correctness model
- [`docs/VERIFICATION.md`](docs/VERIFICATION.md) - test and evidence contract
- [`docs/DATA.md`](docs/DATA.md) - immutable corpus and provenance
- [`docs/DECISIONS.md`](docs/DECISIONS.md) - scientific and engineering decisions
- [`docs/FUTURE.md`](docs/FUTURE.md) - cost-aware cache, serving, and acceleration roadmap

## Roadmap

- adapters for additional Lean rollout formats;
- named, shallow certificate storage for expensive closing-tactic families;
- cost-aware admission, eviction, and straggler isolation;
- integration adapters for Lean rollout and tree-search systems;
- Rust-native high-throughput orchestration and cache service;
- persistent and distributed certificate stores with complete attribution.

SHRED is built around a simple principle: optimize proof computation
aggressively, but never change the proof that Lean is asked to trust.
