Splitting system calls into two transitions#31

Open

YaZko wants to merge 23 commits intodevfrom

askrcv

Commits on Oct 31, 2025

Commits on Nov 5, 2025

quick setup for symmetric
YaZko
committed

Commits on Nov 7, 2025

Better tactics, better instances
YaZko
committed
equivalence upto for sb
YaZko
committed

Commits on Nov 14, 2025

Parameterization of Seq by a value relation
YaZko
committed

Commits on Nov 18, 2025

Merge branch 'dev' into askrcv
Chobbes
committed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Splitting system calls into two transitions#31

Splitting system calls into two transitions#31
YaZko wants to merge 23 commits intodevfrom
askrcv

Commits on Oct 23, 2025

splitting vis nodes into two transitions: wip on the transition theory

inversion of bind transitions ok

bunch of lemmas about weak reductions must be duplicated. Getting close

Commits on Oct 24, 2025

Finished trans, without the ltac

Commits on Oct 27, 2025

Fixed upto bind

Commits on Oct 29, 2025

Iterating on the label relation interface

Enforcing the shape of relations from the very definition of the simulation

pushed back to upto bind with new setup

Commits on Oct 30, 2025

The family of bind lemmas. Need to think about the proper instance now that we have two kind of states

Progress in reestablishing the metatheory, trying to simplify on the way and understanding how to expose a clean interface

Commits on Oct 31, 2025

Fixed all backward lemmas

Some tidying

Finished strong simulation

Adapting and pulling out the monotone condition from cssim

Commits on Nov 3, 2025

Pulled out not_stuck predicate, adapted complete simulation down to up-to bind

minor reformulation. Quite positive there's a stronger up-to bind valid, but failed to prove it

checkpoint

Finished complete simulations, but mirrored a lot strong simulations, need to revisit the inversion lemmas in particular to see if we can be more precise

Commits on Nov 5, 2025

quick setup for symmetric

Commits on Nov 7, 2025

Better tactics, better instances

equivalence upto for sb

Commits on Nov 14, 2025

Parameterization of Seq by a value relation

Commits on Nov 18, 2025

Merge branch 'dev' into askrcv