experiment: Generalize step indices using `local stepindex` across all of Algebra/ by markusdemedeiros · Pull Request #683 · leanprover-community/iris-lean

markusdemedeiros · 2026-08-26T18:46:33Z

DO NOT MERGE

This is an experiment to see the performance impact of local stepindex and to test different mitigations.

… for `Nat` in `StepIndexFinite.lean`

…stances not yet complete

Replace all proofs in section `Fixpoint`, all requires rewrite

…and `Contractive.succ`

Parametrisation of `CMRA` to be done in a future PR

… and so on

…nt with `SI = Nat`

markusdemedeiros · 2026-08-26T18:47:35Z

!bench

markusdemedeiros · 2026-08-26T18:48:17Z

!bench

leanprover-radar · 2026-08-26T18:48:49Z

Benchmark results for f6ff79d against a5f3796 are in. (These commits have already been benchmarked in a previous command.) There are significant results. @markusdemedeiros

🟥 build//instructions: +261.0G (+14.90%)

Large changes (11🟥)

🟥 build/module/Iris.Algebra.CMRA//instructions: +10.6G (+53.42%)
🟥 build/module/Iris.Algebra.COFESolver//instructions: +12.4G (+104.78%)
🟥 build/module/Iris.Algebra.Csum//instructions: +8.3G (+42.88%)
🟥 build/module/Iris.Algebra.Heap//instructions: +5.5G (+44.37%)
🟥 build/module/Iris.Algebra.HeapView//instructions: +7.1G (+42.48%)
🟥 build/module/Iris.Algebra.OFE//instructions: +21.1G (+115.24%)
🟥 build/module/Iris.Examples.Fix//instructions: +6.0G (+157.52%)
🟥 build/module/Iris.Instances.IProp.Instance//instructions: +7.8G (+48.36%)
🟥 build/module/Iris.Instances.Lib.Boxes//instructions: +6.4G (+30.69%)
🟥 build/module/Iris.Instances.Lib.GhostMap//instructions: +13.8G (+29.29%)
and 1 hidden

Medium changes (49🟥)

🟥 build/module/Iris.Algebra.Agree//instructions: +3.8G (+54.69%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Auth//instructions: +4.5G (+64.73%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.BigOp//instructions: +3.3G (+31.85%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Chain//instructions: +2.9G (+128.71%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.DFrac//instructions: +1.8G (+11.76%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.DynReservationMap//instructions: +3.4G (+40.07%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Excl//instructions: +2.3G (+67.14%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Frac//instructions: +1.2G (+26.46%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Functions//instructions: +1.8G (+75.48%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.GenMap//instructions: +4.0G (+50.81%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.IProp//instructions: +3.0G (+104.53%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.IsOp//instructions: +1.0G (+74.91%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.LeibnizMultiSet//instructions: +1.0G (+42.87%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.LeibnizSet//instructions: +1.5G (+24.42%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Lib.DFracAgree//instructions: +1.5G (+69.64%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Lib.ExclAuth//instructions: +1.4G (+55.35%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Lib.FracAuth//instructions: +2.6G (+47.67%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Lib.MonoList//instructions: +1.8G (+37.93%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Lib.MonoNat//instructions: +1.7G (+50.47%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Lib.MonoZ//instructions: +1.2G (+34.07%) (reduced significance based on absolute threshold)
and 29 more

Small changes (129🟥)

🟥 build/lakeprof/longest build path//instructions: +72.3G (+11.95%)
🟥 build/module/Iris.Algebra.Lib//instructions: +734.2M (+61.23%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Monoid//instructions: +992.9M (+74.40%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.StepIndex//instructions: +2.8G (+97.77%) (reduced significance based on *//lines)
🟥 build/module/Iris.Algebra//instructions: +761.3M (+64.01%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.BI.BI//instructions: +622.8M (+20.46%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.BI.BigOp.BigAndList//instructions: +657.5M (+19.33%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.BI.BigOp.BigAndMap//instructions: +665.1M (+17.63%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.BI.BigOp.BigOp//instructions: +922.4M (+5.64%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.BI.BigOp.BigOrList//instructions: +666.3M (+19.75%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.BI.BigOp.BigSepMSet//instructions: +655.1M (+15.06%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.BI.BigOp.BigSepMap//instructions: +762.8M (+9.56%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.BI.BigOp.BigSepSet//instructions: +646.9M (+11.52%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.BI.BigOp//instructions: +450.2M (+30.82%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.BI.Classes//instructions: +454.1M (+29.32%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.BI.Cmra//instructions: +740.9M (+23.09%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.BI.DerivedLawsLater//instructions: +949.1M (+11.12%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.BI.Embedding//instructions: +813.7M (+10.00%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.BI.Extensions//instructions: +465.9M (+29.56%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.BI.Instances//instructions: +454.8M (+28.31%) (reduced significance based on absolute threshold)
and 109 more

leanprover-radar · 2026-08-26T18:48:50Z

Benchmark results for f6ff79d against a5f3796 are in. (These commits have already been benchmarked in a previous command.) There are significant results. @markusdemedeiros

🟥 build//instructions: +261.0G (+14.90%)

Large changes (11🟥)

🟥 build/module/Iris.Algebra.CMRA//instructions: +10.6G (+53.42%)
🟥 build/module/Iris.Algebra.COFESolver//instructions: +12.4G (+104.78%)
🟥 build/module/Iris.Algebra.Csum//instructions: +8.3G (+42.88%)
🟥 build/module/Iris.Algebra.Heap//instructions: +5.5G (+44.37%)
🟥 build/module/Iris.Algebra.HeapView//instructions: +7.1G (+42.48%)
🟥 build/module/Iris.Algebra.OFE//instructions: +21.1G (+115.24%)
🟥 build/module/Iris.Examples.Fix//instructions: +6.0G (+157.52%)
🟥 build/module/Iris.Instances.IProp.Instance//instructions: +7.8G (+48.36%)
🟥 build/module/Iris.Instances.Lib.Boxes//instructions: +6.4G (+30.69%)
🟥 build/module/Iris.Instances.Lib.GhostMap//instructions: +13.8G (+29.29%)
and 1 hidden

Medium changes (49🟥)

🟥 build/module/Iris.Algebra.Agree//instructions: +3.8G (+54.69%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Auth//instructions: +4.5G (+64.73%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.BigOp//instructions: +3.3G (+31.85%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Chain//instructions: +2.9G (+128.71%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.DFrac//instructions: +1.8G (+11.76%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.DynReservationMap//instructions: +3.4G (+40.07%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Excl//instructions: +2.3G (+67.14%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Frac//instructions: +1.2G (+26.46%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Functions//instructions: +1.8G (+75.48%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.GenMap//instructions: +4.0G (+50.81%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.IProp//instructions: +3.0G (+104.53%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.IsOp//instructions: +1.0G (+74.91%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.LeibnizMultiSet//instructions: +1.0G (+42.87%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.LeibnizSet//instructions: +1.5G (+24.42%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Lib.DFracAgree//instructions: +1.5G (+69.64%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Lib.ExclAuth//instructions: +1.4G (+55.35%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Lib.FracAuth//instructions: +2.6G (+47.67%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Lib.MonoList//instructions: +1.8G (+37.93%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Lib.MonoNat//instructions: +1.7G (+50.47%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Lib.MonoZ//instructions: +1.2G (+34.07%) (reduced significance based on absolute threshold)
and 29 more

Small changes (129🟥)

🟥 build/lakeprof/longest build path//instructions: +72.3G (+11.95%)
🟥 build/module/Iris.Algebra.Lib//instructions: +734.2M (+61.23%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Monoid//instructions: +992.9M (+74.40%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.StepIndex//instructions: +2.8G (+97.77%) (reduced significance based on *//lines)
🟥 build/module/Iris.Algebra//instructions: +761.3M (+64.01%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.BI.BI//instructions: +622.8M (+20.46%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.BI.BigOp.BigAndList//instructions: +657.5M (+19.33%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.BI.BigOp.BigAndMap//instructions: +665.1M (+17.63%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.BI.BigOp.BigOp//instructions: +922.4M (+5.64%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.BI.BigOp.BigOrList//instructions: +666.3M (+19.75%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.BI.BigOp.BigSepMSet//instructions: +655.1M (+15.06%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.BI.BigOp.BigSepMap//instructions: +762.8M (+9.56%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.BI.BigOp.BigSepSet//instructions: +646.9M (+11.52%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.BI.BigOp//instructions: +450.2M (+30.82%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.BI.Classes//instructions: +454.1M (+29.32%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.BI.Cmra//instructions: +740.9M (+23.09%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.BI.DerivedLawsLater//instructions: +949.1M (+11.12%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.BI.Embedding//instructions: +813.7M (+10.00%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.BI.Extensions//instructions: +465.9M (+29.56%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.BI.Instances//instructions: +454.8M (+28.31%) (reduced significance based on absolute threshold)
and 109 more

alvinylt added 30 commits July 28, 2026 11:51

Towards parametrised step-indexing in OFE.lean, add SIdx instance…

1e36968

… for `Nat` in `StepIndexFinite.lean`

Remove redundant change

9e9cd3a

Update proofs in OFE.lean

acbccb8

More proof updates in OFE.lean

3d88a76

Update proof of isCOFE_later

ee7e8cf

Update proof for DiscreteO.dist_inj

f5e71e5

Update proofs that involve letI/haveI

2feacf2

Two more minor proof updates

f59dcf0

Port bchain as BChain

a6baad5

Extend IsCOFE with bounded completion fields, proofs of IsCOFE in…

d5ae9fd

…stances not yet complete

Port bcompl-related theorems, proofs not complete

858fb80

Introduce BFChain definitions with sorry for proofs

3efce59

Replace all proofs in section `Fixpoint`, all requires rewrite

Fix StepIndexFinite.lean: Nat-specific formulations of Dist.le …

b7565a9

…and `Contractive.succ`

CMRA.lean: CMRA α extends OFE Nat α

a952ca9

Parametrisation of `CMRA` to be done in a future PR

COFESolver.lean: OFE Nat ..., some proofs with sorry

15ac195

Replace OFE ... with OFE Nat ..., COFE ... with COFE Nat ...,…

04cc2c7

… and so on

Merge remote-tracking branch 'upstream/master' into StepIndexOFE

54400ee

Update limitPreserving_emp_valid

fd1b341

Update Algebra/Lib/UFracAuth.lean and Algebra/Functions.lean

86d0e37

Fill in proofs for the new IsCOFE fields

cb0943e

Fill in the proofs for the extra IsCOFE fields, trivial at the mome…

b9b3587

…nt with `SI = Nat`

sigT_cofe: proofs for extra IsCOFE fields with helper lemmas

60aa4f3

Complete LimitPreserving proofs

29f4eba

Complete proofs in section Fixpoint

57efae6

Proof formatting in OFE.lean

6314a22

Clean up unnecessary local instance declarations

8161923

Switch of LimitPreserving back to a type class

f99f9ae

Remove duplicate [SIdx SI] assumption

ddf2c83

Update IrisMath/MeasureTheory.lean

f2f5287

Add missing rocq_alias annotations, remove duplicate instance

6109995

alvinylt and others added 24 commits August 3, 2026 19:26

ProdOF and SumOF: SI as an implicit parameter

366c6bf

Remove redundant rocq_alias entry

e370972

chore: minor cleanup in GhostMap and StepIndexFinite

b41c97c

cleanup OFE

da2bfba

checkpoint

c8f8cfb

implement repo-wide pass

05cb018

remove some comments

d1a8909

Remove duplicate import of StepIndexRegistry

ed97fd5

restore Unit OFE to an instance

f6960eb

Merge branch 'master' into sidx-defaults

8063470

fix build

f68356e

autoParam for eq_dist

4bb8758

cleanup eq_dist

285b870

Merge remote-tracking branch 'origin/master' into sidx-defaults

82ae4d3

cleanup

57b471c

final cleanup

ece2feb

bubble up local stepindex annotations

6f64adf

prune some SI annotations

9f29aae

prune OFE

d940990

fix numbers

52a7553

move BigOp

0248316

Merge remote-tracking branch 'origin/master' into sidx-defaults

63e2f11

hopefully fix build

782f99f

generalize algebra

f6ff79d

markusdemedeiros marked this pull request as ready for review August 26, 2026 18:48

Navigation Menu

Uh oh!

experiment: Generalize step indices using `local stepindex` across all of Algebra/ - #683

experiment: Generalize step indices using `local stepindex` across all of Algebra/#683
markusdemedeiros wants to merge 54 commits into
masterfrom
sidx-defaults-algebra-experiment

markusdemedeiros commented Aug 26, 2026

Uh oh!

markusdemedeiros commented Aug 26, 2026

Uh oh!

markusdemedeiros commented Aug 26, 2026

Uh oh!

leanprover-radar commented Aug 26, 2026 •

edited

Loading

Uh oh!

leanprover-radar commented Aug 26, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Uh oh!

Conversation

markusdemedeiros commented Aug 26, 2026

Uh oh!

markusdemedeiros commented Aug 26, 2026

Uh oh!

markusdemedeiros commented Aug 26, 2026

Uh oh!

leanprover-radar commented Aug 26, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-radar commented Aug 26, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

leanprover-radar commented Aug 26, 2026 •

edited

Loading

leanprover-radar commented Aug 26, 2026 •

edited

Loading