Lean Kernel Arena / kefir

Checker "kefir"

Version: e00bbd5 · 📄 Declaration · 🔗 Source

Kernel Enforcing Formal Inference Rules — an independent external proof checker for Lean 4, in Rust, built for low peak memory. Declarations are checked as they stream in and their terms are freed once checked; expressions are stored compactly, and most caches are small fixed-size tables that overwrite on collision. Conversion runs on an environment-based evaluator with call-by-need sharing; anything it cannot confirm is rechecked by a substitution-based checker. Hot definitions get reduction rules derived from their own bodies. Recursors are re-derived and must match the export exactly. Single-threaded.

Soundness (rightfully rejected tests)

80 ✅ 0 ❌ 0 🚫

Completeness (rightfully accepted tests)

138 ✅ 0 ❌ 0 🚫

Corner cases (no outcome prescribed)

30 ✅ 0 🚫

Test Expected Result ⏱️ 🧠
cedar 👍 👍 41.0 s (÷3.4) 415.1 MB (÷3.3)
con-leche 👍 👍 38.0 s (÷2.9) 325.3 MB (÷2.6)
cslib 👍 👍 2.07 min (÷4.2) 995.9 MB (÷3.5)
init 👍 👍 16.7 s (÷4.0) 211.6 MB (÷2.7)
init-prelude 👍 👍 108 ms (÷3.4) 13.6 MB (÷5.4)
mathlib 👍 👍 6.18 min (÷5.2) 2.3 GB (÷4.2)
navier-stokes-euler 👍 👍 2.02 min (÷5.6) 635.3 MB (÷4.0)
reachability 👍 👍 3.28 s (÷7.2) 354.2 MB (÷4.7)
std 👍 👍 30.2 s (÷3.7) 307.0 MB (÷3.0)
26 62.4 ms 8.5 MB
closure-level-subst ✋ ✋ 0.444 ms 5.8 MB
constlevels ✋ ✋ 0.972 ms 6.5 MB
ctor-num-fields ✋ ✋ 1.01 ms 6.1 MB
eta-ctor-alias ✋ ✋ 0.776 ms 6.4 MB
forged-quot-ind ✋ ✋ 0.855 ms 6.2 MB
k-rec-conv ✋ ✋ 1.10 ms 6.4 MB
large-elim-param ✋ ✋ 0.548 ms 6.2 MB
large-elim-prop-bool ✋ ✋ 0.873 ms 6.3 MB
level-imax-leq ✋ ✋ 0.425 ms 5.5 MB
level-imax-normalization ✋ ✋ 0.611 ms 6.0 MB
loose-bvar-value ✋ ✋ 0.395 ms 5.0 MB
nat-rec-k-lie ✋ ✋ 0.447 ms 6.0 MB
nat-rec-rules ✋ ✋ 0.437 ms 5.5 MB
nested-name-capture ✋ ✋ 1.70 ms 6.4 MB
nested-rec-rule-nfields ✋ ✋ 1.85 ms 6.4 MB
nested-unused-param ✋ ✋ 2.62 ms 6.5 MB
orphan-rec ✋ ✋ 0.399 ms 5.2 MB
pi-closure-context ✋ ✋ 0.417 ms 5.8 MB
proj-non-structure ✋ ✋ 0.601 ms 6.3 MB
proj-of-imax-prop ✋ ✋ 0.996 ms 6.5 MB
proj-of-stuck-prop ✋ ✋ 10.6 ms 8.3 MB
proj-of-subst-prop ✋ ✋ 11.0 ms 8.2 MB
rec-k-lie ✋ ✋ 0.413 ms 5.5 MB
rec-missing-ih ✋ ✋ 10.8 ms 8.5 MB
rec-of-subst-prop ✋ ✋ 11.7 ms 8.0 MB
unit-rec-rule ✋ ✋ 0.450 ms 5.8 MB
1 44.1 ms 7.0 MB
alg-conv-trans-acc 🤷 ✋ 4.11 ms 6.8 MB
alg-conv-trans-acc-left 🤷 👍 3.94 ms 6.7 MB
alg-conv-trans-acc-right 🤷 👍 3.97 ms 6.6 MB
alg-conv-trans-quot 🤷 ✋ 0.882 ms 6.3 MB
alg-conv-trans-quot-left 🤷 ✋ 0.898 ms 6.4 MB
alg-conv-trans-quot-left-def 🤷 👍 0.782 ms 6.0 MB
alg-conv-trans-quot-right 🤷 👍 0.735 ms 6.4 MB
eta-ctor 🤷 ✋ 0.858 ms 6.4 MB
eta-rec-struct 🤷 ✋ 0.953 ms 6.3 MB
eta-rule-k 🤷 ✋ 0.748 ms 6.4 MB
eta-struct-major-and 🤷 👍 0.762 ms 6.1 MB
eta-struct-major-and-no-whnf 🤷 👍 1.45 ms 6.4 MB
eta-struct-major-no-whnf 🤷 👍 1.90 ms 6.6 MB
eta-unit-like-nested 🤷 ✋ 1.28 ms 6.3 MB
eta-unit-like-pi 🤷 ✋ 0.716 ms 6.4 MB
eta-unit-like-proof-field 🤷 ✋ 0.732 ms 6.3 MB
eta-unit-like-struct 🤷 ✋ 0.754 ms 6.4 MB
imax-nested-absorption 🤷 ✋ 0.401 ms 5.6 MB
imax-right-successor 🤷 ✋ 0.402 ms 5.6 MB
large-elim-maybe-prop 🤷 ✋ 0.424 ms 5.7 MB
let-value-type-mismatch 🤷 ✋ 0.399 ms 5.4 MB
nested-nonuniform-param 🤷 ✋ 0.662 ms 6.3 MB
nested-redex-aux 🤷 👍 4.66 ms 6.7 MB
positivity-whnf 🤷 ✋ 0.554 ms 6.3 MB
proj-maybe-prop 🤷 👍 0.861 ms 6.3 MB
proj-maybe-prop-past 🤷 👍 0.861 ms 6.4 MB
proof-param-ok 👍 👍 0.520 ms 6.1 MB
proof-param-swap 🤷 ✋ 0.408 ms 5.2 MB
subject-reduction-redex 🤷 👍 3.85 ms 6.5 MB
subject-reduction-reduct 🤷 ✋ 3.98 ms 7.0 MB
vanishing-occurrence 🤷 ✋ 0.585 ms 6.4 MB
10 9.35 ms 6.6 MB
extra-rec ✋ ✋ 0.399 ms 4.9 MB
inductive-undeclared-universe ✋ ✋ 0.415 ms 5.0 MB
level-index-out-of-order 👍 👍 0.396 ms 5.5 MB
nat-lit-add 👍 👍 1.63 ms 6.3 MB
nat-lit-add-bad ✋ ✋ 1.68 ms 6.6 MB
nat-lit-ble 👍 👍 1.74 ms 6.4 MB
nat-lit-sub 👍 👍 1.73 ms 6.2 MB
orphan-ctor ✋ ✋ 0.400 ms 4.9 MB
proj-of-prop ✋ ✋ 0.559 ms 6.4 MB
sparse-name-index 👍 👍 0.395 ms 5.5 MB
31 6.57 s (÷12) 988.7 MB
app-lam 👍 👍 37.7 ms (÷129) 27.0 MB (÷53)
args-before-unfold 👍 👍 2.82 ms (÷13) 9.4 MB (÷7.0)
beta-ladder 👍 👍 16.4 ms (÷102) 18.7 MB (÷27)
church-numerals 👍 👍 9.93 ms (÷4.7) 27.8 MB (÷2.8)
discarded-argument 👍 👍 0.821 ms (÷202) 6.5 MB (÷10)
discarded-argument-match 👍 👍 1.38 ms (÷103) 6.5 MB (÷10)
folded-constant-first 👍 👍 3.33 ms (÷12) 10.2 MB (÷6.8)
folded-constant-last 👍 👍 3.33 ms (÷12) 10.1 MB (÷6.8)
fueled-chain 👍 👍 37.6 ms (÷3.4) 22.9 MB (÷3.3)
grind-ring-5 👍 👍 529 ms (÷4.1) 152.0 MB (-33%)
identical-nesting 👍 👍 0.723 ms (÷39) 6.3 MB (÷10)
irrelevance-before-evaluation 👍 👍 0.889 ms (÷32) 6.6 MB (÷10)
irrelevance-refutes 👍 👍 1.02 ms (÷28) 6.3 MB (÷11)
let-fold 👍 👍 13.0 ms (÷4.5) 8.7 MB (÷7.6)
let-ladder 👍 👍 12.7 ms (÷80) 16.4 MB (÷19)
magma-list-deep-n21 👍 👍 79.6 ms (÷34) 31.1 MB (÷21)
magma-list-deep-n36 👍 👍 451 ms (÷78) 74.4 MB (÷108)
magma-list-pair-n21 👍 👍 2.87 s (÷6.4) 988.7 MB (÷4.1)
magma-list-pair-n7 👍 👍 247 ms (÷6.8) 131.5 MB (÷3.2)
magma-string-n4 👍 👍 795 ms (÷4.5) 82.3 MB (-32%)
magma-string-pair-n9 👍 👍 1.36 s (÷6.0) 232.9 MB (÷4.3)
proj-cheap-struct 👍 👍 4.14 ms (÷8.4) 6.5 MB (÷10)
proj-lazy-struct 👍 👍 2.58 ms (÷12) 6.3 MB (÷10)
proj-stuck-struct 👍 👍 2.68 ms (÷12) 6.4 MB (÷10)
prop-struct-projections 👍 👍 65.8 ms (-34%) 13.2 MB (÷5.3)
refute-cheap-first ✋ ✋ 1.44 ms (÷29) 6.7 MB (÷10)
refute-cheap-last ✋ ✋ 1.41 ms (÷128) 6.5 MB (÷11)
repeated-subproblem 👍 👍 0.917 ms (÷31) 6.4 MB (÷10)
shared-subterm 👍 👍 15.9 ms (÷3.6) 21.6 MB (÷3.4)
shift-cascade 👍 👍 3.68 ms (÷12) 7.2 MB (÷9.4)
unroll-versus-evaluate 👍 👍 1.25 ms (÷25) 8.1 MB (÷8.2)
141 84.4 ms 6.7 MB
001_basicDef 👍 👍 0.396 ms 5.6 MB
002_badDef ✋ ✋ 0.398 ms 5.6 MB
003_arrowType 👍 👍 0.398 ms 5.6 MB
004_dependentType 👍 👍 0.397 ms 5.7 MB
005_constType 👍 👍 0.401 ms 5.6 MB
006_betaReduction 👍 👍 0.408 ms 5.7 MB
007_betaReduction2 👍 👍 0.408 ms 5.8 MB
008_forallSortWhnf 👍 👍 0.411 ms 6.1 MB
009_forallSortBad ✋ ✋ 0.418 ms 6.0 MB
010_nonTypeType ✋ ✋ 0.404 ms 5.7 MB
011_nonTypeAxiom ✋ ✋ 0.404 ms 5.8 MB
012_nonPropThm ✋ ✋ 0.397 ms 5.6 MB
013_thmProof 👍 👍 0.408 ms 5.5 MB
014_selfProof ✋ ✋ 0.400 ms 5.5 MB
015_levelComp1 👍 👍 0.398 ms 5.5 MB
016_levelComp2 👍 👍 0.398 ms 5.7 MB
017_levelComp3 👍 👍 0.398 ms 5.4 MB
018_levelParams 👍 👍 0.410 ms 5.5 MB
019_tut06_bad01 ✋ ✋ 0.394 ms 5.1 MB
020_levelComp4 👍 👍 0.397 ms 5.7 MB
021_levelComp5 👍 👍 0.397 ms 5.5 MB
022_imax1 👍 👍 0.400 ms 5.6 MB
023_imax2 👍 👍 0.400 ms 5.6 MB
024_levelMaxComm 👍 👍 0.401 ms 5.7 MB
025_levelMaxAssoc 👍 👍 0.405 ms 5.6 MB
026_levelMaxIdem 👍 👍 0.399 ms 5.9 MB
027_levelMaxAbsorb 👍 👍 0.401 ms 5.6 MB
028_inferVar 👍 👍 0.399 ms 5.7 MB
029_defEqLambda 👍 👍 0.408 ms 5.7 MB
030_peano1 👍 👍 0.452 ms 5.7 MB
031_peano2 👍 👍 0.482 ms 5.7 MB
032_peano3 👍 👍 0.510 ms 6.0 MB
033_letType 👍 👍 0.397 ms 5.6 MB
034_letTypeDep 👍 👍 0.409 ms 5.7 MB
035_letRed 👍 👍 0.400 ms 5.7 MB
036_empty 👍 👍 0.417 ms 5.9 MB
037_boolType 👍 👍 0.504 ms 6.2 MB
038_twoBool 👍 👍 0.584 ms 6.0 MB
039_andType 👍 👍 0.536 ms 6.4 MB
040_prodType 👍 👍 0.594 ms 6.2 MB
041_pprodType 👍 👍 0.655 ms 6.4 MB
042_pUnitType 👍 👍 0.481 ms 6.2 MB
043_eqType 👍 👍 0.577 ms 6.3 MB
044_natDef 👍 👍 0.512 ms 6.0 MB
045_rbTreeDef 👍 👍 1.54 ms 6.2 MB
046_inductBadNonSort ✋ ✋ 0.403 ms 5.6 MB
047_inductBadNonSort2 ✋ ✋ 0.398 ms 5.6 MB
048_inductLevelParam ✋ ✋ 0.395 ms 5.0 MB
049_inductTooFewParams ✋ ✋ 0.395 ms 5.0 MB
050_inductWrongCtorParams ✋ ✋ 0.402 ms 5.4 MB
051_inductWrongCtorResParams ✋ ✋ 0.400 ms 5.0 MB
052_inductWrongCtorResLevel ✋ ✋ 0.402 ms 5.1 MB
053_inductInIndex ✋ ✋ 0.402 ms 5.6 MB
054_indNeg ✋ ✋ 0.401 ms 5.5 MB
055_reduceCtorParam.mk 👍 👍 0.579 ms 6.0 MB
056_reduceCtorType.mk ✋ ✋ 0.410 ms 6.1 MB
057_indNegReducible ✋ ✋ 0.412 ms 5.8 MB
058_predWithTypeField 👍 👍 0.461 ms 6.0 MB
059_typeWithTypeField 👍 👍 0.468 ms 5.9 MB
060_typeWithTypeFieldPoly 👍 👍 0.484 ms 6.1 MB
061_typeWithTooHighTypeField.mk ✋ ✋ 0.401 ms 5.2 MB
062_emptyRec 👍 👍 0.422 ms 5.9 MB
063_boolRec 👍 👍 0.517 ms 6.1 MB
064_twoBoolRec 👍 👍 0.598 ms 6.2 MB
065_andRec 👍 👍 0.549 ms 6.3 MB
066_prodRec 👍 👍 0.617 ms 6.1 MB
067_pprodRec 👍 👍 0.679 ms 6.3 MB
068_punitRec 👍 👍 0.494 ms 6.1 MB
069_eqRec 👍 👍 0.591 ms 6.1 MB
070_nRec 👍 👍 0.525 ms 6.0 MB
071_rbTreeRef 👍 👍 1.60 ms 6.2 MB
072_boolPropRec 👍 👍 0.468 ms 5.9 MB
073_BogusRecursor ✋ ✋ 0.429 ms 5.9 MB
074_existsRec 👍 👍 0.609 ms 6.2 MB
075_typeSingletonRecReduction 👍 👍 0.747 ms 6.4 MB
076_sortElimPropRec 👍 👍 0.678 ms 6.3 MB
077_sortElimProp2Rec 👍 👍 0.699 ms 6.4 MB
078_boolRecEqns 👍 👍 0.848 ms 6.3 MB
079_prodRecEqns 👍 👍 0.820 ms 6.3 MB
080_nRecReduction 👍 👍 0.885 ms 6.3 MB
081_listRecReduction 👍 👍 1.11 ms 6.3 MB
082_RBTree.id_spec 👍 👍 2.37 ms 6.5 MB
083_And.right 👍 👍 0.550 ms 6.2 MB
084_Prod.snd 👍 👍 0.610 ms 6.0 MB
085_PProd.snd 👍 👍 0.671 ms 6.3 MB
086_PSigma.snd 👍 👍 0.674 ms 6.4 MB
087_projOutOfRange ✋ ✋ 0.551 ms 6.2 MB
088_projNotStruct ✋ ✋ 0.517 ms 5.7 MB
089_projProp1 👍 👍 0.858 ms 6.3 MB
090_projProp2 ✋ ✋ 0.867 ms 6.0 MB
091_projProp3 👍 👍 0.868 ms 6.4 MB
092_projProp4 ✋ ✋ 0.867 ms 6.4 MB
093_projProp5 ✋ ✋ 0.870 ms 6.2 MB
094_projProp6 ✋ ✋ 0.867 ms 6.4 MB
095_projDataIndexRec 👍 👍 0.679 ms 6.3 MB
096_projIndexData ✋ ✋ 1.13 ms 6.2 MB
097_projIndexData2 ✋ ✋ 1.13 ms 6.2 MB
098_projRed 👍 👍 0.901 ms 6.3 MB
099_ruleK 👍 👍 0.695 ms 6.2 MB
100_ruleKbad ✋ ✋ 0.768 ms 6.4 MB
101_ruleKAcc ✋ ✋ 1.23 ms 6.6 MB
102_aNatLit 👍 👍 0.563 ms 6.3 MB
103_natLitEq 👍 👍 0.741 ms 6.4 MB
104_proofIrrelevance 👍 👍 0.599 ms 6.4 MB
105_proofIrrelevanceBad ✋ ✋ 0.622 ms 6.4 MB
106_proofIrrelevanceWhnf 👍 👍 0.611 ms 6.2 MB
107_proofIrrelevanceUnderBinder 👍 👍 0.423 ms 5.6 MB
108_unitEta1 👍 👍 0.683 ms 6.4 MB
109_unitEta2 👍 👍 0.677 ms 6.1 MB
110_unitEta3 👍 👍 0.676 ms 6.3 MB
111_indexedUnitEta ✋ ✋ 0.782 ms 6.5 MB
112_structEta 👍 👍 0.968 ms 6.4 MB
113_indexedStructEta ✋ ✋ 0.864 ms 6.4 MB
114_funEta 👍 👍 0.604 ms 6.3 MB
115_funEtaDep 👍 👍 0.605 ms 6.4 MB
116_funEtaBad ✋ ✋ 0.656 ms 6.4 MB
117_reflOccLeft ✋ ✋ 0.568 ms 6.4 MB
118_reflOccInIndex ✋ ✋ 0.567 ms 6.2 MB
119_reduceCtorParamRefl.mk 👍 👍 0.605 ms 6.2 MB
120_reduceCtorParamRefl2.mk 👍 👍 0.605 ms 6.3 MB
121_rTreeRec 👍 👍 0.654 ms 6.3 MB
122_rtreeRecReduction 👍 👍 0.858 ms 6.2 MB
123_accRecType 👍 👍 0.821 ms 6.3 MB
124_accRecReduction 👍 👍 1.09 ms 6.6 MB
125_accRecNoEta ✋ ✋ 1.22 ms 6.7 MB
126_quotMkType 👍 👍 0.678 ms 6.2 MB
127_quotIndType 👍 👍 0.688 ms 6.3 MB
128_quotLiftType 👍 👍 0.695 ms 6.4 MB
129_quotSoundType 👍 👍 0.716 ms 6.2 MB
130_quotLiftReduction 👍 👍 0.710 ms 6.3 MB
131_quotIndReduction 👍 👍 0.708 ms 6.4 MB
132_dup_defs ✋ ✋ 0.397 ms 5.8 MB
133_dup_ind_def ✋ ✋ 0.405 ms 5.6 MB
134_dup_ctor_def ✋ ✋ 0.410 ms 5.8 MB
135_dup_rec_def ✋ ✋ 0.414 ms 5.8 MB
136_misnamed_rec_user ✋ ✋ 0.401 ms 5.0 MB
137_dup_rec_def2 ✋ ✋ 0.415 ms 5.9 MB
138_dup_ctor_rec ✋ ✋ 0.401 ms 5.0 MB
139_DupConCon ✋ ✋ 0.404 ms 4.8 MB
140_falseFromUnsafe ✋ ✋ 0.430 ms 6.1 MB
141_falseFromPartial ✋ ✋ 0.425 ms 6.2 MB