Use Iris cmra & Iris style upred by Lee-Janggun · Pull Request #78 · snu-sf/fairness

Lee-Janggun · 2024-08-07T17:26:56Z

Iris style upred으로 갈아 끼운 이유는, 원래 있던 iProp에 Iris에서 하는 seal을 추가해야 하는데, 이걸 하는 김에 그냥 했습니다.
- 근데 이러니까 신기하게 원래 iFrame이 잘 되던게 안되고 반대도 좀 있는거 같네요;; 이건 typeclass inference 을 보면서 디버깅 해야 되서 되게 해결이 좀 귀찮을꺼 같습니다.
- 이건 이제 문제가 아닌 것 같습니다.
이걸 하니까 타입클래스의 량이 늘어서 증명 속도가 좀 느려지는거 같아서 머지 전에 시간 측정을 해봐야 합니다.

Lee-Janggun · 2024-08-15T05:57:39Z

커밋을 3개로 정리했습니다.

Lee-Janggun · 2024-09-12T20:11:44Z

일단 제가 하고 싶은 리팩토링 중 혼자서 할만한건 다 했습니다. 이 이상은 metatheory를 갈아엎는 거라서 혼자선 하기가 좀 어렵네요.

* Note: fos_ticketlock doesn't work on this commit.

* Restore fos_ticketlock. * Also cleanup some impls.

* Requires custom coq-ext-lib, coq-itree, and coq-promising-seq

* Make maps_to_res a special case of discrete_fun_singleton w. excluded middle. * Remove most uses of maps_to_res. Use discrete_fun_singleton as much as possible. * Minimize PCM.v. * Other improvements here and there.

Copilot

Copilot reviewed 147 out of 166 changed files in this pull request and generated 8 comments.

Files not reviewed (19)

Makefile: Language not supported
configure: Language not supported
src/bi/lib/ghost_excl.v: Language not supported
src/bi/lib/ghost_map.v: Language not supported
src/bi/lib/ghost_var.v: Language not supported
src/example/AuthExclAnysRA.v: Language not supported
src/example/AuthExclsRA.v: Language not supported
src/example/Client01.v: Language not supported
src/example/Client01Adeq.v: Language not supported
src/example/Client04.v: Language not supported
src/example/Client04Adeq.v: Language not supported
src/example/Client05.v: Language not supported
src/example/Client05Adeq.v: Language not supported
src/example/ClientSpinlock2.v: Language not supported
src/example/ClientSpinlock2Adeq.v: Language not supported
src/example/DoubleIncr.v: Language not supported
src/example/DoubleIncrTicket.v: Language not supported
src/example/ExclsRA.v: Language not supported
src/example/LifetimeRA.v: Language not supported

Comments suppressed due to low confidence (1)

Refactor-Iris.md:3

[nitpick] The phrase 'own that used' is unclear; consider revising it (for example, to 'and the ownership model used') for clarity.

+- The goal of this document is to dump the basic definitions of Iris CMRAs and own that used after the refactoring by Janggun Lee.

Copilot · 2025-04-08T09:14:25Z

+  but literally being able to import `iris.algebra` at the coq level and use it, without having to define a single line of additional cmra metathory in Coq.
+  - For example, proper usage of auth cmra (and advanced variants) requires the
+    concept of "local-updates", which is not present in the current general form of Lilo.
+  - I needed such advanded variant of auth for proofs of stacks, and had to copy and


The word 'advanded' appears to be a typo; it should be 'advanced'.

Suggested change

- I needed such advanded variant of auth for proofs of stacks, and had to copy and

- I needed such advanced variant of auth for proofs of stacks, and had to copy and

Copilot · 2025-04-08T09:14:25Z

+  - For example, proper usage of auth cmra (and advanced variants) requires the
+    concept of "local-updates", which is not present in the current general form of Lilo.
+  - I needed such advanded variant of auth for proofs of stacks, and had to copy and
+    paste the entierty of `iris/algebra` source code and hand-remove the parts


The word 'entierty' is likely a misspelling of 'entirety'.

Suggested change

paste the entierty of `iris/algebra` source code and hand-remove the parts

paste the entirety of `iris/algebra` source code and hand-remove the parts

Copilot · 2025-04-08T09:14:26Z

+## cmra
+
+- In Lilo, RA.t is a type that with on binary operation (⋅) and unary wellformedness WF, such that
+  - ⋅ is associativitve and commutativive.


Both 'associativitve' and 'commutativive' appear to be typos; consider changing them to 'associative' and 'commutative'.

Suggested change

- ⋅ is associativitve and commutativive.

- ⋅ is associative and commutative.

Copilot · 2025-04-08T09:14:26Z

+
+- In Lilo, RA.t is a type that with on binary operation (⋅) and unary wellformedness WF, such that
+  - ⋅ is associativitve and commutativive.
+  - WF is monotonically decresing w.r.t (⋅). I.e, WF (a ⋅ b) → WF a.


The word 'decresing' should be corrected to 'decreasing'.

Suggested change

- WF is monotonically decresing w.r.t (⋅). I.e, WF (a ⋅ b) → WF a.

- WF is monotonically decreasing w.r.t (⋅). I.e, WF (a ⋅ b) → WF a.

Copilot · 2025-04-08T09:14:26Z

+  - WF is monotonically decresing w.r.t (⋅). I.e, WF (a ⋅ b) → WF a.
+- CMRAs are OFE with a binary operation ⋅, unary validity ✓, unary **n-validity** ✓{n}, and a partical function **pcore** such that
+  - ⋅ is associative and commutative.
+  - ✓, ✓{n} is monotonically decresing w.r.t (⋅).


Again, 'decresing' should be corrected to 'decreasing'.

Copilot · 2025-04-08T09:14:26Z

+  - The OwnM r constuctor allows for one to own the cmra element r without worrying about putting it in the global RA.
+


The term 'constuctor' is misspelled; please update it to 'constructor'.

Suggested change

- The OwnM r constuctor allows for one to own the cmra element r without worrying about putting it in the global RA.

- The OwnM r constructor allows for one to own the cmra element r without worrying about putting it in the global RA.

Copilot · 2025-04-08T09:14:27Z

+
+- Look over the individual RA implementations, and see if we can simplify them.
+- Clear up duplicate "ListIProp" usages. This should really all be big_sepL or big_sepM.
+- Dependency structore of temporal logic and fairness ghost is weird. Ideally, the temporal logic should only depend on the existance of iprop (and maybe invariant), without the fairness ghosts.


The word 'structore' should be corrected to 'structure'.

Suggested change

- Dependency structore of temporal logic and fairness ghost is weird. Ideally, the temporal logic should only depend on the existance of iprop (and maybe invariant), without the fairness ghosts.

- Dependency structure of temporal logic and fairness ghost is weird. Ideally, the temporal logic should only depend on the existance of iprop (and maybe invariant), without the fairness ghosts.

Copilot · 2025-04-08T09:14:27Z

+- Clear up duplicate "ListIProp" usages. This should really all be big_sepL or big_sepM.
+- Dependency structore of temporal logic and fairness ghost is weird. Ideally, the temporal logic should only depend on the existance of iprop (and maybe invariant), without the fairness ghosts.
+- In the long term, it will be nice if the simulation relation can be
+  defined inside the logic, to simpily the adequacy proofs and have a


The word 'simpily' is a typo; consider changing it to 'simplify'.

Suggested change

defined inside the logic, to simpily the adequacy proofs and have a

defined inside the logic, to simplify the adequacy proofs and have a

Lee-Janggun force-pushed the iris-cmra-upred branch 2 times, most recently from e60ac40 to 172f188 Compare August 15, 2024 05:57

Lee-Janggun force-pushed the iris-cmra-upred branch from dcc2eb3 to dcdbce6 Compare August 19, 2024 16:32

Lee-Janggun force-pushed the iris-cmra-upred branch 2 times, most recently from 2fbc78e to 2e43589 Compare August 29, 2024 04:28

Lee-Janggun force-pushed the iris-cmra-upred branch 6 times, most recently from 0c8907b to f5a138b Compare September 12, 2024 15:32

Lee-Janggun added 15 commits December 9, 2024 15:45

Refactor to use iris cmras

67621f8

* Note: fos_ticketlock doesn't work on this commit.

Migrate to uPred like iProp.

a016bfa

* Restore fos_ticketlock. * Also cleanup some impls.

Bump to Coq 8.18.0

1175abf

* Requires custom coq-ext-lib, coq-itree, and coq-promising-seq

Documentation

88ae1eb

Cleanups

b150197

* Make maps_to_res a special case of discrete_fun_singleton w. excluded middle. * Remove most uses of maps_to_res. Use discrete_fun_singleton as much as possible. * Minimize PCM.v. * Other improvements here and there.

Even more cleanups

4c3b899

Even more Cleanup

e18450b

Fix embed_add

6c97b0e

cmt

f7ada2d

More cleanup

2bb5294

Cleanup: better usage of gmap_view

9c27a27

Fix compile

7039833

Really fix compile

c24cf7a

Refactor ListIProp

ab89d0a

Remove Own, its the same as uPred_ownM.

8b4875d

Lee-Janggun force-pushed the iris-cmra-upred branch from b5399d2 to 8b4875d Compare December 9, 2024 07:33

Merge DoubleIncr

6a77212

Move & remove stuff

86c5dbe

Lee-Janggun requested a review from Copilot April 8, 2025 09:12

Copilot AI reviewed Apr 8, 2025

View reviewed changes

Lee-Janggun force-pushed the iris-cmra-upred branch from 6dc645f to 86c5dbe Compare May 13, 2025 16:03

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Use Iris cmra & Iris style upred#78

Use Iris cmra & Iris style upred#78
Lee-Janggun wants to merge 17 commits into
tlogicfrom
iris-cmra-upred

Lee-Janggun commented Aug 7, 2024 •

edited

Loading

Uh oh!

Lee-Janggun commented Aug 15, 2024

Uh oh!

Lee-Janggun commented Sep 12, 2024 •

edited

Loading

Uh oh!

Copilot AI left a comment

Uh oh!

Copilot AI Apr 8, 2025

Uh oh!

Copilot AI Apr 8, 2025

Uh oh!

Copilot AI Apr 8, 2025

Uh oh!

Copilot AI Apr 8, 2025

Uh oh!

Copilot AI Apr 8, 2025

Uh oh!

Copilot AI Apr 8, 2025

Uh oh!

Copilot AI Apr 8, 2025

Uh oh!

Copilot AI Apr 8, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

	- I needed such advanded variant of auth for proofs of stacks, and had to copy and
	- I needed such advanced variant of auth for proofs of stacks, and had to copy and

	paste the entierty of `iris/algebra` source code and hand-remove the parts
	paste the entirety of `iris/algebra` source code and hand-remove the parts

	- ⋅ is associativitve and commutativive.
	- ⋅ is associative and commutative.

	- WF is monotonically decresing w.r.t (⋅). I.e, WF (a ⋅ b) → WF a.
	- WF is monotonically decreasing w.r.t (⋅). I.e, WF (a ⋅ b) → WF a.

		- The OwnM r constuctor allows for one to own the cmra element r without worrying about putting it in the global RA.

	- The OwnM r constuctor allows for one to own the cmra element r without worrying about putting it in the global RA.
	- The OwnM r constructor allows for one to own the cmra element r without worrying about putting it in the global RA.

	- Dependency structore of temporal logic and fairness ghost is weird. Ideally, the temporal logic should only depend on the existance of iprop (and maybe invariant), without the fairness ghosts.
	- Dependency structure of temporal logic and fairness ghost is weird. Ideally, the temporal logic should only depend on the existance of iprop (and maybe invariant), without the fairness ghosts.

	defined inside the logic, to simpily the adequacy proofs and have a
	defined inside the logic, to simplify the adequacy proofs and have a

Uh oh!

Conversation

Lee-Janggun commented Aug 7, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Lee-Janggun commented Aug 15, 2024

Uh oh!

Lee-Janggun commented Sep 12, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 8, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 8, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 8, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 8, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 8, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 8, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 8, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 8, 2025

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Lee-Janggun commented Aug 7, 2024 •

edited

Loading

Lee-Janggun commented Sep 12, 2024 •

edited

Loading