WIP: Experiment (outParam): Generalize type of step indices with metaprogramming and typeclasses and outParam by MackieLoeffel · Pull Request #627 · leanprover-community/iris-lean

MackieLoeffel · 2026-08-13T11:05:49Z

Description

This is an experiment for a version of #576 using outParam to see the performance impact.

THIS IS SHOULD NOT BE MERGED!

… 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`

MackieLoeffel · 2026-08-13T11:06:01Z

!bench

leanprover-radar · 2026-08-13T11:06:46Z

Benchmark results for 333efaa against a5f3796 are in. There are significant results. @MackieLoeffel

🟥 build//instructions: +131.2G (+7.49%)

Large changes (1🟥)

1 hidden

Medium changes (21🟥)

🟥 build/module/Iris.Algebra.Agree//instructions: +1.6G (+22.86%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Auth//instructions: +1.1G (+16.55%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.BigOp//instructions: +1.2G (+11.31%)
🟥 build/module/Iris.Algebra.CMRA//instructions: +2.7G (+13.71%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.COFESolver//instructions: +3.9G (+32.71%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Csum//instructions: +2.4G (+12.28%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.DFrac//instructions: +1.1G (+7.21%)
🟥 build/module/Iris.Algebra.DynReservationMap//instructions: +1.1G (+12.60%)
🟥 build/module/Iris.Algebra.Excl//instructions: +1.3G (+37.53%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.GenMap//instructions: +1.5G (+18.70%)
🟥 build/module/Iris.Algebra.Heap//instructions: +2.4G (+19.36%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.HeapView//instructions: +1.5G (+8.80%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.IProp//instructions: +1.6G (+55.63%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.List//instructions: +1.5G (+31.30%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.ReservationMap//instructions: +1.1G (+15.35%)
🟥 build/module/Iris.Algebra.UPred//instructions: +1.0G (+43.24%)
🟥 build/module/Iris.Algebra.View//instructions: +2.2G (+10.18%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.BI.MonPred//instructions: +1.1G (+7.56%)
🟥 build/module/Iris.Examples.Fix//instructions: +2.2G (+58.35%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Instances.IProp.Instance//instructions: +1.6G (+9.97%) (reduced significance based on absolute threshold)
and 1 more

Small changes (149🟥)

🟥 build/module/Iris.Algebra.Frac//instructions: +899.7M (+20.58%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Functions//instructions: +944.4M (+40.63%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.IsOp//instructions: +833.7M (+60.59%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.LeibnizSet//instructions: +884.6M (+14.74%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Lib.DFracAgree//instructions: +946.0M (+42.66%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Lib.ExclAuth//instructions: +908.6M (+36.52%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Lib.FracAuth//instructions: +877.3M (+16.24%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Lib.MonoNat//instructions: +841.3M (+24.28%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Lib.UFracAuth//instructions: +880.8M (+19.17%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Lib//instructions: +731.8M (+61.03%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.LocalUpdates//instructions: +927.8M (+26.87%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Monoid//instructions: +866.6M (+64.93%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Mra//instructions: +861.4M (+42.10%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Numbers//instructions: +853.4M (+16.27%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.OFE//instructions: +12.7G (+69.26%) (reduced significance based on *//lines)
🟥 build/module/Iris.Algebra.StepIndex//instructions: +2.5G (+88.47%) (reduced significance based on *//lines)
🟥 build/module/Iris.Algebra.UFrac//instructions: +866.1M (+33.07%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Updates//instructions: +863.4M (+26.24%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra//instructions: +747.9M (+62.89%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.BI.Algebra//instructions: +575.6M (+9.66%)
and 129 more

MackieLoeffel · 2026-08-13T16:02:53Z

!bench

leanprover-radar · 2026-08-13T16:25:41Z

Benchmark results for 83591a7 against a5f3796 are in. There are significant results. @MackieLoeffel

🟥 build//instructions: +139.9G (+7.99%)

Large changes (1🟥)

1 hidden

Medium changes (25🟥)

🟥 build/module/Iris.Algebra.Agree//instructions: +1.7G (+24.44%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Auth//instructions: +1.3G (+18.50%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.BigOp//instructions: +1.2G (+12.00%)
🟥 build/module/Iris.Algebra.CMRA//instructions: +2.8G (+13.95%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.COFESolver//instructions: +3.9G (+33.26%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Csum//instructions: +2.5G (+12.86%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.DFrac//instructions: +1.2G (+7.56%)
🟥 build/module/Iris.Algebra.DynReservationMap//instructions: +1.1G (+13.40%)
🟥 build/module/Iris.Algebra.Excl//instructions: +1.4G (+39.65%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.GenMap//instructions: +1.6G (+20.21%)
🟥 build/module/Iris.Algebra.Heap//instructions: +2.6G (+20.50%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.HeapView//instructions: +1.7G (+10.34%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.IProp//instructions: +1.7G (+59.41%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.List//instructions: +1.5G (+32.11%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.ReservationMap//instructions: +1.2G (+16.49%)
🟥 build/module/Iris.Algebra.UPred//instructions: +1.1G (+45.34%)
🟥 build/module/Iris.Algebra.View//instructions: +2.4G (+11.05%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.BI.InternalEq//instructions: +1.1G (+17.12%)
🟥 build/module/Iris.BI.MonPred//instructions: +1.3G (+9.00%)
🟥 build/module/Iris.Examples.Fix//instructions: +3.2G (+82.80%) (reduced significance based on absolute threshold)
and 5 more

Small changes (144🟥)

🟥 build/module/Iris.Algebra.Frac//instructions: +915.7M (+20.95%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Functions//instructions: +963.4M (+41.45%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.IsOp//instructions: +839.7M (+61.03%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.LeibnizSet//instructions: +898.4M (+14.97%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Lib.DFracAgree//instructions: +976.0M (+44.00%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Lib.ExclAuth//instructions: +950.1M (+38.19%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Lib.FracAuth//instructions: +925.9M (+17.13%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Lib.MonoNat//instructions: +881.6M (+25.45%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Lib.UFracAuth//instructions: +946.6M (+20.60%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Lib//instructions: +735.9M (+61.37%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.LocalUpdates//instructions: +941.4M (+27.27%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Monoid//instructions: +873.4M (+65.44%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Mra//instructions: +880.7M (+43.04%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Numbers//instructions: +897.4M (+17.11%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.OFE//instructions: +12.7G (+69.24%) (reduced significance based on *//lines)
🟥 build/module/Iris.Algebra.StepIndex//instructions: +3.1G (+107.61%) (reduced significance based on *//lines)
🟥 build/module/Iris.Algebra.UFrac//instructions: +882.5M (+33.70%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra.Updates//instructions: +879.2M (+26.72%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.Algebra//instructions: +748.7M (+62.95%) (reduced significance based on absolute threshold)
🟥 build/module/Iris.BI.Algebra//instructions: +622.7M (+10.45%)
and 124 more

This reverts commit 83591a7.

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

markusdemedeiros and others added 22 commits August 3, 2026 16:10

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

try performance of outParam

333efaa

MackieLoeffel marked this pull request as draft August 13, 2026 11:06

MackieLoeffel mentioned this pull request Aug 13, 2026

feat: Generalize type of step indices with metaprogramming and typeclasses #576

Open

try different version of the hierarchy

83591a7

Revert "try different version of the hierarchy"

b68f698

This reverts commit 83591a7.

Navigation Menu

Uh oh!

WIP: Experiment (outParam): Generalize type of step indices with metaprogramming and typeclasses and outParam - #627

WIP: Experiment (outParam): Generalize type of step indices with metaprogramming and typeclasses and outParam#627
MackieLoeffel wants to merge 56 commits into
masterfrom
sidx-outparam

MackieLoeffel commented Aug 13, 2026

Uh oh!

MackieLoeffel commented Aug 13, 2026

Uh oh!

leanprover-radar commented Aug 13, 2026 •

edited

Loading

Uh oh!

MackieLoeffel commented Aug 13, 2026

Uh oh!

leanprover-radar commented Aug 13, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Uh oh!

Conversation

MackieLoeffel commented Aug 13, 2026

Description

Uh oh!

MackieLoeffel commented Aug 13, 2026

Uh oh!

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

Uh oh!

Uh oh!

MackieLoeffel commented Aug 13, 2026

Uh oh!

leanprover-radar commented Aug 13, 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 13, 2026 •

edited

Loading

leanprover-radar commented Aug 13, 2026 •

edited

Loading