Scatter termination.sail

[Ptival]

Following the merge of #1219 , it would be nice to scatter the termination module, in such a way that one could require some termination measures without having to include every single instruction in their output.

The main culprit here was compressed_measure, but once that one is scattered (thanks @jn80842), it's a small extra step to just move around the rest of the code and get rid of the termination module altogether.

I tried to remove all references to the module, but may have missed some.

I was also instructed that the termination measures for vmem_read_addr and vmem_write_addr might no longer need to be protected only for the Rocq output, so they get taken out of the $iftarget coq.

I have only tested the Lean output, so I'm hoping the CI will check whether my changes are consistent.

Happy to discuss any of the decisions I made, they could be based on incorrect assumptions on my end.

[jordancarlin]

Would #905 eliminate the need for compressed_measure? If so, maybe we should get that PR updated and merged first.

[pmundkur]

Would #905 eliminate the need for compressed_measure? If so, maybe we should get that PR updated and merged first.

That's blocked on rems-project/sail#1357, so I'm okay with merging this first and removing compressed_measure later.

[pmundkur]

@Ptival looks like this needs newlines at end-of-file fixes to pass pre-commit.

[Ptival]

Looks like I might have broken something on the Lean side too, I'll investigate:

https://github.com/riscv/sail-riscv/actions/runs/19080408022/job/54510837967

[github-actions]

Test Results

2 115 tests  ±0   2 115 ✅ ±0   20m 53s ⏱️ +4s
    1 suites ±0       0 💤 ±0 
    1 files   ±0       0 ❌ ±0 

Results for commit 762e228. ± Comparison against base commit 91178c8.

♻️ This comment has been updated with latest results.

[Timmmm]

This looks much better to me! It would be good to get an explanation of exactly what this is for and how it works for people who aren't formal experts.

[pmundkur]

FYI, I was able to rebase #905 (as #1382), which removed the measure for execute but also broke Lean in a new way (I think).

[Ptival]

FYI, I was able to rebase #905 (as #1382), which removed the measure for execute but also broke Lean in a new way (I think).

Ah interesting, I'm going to have a quick look at why your error happens.

In the meantime, I have updated the currentlyEnabled_measure with working values. I added comment with the dependency chain I witnessed for future reference.

Leaving this as a draft PR until we figure out whether we can remove the whole compressed_measure.

[Ptival]

I have followed the removal of compressed_measure, added some comments over the termination measures, and it seems to work well for my purposes.

[pmundkur]

LGTM. Since the measures are now appearing in the main code, it would be helpful to have some explanatory comments where previously there weren't any.

[pmundkur]

It would be helpful to explain the repeat construct here, and refer to it for the vmem_write_addr case below.

[Ptival]

I honestly don't know what this does precisely.

It's not very documented... according to the syntax documentation in the SAIL repo this shouldn't even be valid syntax...

@Alasdair I think maybe you added this, could you explain to me what this variant of termination_measure is?

[Alasdair]

Not sure if I added it, but it's a termination measure for the loop in the function body. In the syntax repeat n is a valid loop_measure.

I think this can be placed inline and attached to the loop itself, which might be more clear.

[Ptival]

Ah, I think I saw the syntax for putting it next to the loop, I will give it a try, as I agree it would be more clear.

[Ptival]

Alright, I attempted something. It needs magic_hash for some reason. I'll wait for CI to check because I think this is specifically exercised by the Rocq backend.

[Alasdair]

We shouldn't use that option in the model, it's for debugging generated code that uses internally generated identifiers that can't clash with user identifiers (by allowing it to be passed back into the frontend) . If it doesn't support it we should just keep the termination measure separate for now. I also don't guarantee that debug flags will persist between Sail versions, and that flag has mostly been superseeded by the $sail_internal directive which is file-local and more descriptive, so it is actual risk of being removed.

I'm really not sure why using an inline termination measure would require that option anyway. I'll look into changing that.

[Ptival]

Alright I reverted it!