Lean Kernel Arena / nanoclo-fortran

Checker "nanoclo-fortran"

Version: b3a13ef · 📄 Declaration · 🔗 Source

Fortran 2018 translation of nanoclo's delayed-substitution Lean 4 kernel. Stores kernel objects in parallel arrays referenced by integer IDs, with interned closure environments and private OpenMP worker contexts. Exported expressions are shared and immutable. Follows nanoclo 4cdd12f; algorithm fidelity is checked with all 26 counters on every Init declaration. Supports nested inductives and Nat/String literals.

Soundness (rightfully rejected tests)

75 ✅ 5 ❌ 0 🚫

Completeness (rightfully accepted tests)

137 ✅ 1 ❌ 0 🚫

Corner cases (no outcome prescribed)

28 ✅ 2 🚫

Test Expected Result ⏱️ 🧠
cedar 👍 👍 5.45 min (×2.3) 2.8 GB (×2.1)
con-leche 👍 👍 2.33 min (+27%) 2.6 GB (×3.1)
cslib 👍 👍 11.8 min (+37%) 6.1 GB (+78%)
init 👍 👍 70.2 s (+6%) 1.1 GB (×2.0)
init-prelude 👍 👍 229 ms (-37%) 19.7 MB (÷3.7)
mathlib 👍 ✋ 16.6 min 14.3 GB
navier-stokes-euler 👍 👍 10.8 min (-4%) 5.0 GB (×2.0)
reachability 👍 👍 13.3 s (-43%) 5.9 GB (×3.6)
std 👍 👍 2.33 min (+24%) 1.7 GB (+89%)
22 99.5 ms 7.0 MB
closure-level-subst ✋ ✋ 0.814 ms 4.5 MB
constlevels ✋ ✋ 1.38 ms 4.4 MB
ctor-num-fields ✋ ✋ 2.00 ms 4.6 MB
eta-ctor-alias ✋ ✋ 1.00 ms 4.5 MB
forged-quot-ind ✋ 👍 1.24 ms 4.5 MB
k-rec-conv ✋ ✋ 1.35 ms 4.7 MB
large-elim-param ✋ ✋ 0.813 ms 4.4 MB
large-elim-prop-bool ✋ ✋ 1.65 ms 4.6 MB
level-imax-leq ✋ ✋ 0.803 ms 4.6 MB
level-imax-normalization ✋ ✋ 0.864 ms 4.7 MB
loose-bvar-value ✋ ✋ 0.729 ms 4.5 MB
nat-rec-k-lie ✋ ✋ 0.921 ms 4.3 MB
nat-rec-rules ✋ ✋ 0.995 ms 4.6 MB
nested-name-capture ✋ 👍 2.11 ms 4.4 MB
nested-rec-rule-nfields ✋ 👍 2.83 ms 4.6 MB
nested-unused-param ✋ ✋ 4.00 ms 5.1 MB
orphan-rec ✋ ✋ 0.653 ms 4.6 MB
pi-closure-context ✋ ✋ 0.662 ms 4.4 MB
proj-non-structure ✋ ✋ 0.836 ms 4.3 MB
proj-of-imax-prop ✋ ✋ 1.52 ms 4.8 MB
proj-of-stuck-prop ✋ ✋ 17.6 ms 6.6 MB
proj-of-subst-prop ✋ ✋ 16.9 ms 6.5 MB
rec-k-lie ✋ ✋ 0.828 ms 4.8 MB
rec-missing-ih ✋ ✋ 18.1 ms 6.8 MB
rec-of-subst-prop ✋ ✋ 18.1 ms 7.0 MB
unit-rec-rule ✋ 👍 0.759 ms 4.3 MB
1 51.1 ms 5.4 MB
alg-conv-trans-acc 🤷 ✋ 4.91 ms 5.1 MB
alg-conv-trans-acc-left 🤷 👍 4.91 ms 5.3 MB
alg-conv-trans-acc-right 🤷 👍 5.04 ms 5.3 MB
alg-conv-trans-quot 🤷 ✋ 1.13 ms 4.7 MB
alg-conv-trans-quot-left 🤷 👍 1.13 ms 4.6 MB
alg-conv-trans-quot-left-def 🤷 👍 1.24 ms 4.5 MB
alg-conv-trans-quot-right 🤷 👍 1.15 ms 4.5 MB
eta-ctor 🤷 ✋ 1.06 ms 4.8 MB
eta-rec-struct 🤷 ✋ 1.17 ms 4.5 MB
eta-rule-k 🤷 ✋ 1.01 ms 4.6 MB
eta-struct-major-and 🤷 👍 1.14 ms 4.5 MB
eta-struct-major-and-no-whnf 🤷 ⌛ 0 ms 0 B
eta-struct-major-no-whnf 🤷 ⌛ 0 ms 0 B
eta-unit-like-nested 🤷 ✋ 1.47 ms 4.6 MB
eta-unit-like-pi 🤷 ✋ 0.910 ms 4.5 MB
eta-unit-like-proof-field 🤷 ✋ 0.973 ms 4.5 MB
eta-unit-like-struct 🤷 ✋ 0.951 ms 4.5 MB
imax-nested-absorption 🤷 👍 0.602 ms 4.4 MB
imax-right-successor 🤷 👍 0.602 ms 4.3 MB
large-elim-maybe-prop 🤷 ✋ 0.790 ms 4.5 MB
let-value-type-mismatch 🤷 ✋ 0.612 ms 4.3 MB
nested-nonuniform-param 🤷 👍 1.20 ms 4.5 MB
nested-redex-aux 🤷 👍 3.76 ms 5.0 MB
positivity-whnf 🤷 ✋ 0.793 ms 4.6 MB
proj-maybe-prop 🤷 ✋ 1.11 ms 4.5 MB
proj-maybe-prop-past 🤷 ✋ 1.09 ms 4.4 MB
proof-param-ok 👍 👍 0.766 ms 4.6 MB
proof-param-swap 🤷 ✋ 0.769 ms 4.5 MB
subject-reduction-redex 🤷 👍 5.02 ms 5.4 MB
subject-reduction-reduct 🤷 ✋ 4.85 ms 5.1 MB
vanishing-occurrence 🤷 👍 0.947 ms 4.5 MB
9 12.6 ms 4.7 MB
extra-rec ✋ ✋ 0.649 ms 4.5 MB
inductive-undeclared-universe ✋ 👍 0.727 ms 4.2 MB
level-index-out-of-order 👍 👍 0.581 ms 4.2 MB
nat-lit-add 👍 👍 2.06 ms 4.7 MB
nat-lit-add-bad ✋ ✋ 2.05 ms 4.4 MB
nat-lit-ble 👍 👍 2.21 ms 4.6 MB
nat-lit-sub 👍 👍 2.26 ms 4.6 MB
orphan-ctor ✋ ✋ 0.649 ms 4.4 MB
proj-of-prop ✋ ✋ 0.803 ms 4.5 MB
sparse-name-index 👍 👍 0.569 ms 4.4 MB
31 35.6 s (÷2.3) 10.3 GB
app-lam 👍 👍 53.4 ms (÷91) 35.0 MB (÷41)
args-before-unfold 👍 👍 6.80 ms (÷5.3) 7.5 MB (÷8.8)
beta-ladder 👍 👍 22.8 ms (÷73) 13.5 MB (÷37)
church-numerals 👍 👍 16.5 ms (÷2.8) 22.0 MB (÷3.6)
discarded-argument 👍 👍 3.90 ms (÷43) 4.7 MB (÷14)
discarded-argument-match 👍 👍 4.81 ms (÷30) 5.1 MB (÷13)
folded-constant-first 👍 👍 9.24 ms (÷4.4) 8.2 MB (÷8.4)
folded-constant-last 👍 👍 9.25 ms (÷4.4) 8.0 MB (÷8.5)
fueled-chain 👍 👍 173 ms (+36%) 56.9 MB (-25%)
grind-ring-5 👍 👍 1.40 s (-35%) 310.6 MB (+36%)
identical-nesting 👍 👍 1.08 ms (÷26) 4.3 MB (÷15)
irrelevance-before-evaluation 👍 👍 1.53 ms (÷19) 4.8 MB (÷14)
irrelevance-refutes 👍 👍 1.31 ms (÷22) 4.5 MB (÷15)
let-fold 👍 👍 21.4 ms (÷2.7) 6.9 MB (÷9.6)
let-ladder 👍 👍 21.1 ms (÷48) 13.1 MB (÷24)
magma-list-deep-n21 👍 👍 930 ms (÷2.9) 463.9 MB (-31%)
magma-list-deep-n36 👍 👍 11.2 s (÷3.2) 5.8 GB (-26%)
magma-list-pair-n21 👍 👍 13.3 s (-28%) 10.3 GB (×2.6)
magma-list-pair-n7 👍 👍 1.25 s (-26%) 811.9 MB (+91%)
magma-string-n4 👍 👍 2.37 s (-33%) 207.8 MB (+71%)
magma-string-pair-n9 👍 👍 4.47 s (-46%) 1.5 GB (+51%)
proj-cheap-struct 👍 👍 5.26 ms (÷6.6) 5.0 MB (÷13)
proj-lazy-struct 👍 👍 23.4 ms (-25%) 16.1 MB (÷4.1)
proj-stuck-struct 👍 👍 3.36 ms (÷9.4) 4.7 MB (÷14)
prop-struct-projections 👍 👍 183 ms (+85%) 19.1 MB (÷3.7)
refute-cheap-first ✋ ✋ 1.71 ms (÷24) 4.6 MB (÷15)
refute-cheap-last ✋ ✋ 31.9 ms (÷5.7) 5.8 MB (÷12)
repeated-subproblem 👍 👍 1.57 ms (÷18) 4.6 MB (÷14)
shared-subterm 👍 👍 18.4 ms (÷3.1) 12.0 MB (÷6.1)
shift-cascade 👍 👍 13.5 ms (÷3.4) 7.6 MB (÷8.9)
unroll-versus-evaluate 👍 👍 8.93 ms (÷3.5) 8.2 MB (÷8.1)
141 121 ms 5.2 MB
001_basicDef 👍 👍 0.604 ms 4.2 MB
002_badDef ✋ ✋ 0.586 ms 4.4 MB
003_arrowType 👍 👍 0.605 ms 4.2 MB
004_dependentType 👍 👍 0.610 ms 4.2 MB
005_constType 👍 👍 0.606 ms 4.1 MB
006_betaReduction 👍 👍 0.667 ms 4.4 MB
007_betaReduction2 👍 👍 0.650 ms 4.2 MB
008_forallSortWhnf 👍 👍 0.647 ms 4.3 MB
009_forallSortBad ✋ ✋ 0.628 ms 4.3 MB
010_nonTypeType ✋ ✋ 0.630 ms 4.4 MB
011_nonTypeAxiom ✋ ✋ 0.634 ms 4.3 MB
012_nonPropThm ✋ ✋ 0.584 ms 4.3 MB
013_thmProof 👍 👍 0.652 ms 4.2 MB
014_selfProof ✋ ✋ 0.605 ms 4.5 MB
015_levelComp1 👍 👍 0.594 ms 4.2 MB
016_levelComp2 👍 👍 0.596 ms 4.3 MB
017_levelComp3 👍 👍 0.600 ms 4.2 MB
018_levelParams 👍 👍 0.653 ms 4.2 MB
019_tut06_bad01 ✋ ✋ 0.577 ms 4.3 MB
020_levelComp4 👍 👍 0.591 ms 4.2 MB
021_levelComp5 👍 👍 0.605 ms 4.3 MB
022_imax1 👍 👍 0.614 ms 4.6 MB
023_imax2 👍 👍 0.601 ms 4.4 MB
024_levelMaxComm 👍 👍 0.600 ms 4.3 MB
025_levelMaxAssoc 👍 👍 0.608 ms 4.2 MB
026_levelMaxIdem 👍 👍 0.585 ms 4.2 MB
027_levelMaxAbsorb 👍 👍 0.581 ms 4.1 MB
028_inferVar 👍 👍 0.603 ms 4.2 MB
029_defEqLambda 👍 👍 0.647 ms 4.6 MB
030_peano1 👍 👍 0.784 ms 4.2 MB
031_peano2 👍 👍 0.837 ms 4.2 MB
032_peano3 👍 👍 0.948 ms 4.2 MB
033_letType 👍 👍 0.585 ms 4.3 MB
034_letTypeDep 👍 👍 0.637 ms 4.3 MB
035_letRed 👍 👍 0.611 ms 4.2 MB
036_empty 👍 👍 0.647 ms 4.5 MB
037_boolType 👍 👍 0.687 ms 4.5 MB
038_twoBool 👍 👍 0.774 ms 4.3 MB
039_andType 👍 👍 0.772 ms 4.4 MB
040_prodType 👍 👍 0.836 ms 4.6 MB
041_pprodType 👍 👍 0.824 ms 4.6 MB
042_pUnitType 👍 👍 0.662 ms 4.4 MB
043_eqType 👍 👍 0.790 ms 4.4 MB
044_natDef 👍 👍 0.763 ms 4.4 MB
045_rbTreeDef 👍 👍 1.88 ms 4.6 MB
046_inductBadNonSort ✋ ✋ 0.622 ms 4.6 MB
047_inductBadNonSort2 ✋ ✋ 0.604 ms 4.4 MB
048_inductLevelParam ✋ ✋ 0.584 ms 4.2 MB
049_inductTooFewParams ✋ ✋ 0.616 ms 4.5 MB
050_inductWrongCtorParams ✋ ✋ 0.636 ms 4.5 MB
051_inductWrongCtorResParams ✋ ✋ 0.653 ms 4.3 MB
052_inductWrongCtorResLevel ✋ ✋ 0.674 ms 4.4 MB
053_inductInIndex ✋ ✋ 0.630 ms 4.4 MB
054_indNeg ✋ ✋ 0.617 ms 4.4 MB
055_reduceCtorParam.mk 👍 👍 0.875 ms 4.3 MB
056_reduceCtorType.mk ✋ ✋ 0.658 ms 4.5 MB
057_indNegReducible ✋ ✋ 0.674 ms 4.3 MB
058_predWithTypeField 👍 👍 0.681 ms 4.2 MB
059_typeWithTypeField 👍 👍 0.691 ms 4.6 MB
060_typeWithTypeFieldPoly 👍 👍 0.691 ms 4.6 MB
061_typeWithTooHighTypeField.mk ✋ ✋ 0.616 ms 4.6 MB
062_emptyRec 👍 👍 0.640 ms 4.3 MB
063_boolRec 👍 👍 0.744 ms 4.6 MB
064_twoBoolRec 👍 👍 0.810 ms 4.4 MB
065_andRec 👍 👍 0.809 ms 4.3 MB
066_prodRec 👍 👍 0.869 ms 4.3 MB
067_pprodRec 👍 👍 0.852 ms 4.5 MB
068_punitRec 👍 👍 0.693 ms 4.5 MB
069_eqRec 👍 👍 0.833 ms 4.4 MB
070_nRec 👍 👍 0.827 ms 4.3 MB
071_rbTreeRef 👍 👍 2.02 ms 4.6 MB
072_boolPropRec 👍 👍 0.705 ms 4.4 MB
073_BogusRecursor ✋ ✋ 0.679 ms 4.6 MB
074_existsRec 👍 👍 0.882 ms 4.4 MB
075_typeSingletonRecReduction 👍 👍 1.01 ms 4.5 MB
076_sortElimPropRec 👍 👍 0.922 ms 4.5 MB
077_sortElimProp2Rec 👍 👍 0.988 ms 4.4 MB
078_boolRecEqns 👍 👍 1.21 ms 4.6 MB
079_prodRecEqns 👍 👍 1.19 ms 4.7 MB
080_nRecReduction 👍 👍 1.33 ms 4.6 MB
081_listRecReduction 👍 👍 1.84 ms 4.9 MB
082_RBTree.id_spec 👍 👍 4.54 ms 5.2 MB
083_And.right 👍 👍 0.828 ms 4.3 MB
084_Prod.snd 👍 👍 0.863 ms 4.4 MB
085_PProd.snd 👍 👍 0.877 ms 4.6 MB
086_PSigma.snd 👍 👍 0.924 ms 4.5 MB
087_projOutOfRange ✋ ✋ 0.824 ms 4.7 MB
088_projNotStruct ✋ ✋ 0.772 ms 4.5 MB
089_projProp1 👍 👍 1.08 ms 4.6 MB
090_projProp2 ✋ ✋ 1.05 ms 4.5 MB
091_projProp3 👍 👍 1.07 ms 4.6 MB
092_projProp4 ✋ ✋ 1.08 ms 4.7 MB
093_projProp5 ✋ ✋ 1.08 ms 4.6 MB
094_projProp6 ✋ ✋ 1.08 ms 4.4 MB
095_projDataIndexRec 👍 👍 0.928 ms 4.6 MB
096_projIndexData ✋ ✋ 1.38 ms 4.7 MB
097_projIndexData2 ✋ ✋ 1.39 ms 4.6 MB
098_projRed 👍 👍 1.15 ms 4.6 MB
099_ruleK 👍 👍 0.970 ms 4.5 MB
100_ruleKbad ✋ ✋ 0.984 ms 4.4 MB
101_ruleKAcc ✋ ✋ 1.48 ms 4.6 MB
102_aNatLit 👍 👍 0.747 ms 4.4 MB
103_natLitEq 👍 👍 0.948 ms 4.5 MB
104_proofIrrelevance 👍 👍 0.868 ms 4.5 MB
105_proofIrrelevanceBad ✋ ✋ 0.909 ms 4.3 MB
106_proofIrrelevanceWhnf 👍 👍 0.907 ms 4.5 MB
107_proofIrrelevanceUnderBinder 👍 👍 0.667 ms 4.3 MB
108_unitEta1 👍 👍 0.921 ms 4.4 MB
109_unitEta2 👍 👍 0.920 ms 4.5 MB
110_unitEta3 👍 👍 0.940 ms 4.4 MB
111_indexedUnitEta ✋ ✋ 1.01 ms 4.5 MB
112_structEta 👍 👍 1.36 ms 4.7 MB
113_indexedStructEta ✋ ✋ 1.06 ms 4.7 MB
114_funEta 👍 👍 0.917 ms 4.4 MB
115_funEtaDep 👍 👍 0.927 ms 4.3 MB
116_funEtaBad ✋ ✋ 0.897 ms 4.3 MB
117_reflOccLeft ✋ ✋ 0.804 ms 4.2 MB
118_reflOccInIndex ✋ ✋ 0.814 ms 4.3 MB
119_reduceCtorParamRefl.mk 👍 👍 0.897 ms 4.6 MB
120_reduceCtorParamRefl2.mk 👍 👍 0.935 ms 4.5 MB
121_rTreeRec 👍 👍 0.888 ms 4.4 MB
122_rtreeRecReduction 👍 👍 1.20 ms 4.5 MB
123_accRecType 👍 👍 1.18 ms 4.7 MB
124_accRecReduction 👍 👍 1.53 ms 4.5 MB
125_accRecNoEta ✋ ✋ 1.49 ms 4.5 MB
126_quotMkType 👍 👍 0.999 ms 4.3 MB
127_quotIndType 👍 👍 1.01 ms 4.6 MB
128_quotLiftType 👍 👍 1.05 ms 4.5 MB
129_quotSoundType 👍 👍 1.05 ms 4.8 MB
130_quotLiftReduction 👍 👍 1.14 ms 4.5 MB
131_quotIndReduction 👍 👍 1.10 ms 4.3 MB
132_dup_defs ✋ ✋ 0.499 ms 3.8 MB
133_dup_ind_def ✋ ✋ 0.534 ms 4.0 MB
134_dup_ctor_def ✋ ✋ 0.535 ms 3.9 MB
135_dup_rec_def ✋ ✋ 0.538 ms 3.7 MB
136_misnamed_rec_user ✋ ✋ 0.668 ms 4.4 MB
137_dup_rec_def2 ✋ ✋ 0.660 ms 4.3 MB
138_dup_ctor_rec ✋ ✋ 0.533 ms 3.6 MB
139_DupConCon ✋ ✋ 0.550 ms 3.9 MB
140_falseFromUnsafe ✋ ✋ 0.523 ms 3.7 MB
141_falseFromPartial ✋ ✋ 0.523 ms 3.9 MB