Lean Kernel Arena / pestka-wasm

Checker "pestka-wasm"

Version: 7caa557 · 📄 Declaration · 🔗 Source

pestka-wasm is the Pestka kernel as WebAssembly. The same Aver source as the pestka entry is compiled by Aver's own wasm-gc backend (not through Rust or LLVM) and runs on V8 under Node. Terms, maps and closures are objects of the engine's garbage collector, and the module is about 0.4 MB. It gives the same answers as pestka; the gap between the two entries is what a garbage-collected wasm target costs a Lean kernel, and Aver's backend keeps working on it.

Declarations are checked on one thread, grouped by namespace as in pestka, with --low-memory: Pestka's caches stay bounded, which under the garbage collector costs no extra work. bin/run-wasm passes on Pestka's exit status only when its verdict line agrees with it, and exits with 3 otherwise, so a crash of V8 or of the host never reads as a verdict.

The build installs the Aver release pinned in .aver-version from crates.io and optimizes the module for speed with Binaryen's wasm-opt.

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 👍 👍 1.82 min (-23%) 4.4 GB (×3.3)
con-leche 👍 👍 73.0 s (-34%) 3.1 GB (×3.8)
cslib 👍 👍 5.92 min (-32%) 8.8 GB (×2.6)
init 👍 👍 45.1 s (-32%) 2.2 GB (×4.0)
init-prelude 👍 👍 555 ms (+53%) 403.7 MB (×5.5)
mathlib 👍 👍 22.8 min (-29%) 10.7 GB (+8%)
navier-stokes-euler 👍 👍 5.70 min (-49%) 7.6 GB (×3.1)
reachability 👍 👍 12.3 s (-48%) 1.2 GB (-24%)
std 👍 👍 78.7 s (-30%) 3.7 GB (×4.0)
26 2.61 s 121.6 MB
closure-level-subst ✋ ✋ 78.4 ms 91.9 MB
constlevels ✋ ✋ 94.0 ms 100.7 MB
ctor-num-fields ✋ ✋ 95.7 ms 100.9 MB
eta-ctor-alias ✋ ✋ 82.8 ms 92.2 MB
forged-quot-ind ✋ ✋ 93.2 ms 99.9 MB
k-rec-conv ✋ ✋ 95.5 ms 100.0 MB
large-elim-param ✋ ✋ 80.7 ms 91.8 MB
large-elim-prop-bool ✋ ✋ 92.9 ms 100.9 MB
level-imax-leq ✋ ✋ 78.0 ms 91.6 MB
level-imax-normalization ✋ ✋ 80.3 ms 92.2 MB
loose-bvar-value ✋ ✋ 78.0 ms 91.6 MB
nat-rec-k-lie ✋ ✋ 81.3 ms 91.9 MB
nat-rec-rules ✋ ✋ 78.2 ms 92.1 MB
nested-name-capture ✋ ✋ 108 ms 103.8 MB
nested-rec-rule-nfields ✋ ✋ 117 ms 106.5 MB
nested-unused-param ✋ ✋ 120 ms 105.8 MB
orphan-rec ✋ ✋ 77.6 ms 91.8 MB
pi-closure-context ✋ ✋ 77.5 ms 91.8 MB
proj-non-structure ✋ ✋ 80.3 ms 92.1 MB
proj-of-imax-prop ✋ ✋ 94.1 ms 100.4 MB
proj-of-stuck-prop ✋ ✋ 167 ms 120.5 MB
proj-of-subst-prop ✋ ✋ 164 ms 120.0 MB
rec-k-lie ✋ ✋ 79.6 ms 91.9 MB
rec-missing-ih ✋ ✋ 168 ms 120.8 MB
rec-of-subst-prop ✋ ✋ 169 ms 121.6 MB
unit-rec-rule ✋ ✋ 78.9 ms 92.0 MB
1 2.85 s 108.4 MB
alg-conv-trans-acc 🤷 ✋ 119 ms 106.5 MB
alg-conv-trans-acc-left 🤷 👍 118 ms 105.7 MB
alg-conv-trans-acc-right 🤷 👍 118 ms 105.1 MB
alg-conv-trans-quot 🤷 ✋ 92.1 ms 100.0 MB
alg-conv-trans-quot-left 🤷 ✋ 92.0 ms 99.9 MB
alg-conv-trans-quot-left-def 🤷 👍 92.6 ms 100.1 MB
alg-conv-trans-quot-right 🤷 👍 92.5 ms 99.6 MB
eta-ctor 🤷 ✋ 91.7 ms 100.1 MB
eta-rec-struct 🤷 ✋ 92.9 ms 100.5 MB
eta-rule-k 🤷 ✋ 81.7 ms 92.6 MB
eta-struct-major-and 🤷 👍 94.3 ms 99.5 MB
eta-struct-major-and-no-whnf 🤷 👍 95.2 ms 101.5 MB
eta-struct-major-no-whnf 🤷 👍 97.7 ms 101.4 MB
eta-unit-like-nested 🤷 ✋ 93.4 ms 100.8 MB
eta-unit-like-pi 🤷 ✋ 81.7 ms 92.4 MB
eta-unit-like-proof-field 🤷 ✋ 81.6 ms 92.3 MB
eta-unit-like-struct 🤷 ✋ 81.8 ms 92.5 MB
imax-nested-absorption 🤷 ✋ 73.9 ms 91.3 MB
imax-right-successor 🤷 👍 74.6 ms 91.2 MB
large-elim-maybe-prop 🤷 ✋ 81.2 ms 92.0 MB
let-value-type-mismatch 🤷 ✋ 74.1 ms 91.4 MB
nested-nonuniform-param 🤷 ✋ 90.3 ms 98.8 MB
nested-redex-aux 🤷 👍 126 ms 108.4 MB
positivity-whnf 🤷 ✋ 80.7 ms 92.0 MB
proj-maybe-prop 🤷 👍 80.8 ms 92.3 MB
proj-maybe-prop-past 🤷 👍 81.5 ms 92.3 MB
proof-param-ok 👍 👍 79.8 ms 91.6 MB
proof-param-swap 🤷 ✋ 74.0 ms 91.2 MB
subject-reduction-redex 🤷 👍 118 ms 107.2 MB
subject-reduction-reduct 🤷 ✋ 120 ms 104.8 MB
vanishing-occurrence 🤷 👍 80.5 ms 92.3 MB
10 852 ms 101.7 MB
extra-rec ✋ ✋ 78.1 ms 91.5 MB
inductive-undeclared-universe ✋ ✋ 74.8 ms 91.4 MB
level-index-out-of-order 👍 👍 73.0 ms 91.1 MB
nat-lit-add 👍 👍 98.3 ms 101.2 MB
nat-lit-add-bad ✋ ✋ 97.1 ms 100.3 MB
nat-lit-ble 👍 👍 98.6 ms 101.4 MB
nat-lit-sub 👍 👍 99.1 ms 101.7 MB
orphan-ctor ✋ ✋ 77.9 ms 91.0 MB
proj-of-prop ✋ ✋ 81.1 ms 92.1 MB
sparse-name-index 👍 👍 73.6 ms 90.6 MB
31 34.6 s (÷2.3) 1.8 GB
app-lam 👍 👍 1.50 s (÷3.2) 696.7 MB (÷2.1)
args-before-unfold 👍 👍 127 ms (×3.5) 108.7 MB (+65%)
beta-ladder 👍 👍 394 ms (÷4.2) 406.9 MB (-19%)
church-numerals 👍 👍 183 ms (×3.9) 153.0 MB (+96%)
discarded-argument 👍 👍 94.2 ms (-43%) 100.5 MB (+53%)
discarded-argument-match 👍 👍 97.9 ms (-31%) 100.8 MB (+48%)
folded-constant-first 👍 👍 130 ms (×3.2) 110.2 MB (+60%)
folded-constant-last 👍 👍 130 ms (×3.2) 110.1 MB (+61%)
fueled-chain 👍 👍 271 ms (×2.1) 180.5 MB (×2.4)
grind-ring-5 👍 👍 2.20 s (+2%) 709.5 MB (×3.1)
identical-nesting 👍 👍 91.0 ms (×3.2) 99.2 MB (+50%)
irrelevance-before-evaluation 👍 👍 93.2 ms (×3.2) 100.8 MB (+53%)
irrelevance-refutes 👍 👍 94.2 ms (×3.3) 100.2 MB (+51%)
let-fold 👍 👍 178 ms (×3.1) 126.6 MB (+91%)
let-ladder 👍 👍 398 ms (÷2.5) 400.9 MB (+25%)
magma-list-deep-n21 👍 👍 478 ms (÷5.6) 412.0 MB (-38%)
magma-list-deep-n36 👍 👍 1.78 s (÷20) 629.1 MB (÷13)
magma-list-pair-n21 👍 👍 16.2 s (-12%) 1.8 GB (÷2.2)
magma-list-pair-n7 👍 👍 1.61 s (-5%) 673.4 MB (+58%)
magma-string-n4 👍 👍 2.84 s (-20%) 732.6 MB (×6.0)
magma-string-pair-n9 👍 👍 4.33 s (-47%) 852.1 MB (-15%)
proj-cheap-struct 👍 👍 124 ms (×3.6) 106.8 MB (+62%)
proj-lazy-struct 👍 👍 106 ms (×3.4) 104.7 MB (+59%)
proj-stuck-struct 👍 👍 109 ms (×3.4) 104.2 MB (+59%)
prop-struct-projections 👍 👍 260 ms (×2.6) 209.9 MB (×3.0)
refute-cheap-first ✋ ✋ 94.5 ms (×2.3) 100.6 MB (+46%)
refute-cheap-last ✋ ✋ 150 ms (-17%) 112.8 MB (+63%)
repeated-subproblem 👍 👍 94.6 ms (×3.3) 100.3 MB (+52%)
shared-subterm 👍 👍 211 ms (×3.7) 127.6 MB (+75%)
shift-cascade 👍 👍 176 ms (×3.8) 184.2 MB (×2.7)
unroll-versus-evaluate 👍 👍 107 ms (×3.4) 101.8 MB (+54%)
141 11.4 s 105.1 MB
001_basicDef 👍 👍 74.0 ms 91.1 MB
002_badDef ✋ ✋ 74.4 ms 91.0 MB
003_arrowType 👍 👍 74.9 ms 91.5 MB
004_dependentType 👍 👍 75.5 ms 91.3 MB
005_constType 👍 👍 75.1 ms 91.2 MB
006_betaReduction 👍 👍 76.3 ms 91.3 MB
007_betaReduction2 👍 👍 76.8 ms 91.6 MB
008_forallSortWhnf 👍 👍 76.1 ms 91.2 MB
009_forallSortBad ✋ ✋ 76.3 ms 91.4 MB
010_nonTypeType ✋ ✋ 75.2 ms 91.2 MB
011_nonTypeAxiom ✋ ✋ 75.6 ms 91.6 MB
012_nonPropThm ✋ ✋ 73.3 ms 91.2 MB
013_thmProof 👍 👍 75.7 ms 91.4 MB
014_selfProof ✋ ✋ 76.2 ms 91.1 MB
015_levelComp1 👍 👍 75.9 ms 91.1 MB
016_levelComp2 👍 👍 73.6 ms 91.4 MB
017_levelComp3 👍 👍 73.4 ms 91.2 MB
018_levelParams 👍 👍 77.3 ms 91.6 MB
019_tut06_bad01 ✋ ✋ 72.1 ms 91.1 MB
020_levelComp4 👍 👍 73.2 ms 91.3 MB
021_levelComp5 👍 👍 73.4 ms 90.9 MB
022_imax1 👍 👍 75.4 ms 91.4 MB
023_imax2 👍 👍 75.3 ms 91.3 MB
024_levelMaxComm 👍 👍 74.7 ms 91.4 MB
025_levelMaxAssoc 👍 👍 74.9 ms 91.4 MB
026_levelMaxIdem 👍 👍 74.4 ms 91.3 MB
027_levelMaxAbsorb 👍 👍 74.5 ms 91.3 MB
028_inferVar 👍 👍 75.0 ms 91.2 MB
029_defEqLambda 👍 👍 75.6 ms 91.4 MB
030_peano1 👍 👍 78.2 ms 91.6 MB
031_peano2 👍 👍 78.6 ms 92.0 MB
032_peano3 👍 👍 79.9 ms 92.7 MB
033_letType 👍 👍 75.7 ms 91.4 MB
034_letTypeDep 👍 👍 77.9 ms 91.9 MB
035_letRed 👍 👍 76.7 ms 91.3 MB
036_empty 👍 👍 77.9 ms 91.7 MB
037_boolType 👍 👍 79.8 ms 91.6 MB
038_twoBool 👍 👍 80.1 ms 91.8 MB
039_andType 👍 👍 80.3 ms 92.2 MB
040_prodType 👍 👍 80.1 ms 92.0 MB
041_pprodType 👍 👍 80.6 ms 92.1 MB
042_pUnitType 👍 👍 79.3 ms 91.7 MB
043_eqType 👍 👍 79.8 ms 91.9 MB
044_natDef 👍 👍 81.3 ms 91.9 MB
045_rbTreeDef 👍 👍 92.4 ms 100.6 MB
046_inductBadNonSort ✋ ✋ 77.4 ms 91.4 MB
047_inductBadNonSort2 ✋ ✋ 74.5 ms 91.2 MB
048_inductLevelParam ✋ ✋ 72.7 ms 91.2 MB
049_inductTooFewParams ✋ ✋ 74.3 ms 91.4 MB
050_inductWrongCtorParams ✋ ✋ 75.6 ms 91.5 MB
051_inductWrongCtorResParams ✋ ✋ 75.5 ms 91.1 MB
052_inductWrongCtorResLevel ✋ ✋ 74.4 ms 91.1 MB
053_inductInIndex ✋ ✋ 77.2 ms 91.3 MB
054_indNeg ✋ ✋ 75.8 ms 91.3 MB
055_reduceCtorParam.mk 👍 👍 83.5 ms 92.0 MB
056_reduceCtorType.mk ✋ ✋ 77.1 ms 91.6 MB
057_indNegReducible ✋ ✋ 78.2 ms 91.5 MB
058_predWithTypeField 👍 👍 79.4 ms 91.4 MB
059_typeWithTypeField 👍 👍 80.1 ms 92.3 MB
060_typeWithTypeFieldPoly 👍 👍 80.7 ms 91.8 MB
061_typeWithTooHighTypeField.mk ✋ ✋ 76.8 ms 91.3 MB
062_emptyRec 👍 👍 79.1 ms 91.6 MB
063_boolRec 👍 👍 80.4 ms 91.7 MB
064_twoBoolRec 👍 👍 80.5 ms 91.7 MB
065_andRec 👍 👍 80.9 ms 92.1 MB
066_prodRec 👍 👍 81.1 ms 92.0 MB
067_pprodRec 👍 👍 81.6 ms 92.2 MB
068_punitRec 👍 👍 79.6 ms 91.7 MB
069_eqRec 👍 👍 79.8 ms 92.0 MB
070_nRec 👍 👍 79.7 ms 92.2 MB
071_rbTreeRef 👍 👍 92.4 ms 100.5 MB
072_boolPropRec 👍 👍 78.8 ms 91.7 MB
073_BogusRecursor ✋ ✋ 79.4 ms 91.7 MB
074_existsRec 👍 👍 81.4 ms 92.2 MB
075_typeSingletonRecReduction 👍 👍 92.7 ms 99.6 MB
076_sortElimPropRec 👍 👍 80.8 ms 92.0 MB
077_sortElimProp2Rec 👍 👍 81.6 ms 92.3 MB
078_boolRecEqns 👍 👍 92.4 ms 100.3 MB
079_prodRecEqns 👍 👍 92.2 ms 100.3 MB
080_nRecReduction 👍 👍 94.0 ms 100.6 MB
081_listRecReduction 👍 👍 94.9 ms 99.9 MB
082_RBTree.id_spec 👍 👍 112 ms 105.1 MB
083_And.right 👍 👍 80.5 ms 92.2 MB
084_Prod.snd 👍 👍 80.9 ms 91.9 MB
085_PProd.snd 👍 👍 81.9 ms 92.4 MB
086_PSigma.snd 👍 👍 83.0 ms 92.4 MB
087_projOutOfRange ✋ ✋ 79.9 ms 92.1 MB
088_projNotStruct ✋ ✋ 80.7 ms 92.1 MB
089_projProp1 👍 👍 93.3 ms 100.0 MB
090_projProp2 ✋ ✋ 93.2 ms 99.5 MB
091_projProp3 👍 👍 91.9 ms 100.1 MB
092_projProp4 ✋ ✋ 91.1 ms 99.0 MB
093_projProp5 ✋ ✋ 91.9 ms 99.3 MB
094_projProp6 ✋ ✋ 91.8 ms 100.3 MB
095_projDataIndexRec 👍 👍 81.0 ms 92.4 MB
096_projIndexData ✋ ✋ 92.8 ms 99.3 MB
097_projIndexData2 ✋ ✋ 94.4 ms 100.6 MB
098_projRed 👍 👍 94.4 ms 100.1 MB
099_ruleK 👍 👍 81.4 ms 92.3 MB
100_ruleKbad ✋ ✋ 82.6 ms 92.2 MB
101_ruleKAcc ✋ ✋ 92.7 ms 100.3 MB
102_aNatLit 👍 👍 80.9 ms 92.4 MB
103_natLitEq 👍 👍 82.1 ms 92.8 MB
104_proofIrrelevance 👍 👍 81.3 ms 91.9 MB
105_proofIrrelevanceBad ✋ ✋ 81.2 ms 91.7 MB
106_proofIrrelevanceWhnf 👍 👍 82.2 ms 92.2 MB
107_proofIrrelevanceUnderBinder 👍 👍 77.0 ms 92.0 MB
108_unitEta1 👍 👍 81.8 ms 92.4 MB
109_unitEta2 👍 👍 81.8 ms 92.3 MB
110_unitEta3 👍 👍 81.2 ms 92.2 MB
111_indexedUnitEta ✋ ✋ 82.3 ms 92.2 MB
112_structEta 👍 👍 93.7 ms 99.4 MB
113_indexedStructEta ✋ ✋ 92.0 ms 99.9 MB
114_funEta 👍 👍 81.2 ms 92.4 MB
115_funEtaDep 👍 👍 82.2 ms 92.2 MB
116_funEtaBad ✋ ✋ 81.9 ms 92.3 MB
117_reflOccLeft ✋ ✋ 79.6 ms 92.0 MB
118_reflOccInIndex ✋ ✋ 80.3 ms 92.4 MB
119_reduceCtorParamRefl.mk 👍 👍 82.5 ms 92.1 MB
120_reduceCtorParamRefl2.mk 👍 👍 82.4 ms 92.4 MB
121_rTreeRec 👍 👍 80.9 ms 92.2 MB
122_rtreeRecReduction 👍 👍 93.3 ms 100.2 MB
123_accRecType 👍 👍 92.1 ms 99.2 MB
124_accRecReduction 👍 👍 93.0 ms 100.3 MB
125_accRecNoEta ✋ ✋ 93.9 ms 100.4 MB
126_quotMkType 👍 👍 81.1 ms 92.0 MB
127_quotIndType 👍 👍 80.5 ms 92.1 MB
128_quotLiftType 👍 👍 81.4 ms 92.3 MB
129_quotSoundType 👍 👍 91.7 ms 99.2 MB
130_quotLiftReduction 👍 👍 91.6 ms 99.5 MB
131_quotIndReduction 👍 👍 92.0 ms 99.7 MB
132_dup_defs ✋ ✋ 73.4 ms 91.4 MB
133_dup_ind_def ✋ ✋ 75.3 ms 91.5 MB
134_dup_ctor_def ✋ ✋ 75.9 ms 91.5 MB
135_dup_rec_def ✋ ✋ 75.7 ms 91.3 MB
136_misnamed_rec_user ✋ ✋ 78.8 ms 91.7 MB
137_dup_rec_def2 ✋ ✋ 76.5 ms 91.4 MB
138_dup_ctor_rec ✋ ✋ 78.2 ms 91.4 MB
139_DupConCon ✋ ✋ 76.1 ms 91.6 MB
140_falseFromUnsafe ✋ ✋ 77.4 ms 91.7 MB
141_falseFromPartial ✋ ✋ 78.6 ms 91.6 MB