5Fmpwt…ipbLkW
MinerAcceptedAdmittedSubmitted 1 Oct 2026, 05:39 UTC5FmpwtQSDe29r2iQ7gCyamBQjue27sZhMLUA9VFd1nipbLkWDigest b06a68eeda6aced8…
On the frontier · <0.1% of pay · 0.773 α of 3,600 α earned
- Time vs incumbent
- 5.42×
- Mean compressed size
- 34.11%
- Compression time
- 7.02 s
- Size, byte-weighted
- 30.84%
Gate
- Rust checksPassed
- Lean proofPassed
- BenchmarkPassed
- AggregationPassed
Where it sits
- Miner
- Reference parser
- Not admitted
- Pareto frontier
- Scoring limit
Standing
- Share of pay
- <0.1%
- Bounty earned
- 0.773 α of 3,600 α
Scoring limits
- Time vs incumbent5.42× · limit 10.0×Inside
- Mean compressed size34.11% · limit 40.00%Inside
Admission
No speed comparison is required for this contribution.
No speed test ran: Admitted
Source
Private while this parser is on the frontier. It is published once another submission beats it.
Gate report
Show report
verifying [internal-path]
workspace: [internal-path]
0 intake ok — 165: parse.rs, Parse.lean
1 policy ok — source prefilters passed
2 static ok — resolved operations: alloc::alloc::Global::{impl}::drop_glue, alloc::vec::Vec::{impl}::drop_glue, alloc::vec::{impl}::deref, alloc::vec::{impl}::deref_mut, alloc::vec::{impl}::index, alloc::vec::{impl}::index_mut, alloc::vec::{impl}::len, alloc::vec::{impl}::new, alloc::vec::{impl}::push, alloc::vec::{impl}::with_capacity, core::num::{impl}::leading_zeros, core::num::{impl}::saturating_add, core::num::{impl}::wrapping_add, core::num::{impl}::wrapping_mul, core::num::{impl}::wrapping_shr, core::num::{impl}::wrapping_sub, core::slice::index::{impl}::get, core::slice::index::{impl}::get_mut, core::slice::index::{impl}::get_unchecked, core::slice::index::{impl}::get_unchecked_mut, core::slice::index::{impl}::index, core::slice::index::{impl}::index_mut, core::slice::{impl}::len
3 extract ok — charon+aeneas re-run by the verifier, no new axioms
4 statement ok — `LZ77.Obligation slot.parse` typechecks (bwrap, 900s, 16384 MB)
5 axioms ok — ['Classical.choice', 'Quot.sound', 'propext']; extraction intact
6 score running…
Corpus: corpus-stage1
file raw incumbent submission
-----------------------------------------------------
binary.db.bin 500000 76338 70994
bundle.min.js.txt 1000000 301618 287551
catalog.xml.txt 500000 62314 58127
compressed.bin 300000 300194 299566
config.yaml.txt 400000 85384 81034
docs.md.txt 800000 226973 215666
dump.sql.txt 150000 20817 16400
genome.fasta 900000 292479 256489
images.bin 250000 223767 223464
lean.txt 1000000 235059 222966
machine-code.bin 500000 167357 159593
metrics.csv.txt 1300000 287282 251906
multibyte.txt 1100000 273630 254449
page.html.txt 600000 103618 98935
prose.txt 1500000 579041 541103
records.json.txt 400000 72255 69131
server.log 300000 29404 25953
source.c.txt 1400000 354325 333233
source.py.txt 600000 132748 125186
source.rs.txt 700000 134069 126017
sourcemap.map.txt 350000 68389 64436
sparse.bin 40000 1234 1193
tiny-app.log 28000 965 852
tiny-config.json.txt 12000 2107 2077
weights-bf16.bin 450000 362200 353965
weights-f16.bin 250000 216274 212660
weights-f32.bin 350000 284747 279059
weights-q8.bin 250000 236246 235572
-----------------------------------------------------
TOTAL 15930000 5130834 4867577
method bytes ratio lz77 encode total slowdown
--------------------------------------------------------------------------------------------------------------
incumbent 5130834 1.00000x 0.622s 0.225s 0.848s 1.00x the incumbent
submission 4867577 0.94869x 3.227s 0.243s 3.471s 4.09x ACCEPTED — 5.131% smaller than the incumbent.
ACCEPTED — 5.131% smaller than the incumbent.
Corpus: corpus-stage2
corpus corpus-stage2 is held out; totals only.
method bytes ratio lz77 encode total slowdown
--------------------------------------------------------------------------------------------------------------
incumbent 5218788 1.00000x 0.629s 0.229s 0.858s 1.00x the incumbent
submission 4956921 0.94982x 3.298s 0.249s 3.548s 4.13x ACCEPTED — 5.018% smaller than the incumbent.
ACCEPTED — 5.018% smaller than the incumbent.