Lean Kernel Arena / tenet

Checker "tenet"

Version: 0.11.3 · 📄 Declaration · 🔗 Source

Tenet is an independent implementation of the Lean 4 kernel in C# on .NET, written from the type theory and the reference kernel's behavior rather than translated from it. It shares no code with Lean, which is the point of it: a defect in the C++ kernel's code is one Tenet would not reproduce. A defect in its design is one it likely would, since matching the reference kernel's decisions was the goal.

It reads lean4export NDJSON and also reads Lean's compiled .olean files directly, with no Lean toolchain installed.

Everywhere Tenet deliberately decides something differently from Lean is written down in docs/divergences.md. Two are relevant here: it checks that the constant named Nat.add behaves like addition before taking the arithmetic shortcut named after it, and it refuses a numeric literal unless the environment's Nat is the inductive the literal denotes. Both are extra checks on the prelude of the kind the arena's README permits.

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 👍 👍 2.50 min (+6%) 3.4 GB (×2.5)
con-leche 👍 👍 2.38 min (+29%) 3.6 GB (×4.3)
cslib 👍 👍 8.58 min (-1%) 5.5 GB (+62%)
init 👍 👍 68.5 s (+4%) 2.7 GB (×4.9)
init-prelude 👍 👍 568 ms (+57%) 127.8 MB (+74%)
mathlib 👍 👍 44.2 min (+37%) 11.6 GB (+16%)
navier-stokes-euler 👍 👍 18.5 min (+64%) 6.6 GB (×2.7)
reachability 👍 👍 46.1 s (+96%) 6.5 GB (×4.0)
std 👍 👍 1.97 min (+5%) 2.9 GB (×3.2)
26 3.67 s 52.6 MB
closure-level-subst ✋ ✋ 116 ms 44.5 MB
constlevels ✋ ✋ 140 ms 44.8 MB
ctor-num-fields ✋ ✋ 140 ms 45.4 MB
eta-ctor-alias ✋ ✋ 136 ms 44.3 MB
forged-quot-ind ✋ ✋ 136 ms 44.6 MB
k-rec-conv ✋ ✋ 144 ms 44.8 MB
large-elim-param ✋ ✋ 132 ms 44.6 MB
large-elim-prop-bool ✋ ✋ 136 ms 45.0 MB
level-imax-leq ✋ ✋ 134 ms 44.6 MB
level-imax-normalization ✋ ✋ 135 ms 45.0 MB
loose-bvar-value ✋ ✋ 122 ms 44.4 MB
nat-rec-k-lie ✋ ✋ 142 ms 44.9 MB
nat-rec-rules ✋ ✋ 143 ms 45.4 MB
nested-name-capture ✋ ✋ 139 ms 44.9 MB
nested-rec-rule-nfields ✋ ✋ 143 ms 45.5 MB
nested-unused-param ✋ ✋ 157 ms 46.7 MB
orphan-rec ✋ ✋ 119 ms 43.7 MB
pi-closure-context ✋ ✋ 111 ms 44.1 MB
proj-non-structure ✋ ✋ 131 ms 44.4 MB
proj-of-imax-prop ✋ ✋ 139 ms 45.0 MB
proj-of-stuck-prop ✋ ✋ 180 ms 52.6 MB
proj-of-subst-prop ✋ ✋ 175 ms 51.6 MB
rec-k-lie ✋ ✋ 132 ms 44.8 MB
rec-missing-ih ✋ ✋ 179 ms 52.3 MB
rec-of-subst-prop ✋ ✋ 178 ms 51.6 MB
unit-rec-rule ✋ ✋ 132 ms 44.6 MB
1 80.8 s 549.9 MB
alg-conv-trans-acc 🤷 ✋ 153 ms 47.1 MB
alg-conv-trans-acc-left 🤷 👍 148 ms 46.3 MB
alg-conv-trans-acc-right 🤷 👍 149 ms 46.6 MB
alg-conv-trans-quot 🤷 ✋ 138 ms 45.0 MB
alg-conv-trans-quot-left 🤷 ✋ 137 ms 44.9 MB
alg-conv-trans-quot-left-def 🤷 👍 134 ms 44.3 MB
alg-conv-trans-quot-right 🤷 👍 134 ms 44.3 MB
eta-ctor 🤷 ✋ 136 ms 45.0 MB
eta-rec-struct 🤷 ✋ 137 ms 45.0 MB
eta-rule-k 🤷 ✋ 134 ms 44.9 MB
eta-struct-major-and 🤷 ✋ 136 ms 44.9 MB
eta-struct-major-and-no-whnf 🤷 ✋ 38.5 s 549.9 MB
eta-struct-major-no-whnf 🤷 ✋ 38.4 s 538.8 MB
eta-unit-like-nested 🤷 ✋ 140 ms 44.6 MB
eta-unit-like-pi 🤷 ✋ 135 ms 44.5 MB
eta-unit-like-proof-field 🤷 ✋ 135 ms 45.3 MB
eta-unit-like-struct 🤷 ✋ 136 ms 44.9 MB
imax-nested-absorption 🤷 ✋ 100 ms 43.4 MB
imax-right-successor 🤷 ✋ 100 ms 43.6 MB
large-elim-maybe-prop 🤷 ✋ 131 ms 44.3 MB
let-value-type-mismatch 🤷 ✋ 100 ms 43.8 MB
nested-nonuniform-param 🤷 ✋ 129 ms 44.4 MB
nested-redex-aux 🤷 👍 150 ms 46.0 MB
positivity-whnf 🤷 ✋ 131 ms 44.0 MB
proj-maybe-prop 🤷 👍 131 ms 43.8 MB
proj-maybe-prop-past 🤷 👍 131 ms 44.1 MB
proof-param-ok 👍 👍 124 ms 43.7 MB
proof-param-swap 🤷 ✋ 97.6 ms 43.7 MB
subject-reduction-redex 🤷 👍 148 ms 46.2 MB
subject-reduction-reduct 🤷 ✋ 152 ms 47.1 MB
vanishing-occurrence 🤷 👍 130 ms 44.6 MB
10 1.25 s 45.5 MB
extra-rec ✋ ✋ 119 ms 44.4 MB
inductive-undeclared-universe ✋ ✋ 115 ms 44.3 MB
level-index-out-of-order 👍 👍 90.9 ms 42.9 MB
nat-lit-add 👍 👍 144 ms 45.4 MB
nat-lit-add-bad ✋ ✋ 149 ms 45.5 MB
nat-lit-ble 👍 👍 145 ms 45.3 MB
nat-lit-sub 👍 👍 144 ms 44.9 MB
orphan-ctor ✋ ✋ 120 ms 44.7 MB
proj-of-prop ✋ ✋ 132 ms 44.4 MB
sparse-name-index 👍 👍 90.9 ms 42.7 MB
31 2.52 min (+87%) 11.9 GB
app-lam 👍 👍 5.99 s (+23%) 1.7 GB (+20%)
args-before-unfold 👍 👍 147 ms (×4.1) 47.9 MB (-27%)
beta-ladder 👍 👍 2.57 s (+54%) 574.4 MB (+15%)
church-numerals 👍 👍 182 ms (×3.9) 57.9 MB (-26%)
discarded-argument 👍 👍 153 ms (-8%) 48.8 MB (-26%)
discarded-argument-match 👍 👍 195 ms (+37%) 57.8 MB (-15%)
folded-constant-first 👍 👍 160 ms (×3.9) 51.8 MB (-25%)
folded-constant-last 👍 👍 160 ms (×3.9) 51.7 MB (-25%)
fueled-chain 👍 👍 319 ms (×2.5) 73.1 MB (-3%)
grind-ring-5 👍 👍 3.56 s (+66%) 555.8 MB (×2.4)
identical-nesting 👍 👍 131 ms (×4.6) 44.2 MB (-33%)
irrelevance-before-evaluation 👍 👍 133 ms (×4.6) 44.3 MB (-33%)
irrelevance-refutes 👍 👍 141 ms (×4.9) 44.7 MB (-33%)
let-fold 👍 👍 182 ms (×3.1) 53.0 MB (-20%)
let-ladder 👍 👍 1.46 s (+44%) 330.4 MB (+3%)
magma-list-deep-n21 👍 👍 3.41 s (+26%) 1.3 GB (+93%)
magma-list-deep-n36 👍 👍 76.7 s (×2.2) 11.9 GB (+52%)
magma-list-pair-n21 👍 👍 31.3 s (+69%) 6.1 GB (+54%)
magma-list-pair-n7 👍 👍 2.41 s (+43%) 777.9 MB (+83%)
magma-string-n4 👍 👍 6.56 s (+85%) 669.5 MB (×5.5)
magma-string-pair-n9 👍 👍 13.3 s (+62%) 2.2 GB (×2.3)
proj-cheap-struct 👍 👍 148 ms (×4.3) 46.4 MB (-29%)
proj-lazy-struct 👍 👍 144 ms (×4.6) 45.7 MB (-31%)
proj-stuck-struct 👍 👍 145 ms (×4.6) 45.0 MB (-31%)
prop-struct-projections 👍 👍 314 ms (×3.2) 70.5 MB (+1%)
refute-cheap-first ✋ ✋ 141 ms (×3.4) 45.1 MB (-35%)
refute-cheap-last ✋ ✋ 570 ms (×3.2) 119.4 MB (+73%)
repeated-subproblem 👍 👍 134 ms (×4.7) 44.4 MB (-33%)
shared-subterm 👍 👍 202 ms (×3.5) 60.7 MB (-17%)
shift-cascade 👍 👍 151 ms (×3.3) 51.5 MB (-24%)
unroll-versus-evaluate 👍 👍 135 ms (×4.3) 44.5 MB (-33%)
141 16.8 s 45.4 MB
001_basicDef 👍 👍 94.1 ms 43.1 MB
002_badDef ✋ ✋ 99.3 ms 43.4 MB
003_arrowType 👍 👍 96.9 ms 43.0 MB
004_dependentType 👍 👍 98.5 ms 43.6 MB
005_constType 👍 👍 99.3 ms 43.4 MB
006_betaReduction 👍 👍 107 ms 43.5 MB
007_betaReduction2 👍 👍 107 ms 43.5 MB
008_forallSortWhnf 👍 👍 109 ms 43.2 MB
009_forallSortBad ✋ ✋ 113 ms 44.2 MB
010_nonTypeType ✋ ✋ 105 ms 44.2 MB
011_nonTypeAxiom ✋ ✋ 105 ms 44.1 MB
012_nonPropThm ✋ ✋ 96.6 ms 43.6 MB
013_thmProof 👍 👍 104 ms 43.5 MB
014_selfProof ✋ ✋ 90.4 ms 43.4 MB
015_levelComp1 👍 👍 95.2 ms 43.0 MB
016_levelComp2 👍 👍 95.4 ms 42.9 MB
017_levelComp3 👍 👍 95.4 ms 43.3 MB
018_levelParams 👍 👍 110 ms 43.8 MB
019_tut06_bad01 ✋ ✋ 93.6 ms 43.0 MB
020_levelComp4 👍 👍 93.9 ms 43.2 MB
021_levelComp5 👍 👍 94.2 ms 43.4 MB
022_imax1 👍 👍 101 ms 43.2 MB
023_imax2 👍 👍 101 ms 43.3 MB
024_levelMaxComm 👍 👍 95.8 ms 43.2 MB
025_levelMaxAssoc 👍 👍 95.8 ms 42.8 MB
026_levelMaxIdem 👍 👍 95.4 ms 43.1 MB
027_levelMaxAbsorb 👍 👍 96.0 ms 43.1 MB
028_inferVar 👍 👍 99.7 ms 43.3 MB
029_defEqLambda 👍 👍 104 ms 43.4 MB
030_peano1 👍 👍 112 ms 43.3 MB
031_peano2 👍 👍 113 ms 43.3 MB
032_peano3 👍 👍 113 ms 43.8 MB
033_letType 👍 👍 99.5 ms 43.1 MB
034_letTypeDep 👍 👍 106 ms 43.7 MB
035_letRed 👍 👍 101 ms 43.6 MB
036_empty 👍 👍 118 ms 43.7 MB
037_boolType 👍 👍 126 ms 44.0 MB
038_twoBool 👍 👍 127 ms 43.9 MB
039_andType 👍 👍 127 ms 44.0 MB
040_prodType 👍 👍 129 ms 44.1 MB
041_pprodType 👍 👍 129 ms 44.1 MB
042_pUnitType 👍 👍 126 ms 43.7 MB
043_eqType 👍 👍 128 ms 43.8 MB
044_natDef 👍 👍 128 ms 43.8 MB
045_rbTreeDef 👍 👍 131 ms 44.4 MB
046_inductBadNonSort ✋ ✋ 113 ms 44.2 MB
047_inductBadNonSort2 ✋ ✋ 103 ms 43.7 MB
048_inductLevelParam ✋ ✋ 96.1 ms 43.5 MB
049_inductTooFewParams ✋ ✋ 96.7 ms 43.3 MB
050_inductWrongCtorParams ✋ ✋ 99.7 ms 43.5 MB
051_inductWrongCtorResParams ✋ ✋ 97.6 ms 43.8 MB
052_inductWrongCtorResLevel ✋ ✋ 98.7 ms 43.6 MB
053_inductInIndex ✋ ✋ 113 ms 43.7 MB
054_indNeg ✋ ✋ 110 ms 44.3 MB
055_reduceCtorParam.mk 👍 👍 131 ms 44.2 MB
056_reduceCtorType.mk ✋ ✋ 117 ms 44.1 MB
057_indNegReducible ✋ ✋ 118 ms 44.1 MB
058_predWithTypeField 👍 👍 126 ms 43.9 MB
059_typeWithTypeField 👍 👍 127 ms 44.1 MB
060_typeWithTypeFieldPoly 👍 👍 128 ms 44.1 MB
061_typeWithTooHighTypeField.mk ✋ ✋ 109 ms 44.1 MB
062_emptyRec 👍 👍 120 ms 43.9 MB
063_boolRec 👍 👍 127 ms 44.0 MB
064_twoBoolRec 👍 👍 129 ms 43.8 MB
065_andRec 👍 👍 128 ms 44.2 MB
066_prodRec 👍 👍 130 ms 44.2 MB
067_pprodRec 👍 👍 130 ms 44.2 MB
068_punitRec 👍 👍 127 ms 43.5 MB
069_eqRec 👍 👍 128 ms 43.8 MB
070_nRec 👍 👍 128 ms 43.8 MB
071_rbTreeRef 👍 👍 131 ms 44.6 MB
072_boolPropRec 👍 👍 125 ms 43.5 MB
073_BogusRecursor ✋ ✋ 127 ms 44.1 MB
074_existsRec 👍 👍 129 ms 44.1 MB
075_typeSingletonRecReduction 👍 👍 131 ms 44.3 MB
076_sortElimPropRec 👍 👍 129 ms 44.2 MB
077_sortElimProp2Rec 👍 👍 131 ms 44.1 MB
078_boolRecEqns 👍 👍 131 ms 44.4 MB
079_prodRecEqns 👍 👍 132 ms 44.4 MB
080_nRecReduction 👍 👍 133 ms 44.3 MB
081_listRecReduction 👍 👍 134 ms 44.1 MB
082_RBTree.id_spec 👍 👍 138 ms 45.4 MB
083_And.right 👍 👍 128 ms 44.0 MB
084_Prod.snd 👍 👍 130 ms 44.3 MB
085_PProd.snd 👍 👍 130 ms 44.4 MB
086_PSigma.snd 👍 👍 132 ms 43.9 MB
087_projOutOfRange ✋ ✋ 132 ms 44.6 MB
088_projNotStruct ✋ ✋ 132 ms 44.1 MB
089_projProp1 👍 👍 131 ms 44.0 MB
090_projProp2 ✋ ✋ 135 ms 44.7 MB
091_projProp3 👍 👍 132 ms 44.2 MB
092_projProp4 ✋ ✋ 135 ms 44.4 MB
093_projProp5 ✋ ✋ 134 ms 44.4 MB
094_projProp6 ✋ ✋ 135 ms 44.4 MB
095_projDataIndexRec 👍 👍 129 ms 43.7 MB
096_projIndexData ✋ ✋ 136 ms 45.1 MB
097_projIndexData2 ✋ ✋ 136 ms 44.8 MB
098_projRed 👍 👍 133 ms 44.4 MB
099_ruleK 👍 👍 130 ms 43.8 MB
100_ruleKbad ✋ ✋ 134 ms 43.9 MB
101_ruleKAcc ✋ ✋ 137 ms 44.9 MB
102_aNatLit 👍 👍 134 ms 44.1 MB
103_natLitEq 👍 👍 136 ms 44.2 MB
104_proofIrrelevance 👍 👍 130 ms 43.8 MB
105_proofIrrelevanceBad ✋ ✋ 134 ms 44.5 MB
106_proofIrrelevanceWhnf 👍 👍 130 ms 44.3 MB
107_proofIrrelevanceUnderBinder 👍 👍 106 ms 43.5 MB
108_unitEta1 👍 👍 131 ms 44.2 MB
109_unitEta2 👍 👍 131 ms 44.2 MB
110_unitEta3 👍 👍 130 ms 44.1 MB
111_indexedUnitEta ✋ ✋ 135 ms 44.8 MB
112_structEta 👍 👍 134 ms 44.3 MB
113_indexedStructEta ✋ ✋ 136 ms 44.7 MB
114_funEta 👍 👍 130 ms 44.3 MB
115_funEtaDep 👍 👍 130 ms 43.9 MB
116_funEtaBad ✋ ✋ 134 ms 44.3 MB
117_reflOccLeft ✋ ✋ 131 ms 44.5 MB
118_reflOccInIndex ✋ ✋ 134 ms 44.5 MB
119_reduceCtorParamRefl.mk 👍 👍 131 ms 44.1 MB
120_reduceCtorParamRefl2.mk 👍 👍 131 ms 43.8 MB
121_rTreeRec 👍 👍 129 ms 44.0 MB
122_rtreeRecReduction 👍 👍 133 ms 43.6 MB
123_accRecType 👍 👍 130 ms 44.3 MB
124_accRecReduction 👍 👍 133 ms 44.1 MB
125_accRecNoEta ✋ ✋ 137 ms 44.8 MB
126_quotMkType 👍 👍 131 ms 44.0 MB
127_quotIndType 👍 👍 132 ms 44.2 MB
128_quotLiftType 👍 👍 131 ms 43.7 MB
129_quotSoundType 👍 👍 132 ms 44.3 MB
130_quotLiftReduction 👍 👍 133 ms 44.0 MB
131_quotIndReduction 👍 👍 133 ms 44.1 MB
132_dup_defs ✋ ✋ 96.7 ms 43.0 MB
133_dup_ind_def ✋ ✋ 98.8 ms 43.3 MB
134_dup_ctor_def ✋ ✋ 98.8 ms 43.5 MB
135_dup_rec_def ✋ ✋ 98.8 ms 43.3 MB
136_misnamed_rec_user ✋ ✋ 128 ms 44.6 MB
137_dup_rec_def2 ✋ ✋ 109 ms 44.0 MB
138_dup_ctor_rec ✋ ✋ 85.6 ms 43.1 MB
139_DupConCon ✋ ✋ 85.3 ms 42.8 MB
140_falseFromUnsafe ✋ ✋ 121 ms 43.9 MB
141_falseFromPartial ✋ ✋ 121 ms 43.9 MB