Lean Kernel Arena / nano-lean

Checker "nano-lean"

Version: v0.3.2 (54ce971) · 📄 Declaration · 🔗 Source

A parallel Lean 4 kernel written in Rust using hash-consing and de Bruijn indices

Soundness (rightfully rejected tests)

80 ✅ 0 ❌ 0 🚫

Completeness (rightfully accepted tests)

138 ✅ 0 ❌ 0 🚫

Corner cases (no outcome prescribed)

28 ✅ 2 🚫

Test Expected Result ⏱️ 🧠
cedar 👍 👍 10.7 s (÷13) 1.3 GB (-3%)
con-leche 👍 👍 8.47 s (÷13) 1.2 GB (+45%)
cslib 👍 👍 25.5 s (÷20) 2.2 GB (-36%)
init 👍 👍 4.25 s (÷16) 838.2 MB (+48%)
init-prelude 👍 👍 26.8 ms (÷14) 163.8 MB (×2.2)
mathlib 👍 👍 70.1 s (÷28) 4.6 GB (÷2.2)
navier-stokes-euler 👍 👍 17.5 s (÷38) 2.0 GB (-20%)
reachability 👍 👍 1.93 s (÷12) 1.3 GB (-21%)
std 👍 👍 7.36 s (÷15) 1.1 GB (+21%)
26 25.0 ms 67.8 MB
closure-level-subst ✋ ✋ 0.520 ms 15.7 MB
constlevels ✋ ✋ 0.615 ms 24.0 MB
ctor-num-fields ✋ ✋ 0.767 ms 28.2 MB
eta-ctor-alias ✋ ✋ 0.550 ms 22.0 MB
forged-quot-ind ✋ ✋ 0.472 ms 10.7 MB
k-rec-conv ✋ ✋ 0.601 ms 26.3 MB
large-elim-param ✋ ✋ 0.597 ms 24.0 MB
large-elim-prop-bool ✋ ✋ 0.675 ms 26.1 MB
level-imax-leq ✋ ✋ 0.568 ms 22.1 MB
level-imax-normalization ✋ ✋ 0.572 ms 22.0 MB
loose-bvar-value ✋ ✋ 0.484 ms 13.9 MB
nat-rec-k-lie ✋ ✋ 0.552 ms 22.1 MB
nat-rec-rules ✋ ✋ 0.652 ms 24.1 MB
nested-name-capture ✋ ✋ 0.777 ms 32.0 MB
nested-rec-rule-nfields ✋ ✋ 1.14 ms 32.5 MB
nested-unused-param ✋ ✋ 1.35 ms 36.2 MB
orphan-rec ✋ ✋ 0.469 ms 13.9 MB
pi-closure-context ✋ ✋ 0.477 ms 11.4 MB
proj-non-structure ✋ ✋ 0.523 ms 22.1 MB
proj-of-imax-prop ✋ ✋ 0.669 ms 24.1 MB
proj-of-stuck-prop ✋ ✋ 2.75 ms 59.7 MB
proj-of-subst-prop ✋ ✋ 2.58 ms 61.4 MB
rec-k-lie ✋ ✋ 0.534 ms 22.0 MB
rec-missing-ih ✋ ✋ 2.94 ms 67.8 MB
rec-of-subst-prop ✋ ✋ 2.66 ms 61.7 MB
unit-rec-rule ✋ ✋ 0.533 ms 21.9 MB
1 7.01 s 3.5 GB
alg-conv-trans-acc 🤷 ✋ 1.06 ms 37.9 MB
alg-conv-trans-acc-left 🤷 👍 1.04 ms 34.1 MB
alg-conv-trans-acc-right 🤷 👍 1.05 ms 36.0 MB
alg-conv-trans-quot 🤷 ✋ 0.623 ms 17.7 MB
alg-conv-trans-quot-left 🤷 ✋ 0.628 ms 19.8 MB
alg-conv-trans-quot-left-def 🤷 👍 0.639 ms 21.8 MB
alg-conv-trans-quot-right 🤷 👍 0.628 ms 19.8 MB
eta-ctor 🤷 ✋ 0.552 ms 22.0 MB
eta-rec-struct 🤷 ✋ 0.569 ms 24.0 MB
eta-rule-k 🤷 ✋ 0.534 ms 17.9 MB
eta-struct-major-and 🤷 ✋ 0.564 ms 23.8 MB
eta-struct-major-and-no-whnf 🤷 🚫 3.50 s 3.5 GB
eta-struct-major-no-whnf 🤷 🚫 3.50 s 3.5 GB
eta-unit-like-nested 🤷 ✋ 0.616 ms 21.7 MB
eta-unit-like-pi 🤷 ✋ 0.528 ms 17.7 MB
eta-unit-like-proof-field 🤷 ✋ 0.546 ms 19.8 MB
eta-unit-like-struct 🤷 ✋ 0.547 ms 22.0 MB
imax-nested-absorption 🤷 👍 0.459 ms 10.2 MB
imax-right-successor 🤷 👍 0.454 ms 11.5 MB
large-elim-maybe-prop 🤷 ✋ 0.492 ms 17.7 MB
let-value-type-mismatch 🤷 ✋ 0.444 ms 10.4 MB
nested-nonuniform-param 🤷 👍 0.564 ms 22.0 MB
nested-redex-aux 🤷 👍 0.816 ms 28.1 MB
positivity-whnf 🤷 ✋ 0.510 ms 13.8 MB
proj-maybe-prop 🤷 👍 0.563 ms 22.3 MB
proj-maybe-prop-past 🤷 👍 0.564 ms 24.1 MB
proof-param-ok 👍 👍 0.478 ms 13.8 MB
proof-param-swap 🤷 ✋ 0.476 ms 13.6 MB
subject-reduction-redex 🤷 👍 1.02 ms 36.2 MB
subject-reduction-reduct 🤷 ✋ 1.08 ms 32.2 MB
vanishing-occurrence 🤷 👍 0.535 ms 17.8 MB
10 5.67 ms 30.4 MB
extra-rec ✋ ✋ 0.470 ms 13.7 MB
inductive-undeclared-universe ✋ ✋ 0.502 ms 13.7 MB
level-index-out-of-order 👍 👍 0.442 ms 8.4 MB
nat-lit-add 👍 👍 0.711 ms 30.4 MB
nat-lit-add-bad ✋ ✋ 0.695 ms 28.4 MB
nat-lit-ble 👍 👍 0.709 ms 26.1 MB
nat-lit-sub 👍 👍 0.713 ms 24.0 MB
orphan-ctor ✋ ✋ 0.471 ms 13.3 MB
proj-of-prop ✋ ✋ 0.514 ms 21.9 MB
sparse-name-index 👍 👍 0.441 ms 8.3 MB
31 4.84 s (÷17) 2.6 GB
app-lam 👍 👍 7.56 ms (÷641) 63.8 MB (÷22)
args-before-unfold 👍 👍 1.48 ms (÷24) 28.0 MB (÷2.4)
beta-ladder 👍 👍 3.77 ms (÷443) 42.5 MB (÷12)
church-numerals 👍 👍 3.63 ms (÷13) 32.0 MB (÷2.4)
discarded-argument 👍 👍 0.611 ms (÷272) 21.8 MB (÷3.0)
discarded-argument-match 👍 👍 0.696 ms (÷204) 21.8 MB (÷3.1)
folded-constant-first 👍 👍 1.85 ms (÷22) 31.1 MB (÷2.2)
folded-constant-last 👍 👍 1.84 ms (÷22) 31.3 MB (÷2.2)
fueled-chain 👍 👍 23.5 ms (÷5.4) 122.8 MB (+62%)
grind-ring-5 👍 👍 215 ms (÷10) 350.5 MB (+54%)
identical-nesting 👍 👍 0.555 ms (÷51) 22.1 MB (÷3.0)
irrelevance-before-evaluation 👍 👍 0.628 ms (÷46) 28.1 MB (÷2.3)
irrelevance-refutes 👍 👍 0.597 ms (÷48) 24.3 MB (÷2.7)
let-fold 👍 👍 3.23 ms (÷18) 77.8 MB (+18%)
let-ladder 👍 👍 3.17 ms (÷319) 55.8 MB (÷5.7)
magma-list-deep-n21 👍 👍 51.3 ms (÷53) 146.5 MB (÷4.6)
magma-list-deep-n36 👍 👍 433 ms (÷82) 453.4 MB (÷18)
magma-list-pair-n21 👍 👍 3.04 s (÷6.1) 2.6 GB (-35%)
magma-list-pair-n7 👍 👍 267 ms (÷6.3) 353.8 MB (-17%)
magma-string-n4 👍 👍 233 ms (÷15) 376.8 MB (×3.1)
magma-string-pair-n9 👍 👍 517 ms (÷16) 541.8 MB (-46%)
proj-cheap-struct 👍 👍 1.11 ms (÷31) 37.7 MB (-43%)
proj-lazy-struct 👍 👍 0.964 ms (÷32) 40.2 MB (-39%)
proj-stuck-struct 👍 👍 0.878 ms (÷36) 34.1 MB (-48%)
prop-struct-projections 👍 👍 10.1 ms (÷9.8) 125.6 MB (+79%)
refute-cheap-first ✋ ✋ 0.641 ms (÷65) 24.1 MB (÷2.9)
refute-cheap-last ✋ ✋ 2.19 ms (÷82) 26.1 MB (÷2.7)
repeated-subproblem 👍 👍 0.612 ms (÷47) 26.2 MB (÷2.5)
shared-subterm 👍 👍 4.49 ms (÷13) 45.2 MB (-38%)
shift-cascade 👍 👍 2.19 ms (÷21) 36.2 MB (-46%)
unroll-versus-evaluate 👍 👍 0.771 ms (÷40) 26.0 MB (÷2.5)
141 71.1 ms 27.6 MB
001_basicDef 👍 👍 0.442 ms 8.3 MB
002_badDef ✋ ✋ 0.443 ms 8.4 MB
003_arrowType 👍 👍 0.445 ms 11.8 MB
004_dependentType 👍 👍 0.443 ms 9.5 MB
005_constType 👍 👍 0.446 ms 11.8 MB
006_betaReduction 👍 👍 0.459 ms 11.6 MB
007_betaReduction2 👍 👍 0.461 ms 11.6 MB
008_forallSortWhnf 👍 👍 0.461 ms 12.4 MB
009_forallSortBad ✋ ✋ 0.464 ms 12.3 MB
010_nonTypeType ✋ ✋ 0.455 ms 12.6 MB
011_nonTypeAxiom ✋ ✋ 0.456 ms 12.4 MB
012_nonPropThm ✋ ✋ 0.443 ms 8.3 MB
013_thmProof 👍 👍 0.461 ms 13.6 MB
014_selfProof ✋ ✋ 0.445 ms 9.6 MB
015_levelComp1 👍 👍 0.442 ms 8.4 MB
016_levelComp2 👍 👍 0.442 ms 8.3 MB
017_levelComp3 👍 👍 0.443 ms 8.3 MB
018_levelParams 👍 👍 0.461 ms 11.6 MB
019_tut06_bad01 ✋ ✋ 0.425 ms 8.3 MB
020_levelComp4 👍 👍 0.442 ms 8.5 MB
021_levelComp5 👍 👍 0.442 ms 8.5 MB
022_imax1 👍 👍 0.446 ms 11.6 MB
023_imax2 👍 👍 0.447 ms 11.9 MB
024_levelMaxComm 👍 👍 0.444 ms 10.3 MB
025_levelMaxAssoc 👍 👍 0.445 ms 10.3 MB
026_levelMaxIdem 👍 👍 0.442 ms 8.3 MB
027_levelMaxAbsorb 👍 👍 0.444 ms 10.4 MB
028_inferVar 👍 👍 0.445 ms 11.6 MB
029_defEqLambda 👍 👍 0.455 ms 11.7 MB
030_peano1 👍 👍 0.509 ms 17.5 MB
031_peano2 👍 👍 0.527 ms 17.5 MB
032_peano3 👍 👍 0.535 ms 17.8 MB
033_letType 👍 👍 0.443 ms 9.6 MB
034_letTypeDep 👍 👍 0.477 ms 15.9 MB
035_letRed 👍 👍 0.453 ms 11.6 MB
036_empty 👍 👍 0.467 ms 12.6 MB
037_boolType 👍 👍 0.481 ms 12.4 MB
038_twoBool 👍 👍 0.502 ms 17.9 MB
039_andType 👍 👍 0.491 ms 15.5 MB
040_prodType 👍 👍 0.495 ms 15.8 MB
041_pprodType 👍 👍 0.494 ms 15.8 MB
042_pUnitType 👍 👍 0.478 ms 11.7 MB
043_eqType 👍 👍 0.493 ms 15.8 MB
044_natDef 👍 👍 0.486 ms 13.7 MB
045_rbTreeDef 👍 👍 0.590 ms 21.8 MB
046_inductBadNonSort ✋ ✋ 0.461 ms 13.9 MB
047_inductBadNonSort2 ✋ ✋ 0.456 ms 9.7 MB
048_inductLevelParam ✋ ✋ 0.427 ms 8.2 MB
049_inductTooFewParams ✋ ✋ 0.449 ms 11.8 MB
050_inductWrongCtorParams ✋ ✋ 0.475 ms 13.6 MB
051_inductWrongCtorResParams ✋ ✋ 0.470 ms 13.7 MB
052_inductWrongCtorResLevel ✋ ✋ 0.472 ms 13.8 MB
053_inductInIndex ✋ ✋ 0.475 ms 13.6 MB
054_indNeg ✋ ✋ 0.466 ms 13.7 MB
055_reduceCtorParam.mk 👍 👍 0.503 ms 15.7 MB
056_reduceCtorType.mk ✋ ✋ 0.480 ms 13.6 MB
057_indNegReducible ✋ ✋ 0.482 ms 13.8 MB
058_predWithTypeField 👍 👍 0.478 ms 13.8 MB
059_typeWithTypeField 👍 👍 0.480 ms 13.5 MB
060_typeWithTypeFieldPoly 👍 👍 0.481 ms 13.6 MB
061_typeWithTooHighTypeField.mk ✋ ✋ 0.462 ms 10.5 MB
062_emptyRec 👍 👍 0.472 ms 13.6 MB
063_boolRec 👍 👍 0.490 ms 15.8 MB
064_twoBoolRec 👍 👍 0.515 ms 19.4 MB
065_andRec 👍 👍 0.501 ms 17.7 MB
066_prodRec 👍 👍 0.510 ms 15.7 MB
067_pprodRec 👍 👍 0.507 ms 15.6 MB
068_punitRec 👍 👍 0.491 ms 16.0 MB
069_eqRec 👍 👍 0.500 ms 13.8 MB
070_nRec 👍 👍 0.497 ms 13.9 MB
071_rbTreeRef 👍 👍 0.623 ms 24.1 MB
072_boolPropRec 👍 👍 0.488 ms 13.6 MB
073_BogusRecursor ✋ ✋ 0.486 ms 13.7 MB
074_existsRec 👍 👍 0.504 ms 15.5 MB
075_typeSingletonRecReduction 👍 👍 0.560 ms 23.8 MB
076_sortElimPropRec 👍 👍 0.522 ms 17.8 MB
077_sortElimProp2Rec 👍 👍 0.535 ms 19.8 MB
078_boolRecEqns 👍 👍 0.576 ms 21.9 MB
079_prodRecEqns 👍 👍 0.558 ms 22.1 MB
080_nRecReduction 👍 👍 0.601 ms 20.1 MB
081_listRecReduction 👍 👍 0.633 ms 23.9 MB
082_RBTree.id_spec 👍 👍 0.844 ms 27.6 MB
083_And.right 👍 👍 0.509 ms 17.8 MB
084_Prod.snd 👍 👍 0.514 ms 17.6 MB
085_PProd.snd 👍 👍 0.514 ms 18.0 MB
086_PSigma.snd 👍 👍 0.521 ms 15.8 MB
087_projOutOfRange ✋ ✋ 0.496 ms 15.7 MB
088_projNotStruct ✋ ✋ 0.487 ms 15.9 MB
089_projProp1 👍 👍 0.547 ms 17.9 MB
090_projProp2 ✋ ✋ 0.540 ms 17.7 MB
091_projProp3 👍 👍 0.551 ms 19.9 MB
092_projProp4 ✋ ✋ 0.551 ms 20.1 MB
093_projProp5 ✋ ✋ 0.558 ms 20.0 MB
094_projProp6 ✋ ✋ 0.556 ms 18.1 MB
095_projDataIndexRec 👍 👍 0.547 ms 20.0 MB
096_projIndexData ✋ ✋ 0.597 ms 21.9 MB
097_projIndexData2 ✋ ✋ 0.594 ms 21.7 MB
098_projRed 👍 👍 0.577 ms 25.8 MB
099_ruleK 👍 👍 0.534 ms 17.7 MB
100_ruleKbad ✋ ✋ 0.536 ms 17.9 MB
101_ruleKAcc ✋ ✋ 0.595 ms 22.0 MB
102_aNatLit 👍 👍 0.485 ms 16.0 MB
103_natLitEq 👍 👍 0.531 ms 19.7 MB
104_proofIrrelevance 👍 👍 0.518 ms 17.9 MB
105_proofIrrelevanceBad ✋ ✋ 0.507 ms 17.8 MB
106_proofIrrelevanceWhnf 👍 👍 0.523 ms 17.6 MB
107_proofIrrelevanceUnderBinder 👍 👍 0.492 ms 13.8 MB
108_unitEta1 👍 👍 0.542 ms 21.9 MB
109_unitEta2 👍 👍 0.539 ms 21.9 MB
110_unitEta3 👍 👍 0.538 ms 19.8 MB
111_indexedUnitEta ✋ ✋ 0.545 ms 20.3 MB
112_structEta 👍 👍 0.593 ms 21.9 MB
113_indexedStructEta ✋ ✋ 0.567 ms 20.0 MB
114_funEta 👍 👍 0.522 ms 18.1 MB
115_funEtaDep 👍 👍 0.523 ms 17.8 MB
116_funEtaBad ✋ ✋ 0.511 ms 18.0 MB
117_reflOccLeft ✋ ✋ 0.499 ms 19.9 MB
118_reflOccInIndex ✋ ✋ 0.500 ms 15.8 MB
119_reduceCtorParamRefl.mk 👍 👍 0.506 ms 15.7 MB
120_reduceCtorParamRefl2.mk 👍 👍 0.506 ms 15.7 MB
121_rTreeRec 👍 👍 0.529 ms 19.9 MB
122_rtreeRecReduction 👍 👍 0.583 ms 25.9 MB
123_accRecType 👍 👍 0.538 ms 17.8 MB
124_accRecReduction 👍 👍 0.609 ms 22.3 MB
125_accRecNoEta ✋ ✋ 0.596 ms 20.4 MB
126_quotMkType 👍 👍 0.612 ms 17.6 MB
127_quotIndType 👍 👍 0.610 ms 15.7 MB
128_quotLiftType 👍 👍 0.614 ms 17.6 MB
129_quotSoundType 👍 👍 0.626 ms 22.1 MB
130_quotLiftReduction 👍 👍 0.623 ms 17.7 MB
131_quotIndReduction 👍 👍 0.619 ms 19.8 MB
132_dup_defs ✋ ✋ 0.424 ms 8.4 MB
133_dup_ind_def ✋ ✋ 0.433 ms 10.5 MB
134_dup_ctor_def ✋ ✋ 0.433 ms 10.4 MB
135_dup_rec_def ✋ ✋ 0.434 ms 10.6 MB
136_misnamed_rec_user ✋ ✋ 0.488 ms 15.8 MB
137_dup_rec_def2 ✋ ✋ 0.471 ms 11.8 MB
138_dup_ctor_rec ✋ ✋ 0.432 ms 10.5 MB
139_DupConCon ✋ ✋ 0.435 ms 10.4 MB
140_falseFromUnsafe ✋ ✋ 0.432 ms 10.6 MB
141_falseFromPartial ✋ ✋ 0.432 ms 10.4 MB