Skip to content
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.

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

Remove Asrt.Star (fix #159) #316

Open
wants to merge 26 commits into
base: master
Choose a base branch
from

Conversation

N1ark
Copy link
Contributor

@N1ark N1ark commented Oct 10, 2024

Remove Asrt.Star; what used to be Asrt.t is now Asrt.atom (atomic assertions), and Asrt.t is now atom list, avoiding the need for recursive functions when traversing assertions, and making the distinction much clearer and simpler.
Rename Asrt.GA -> Asrt.CorePred

@giltho
Copy link
Contributor

giltho commented Oct 10, 2024

I think if you fix this problem, it will also fix #301
This PR also re-orders the fields and it breaks something

@N1ark
Copy link
Contributor Author

N1ark commented Oct 11, 2024

I think if you fix this problem, it will also fix #301 This PR also re-orders the fields and it breaks something

Ah yes interesting you seem to have stumbled upon similar things... When I have more time (🫠) I'll look; what's odd is that the version that works doesn't sort the assertions, so I'm not certain how sorting then (Types>Pure>CorePred>Wand) causes the issue; will update

And yes sure I'll rename it to atom it's nicer

Additional note: running Gillian-JS with this causes a stack overflow so something somewhere isn't tail-recursive anymore...

@N1ark N1ark marked this pull request as ready for review December 11, 2024 11:16
@N1ark N1ark marked this pull request as draft December 11, 2024 12:27
@N1ark
Copy link
Contributor Author

N1ark commented Dec 11, 2024

JS works but something is still odd for Gillian-C, which ends up verifying less branches than it used to, possibly due to ordering issues. Will leave as is for now and maybe come back later to it...

@N1ark N1ark marked this pull request as ready for review December 19, 2024 08:45
@N1ark
Copy link
Contributor Author

N1ark commented Dec 21, 2024

The tests pass which is a miracle but from diffing some of my local tests I get a few mismatches so not ready to merge yet fyi

@N1ark
Copy link
Contributor Author

N1ark commented Dec 23, 2024

@giltho @NatKarmios fyi this is ready for review :)

After some evaluation, I get:

  • 4% perf improvement on Collections-C
  • AWS passes
  • One specific proc is ~3 times slower, because more branches (77 rather than 13) are covered than before. I checked and they're ok, it's caused by some assertions being re-ordered and Gillian-C used to incorrectly die because of ALoc mismatches. I wonder if there's a way of avoiding this branch explosion though :/ Overall sorting still seems to give better perf in most cases

@N1ark N1ark mentioned this pull request Dec 25, 2024
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