feat: add total weakest preconditions

[mfornet]

We recently migrated to use iris-lean on talos, our project to verify wasm binaries. However, during the migration we loose the ability to reason about code termination, due to the state of TotalWP in the repo. This introduces an initial implementaiton that is already useful to us:

cajal-technologies/talos#166

In particular, one assumption done in this PR is that all transitions under twp produce no forks, as it is this is mostly useful for non-concurrent code. This is similar to how it works in rocq as well.

Claude summary

## Summary

• add a faithful Iris-Rocq total weakest-precondition core based on BI least fixpoints
• add total primitive and evaluation-context lifting rules, including deterministic no-fork APIs intended for single-threaded Wasm semantics
• add fork-aware total adequacy and strong-normalization theorems, with sequential corollaries
• add proof-mode framing/update instances and a conversion from TWP to partial WP
• add a deterministic test language covering multi-step execution, state changes, nondeterministic countdown branching, no-fork adequacy, stuck terms, and observable steps
• add a HeapLang pure-execution smoke test while documenting deferred HeapLang-specific and concurrency-specific APIs

Motivation

This provides the total-correctness layer needed to prove termination of first-order, single-threaded Wasm-style programs while keeping the generic definition and adequacy result compatible with Iris-Rocq's fork-aware semantics. Silent reductions and explicit trap modeling are documented as part of the Wasm integration contract.

Upstream compatibility

The branch is rebased onto current master (3d3dfe0) and its TWP proof-mode instances follow the new ElimModal InOut parameter introduced upstream.

Validation

• lake build — all 269 jobs passed
• Lean language-server diagnostics — zero errors and zero warnings in all added/modified TWP modules, tests, and aggregate imports
• axiom checks for Iris.twp.to_wp, Iris.ProgramLogic.twp_total, and the end-to-end strong-normalization test — only propext, Classical.choice, and Quot.sound
• git diff --check — clean

[lzy0505]

Thanks for the PR.

From a quick scan, I found some signs that suggest AI-generated content wasn’t properly reviewed by you. For example, please use your own name in the copyright header and remove any comments mentioning WASM.

[mfornet]

@lzy0505 I took care of your comments, and reviewed all the code. Can you please take another look.

[lzy0505]

I golfed the Iris proofs in Iris/Iris/ProgramLogic/TotalWeakestPre.lean. This was a quick pass and I’ll do another round later.

Several patterns appeared so many times so I believe you could point AI to my commit and let it golf the remaining files.
I will continue my pass after that.

[mfornet]

@lzy0505 I ran a few rounds of golfing.

Thanks for taking a look to this PR. What do you think are the chances this gets merged? if there is any chance this doesn't get merged I'd rather move all this proofs to my library and just have a regular dependency on iris-lean rather than maintaining a dependency on my fork.

[lzy0505]

@mfornet Thanks! I think this PR is a solid starting point. I will make a pass and try to get it merged by the end of this week.