feat: fixpoint base of weakest precondition

[lihaokun]

Description

Lean 4 port of the fixpoint base of Coq Iris's program logic weakest
precondition (iris/program_logic/weakestpre.v). Adds Stuckness, the
IrisGS typeclass, wp_pre (with num_laters_per_step parameterization),
its Contractive instance, and wp / wp_unfold via the upstream
fixpoint / fixpoint_unfold machinery.

Builds on #370 (Language interface).

Contributes to porting weakestpre.v in PORTING.md.

Iris/Iris/ProgramLogic/WeakestPre.lean

• Stuckness inductive — 1:1 with Coq stuckness
• IrisGS typeclass — all 5 fields of Coq irisGS_gen:
  • iris_invGS via extends InvGS_gen hlc GF
  • state_interp / fork_post
  • num_laters_per_step / state_interp_mono
• wp_pre (body 1:1 with Coq, using ={∅}▷=∗^[num_laters_per_step ns + 1])
• wp_pre_contractive Contractive instance
• wp := fixpoint (wp_pre s)
• wp_unfold via upstream fixpoint_unfold

Adds one private helper step_fupdN_ne to factor out the
BIFUpdate.ne + later_ne + BIFUpdate.ne induction over
num_laters_per_step ns needed by the Contractive proof.

Adaptations vs Coq

• Stuckness constructors lowercase: notStuck / maybeStuck per Lean
  convention.
• Plain function-space arrows: CoPset → Expr → (Val → IProp GF) → IProp GF
  rather than Coq's explicit discrete-OFE arrows -d>. The upstream
  function-space COFE instance derives the equivalent OFE structure
  automatically (and the source types here have no non-trivial OFE structure).
• wp_pre_contractive proof is manual: ~25 lines plus the small private
  step_fupdN_ne helper, since iris-lean doesn't yet have the equivalent of
  Coq's f_contractive tactic. Structure follows
  Iris/Examples/IProp.lean:wp_F_contractive. Once tactic automation lands
  (cf. feat: iloeb #387 for iLöb), this can likely be shortened.
• wp_unfold proof: wraps wp_pre s into a ContractiveHom, then
  combines fixpoint_unfold with pointwise evaluation on the function-space
  OFE and BI.equiv_iff to convert ≡ to ⊣⊢. Same pattern as
  Iris/Examples/IProp.lean:wp_unfold.
• Auxiliary instance: Inhabited (WPFun) (required by fixpoint); set to
  the constant True proposition.

Checklist

• My code follows the mathlib naming and code style conventions
• I have updated PORTING.md as appropriate
• I have added my name to the authors section of any appropriate files

[lzy0505]

Thanks for the PR. Before reviewing it, can you clean up all the AI generated comments, and add @[rocq_alias] annotations?

[lihaokun]

Thanks @lzy0505, addressed both points in 8238b50:

• Trimmed comments: removed the section-level blocks and inline tactic
  comments; kept only the file header summary and a single-line per-field doc
  on IrisGS. Happy to add specific docs back if anything is unclear.
• @[rocq_alias] annotations on: Stuckness, Stuckness.le, IrisGS,
  wp_pre, wp_pre_contractive, wp (Coq wp_def), wp_unfold, and
  step_fupdN_ne (in Iris/BI/Updates.lean).

[lzy0505]

@lihaokun BTW, @ayhon is also working on this. So please coordinate to make sure you two don't work on the same thing if you plan to port the rest of the file.

[ayhon]

I think there's a lot of overlap between this PR and mine, see https://github.com/ayhon/iris-lean/tree/fele/feat/add-weakestpre.

[ayhon]

In particular, these seem to be all definitions I had already ported in my PR, although some of the proofs are a bit shorter, in particular I needed many more lines and auxiliary lemmas to prove wp_pre_contractive. Other than that, in my PR I seem to be a bit further ahead, I have also proved wp_contractive, wp_ne, and some lemmas on fupd using the proof mode.

[ayhon]

@lihaokun I had paused development of this PR to develop the iloeb tactic, but if it's something you require right now I wouldn't mind reprioritizing it so you are unblocked. What are you working towards right now?

[lihaokun]

Hi @lzy0505 and @ayhon,

First — thanks @lzy0505 for the careful review on this PR; the feedback will carry over to the next round either way.

And second, I'm sorry — I missed @ayhon's fele/feat/add-weakestpre branch before opening this. There's clear overlap, and his version is more complete than what I have here (real proofs for wp_strong_mono / fupd_wp / wp_fupd / wp_atomic, a three-class decomposition StateInterp / NumLatersPerStep / IrisGS_gen, and consistent style with the merged #370). Before deciding what to do with this PR, I'd like to discuss how we might divide the work.

Some context on why I'm interested in this corner of iris-lean: I'm exploring whether VST (the Verified Software Toolchain for CompCert C) can be ported to Lean 4. For that I'll eventually need the full Iris program logic stack on Lean:

Coq file	issue	who
program_logic/weakestpre.v	#346	@ayhon (in progress on fele/feat/add-weakestpre)
program_logic/lifting.v	#348	unclaimed
program_logic/ectx_lifting.v	#349	unclaimed
program_logic/adequacy.v	#352	unclaimed
base_logic/lib/ghost_map.v	—	unclaimed
base_logic/lib/gen_heap.v	—	unclaimed

@ayhon — if you're taking on weakestpre.v, that's wonderful. In the meantime I can keep moving on my side by stubbing those downstream interfaces (lifting.v / ectx_lifting.v / adequacy.v plus the two base_logic/lib/ files) locally; once yours lands I'd be happy to revisit and turn the work into upstream PRs if that's useful.

Happy to hear thoughts on how to coordinate. Sorry again for the duplicate effort.

[Kaptch]

Hi @lihaokun. Thank you for your PR! I agree that we should discuss the splitting of program logic into chunks for unblocking purposes.
The definition of wp probably should lend first, and then later we could take a look how to merge everything else.

@ayhon would you mind create a separate early PR for just a bare-bone definition of wp + wp-unfold from your branch (and probably some lemmas that you feel could be merged early on)?
It might be better if there is an open PR, so that people can start building on top of it.
In this case, notations/proof mode typeclasses/lifts/adequacy/etc. can be later merged on top, and meanwhile @lihaokun and other people interested in working with HeapLang/VST can already start doing so by using downstream substitutes on top of your PR, and later we can see how to integrate it all together.

@lihaokun would you be okay with that? It might be easier to merge other things that @ayhon was working on, if the definition of wp comes from fele/feat/add-weakestpre.
If both you and @ayhon are okay with this solution, then we could also discuss here if/how you want to split some other parts about program logic, so that there are no overlaps.
It's just a proposal, and other people working on the port are also extremely welcome to voice their opinions.

Just in case of concerns about merging, I can help with backporting and merging, when the need arises.

[ayhon]

@Kaptch I don't mind publishing my current PR as a draft. I need to rebase it so it sits on top of #387 though, since I intend to use the iloeb tactic in my proofs. I will get to it once I finish redacting this message.

EDIT: I published my current draft in #393. I'll try to remember not to force push onto it to ease the work of people basing off of it.

@lihaokun, I just got back form talking with my supervisors and we have no plans to work on program_logic/adequacy.v in the future, so feel free to work on that right now. program_logic/weakestpre.v is what I'm currently working on, and my plans for next steps would be to work on program_logic/lifting.v and program_logic/ectx_lifting.v, since I expect to use them in the future. In particular, because I expect to use them a lot in the future, I would like to have the opportunity of porting them, since I believe this would help me develop a better understanding of their contents. However, I currently have no estimates as to how long it will take me to finish them. What are your time constraints on having these files ready? Would waiting for a week be acceptable to you?

[lihaokun]

Hi @ayhon — sounds good to me, and a week is completely fine. I'm still on the CompCert/VST translation side (currently Common / Clight), so the WP layer isn't on my critical path yet.

So the division would be:

• you: weakestpre.v + lifting.v + ectx_lifting.v (you mentioned wanting to port the latter two yourself for understanding — happy to leave them to you)
• me: program_logic/adequacy.v (thanks for the explicit hand-off)

In the meantime I'll keep sorry'd stubs of the WP interface in lean-vst and rebase onto your draft PR once it's open.

@Kaptch — the proposal works for me, thanks for offering to help with backports.