feat: coPset, gset, and namespace infrastructure for invariant masks (PR A)

PORTING.md

@@ -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
@@ -62,7 +62,7 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
   - [ ] CMRA
   - [ ] Updates
 - [ ] `gset.v` 
-  - [ ] CMRA
+  - [x] CMRA
   - [ ] Updates
 - [ ] `list.v` 
   - Is this an instance of the `Heap` CMRA?
@@ -425,5 +425,3 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
   - [ ] `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