[CN] Meta-issue: syntax overhaul

[dc-mak]

A few existing issues have touched upon the current syntax. The solutions for those bring function and predicate a lot closer together.

1. Remove if-restriction ([CN] Mitigate / remove restrictions on conditional branching in predicates #266)
2. Remove predicate pointer first restriction ([CN] Remove predicate pointer first restriction #303)
3. Unify namespaces for functions and predicates ([CN] Unify scopes of predicates and functions (confusing err msg for "return (Predicate(args))") #288)
4. Type annotations for expressions ([CN] Type annotations for expressions #305)
5. Smarter unfolidng for functions [CN] Use a auto-unfolding scheme for functions #483

Though not strictly dependent on the above, it may be sensible to wait until they are finished for the next tasks (which are closer to nice-to-haves).

6. Add base type heap and disallow that to be used in arguments or in data types
   5a. Add new unified syntax and map to existing backend
   5b. Optional but good engineering: refactor backend to match new sytnax

As mentioned in #288, at the end of this we could write things like

i32 add_one(i32 x) {
  let y = x + 1;
  y;
}

heap<i32> intQueueAux(i32 x) {
  return add_one(x);
 }

heap<i32> intQueue0(i32 x) {
  intQueueAux(0);
}

heap<i32> intQueue(i32 x) {
  let y = add_one(x);
  take q = intQueueAux(y);
  return q;
}

Pros:

• Concise.
• Generics are familiar to many (and monads familiar to theorists).
• Make polymorphism easier to add and explain later.
• Makes the type of locks easier to add and explain later.

Cons:

• Needs a few restrictions to keep things first-order for now (no heap<_> values in datatypes or in arguments).
• Not requiring a return (and using return as the monad heap<_> ) could be confusing for C developers.
• Bit unsure about take. Maybe let* or let <id> = *<heap_expr>;? Like in Idris' !-notation could be nice.

i32 add_one(i32 x) {
  return  x + 1;
}

heap<i32> intQueueAux(i32 x) {
  return heap(add_one(x));
}

heap<i32> intQueue(i32 x) {
  return intQueueAux(0);
}

heap<i32> intQueue(i32 x) {
  let y = add_one(x);
  let q = *intQueueAux(y); // This is redundant and for illustration only; desugars to --
  return heap(q);          // take _genvar = intQueueAux(y); let q = _genvar; return heap(q)
}

[bcpierce00]

One more: - Optional explicit type declarations on take and let (and anywhere else they make sense), to help with documentation and debugging.

…

On Wed, Jun 5, 2024 at 8:01 AM Dhruv Makwana ***@***.***> wrote: A few existing issues have touched upon the current syntax. The solutions for those bring function and `predicate a lot closer together. 1. Remove if-restriction (#266 <https://urldefense.com/v3/__https://github.com/rems-project/cerberus/issues/266__;!!IBzWLUs!WrxvcyM3niw6bzUcqm6-Ie4GOUQSynOR3z6wU7H4tQ3kLFlYzo0A3OgxEQikoeBN1lwPcMBP3UKDw47Z9u4Oo2pOtPdI$> ) 2. Remove predicate pointer first restriction (#303 <https://urldefense.com/v3/__https://github.com/rems-project/cerberus/issues/303__;!!IBzWLUs!WrxvcyM3niw6bzUcqm6-Ie4GOUQSynOR3z6wU7H4tQ3kLFlYzo0A3OgxEQikoeBN1lwPcMBP3UKDw47Z9u4Oo-UGJ1EW$> ) 3. Unify namespaces for functions and predicates (#288 <https://urldefense.com/v3/__https://github.com/rems-project/cerberus/issues/288__;!!IBzWLUs!WrxvcyM3niw6bzUcqm6-Ie4GOUQSynOR3z6wU7H4tQ3kLFlYzo0A3OgxEQikoeBN1lwPcMBP3UKDw47Z9u4Oo1tr5Hzx$> ) Though not strictly dependent on the above 3, it may be sensible to wait until they are finished for the next tasks (which are closer to nice-to-haves). 4. Add base type heap and disallow that to be used in arguments or in data types 5a. Add new unified syntax and map to existing backend 5b. Optional but good engineering: refactor backend to match new sytnax As mentioned in #288 <https://urldefense.com/v3/__https://github.com/rems-project/cerberus/issues/288__;!!IBzWLUs!WrxvcyM3niw6bzUcqm6-Ie4GOUQSynOR3z6wU7H4tQ3kLFlYzo0A3OgxEQikoeBN1lwPcMBP3UKDw47Z9u4Oo1tr5Hzx$>, at the end of this we could write things like i32 add_one(i32 x) { let y = x + 1; y; } heap<i32> intQueueAux(i32 x) { return (add_one(x)); } heap<i32> intQueue0(i32 x) { intQueueAux(0); } heap<i32> intQueue(i32 x) { let y = add_one(x); let* q = intQueueAux(y); return y; } Pros: - Concise. - Generics are familiar to many (and monads familiar to theorists). - Make polymorphism easier to add and explain later. - Makes the type of locks easier to add and explain later. Cons: - Needs a few restrictions to keep things first-order for now (no heap<_> values in datatypes or in arguments). - Not requiring a return (and using return as the monad heap<_> ) could be confusing for C developers. - Still unsure about let*. Maybe let <id> = *<heap_expr>;? Like in Idris <https://urldefense.com/v3/__https://idris2.readthedocs.io/en/latest/tutorial/interfaces.html*notation__;Iw!!IBzWLUs!WrxvcyM3niw6bzUcqm6-Ie4GOUQSynOR3z6wU7H4tQ3kLFlYzo0A3OgxEQikoeBN1lwPcMBP3UKDw47Z9u4Oo2Bt_g88$> ). i32 add_one(i32 x) { return x + 1; } heap intQueueAux(i32 x) { return (heap(add_one(x))); } heap intQueue(i32 x) { return intQueueAux(0); } heap intQueue(i32 x) { let y = add_one(x); let q = *intQueueAux(y); return heap(q); } — Reply to this email directly, view it on GitHub <https://urldefense.com/v3/__https://github.com/rems-project/cerberus/issues/304__;!!IBzWLUs!WrxvcyM3niw6bzUcqm6-Ie4GOUQSynOR3z6wU7H4tQ3kLFlYzo0A3OgxEQikoeBN1lwPcMBP3UKDw47Z9u4Oo1dJoef8$>, or unsubscribe <https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/ABVQQC2V6YY3QNIU2OANNALZF342HAVCNFSM6AAAAABI2R66LOVHI2DSMVQWIX3LMV43ASLTON2WKOZSGMZTKNZRG42TQMI__;!!IBzWLUs!WrxvcyM3niw6bzUcqm6-Ie4GOUQSynOR3z6wU7H4tQ3kLFlYzo0A3OgxEQikoeBN1lwPcMBP3UKDw47Z9u4OoxPdRZbJ$> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[dc-mak]

Added, thanks

[peterohanley]

Are the type annotations in declaration specs ever not fully determined by the declaration? If not, why have a separate form for the declaration spec at all? Concretely:

//before
int foo(int x, const char *y, struct bar **z);
/*@ spec foo(i32 x, pointer y, pointer z);
    requires ...; // hardcoded in grammar
    ensures ...; // hardcoded in grammar
@*/

//after
int foo(int x, const char *y, struct bar **z);
/*@ spec foo(x, y, z); // added to function_spec_item grammar node
    requires ...; // just another function_spec_item
    ensures ...; // just another function_spec_item
    trusted; // parses for free now
    accesses qux; // also parses for free
@*/

The arguments could also be removed. I like concretely bringing them into CN scope in the same block.

[cp526]

Are the type annotations in declaration specs ever not fully determined by the declaration? If not, why have a separate form for the declaration spec at all? Concretely:

//before
int foo(int x, const char *y, struct bar **z);
/*@ spec foo(i32 x, pointer y, pointer z);
    requires ...; // hardcoded in grammar
    ensures ...; // hardcoded in grammar
@*/

//after
int foo(int x, const char *y, struct bar **z);
/*@ spec foo(x, y, z); // added to function_spec_item grammar node
    requires ...; // just another function_spec_item
    ensures ...; // just another function_spec_item
    trusted; // parses for free now
    accesses qux; // also parses for free
@*/

The arguments could also be removed. I like concretely bringing them into CN scope in the same block.

The reason for this aspect of the spec syntax is that C does not require a function prototype to name all the arguments; and if it does, the Cerberus frontend (IIRC) forgets them. So spec has syntax to introduce names for the arguments. AIUI, originally the idea of spec was also to be able to give specifications to functions in a different source location from their declaration.

[thatplguy]

There are enough spec-related tickets (you can see a list of them here) that I've lost track of the broader language design issues we're considering. Here's a rough grouping of the current tickets.

Predicates

• [CN] Consider renaming predicate keyword #525
• [CN] Unify scopes of predicates and functions (confusing err msg for "return (Predicate(args))") #288
• [CN] Remove predicate pointer first restriction #303
• [CN] Mitigate / remove restrictions on conditional branching in predicates #266
• [CN] Add inlined predicate assertions (take in C function / statements) #260
• [CN] Consider replacing Owned or Block with ReadWrite and WriteOnly (and/or shorter aliases) #524
• [CN] Replace take x = .. with something else #312
• [CN] Allow wildcard name / no name for take #466

Taken together, these issues address two broad points:

1. Conceptually, the term "resource predicate" is confusing, both to those familiar with program verification and newcomers. We should find a name for this concept that's more intuitive and use it in the docs/syntax/etc.
2. The syntax around defining and using resource predicates currently imposes certain restrictions that we think can be alleviated. If we make all the changes above, we'll end up with less distinction between resource predicates and logical functions – which is good, because it means there are fewer special cases to learn and remember.

Syntactic sugar

• [CN] Align unchanged syntax with other CN syntax  #468
• [CN] Revisit array_shift and member_shift syntax #349
• [CN] Allow ' in numeric constants #337
• [CN] Semantics of unchanged is confusing (eg. local vars, changed vars)  #443
• [CN] Retire the ability to break up specifications across magic comments #503

Local vs global reasoning (and library models)

• [CN] Scope rules are different for function arguments and spec arguments #316
• [CN] not clear how to use static local variables #353
• [CN] Consolidate trusted and spec keywords  #467
• [CN] Streamline spec syntax #500

These issues are related to how specifications are associated with functions, and how/when specs are trusted vs. verified by CN. There are two use cases to keep in mind:

1. Defining library models by creating trusted function specifications for functions without definitions.
2. Defining specifications for exported functions (i.e. declared in a .h file) without leaking internal state into the external spec (e.g. about non-exported static variables).

Solver hints

• [CN] Make extract and instantiate more idiomatic #471
• [CN] Misleading warning on necessary use of extract  #498
• [CN] Rename the extract statement to focus #499

Types

• [CN] Type annotations for expressions #305
• [CN] Make type names consistent in spec language (eg char vs. u8) #442

Datatypes

• [CN] Require variables to be uniqe to constructor, not whole datatype. #290
• [CN] Currently no good feature for accessing fields of datatypes #356

[peterohanley]

It's not clear when the parser shifts from CN to C and back. I can write &x in a spec, but not in an argument of a lemma application.

[cp526]

&x only works for globals in specifications of C functions. Lemmas have to be “pure” in that they cannot refer to C objects.

[peterohanley]

That is a reasonable restriction but doesn't actually stop me. I can define temp variables equal to the term I wanted to put into the lemma arguments and it works. I'll make a full issue but this is the transformation:

// this function just exists for its spec
dummy_function(x, &x[y], z);

t *tmp = &x; // this is the only difference
t *tmp2 = &x[y];
/*@ apply lemma_function(tmp, tmp2, z); @*/

What is the restriction really doing for us here besides boilerplate?

[cp526]

That is a reasonable restriction but doesn't actually stop me. I can define temp variables equal to the term I wanted to put into the lemma arguments and it works. I'll make a full issue but this is the transformation:

// this function just exists for its spec
dummy_function(x, &x[y], z);

t *tmp = &x; // this is the only difference
t *tmp2 = &x[y];
/*@ apply lemma_function(tmp, tmp2, z); @*/

What is the restriction really doing for us here besides boilerplate?

Sorry, I think I misunderstood.

If you'd like to be able to write apply your_lemma(x, &x[y], z), that's indeed something we should support if it doesn't work yet.

What we can't really support is having a lemma whose statement refers to things like &x for a lemma argument x (because that wouldn't be "pure").