Reconsider the use/explanation of `extract` in the tutorial's "Second loop example"

[samcowger]

I'll start by saying that this issue might just be a result of my misunderstanding.

When I was going through the second loop example in the tutorial, I was surprised by its second use of extract:

  ...
  while (j < n)
  /*@ inv take al = each(u32 i; i < j) { Owned<char>( array_shift<char>(p, i)) };
          take ar = each(u32 i; j <= i && i < n) { Block<char>( array_shift<char>(p, i)) };
          {p} unchanged; {n} unchanged;
          j <= n;
  @*/
  {
    /*@ extract Block<char>, j; @*/
    /*@ extract Owned<char>, j; @*/
    p[j] = 0;
    j++;
  }
  ...

It didn't easily fit into the mental model of extract - a tool to extract individual elements from in-scope iterated resources - that earlier parts of the tutorial had been guiding me towards. Now, the tutorial does offer some explanation of this:

finally, we put extract Owned<char>, j; to allow CN to "attach" this resource to the iterated Owned resource. CN issues a warning, because nothing is, in fact, extracted: we are using extract only for the "reverse" direction.

But, to the extent I understand this explanation, it's describing an entirely different semantics for extract as compared to its prior and subsequent mentions. Not only was I surprised that it's apparently doing the opposite of what extract usually does, I was particularly surprised to see that one is able to write this extract seemingly before the Owned resource is actually introduced (which I would assume would happen at the write to p[j]).

I think that this use case for extract might warrant a bit more explanation, and perhaps another motivating example, to help tutorial consumers gain a better understanding of it.

[cp526]

That sounds like a good idea.

I've, in fact, been looking for a different name for extract that better describes what it does: extract P, i (for some predicate name P) tells CN that it should feel free to instantiate and "reverse-instantiate" iterated resources with predicate name P for index i. So the name "extract" is not representative of what it actually does in two ways:

• it allows CN not just to extract but also to re-attach, and

• the extract does not just prompt a single action, it's more declarative -- following the extract CN knows that for the remainder of this control-flow path it should freely extract and re-attach that index in matching iterated resources. The advantage of this is that it can significantly reduce the annotation burden.

[bcpierce00]

"focus"?

On Mon, Jul 22, 2024 at 9:49 AM Christopher Pulte @.***> wrote:

That sounds like a good idea.

I've, in fact, been looking for a different name for extract that better describes what it does: extract P, i (for some predicate name P) tells CN that it should feel free to instantiate and "reverse-instantiate" iterated resources with predicate name P for index i. So the name "extract" is not representative of what it actually does in two ways:

-

it allows CN not just to extract but also to re-attach, and

the extract does not just prompt a single action, it's more declarative -- following the extract CN knows that for the remainder of this control-flow path it should freely extract and re-attach that index in matching iterated resources.

— Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/rems-project/cn-tutorial/issues/51*issuecomment-2243012776__;Iw!!IBzWLUs!WkHjkGWa2F9gcnwJv5UBC8KxM5A5QHYLVVV-Jx023p3Eez13nxHJmaS4k8htYe4GMrkYpKMKRhQLONIwrAB6HKTl3oQK$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/ABVQQCYLAHZBXFHQ7P7ECRTZNUEX5AVCNFSM6AAAAABLFNO2YSVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDENBTGAYTENZXGY__;!!IBzWLUs!WkHjkGWa2F9gcnwJv5UBC8KxM5A5QHYLVVV-Jx023p3Eez13nxHJmaS4k8htYe4GMrkYpKMKRhQLONIwrAB6HFx7pZ6n$ . You are receiving this because you are subscribed to this thread.Message ID: @.***>

[bcpierce00]

or some variant of "treat specially"

On Mon, Jul 22, 2024 at 9:50 AM Benjamin Pierce @.***> wrote:

"focus"?

On Mon, Jul 22, 2024 at 9:49 AM Christopher Pulte < @.***> wrote:

That sounds like a good idea.

I've, in fact, been looking for a different name for extract that better describes what it does: extract P, i (for some predicate name P) tells CN that it should feel free to instantiate and "reverse-instantiate" iterated resources with predicate name P for index i. So the name "extract" is not representative of what it actually does in two ways:

-

it allows CN not just to extract but also to re-attach, and

the extract does not just prompt a single action, it's more declarative -- following the extract CN knows that for the remainder of this control-flow path it should freely extract and re-attach that index in matching iterated resources.

— Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/rems-project/cn-tutorial/issues/51*issuecomment-2243012776__;Iw!!IBzWLUs!WkHjkGWa2F9gcnwJv5UBC8KxM5A5QHYLVVV-Jx023p3Eez13nxHJmaS4k8htYe4GMrkYpKMKRhQLONIwrAB6HKTl3oQK$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/ABVQQCYLAHZBXFHQ7P7ECRTZNUEX5AVCNFSM6AAAAABLFNO2YSVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDENBTGAYTENZXGY__;!!IBzWLUs!WkHjkGWa2F9gcnwJv5UBC8KxM5A5QHYLVVV-Jx023p3Eez13nxHJmaS4k8htYe4GMrkYpKMKRhQLONIwrAB6HFx7pZ6n$ . You are receiving this because you are subscribed to this thread.Message ID: @.***>

[cp526]

"focus" actually matches quite well!

[cp526]

Just for completeness: it is in principle also possible to change the semantics of extract to something that has a better intuition, if it doesn't lead to too much annotation burden: e.g. extract + inject would probably be more intuitive, but lead to an awkward amount of proof annotations.

But "focus" seems quite good!

[samcowger]

the extract does not just prompt a single action, it's more declarative

Ah, I see - I guess the idiom is probably to put all of your extract statements at the beginning of a loop block, or whenever your index comes into scope? It seems like this is broadly done in the examples, but because they're simple, the extract statements also usually immediately precede the statement that necessitates them, so I must have accidentally learned that as the idiom.

At any rate, I like "focus" as well, though I wouldn't be opposed to two different annotations for the two different directions.

I've also just seen that there is some content in the tutorial about the "reverse" direction for extract, which I guess I must have missed! It's a useful explanation, though I still think switching to a bidirectional word like "focus" would be more intuitive.

[cp526]

Agreed. "Focus" would be better naming (previously I'd been considering "movable", but that isn't ideal either), but more tutorial text+examples would probably also be needed.