Skip to content

Align with spec: fix semantic issues and missing assertions#9

Merged
Aurele-Barriere merged 7 commits intomainfrom
vs/autoformalization/fix-semantics
Mar 16, 2026
Merged

Align with spec: fix semantic issues and missing assertions#9
Aurele-Barriere merged 7 commits intomainfrom
vs/autoformalization/fix-semantics

Conversation

@Valentin889
Copy link
Collaborator

Summary

This PR fixes inconsistencies between the code and the ECMAScript comments.
It also updates the associated proofs to account for the corrected semantics.

Changes

  • Use Term instead of Atom in countLeftCapturingParensBefore to match the specification.
  • Fix variable names to better align with the spec and avoid shadowing.
  • Add a missing assert in the group compilation logic and adapt the proof accordingly.
  • Add a missing OMITTED spec step.
  • Replace an incorrect let! with let where no monadic bind is required.

Goals

  • Improves spec alignment.
  • Fixes the associated proof.

This fix doesn't change the functionnality as the first parameter of countLeftCapturingParensBefore is not used, but it captures better the specs
Since we test for failure later, the use of let! is not necessary here
@Valentin889 Valentin889 self-assigned this Mar 16, 2026
Copy link
Collaborator

@Aurele-Barriere Aurele-Barriere left a comment

Choose a reason for hiding this comment

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

Thank you for these changes!

@Aurele-Barriere Aurele-Barriere merged commit f616381 into main Mar 16, 2026
2 checks passed
@Valentin889 Valentin889 deleted the vs/autoformalization/fix-semantics branch March 16, 2026 12:17
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.

2 participants