World satisfaction, fancy updates, invariants, weakest preconditions, ghost state, adequacy

[hxrts]

Hi there, I'm porting a few things from the coq implementation that I'd like to use for another project I'm working on.

I don't have any acute need to upstream, but thought I'd offer if there's interest. Also happy to modify these to align with maintainer guidance.

These are AI assisted PRs, but trying to keep things organized and understandable.

Cheers!

[hxrts]

Dependency Graph

Phase 1 (parallel):
  PR A: coPset ─────────────────┐
  PR B: big-op ─────────────────┤
  PR C: auth-updates ───────────┤
                                │
Phase 2:                        ▼
  PR D: wsat ───────────────────┤
                                │
Phase 3:                        ▼
  PR E: fupd ───────────────────┤
                  │             │
                  ▼             ▼
  PR F: invariants          PR H: wp
                  │
Phase 4:          ▼
  PR G: cinv

PR Summaries

PR	Fork PR	Branch	Content	Notes
D: Wsat	#5	fork/iris/wsat	World satisfaction (wsat, ownI, ownE, ownD)	No competing upstream PR
E: Fancy Updates	#6	fork/iris/fupd	uPred_fupd, soundness	No competing upstream PR. #141 (imodintro/imod) is proof mode tactics only, not the fupd definition
F: Invariants	—	fork/iris/invariants	inv, inv_alloc, inv_acc	No competing upstream PR
G: Cancelable Invariants	#7	fork/iris/cinv	cinv, cinv_own, cinv_acc, cinv_cancel	No competing upstream PR

Mergeable with coordination

PR	Fork PR	Branch	Content	Notes
A: coPset/Namespaces	#1	fork/iris/copset	CoPset, Positive, Namespace	Upstream #78 (Remyjck) covers same ground but stale since Jul 2025. Ours is likely more complete
H: Weakest Pre	#8	fork/iris/wp	Language, WP fixpoint + rules	Upstream #135 (WP examples, markusdemedeiros) is exploratory; #93 (heaplang, Shreyas4991) touches language interface. Our generic port is complementary but maintainers haven't settled on program logic design

Likely superseded

PR	Fork PR	Branch	Content	Competing upstream PRs
B: Big Op	#2	fork/iris/big-op	Monoid, BigOp (algebra + BI)	#131 (FiniteMap, lzy0505), #132 (monoid+big_op, lzy0505), #113 (BI big ops, lzy0505) — all active Jan 2026
C: Auth/View	#3	fork/iris/auth-updates	Auth CMRA, View, Heap, HeapView	#134 (Auth CMRA, ahuoguo), #130 (Heap/HeapView functors, screenl) — both active Jan 2026

[hxrts]

Dependency Graph

PRs A–H (Phase 1)
    │
    ├── PR I: language ──────────────┐
    │                                │
    │                                ▼
    ├── PR H ──────────► PR J: wp-rules + lifting
    │                                │
    │                                ▼
    ├── PR E ──────────► PR K: adequacy
    │
    ├── PR C, PR D ────► PR L: ghost-map + gen-heap
    │
    ├── PR M: saved-prop + ghost-var (independent)
    │
    └── PR N: auth-own (independent)

Mergeable

PR	Fork PR	Branch	Content	Notes
K: Adequacy	#12	fork/iris/adequacy	wp_strong_adequacy, wp_adequacy, wp_invariance, thread pool helpers, BIFUpdatePlainly	No competing upstream PR. 0 sorries. Split into submodules under Adequacy/ (ThreadPool, WpStep, WptpHelpers A/B/C, Preservation, StrongAdequacy, SimplifiedAdequacy, Invariance, FUpd)
L: Ghost Map + Gen Heap	#13	fork/iris/ghost-state	ghost_map_auth, ghost_map_elem, ghost_map_alloc, lookup/insert/delete/update; gen_heap_interp, pointsto	No competing upstream PR. 0 sorries. GenHeap is thin wrapper over GhostMap. Meta-data infrastructure (meta_token, reservation_map) omitted
M: Saved Prop + Ghost Var	#14	fork/iris/ghost-primitives	saved_prop_own, saved_prop_alloc, saved_prop_agree; ghost_var_alloc, ghost_var_agree, ghost_var_update, ghost_var_persist	No competing upstream PR. 0 sorries. Saved prop agreement uses UPred.eq with bridge infrastructure in Instances/UPred/InternalEq.lean
N: Auth Own	#11	fork/iris/touchup	Auth BI-level ownership theorems (AuthOwn.lean)	No competing upstream PR. 0 sorries. Merged to vendor

Mergeable with coordination

PR	Fork PR	Branch	Content	Notes
I: Language Interface	#9	fork/iris/language	Language, LanguageMixin, EctxLanguage, EctxLanguageMixin	Upstream #93 (heaplang, Shreyas4991) defines a concrete language; #135 (WP examples, markusdemedeiros) is exploratory. Our port is the generic abstract interface from language.v + ectx_language.v
J: WP Rules + Lifting	#10	fork/iris/wp-rules	wp_lift_step, wp_lift_pure_step_no_fork, wp_lift_atomic_step, wp_ectx_bind	Upstream #135 (WP examples) is related but exploratory. Ports lifting.v + ectx_lifting.v

[hxrts]

So the contents of the PRs above are all fully proven. I have a branch here with everything together here: https://github.com/hxrts/iris-lean/tree/fork/iris/vendor.

I realize it's a reviewer's nightmare to have a massive external contribution dropped like this, so no worries if my PRs never make it in. As mentioned above, this is work that unblocked another project for me.

Feel encouraged to cherry pick anything, or use this as a reference. I tried to stay very close to the coq implementation to make the port more-or-less mechanical, however there are certainly cases where a lean-native proof strategy would have been more concise or more elegant.

Appreciate the work you all are doing.