Benchmarks
What has been measured, under which protocol, and what the numbers do not show.
Every figure on this page has a named protocol. A number without its protocol is a hypothesis. Webfold’s own engineering rules grade each result as tested, measured, or a design anchor, and a citation is a pointer, not evidence.
HTML conversion against the Rust html-extractor
The reference set is the 54 public fixtures from Firecrawl’s Rust html-extractor at commit 0a2b7432a20e356c2254f17e1b0acb2e79d88917. Both implementations pass all 211 expected-line and forbidden-phrase assertions across the 52 fixtures that carry assertions. Two fixtures have none.
| Measurement | Webfold | Rust html-extractor |
|---|---|---|
| Hot conversion, lower median of 54 fixture medians | 4.601 µs | 17.829 µs |
| Fresh-process conversion, same aggregation | 0.371781 ms | 4.021488 ms |
| Perfect asserted fixtures | 52/52 | 52/52 |
Protocol
- Five separate runs on one host (Intel Core i9-14900KF, CPU 8 affinity). Two warm-ups, seven samples, 50 conversions per hot sample.
- Hot timing excludes input loading. Fresh-process timing includes startup and input reading with a warm OS cache.
- Each cell is the median of five per-run aggregates. Hot aggregate ranges: 4.580–4.627 µs and 17.772–17.914 µs.
- CPU affinity was not exclusive, later byte-identical repeats varied under heavy host load, and no confidence interval is claimed.
What the assertion score does not show
- The fixtures are development and regression fixtures; fixes were made against them.
- A complete-output review found six malformed tables and one extra code blank line that the assertions missed. The assertion score is not a measure of complete Markdown fidelity.
- A live-page review of Firecrawl’s published 1,000-URL dataset is exploratory. Of the 58 originally empty static results, 47 remain empty in the frozen replay, and the zero-empty gate is still red. The requested-content report for the accepted pre-merge source cut verifies 15 of those 47, leaving 32 unresolved. The merged source has no fresh report.
- A separate run on the same dataset on 13 November used our own scorer, not Firecrawl’s. Of the 850 URLs that have a reference snippet, Webfold’s native scrape covered 56.6%, curl 53.3% and Playwright 60.7%. Webfold returned the page’s non-core lines on 41.8% of rows and Playwright on 64.6%. Firecrawl’s published 75% for curl and 79% for Puppeteer did not reproduce on this scorer. It was one run with no repeats, from a datacentre address, and the headless mode was not used.
- Nonempty text and source retention do not establish independent webpage accuracy. The independent 1,200-page evaluation has collected zero pages under its protocol.
Formal checks
Two Lean suites check the Rust. They are separate and they make different axiom statements.
Constructive suite
It checks finite extracted kernels and bounded flow models. The audit recorded at the accepted pre-merge cut covers 149 authored declarations with zero transitive axiom dependencies. Seven other extracted roots remain reference models, not runtime proofs. Zero axioms in a model is not a proof of the complete Rust implementation.
That audit predates the merge of the BigInt proofs and the folder search into the main branch. The repository’s full gates were not re-run on the merged main branch, so this result is not described as accepted for it.
BigInt suite
It checks Lean 4.31.0 theorems about the real Rust in src/cdp/pw/bigint.rs, extracted with Charon and Aeneas. These theorems depend on the three Lean core axioms propext, Classical.choice and Quot.sound. The zero-axiom statement above does not apply to them. The audit covers 2,184 constants and finds no sorryAx. Several theorems carry size hypotheses, such as at most 2^30 limbs in total for multiplication and division.
| Area | Status |
|---|---|
| Limb kernels: trim, compare, add, subtract, schoolbook and Karatsuba multiply, shifts | Proved |
Division: small divisor, Knuth D (estimate, multiply-subtract, add-back, loop), signed div and rem |
Proved |
| Signed add, multiply and compare | Proved |
| Digit parse and format kernels | Proved |
BigInt::parse, parse_js_literal and to_string_radix wrappers |
Not proved: not extracted |
Bitwise operators, two’s complement, as_int_n, pow, BigInt-level shifts, f64 conversion, MAX_BITS guards |
Not proved: not extracted |
The unproved operations rest on unit tests, a 42,141-vector oracle built from Python integers and a JavaScript parity set. The extraction-drift check was not run for the merged revision, because the pinned Charon toolchain was not installed. A source-line cross-check of all 48 extracted definitions found no mismatch. That is evidence, not the check. Of the mutation controls, the Rust mutants were re-extracted in an earlier run. The parse and format mutants were applied by hand to a copy of the generated Lean file, which is weaker evidence.
Where benchmarks live
Web acquisition and competitive runs belong to the webfold-bench repository. That repository is private until the public release of Webfold. Document conversion quality and latency belong to superdocuments-bench. The competitive directory inside the main repository is a historical compatibility subset, not the active suite.