feat: Weakest preconditions - Language interface and WP fixpoint (PR H)

PORTING.md

@@ -12,12 +12,12 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
 - [ ] `agree.v`
   - [x] CMRA 
   - [x] Functors
-- [ ] `auth.v`
-  - [ ] CMRA
-  - [ ] Updates
-  - [ ] Functors
-- [ ] `big_op.v`
-  - TBD (Zongyuan?)
+- [x] `auth.v`
+  - [x] CMRA
+  - [x] Updates
+  - [x] Functors
+- [x] `big_op.v`
+  - [x] `bigOpL`, `bigOpM` definitions and lemmas
 - [ ] `cmra.v`
   - [x] Lemmas
   - [ ] Total CMRA construction
@@ -33,8 +33,8 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
   - [x] Isomorphisms
 - [ ] `cmra_big_op.v` 
 - [ ] `coPset.v`
-  - [ ] coPset definition
-  - [ ] CMRA
+  - [x] coPset definition
+  - [x] CMRA
 - [x] `cofe_solver.v` 
 - [ ] `csum.v`
   - [ ] CMRA
@@ -54,15 +54,15 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
 - [ ] `functions.v` (nb. contained in `CMRA.lean`)
   - [x] CMRA
   - [ ] Updates
-- [ ] `gmap.v` (nb. generalized in `Heap.lean`)
+- [x] `gmap.v` (nb. generalized in `Heap.lean`)
   - [x] CMRA
   - [ ] Updates
-  - [ ] Functors
+  - [x] Functors
 - [ ] `gmultiset.v` 
   - [ ] CMRA
   - [ ] Updates
 - [ ] `gset.v` 
-  - [ ] CMRA
+  - [x] CMRA
   - [ ] Updates
 - [ ] `list.v` 
   - Is this an instance of the `Heap` CMRA?
@@ -72,7 +72,7 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
 - [ ] `max_prefix_list.v` 
   - [ ] Lemmas
   - [ ] Functors
-- [ ] `monoid.v`
+- [x] `monoid.v`
 - [ ] `mra.v`
 - [x] `numbers.v`
 - [ ]  `ofe.v`
@@ -111,10 +111,10 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
 - [ ] `vector.v` 
   - [ ] CMRA
   - [ ] Functors
-- [ ] `view.v` 
+- [x] `view.v`
   - [x] CMRA
   - [x] Updates
-  - [ ] Functors
+  - [x] Functors
 - [ ] `lib/dfrac_agree.v` 
   - [ ] Lemmas
   - [ ] Updates
@@ -126,10 +126,10 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
   - [ ] Lemmas
   - [ ] Updates
   - [ ] Functors
-- [ ] `lib/gmap_view.v` (nb. generalized in `HeapView.lean`)
+- [x] `lib/gmap_view.v` (nb. generalized in `HeapView.lean`)
   - [x] CMRA
   - [x] Updates
-  - [ ] Functors
+  - [x] Functors
 - [ ] `lib/gset_bij.v` 
 - [ ] `lib/mono_Z.v` (nb. generalize to `MonoNumbers.lean`)
 - [ ] `lib/mono_list.v` 
@@ -163,18 +163,18 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
   - [x] Later lemmas
   - [x] Update lemmas
 - [ ] `lib/boxes.v`
-- [ ] `lib/cancelable_invariants.v`
+- [x] `lib/cancelable_invariants.v`
 - [ ] `lib/fancy_updates.v`
-  - [ ] FUpd instance
-  - [ ] Soundness
+  - [x] FUpd instance
+  - [x] Soundness
   - [ ] ProofMode instances
 - [ ] `lib/fancy_updates_from_vs.v`
 - [ ] `lib/gen_heap.v`
 - [ ] `lib/gen_inv_heap.v`
 - [ ] `lib/ghost_map.v`
 - [ ] `lib/ghost_var.v`
 - [ ] `lib/gset_bij.v`
-- [ ] `lib/invariants.v`
+- [x] `lib/invariants.v`
 - [ ] `lib/iprop.v`
   - [x] Definition
   - [ ] subG 
@@ -192,14 +192,15 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
 - [ ] `lib/proph_map.v`
 - [ ] `lib/saved_prop.v`
 - [ ] `lib/token.v`
-- [ ] `lib/wsat.v`
+- [x] `lib/wsat.v`
 
 ## BI
 
 - [ ] `algebra.v`
 - `ascii.v`
 - [x] `bi.v`
-- [ ] `big_op.v`
+- [x] `big_op.v`
+  - [x] `big_sepL`, `big_sepM` definitions and lemmas
 - [ ] `cmra.v`
 - [x] `derived_connectives.v`
 - [ ] `derived_laws.v`
@@ -231,7 +232,7 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
 - [ ] `updates.v`
   - [x] FUpd class
   - [ ] Big op lemmas
-- [ ] `weakestpre.v`
+- [x] `weakestpre.v`
 - [ ] `lib/atomic.v`
 - [ ] `lib/core.v`
 - [ ] `lib/counterexamples.v`
@@ -422,8 +423,6 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
 
 - Program Logic
   - Final decisions about what to port from this folder have not been made yet.
-  - [ ] `language.v`
+  - [x] `language.v`
   - [ ] `ectx_language.v`
   - [ ] `ectxi_language.v`
-
-

flake.nix

@@ -0,0 +1,42 @@
+{
+  description = "Iris - Separation logic in Lean 4";
+
+  inputs = {
+    nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable";
+    flake-utils.url = "github:numtide/flake-utils";
+  };
+
+  outputs =
+    {
+      self,
+      nixpkgs,
+      flake-utils,
+    }:
+    flake-utils.lib.eachDefaultSystem (
+      system:
+      let
+        pkgs = import nixpkgs { inherit system; };
+
+        nativeBuildInputs = with pkgs; [
+          elan
+        ];
+
+        buildInputs =
+          with pkgs;
+          lib.optionals stdenv.isDarwin [
+            libiconv
+          ];
+
+      in
+      {
+        devShells.default = pkgs.mkShell {
+          inherit nativeBuildInputs buildInputs;
+
+          shellHook = ''
+            echo "Iris development environment"
+            echo "Lean: $(elan show 2>/dev/null | head -1 || echo 'not configured')"
+          '';
+        };
+      }
+    );
+}

src/Iris/Algebra.lean

@@ -1,6 +1,7 @@
 import Iris.Algebra.Agree
 import Iris.Algebra.CMRA
 import Iris.Algebra.COFESolver
+import Iris.Algebra.CoPset
 import Iris.Algebra.DFrac
 import Iris.Algebra.Excl
 import Iris.Algebra.Frac
@@ -13,3 +14,6 @@ import Iris.Algebra.UPred
 import Iris.Algebra.Heap
 import Iris.Algebra.View
 import Iris.Algebra.HeapView
+import Iris.Algebra.Auth
+import Iris.Algebra.Monoid
+import Iris.Algebra.BigOp

src/Iris/Algebra/Agree.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Leo Stefanesco. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leo Stefanesco
+Authors: Leo Stefanesco, Puming Liu
 -/
 
 import Iris.Algebra.CMRA
@@ -349,7 +349,7 @@ section agree_map
 
 variable {α β} [OFE α] [OFE β] {f : α → β} [hne : OFE.NonExpansive f]
 
-local instance : OFE.NonExpansive (Agree.map' f) where
+instance : OFE.NonExpansive (Agree.map' f) where
   ne := by
     intro n x₁ x₂ h
     simp only [Agree.map', Agree.dist_def, Agree.dist, List.mem_map, forall_exists_index, and_imp,
@@ -411,7 +411,7 @@ abbrev AgreeRF (F : COFE.OFunctorPre) : COFE.OFunctorPre :=
 
 instance {F} [COFE.OFunctor F] : RFunctor (AgreeRF F) where
   map f g := Agree.map (COFE.OFunctor.map f g)
-  map_ne.ne _ _ _ Hx _ _ Hy  _ := Agree.map_ne <| COFE.OFunctor.map_ne.ne Hx Hy
+  map_ne.ne _ _ _ Hx _ _ Hy _ := Agree.map_ne <| COFE.OFunctor.map_ne.ne Hx Hy
   map_id x := by
     conv=> right; rw [<- (Agree.map_id x)]
     exact (Agree.map_id x) ▸ Agree.agree_map_ext COFE.OFunctor.map_id