Lean Kernel Arena / kefir-wasm

Checker "kefir-wasm"

Version: e00bbd5 · 📄 Declaration · 🔗 Source

kefir-wasm is the kefir checker built for wasm32-wasip1 from the same Rust source and commit as the kefir entry, and run under Node's WASI on V8. It uses the checking code and resource budgets of the native build, so its reports differ only in the build identity. The module can address at most 4 GiB of memory. The gap between the two entries is the cost of running the same Rust code as WebAssembly.

Declarations are checked in file order on one thread.

The build installs the pinned Rust toolchain with the wasm32-wasip1 standard library through rustup, local to the checkout.

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 👍 👍 62.1 s (÷2.3) 575.4 MB (÷2.4)
con-leche 👍 👍 56.0 s (-49%) 498.3 MB (-42%)
cslib 👍 👍 3.12 min (÷2.8) 1.1 GB (÷3.0)
init 👍 👍 25.6 s (÷2.6) 350.1 MB (-38%)
init-prelude 👍 👍 762 ms (×2.1) 114.8 MB (+56%)
mathlib 👍 👍 9.23 min (÷3.5) 2.5 GB (÷3.9)
navier-stokes-euler 👍 👍 2.97 min (÷3.8) 881.1 MB (÷2.9)
reachability 👍 👍 5.40 s (÷4.4) 636.2 MB (÷2.6)
std 👍 👍 45.7 s (÷2.5) 492.0 MB (-47%)
26 4.66 s 114.5 MB
closure-level-subst ✋ ✋ 109 ms 82.8 MB
constlevels ✋ ✋ 168 ms 103.5 MB
ctor-num-fields ✋ ✋ 160 ms 94.7 MB
eta-ctor-alias ✋ ✋ 137 ms 89.1 MB
forged-quot-ind ✋ ✋ 173 ms 101.7 MB
k-rec-conv ✋ ✋ 218 ms 107.6 MB
large-elim-param ✋ ✋ 106 ms 82.2 MB
large-elim-prop-bool ✋ ✋ 159 ms 92.6 MB
level-imax-leq ✋ ✋ 99.4 ms 81.9 MB
level-imax-normalization ✋ ✋ 113 ms 83.5 MB
loose-bvar-value ✋ ✋ 90.1 ms 81.1 MB
nat-rec-k-lie ✋ ✋ 105 ms 81.9 MB
nat-rec-rules ✋ ✋ 98.6 ms 81.3 MB
nested-name-capture ✋ ✋ 203 ms 107.9 MB
nested-rec-rule-nfields ✋ ✋ 217 ms 107.5 MB
nested-unused-param ✋ ✋ 212 ms 106.1 MB
orphan-rec ✋ ✋ 90.5 ms 80.8 MB
pi-closure-context ✋ ✋ 106 ms 82.8 MB
proj-non-structure ✋ ✋ 113 ms 83.3 MB
proj-of-imax-prop ✋ ✋ 158 ms 99.0 MB
proj-of-stuck-prop ✋ ✋ 415 ms 114.5 MB
proj-of-subst-prop ✋ ✋ 419 ms 109.6 MB
rec-k-lie ✋ ✋ 99.2 ms 81.8 MB
rec-missing-ih ✋ ✋ 361 ms 110.9 MB
rec-of-subst-prop ✋ ✋ 428 ms 112.3 MB
unit-rec-rule ✋ ✋ 104 ms 81.7 MB
1 4.98 s 111.5 MB
alg-conv-trans-acc 🤷 ✋ 272 ms 111.5 MB
alg-conv-trans-acc-left 🤷 👍 243 ms 108.5 MB
alg-conv-trans-acc-right 🤷 👍 220 ms 107.5 MB
alg-conv-trans-quot 🤷 ✋ 187 ms 105.6 MB
alg-conv-trans-quot-left 🤷 ✋ 187 ms 105.0 MB
alg-conv-trans-quot-left-def 🤷 👍 167 ms 103.7 MB
alg-conv-trans-quot-right 🤷 👍 168 ms 92.5 MB
eta-ctor 🤷 ✋ 162 ms 102.9 MB
eta-rec-struct 🤷 ✋ 170 ms 105.1 MB
eta-rule-k 🤷 ✋ 118 ms 83.5 MB
eta-struct-major-and 🤷 👍 151 ms 88.0 MB
eta-struct-major-and-no-whnf 🤷 👍 183 ms 98.9 MB
eta-struct-major-no-whnf 🤷 👍 196 ms 104.5 MB
eta-unit-like-nested 🤷 ✋ 177 ms 105.9 MB
eta-unit-like-pi 🤷 ✋ 120 ms 83.5 MB
eta-unit-like-proof-field 🤷 ✋ 130 ms 87.9 MB
eta-unit-like-struct 🤷 ✋ 134 ms 89.3 MB
imax-nested-absorption 🤷 ✋ 101 ms 82.3 MB
imax-right-successor 🤷 ✋ 102 ms 82.3 MB
large-elim-maybe-prop 🤷 ✋ 102 ms 82.2 MB
let-value-type-mismatch 🤷 ✋ 101 ms 82.3 MB
nested-nonuniform-param 🤷 ✋ 150 ms 90.2 MB
nested-redex-aux 🤷 👍 283 ms 110.1 MB
positivity-whnf 🤷 ✋ 109 ms 82.5 MB
proj-maybe-prop 🤷 👍 129 ms 86.8 MB
proj-maybe-prop-past 🤷 👍 127 ms 87.7 MB
proof-param-ok 👍 👍 107 ms 82.2 MB
proof-param-swap 🤷 ✋ 91.8 ms 81.1 MB
subject-reduction-redex 🤷 👍 210 ms 105.5 MB
subject-reduction-reduct 🤷 ✋ 272 ms 107.2 MB
vanishing-occurrence 🤷 ✋ 110 ms 82.2 MB
10 1.34 s 107.6 MB
extra-rec ✋ ✋ 90.5 ms 80.7 MB
inductive-undeclared-universe ✋ ✋ 92.7 ms 81.0 MB
level-index-out-of-order 👍 👍 93.5 ms 81.0 MB
nat-lit-add 👍 👍 188 ms 106.8 MB
nat-lit-add-bad ✋ ✋ 204 ms 107.6 MB
nat-lit-ble 👍 👍 185 ms 101.3 MB
nat-lit-sub 👍 👍 185 ms 105.0 MB
orphan-ctor ✋ ✋ 91.7 ms 80.8 MB
proj-of-prop ✋ ✋ 117 ms 83.7 MB
sparse-name-index 👍 👍 93.4 ms 80.9 MB
31 18.4 s (÷4.4) 1.7 GB
app-lam 👍 👍 309 ms (÷16) 119.1 MB (÷12)
args-before-unfold 👍 👍 195 ms (×5.4) 110.6 MB (+68%)
beta-ladder 👍 👍 268 ms (÷6.2) 115.1 MB (÷4.3)
church-numerals 👍 👍 222 ms (×4.7) 128.3 MB (+64%)
discarded-argument 👍 👍 167 ms (+1%) 93.6 MB (+42%)
discarded-argument-match 👍 👍 172 ms (+21%) 95.3 MB (+40%)
folded-constant-first 👍 👍 195 ms (×4.8) 110.1 MB (+60%)
folded-constant-last 👍 👍 210 ms (×5.2) 110.0 MB (+61%)
fueled-chain 👍 👍 478 ms (×3.8) 120.7 MB (+59%)
grind-ring-5 👍 👍 1.41 s (-35%) 321.8 MB (+41%)
identical-nesting 👍 👍 151 ms (×5.3) 87.9 MB (+33%)
irrelevance-before-evaluation 👍 👍 167 ms (×5.8) 93.8 MB (+43%)
irrelevance-refutes 👍 👍 160 ms (×5.6) 96.5 MB (+45%)
let-fold 👍 👍 363 ms (×6.3) 112.7 MB (+70%)
let-ladder 👍 👍 251 ms (÷4.0) 114.5 MB (÷2.8)
magma-list-deep-n21 👍 👍 565 ms (÷4.8) 132.9 MB (÷5.0)
magma-list-deep-n36 👍 👍 1.05 s (÷34) 193.3 MB (÷42)
magma-list-pair-n21 👍 👍 4.51 s (÷4.1) 1.7 GB (÷2.3)
magma-list-pair-n7 👍 👍 756 ms (÷2.2) 257.2 MB (-40%)
magma-string-n4 👍 👍 1.83 s (-48%) 211.1 MB (+74%)
magma-string-pair-n9 👍 👍 2.62 s (÷3.1) 398.1 MB (÷2.5)
proj-cheap-struct 👍 👍 197 ms (×5.7) 104.8 MB (+59%)
proj-lazy-struct 👍 👍 184 ms (×5.9) 104.7 MB (+59%)
proj-stuck-struct 👍 👍 206 ms (×6.5) 104.3 MB (+59%)
prop-struct-projections 👍 👍 500 ms (×5.0) 110.4 MB (+57%)
refute-cheap-first ✋ ✋ 217 ms (×5.2) 107.9 MB (+56%)
refute-cheap-last ✋ ✋ 233 ms (+29%) 109.0 MB (+58%)
repeated-subproblem 👍 👍 155 ms (×5.4) 96.0 MB (+46%)
shared-subterm 👍 👍 264 ms (×4.6) 119.6 MB (+64%)
shift-cascade 👍 👍 185 ms (×4.0) 106.9 MB (+58%)
unroll-versus-evaluate 👍 👍 173 ms (×5.6) 100.7 MB (+52%)
141 16.3 s 108.1 MB
001_basicDef 👍 👍 94.3 ms 81.1 MB
002_badDef ✋ ✋ 101 ms 82.3 MB
003_arrowType 👍 👍 94.5 ms 81.3 MB
004_dependentType 👍 👍 94.7 ms 81.3 MB
005_constType 👍 👍 95.4 ms 81.3 MB
006_betaReduction 👍 👍 96.9 ms 81.2 MB
007_betaReduction2 👍 👍 96.6 ms 81.5 MB
008_forallSortWhnf 👍 👍 97.5 ms 81.5 MB
009_forallSortBad ✋ ✋ 107 ms 83.3 MB
010_nonTypeType ✋ ✋ 99.6 ms 82.4 MB
011_nonTypeAxiom ✋ ✋ 101 ms 82.4 MB
012_nonPropThm ✋ ✋ 97.2 ms 81.7 MB
013_thmProof 👍 👍 96.1 ms 81.3 MB
014_selfProof ✋ ✋ 102 ms 82.1 MB
015_levelComp1 👍 👍 94.3 ms 81.2 MB
016_levelComp2 👍 👍 95.5 ms 81.1 MB
017_levelComp3 👍 👍 94.9 ms 80.9 MB
018_levelParams 👍 👍 97.7 ms 81.5 MB
019_tut06_bad01 ✋ ✋ 90.0 ms 80.9 MB
020_levelComp4 👍 👍 94.1 ms 81.2 MB
021_levelComp5 👍 👍 94.1 ms 81.7 MB
022_imax1 👍 👍 95.7 ms 81.4 MB
023_imax2 👍 👍 94.4 ms 81.5 MB
024_levelMaxComm 👍 👍 94.7 ms 81.2 MB
025_levelMaxAssoc 👍 👍 94.9 ms 81.0 MB
026_levelMaxIdem 👍 👍 95.2 ms 81.2 MB
027_levelMaxAbsorb 👍 👍 96.6 ms 81.4 MB
028_inferVar 👍 👍 94.2 ms 81.0 MB
029_defEqLambda 👍 👍 96.6 ms 81.3 MB
030_peano1 👍 👍 97.6 ms 81.1 MB
031_peano2 👍 👍 100 ms 81.7 MB
032_peano3 👍 👍 100 ms 81.5 MB
033_letType 👍 👍 94.4 ms 81.6 MB
034_letTypeDep 👍 👍 96.0 ms 81.4 MB
035_letRed 👍 👍 96.3 ms 81.2 MB
036_empty 👍 👍 103 ms 82.3 MB
037_boolType 👍 👍 108 ms 82.4 MB
038_twoBool 👍 👍 110 ms 82.4 MB
039_andType 👍 👍 109 ms 82.8 MB
040_prodType 👍 👍 109 ms 82.6 MB
041_pprodType 👍 👍 112 ms 82.4 MB
042_pUnitType 👍 👍 107 ms 82.2 MB
043_eqType 👍 👍 111 ms 82.5 MB
044_natDef 👍 👍 110 ms 82.1 MB
045_rbTreeDef 👍 👍 176 ms 104.9 MB
046_inductBadNonSort ✋ ✋ 97.2 ms 81.6 MB
047_inductBadNonSort2 ✋ ✋ 95.9 ms 81.0 MB
048_inductLevelParam ✋ ✋ 91.1 ms 81.0 MB
049_inductTooFewParams ✋ ✋ 91.1 ms 80.6 MB
050_inductWrongCtorParams ✋ ✋ 95.3 ms 81.3 MB
051_inductWrongCtorResParams ✋ ✋ 92.9 ms 80.8 MB
052_inductWrongCtorResLevel ✋ ✋ 92.0 ms 81.3 MB
053_inductInIndex ✋ ✋ 95.5 ms 81.4 MB
054_indNeg ✋ ✋ 97.4 ms 81.8 MB
055_reduceCtorParam.mk 👍 👍 113 ms 82.2 MB
056_reduceCtorType.mk ✋ ✋ 98.3 ms 81.2 MB
057_indNegReducible ✋ ✋ 101 ms 81.8 MB
058_predWithTypeField 👍 👍 108 ms 82.2 MB
059_typeWithTypeField 👍 👍 108 ms 82.1 MB
060_typeWithTypeFieldPoly 👍 👍 108 ms 82.3 MB
061_typeWithTooHighTypeField.mk ✋ ✋ 98.9 ms 81.5 MB
062_emptyRec 👍 👍 104 ms 82.0 MB
063_boolRec 👍 👍 108 ms 82.4 MB
064_twoBoolRec 👍 👍 110 ms 82.5 MB
065_andRec 👍 👍 111 ms 82.6 MB
066_prodRec 👍 👍 110 ms 82.5 MB
067_pprodRec 👍 👍 112 ms 82.5 MB
068_punitRec 👍 👍 109 ms 82.6 MB
069_eqRec 👍 👍 110 ms 82.2 MB
070_nRec 👍 👍 109 ms 82.2 MB
071_rbTreeRef 👍 👍 168 ms 103.7 MB
072_boolPropRec 👍 👍 106 ms 82.3 MB
073_BogusRecursor ✋ ✋ 104 ms 81.9 MB
074_existsRec 👍 👍 110 ms 82.4 MB
075_typeSingletonRecReduction 👍 👍 125 ms 87.2 MB
076_sortElimPropRec 👍 👍 123 ms 85.3 MB
077_sortElimProp2Rec 👍 👍 123 ms 85.8 MB
078_boolRecEqns 👍 👍 155 ms 91.2 MB
079_prodRecEqns 👍 👍 154 ms 92.2 MB
080_nRecReduction 👍 👍 154 ms 93.0 MB
081_listRecReduction 👍 👍 184 ms 108.1 MB
082_RBTree.id_spec 👍 👍 208 ms 106.1 MB
083_And.right 👍 👍 112 ms 82.2 MB
084_Prod.snd 👍 👍 110 ms 82.6 MB
085_PProd.snd 👍 👍 112 ms 82.9 MB
086_PSigma.snd 👍 👍 111 ms 83.0 MB
087_projOutOfRange ✋ ✋ 114 ms 83.3 MB
088_projNotStruct ✋ ✋ 112 ms 83.1 MB
089_projProp1 👍 👍 154 ms 91.8 MB
090_projProp2 ✋ ✋ 157 ms 95.0 MB
091_projProp3 👍 👍 158 ms 98.4 MB
092_projProp4 ✋ ✋ 156 ms 95.5 MB
093_projProp5 ✋ ✋ 158 ms 100.7 MB
094_projProp6 ✋ ✋ 156 ms 95.2 MB
095_projDataIndexRec 👍 👍 122 ms 85.9 MB
096_projIndexData ✋ ✋ 165 ms 97.5 MB
097_projIndexData2 ✋ ✋ 165 ms 101.0 MB
098_projRed 👍 👍 155 ms 91.7 MB
099_ruleK 👍 👍 111 ms 82.5 MB
100_ruleKbad ✋ ✋ 120 ms 83.8 MB
101_ruleKAcc ✋ ✋ 201 ms 106.1 MB
102_aNatLit 👍 👍 110 ms 82.6 MB
103_natLitEq 👍 👍 123 ms 85.9 MB
104_proofIrrelevance 👍 👍 110 ms 82.6 MB
105_proofIrrelevanceBad ✋ ✋ 118 ms 83.4 MB
106_proofIrrelevanceWhnf 👍 👍 110 ms 82.6 MB
107_proofIrrelevanceUnderBinder 👍 👍 98.7 ms 81.6 MB
108_unitEta1 👍 👍 111 ms 82.7 MB
109_unitEta2 👍 👍 111 ms 82.5 MB
110_unitEta3 👍 👍 111 ms 82.4 MB
111_indexedUnitEta ✋ ✋ 133 ms 89.3 MB
112_structEta 👍 👍 155 ms 92.9 MB
113_indexedStructEta ✋ ✋ 134 ms 89.1 MB
114_funEta 👍 👍 111 ms 82.5 MB
115_funEtaDep 👍 👍 111 ms 82.7 MB
116_funEtaBad ✋ ✋ 118 ms 83.2 MB
117_reflOccLeft ✋ ✋ 109 ms 82.5 MB
118_reflOccInIndex ✋ ✋ 109 ms 82.4 MB
119_reduceCtorParamRefl.mk 👍 👍 112 ms 82.7 MB
120_reduceCtorParamRefl2.mk 👍 👍 112 ms 82.4 MB
121_rTreeRec 👍 👍 122 ms 85.2 MB
122_rtreeRecReduction 👍 👍 155 ms 92.9 MB
123_accRecType 👍 👍 157 ms 93.1 MB
124_accRecReduction 👍 👍 163 ms 96.9 MB
125_accRecNoEta ✋ ✋ 201 ms 106.1 MB
126_quotMkType 👍 👍 130 ms 87.5 MB
127_quotIndType 👍 👍 129 ms 87.4 MB
128_quotLiftType 👍 👍 139 ms 89.8 MB
129_quotSoundType 👍 👍 142 ms 89.8 MB
130_quotLiftReduction 👍 👍 168 ms 94.6 MB
131_quotIndReduction 👍 👍 167 ms 94.2 MB
132_dup_defs ✋ ✋ 96.2 ms 81.2 MB
133_dup_ind_def ✋ ✋ 97.7 ms 81.2 MB
134_dup_ctor_def ✋ ✋ 97.7 ms 81.2 MB
135_dup_rec_def ✋ ✋ 97.0 ms 81.6 MB
136_misnamed_rec_user ✋ ✋ 91.7 ms 80.8 MB
137_dup_rec_def2 ✋ ✋ 97.2 ms 80.9 MB
138_dup_ctor_rec ✋ ✋ 90.7 ms 81.4 MB
139_DupConCon ✋ ✋ 91.5 ms 81.1 MB
140_falseFromUnsafe ✋ ✋ 110 ms 83.3 MB
141_falseFromPartial ✋ ✋ 106 ms 82.6 MB