inline clauses in crocq annotations #50

New issue

Closed

opened 2026-10-16 11:25:09 +02:00 by EatOreo · 0 comments

EatOreo commented

2026-10-16 11:25:09 +02:00

Owner

Jesper would like to see this.
For instance could be:

/*@
    INV verif_sumarray.v:loop_invariant
    INV_INLINE <{ 
        EX i: Z,
           PROP  (0 <= i <= size)
          ...
    }>
*/
while (i<n) {
    s+=a[i];
    i = i + 1;
}

When changing it should override the contents at verif_sumarray.v:loop_invariant, it should be the new source of truth for the invariant.
It would be nice to forward the diagnostics from the proof document to it, can be done with vscode.languages.getDiagnostics() and some evil math inspired by https://code.visualstudio.com/api/language-extensions/embedded-languages#language-services-sample? or maybe we need cutdoctor type translations.
We can even listen to when diagnostics change with vscode.languages.onDidChangeDiagnostics()?

Jesper would like to see this. For instance could be: ```c /*@ INV verif_sumarray.v:loop_invariant INV_INLINE <{ EX i: Z, PROP (0 <= i <= size) ... }> */ while (i<n) { s+=a[i]; i = i + 1; } ``` When changing it should override the contents at verif_sumarray.v:loop_invariant, it should be the new source of truth for the invariant. It would be nice to forward the diagnostics from the proof document to it, can be done with vscode.languages.getDiagnostics() and some evil math inspired by https://code.visualstudio.com/api/language-extensions/embedded-languages#language-services-sample? or maybe we need cutdoctor type translations. We can even listen to when diagnostics change with vscode.languages.onDidChangeDiagnostics()?

EatOreo added the

priority!

label

2026-10-16 11:25:09 +02:00

EatOreo self-assigned this

2026-10-16 15:01:56 +02:00

EatOreo changed title from ~~inline specifications in crocq annotations~~ to inline clauses in crocq annotations

2026-10-16 15:30:55 +02:00

EatOreo referenced this issue from a pull request that will close it,

2026-10-21 14:10:54 +02:00

Add inline versions of INV and SPEC clauses #58