Skip to content

Fix async while rule#935

Open
lyonel2017 wants to merge 2 commits intomainfrom
asynchile
Open

Fix async while rule#935
lyonel2017 wants to merge 2 commits intomainfrom
asynchile

Conversation

@lyonel2017
Copy link
Copy Markdown
Contributor

Fix #774

@strub strub changed the title Fix asynchile rule Fix async while rule Mar 12, 2026
@lyonel2017 lyonel2017 force-pushed the asynchile branch 2 times, most recently from 536fb81 to 07e7aa9 Compare March 19, 2026 14:31
@lyonel2017 lyonel2017 marked this pull request as ready for review March 19, 2026 15:09
@lyonel2017 lyonel2017 requested a review from strub March 19, 2026 15:09
@oskgo
Copy link
Copy Markdown
Contributor

oskgo commented Mar 20, 2026

Now that you have a fresh understanding of how the tactic works, could you write up documentation? That would also make review simpler.

@lyonel2017 lyonel2017 marked this pull request as draft March 24, 2026 12:32
@lyonel2017 lyonel2017 force-pushed the asynchile branch 2 times, most recently from 631be1d to ed3f840 Compare March 24, 2026 15:56
@lyonel2017 lyonel2017 marked this pull request as ready for review March 24, 2026 15:56
@lyonel2017 lyonel2017 force-pushed the asynchile branch 2 times, most recently from ac4c525 to 5d7798f Compare March 26, 2026 10:55
@lyonel2017 lyonel2017 requested a review from oskgo March 26, 2026 10:56
Copy link
Copy Markdown
Contributor

@oskgo oskgo left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Mostly nits, other than that the documentation is looking great.

Also, I had a look at the paper again, and there's a small but meaningful difference in how the non-lock-step cases are handled there and in EasyCrypt. In the paper the loop condition for losslessness uses LX, which means that termination is not required, only that we are guaranteed to either terminate OR enter lockstep again. Not a soundness issue, but maybe it's worth being as general as the paper.

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.

Tactic async while is unsound

2 participants