Skip to content

Splitting system calls into two transitions #31

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
YaZko wants to merge 28 commits into
base: dev
Choose a base branch
from
Open

Splitting system calls into two transitions #31

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
28 commits
Select commit Hold shift + click to select a range
8ab960b
splitting vis nodes into two transitions: wip on the transition theory
YaZko Oct 23, 2025
4545e95
inversion of bind transitions ok
YaZko Oct 23, 2025
bd94505
bunch of lemmas about weak reductions must be duplicated. Getting close
YaZko Oct 23, 2025
f4a9204
Finished trans, without the ltac
YaZko Oct 24, 2025
798b082
Fixed upto bind
YaZko Oct 27, 2025
4dedeef
Iterating on the label relation interface
YaZko Oct 29, 2025
e6666e0
Enforcing the shape of relations from the very definition of the simu…
YaZko Oct 29, 2025
f2cdc10
pushed back to upto bind with new setup
YaZko Oct 29, 2025
850ca88
The family of bind lemmas. Need to think about the proper instance no…
YaZko Oct 30, 2025
2db8b97
Progress in reestablishing the metatheory, trying to simplify on the …
YaZko Oct 30, 2025
0de205c
Fixed all backward lemmas
YaZko Oct 31, 2025
90f8bab
Some tidying
YaZko Oct 31, 2025
7a32335
Finished strong simulation
YaZko Oct 31, 2025
7b1ca0e
Adapting and pulling out the monotone condition from cssim
YaZko Oct 31, 2025
6fe6f55
Pulled out not_stuck predicate, adapted complete simulation down to u…
YaZko Nov 3, 2025
15d3dfd
minor reformulation. Quite positive there's a stronger up-to bind val…
YaZko Nov 3, 2025
df61b3f
checkpoint
YaZko Nov 3, 2025
35da3c6
Finished complete simulations, but mirrored a lot strong simulations,…
YaZko Nov 3, 2025
40fc248
quick setup for symmetric
YaZko Nov 5, 2025
c878904
Better tactics, better instances
YaZko Nov 7, 2025
302f8c2
equivalence upto for sb
YaZko Nov 7, 2025
0258802
Parameterization of Seq by a value relation
YaZko Nov 14, 2025
2c6b639
Merge branch 'dev' into askrcv
Chobbes Nov 18, 2025
8276517
WIP
YaZko Apr 15, 2026
2816789
Merge branch 'askrcv' of github.com:vellvm/ctrees into askrcv
YaZko Apr 15, 2026
8420422
Finished proof rules. Not the worst state, but some thought should si…
YaZko Apr 16, 2026
01729d3
elementary laws
YaZko Apr 16, 2026
2f25152
Incompatibility lemmas and a painful fix to tactics
YaZko Apr 16, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 3 additions & 1 deletion theories/CTree.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,10 @@ From ITree Require Export
Indexed.Function
Indexed.Sum.

From CTree.Utils Require Export
Utils.

From CTree.Core Require Export
Utils
Index
CTreeDefinitions.

5 changes: 3 additions & 2 deletions theories/Core/CTreeDefinitions.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,8 +25,9 @@ br.

From ITree Require Import Basics.Basics Core.Subevent Indexed.Sum.

From CTree Require Import
Core.Utils Core.Index.
From CTree Require Export
Utils.Utils.
From CTree Require Import Core.Index.

From ExtLib Require Import
Structures.Functor
Expand Down
2 changes: 1 addition & 1 deletion theories/Core/Index.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
From ITree Require Import Basics Indexed.Sum.
From CTree Require Import Core.Utils.
From CTree Require Import Utils.Utils.

Section Index.

Expand Down
Loading
Loading