Skip to content

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

Open
hxrts wants to merge 1 commit into
masterfrom
fork/iris/copset
Open

hxrts wants to merge 1 commit into
masterfrom
fork/iris/copset

Conversation

@hxrts

@hxrts hxrts commented Jan 29, 2026 •

Copy link
Copy Markdown
Owner

Add the data structures and resource algebras needed for invariant mask reasoning in the base logic (wsat, fancy updates). Includes CoPset/GSet types with set operations, CoPsetDisj/GSetDisj disjoint-union CMRAs, hierarchical namespaces with nclose, and PORTING.md updates.

Description

Briefly describe your changes, and link any issues if appropriate.

Fixes # (issue number)

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

Add the data structures and resource algebras needed for invariant mask
reasoning in the base logic (wsat, fancy updates). Includes CoPset/GSet
types with set operations, CoPsetDisj/GSetDisj disjoint-union CMRAs,
hierarchical namespaces with nclose, and PORTING.md updates.
@hxrts

hxrts commented Jan 29, 2026

Copy link
Copy Markdown
Owner Author

I probably need to remove the flake.nix from this PR but waiting till the end because git needs to see the nix flake for the environment to work.

@hxrts hxrts changed the title feat: coPset, gset, and namespace infrastructure for invariant masks feat: coPset, gset, and namespace infrastructure for invariant masks (PR A) Jan 29, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant