Request for comments: ART on service commitments

[nzarin]

Hi everyone,

@jamie and I would like to invite you to review our ART on service commitments. Here is the link to the pdf in Github repo: https://github.com/anoma/202407-message-logic/blob/main/pdfs/main.pdf

The ART corresponds with the two service commitment sessions we hosted at the Hacker House Q3.

We welcome any thoughts/feedback/questions as a reply to this thread.

Best,
Naqib & Jamie

P.S. Naqib is on vacation until October 11th and may reply later than usual.

[nzarin]

Tagging @cwgoes @degregat @isheff @Jonathan @ray for visibility. Anyone else is of course also welcome to review!

[AHart]

I read through the paper, and made the following notes. Hopefully you find them useful.

In 5. of Definition 2.1.4, we read “ℕ≥0”. Is this different from just “ℕ”? You freely use “ℕ” in 5. of definition 2.2.1.

The letter 𝛾 is used as a variable for datatypes, but isn’t declared to be a variable for such in definition 2.1.5.

We may freely assume standard function symbols, such as 0, 1, +, ∗, and pairing (-, -), with their usual meanings and types

[…]

We may freely assume standard predicate symbols, such as =, <, ≤, tupling
(-, . . . , -) and projections 𝜋𝑖 , with their usual meanings. Meaning will always be
clear.

Tupling and projections are functions, not (generally) predicates. It’s not clear to me what they should mean if we tried interpreting them as predicates.

Unless otherwise stated, we will follow a convention that variable symbols named 𝑎 and 𝑏 (like 𝑎, 𝑎′, 𝑎1, 𝑏′′, and so on) will have a datatype, and variable symbols of the form 𝑐 may have any datatype.

I’m not really sure what this is trying to say. Is it stating that as and bs will always have a fixed datatype given by the context in which they are used, while c will never have such? I also didn’t see anywhere in the paper where c was used as a variable (except for thresholds), so this aside doesn’t seem needed.

f ∈ FSymb to each of which is associated a type type(f) of the form 𝛾 → 𝛾

What is “→”, and where is it? It’s actually used in quite a few places. Obviously, I know it’s a function type, but that’s not declared anywhere, and its semantics is never described. What is “type”; the function you’re applying to f?

an interpretation function 𝜍 (P) : Time → Place → 𝛾 → Bool

[…]

A function 𝜍 (msg) : (N × Place × Place × Data) → Bool.

why is one curried and the other not? Also, some clarification/intuition on why the signature of 𝜍 (msg) looks like that would be good.

1. 𝜍↓𝑛 is the model obtained by restricting 𝜍 to times up to and including 𝑛.
2. 𝜍↑𝑛 is the model obtained by restricting 𝜍 to times from 𝑛 onwards.

Does “from 𝑛 onwards” include 𝑛?

Also, there should be some kind of formal restriction of Time (e.g. that it’s linearly ordered) so that this can always be made sense of. As it stands, you have the naturals as an archetypal example of Time, but the semantics of 𝜍 just says it’s an arbitrary set.

[[{𝑎 | 𝜙}]]𝑛,𝑝,𝜍 = {𝑑 ∈ 𝛼 | 𝑛, 𝑝 ⊨𝜍 𝜙 [𝑎:=𝑑]}

Where does 𝛼 come from?

([[𝑡]]𝑛,𝑝,𝜍 ∈ N≥#Time)/𝑛, 𝑝 ⊨𝜍 @𝑡 𝜙

This is the middle-right formula of Figure 3. Where does 𝜙 come from? If it is free/fresh, etc, that should be stated.

but none of the examples I was given have this form

What a bizarre line to read in a paper. Who gave them to you, and why is that sufficient for dismissal?

𝐵 = {𝑑 ∈ 𝛼 | 𝑛, 𝑝 ⊨𝜍 𝜙 [𝑎:=𝑑]} 𝐴 = {𝑑 ∈ 𝐵 | 𝑛, 𝑝 ⊨𝜍 𝜓 [𝑎:=𝑑]} #𝐴/#𝐵 ≥ 𝑟 𝑛, 𝑝 ⊨𝜍 Π𝑟 𝑎 : 𝜙.𝜓

First formula in figure 3
[…]

𝐵 = {𝑑 ∈ 𝛼 | 𝑛, 𝑝 ⊨𝜍 𝜙 [𝑎:=𝑑]} and 𝐴 = {𝑑 ∈ 𝛼 | 𝑛, 𝑝 ⊨𝜍 𝜙 [𝑎:=𝑑] ∧ 𝜓 [𝑎:=𝑑]}

in remark 2.3.1. Is that first A supposed to be a subset of B? Is that second A meant not to be a subset of B? If both are correct and equivalent, should the notations be made consistent?

Threshold. To express Π𝑟𝑐 𝜙.𝜓 using Π𝑟 𝜙.𝜓 , we just write […]

What is n in that formula? Presumably c?

Future work could explore could explore information flow control

Typo.

but usually that a reasonable first approximation to real life

Typo.

…

I think the paper would be improved with some better intuition early on. For example, it doesn’t seem like intuitive, straightforward explanations of @_𝑡 𝜙, in_𝑝(𝑡), or out_𝑝(𝑡) are ever made.

[cwgoes]

Thanks for sharing! I have a few specific copy-editing comments, which I suspect might be easiest to share as comments directly on the document - is that possible? Otherwise, I can write them here, but it will not be quite as efficient.

General comments

• The introductory content in section 1 is really well-written. Nicely done!
• Section 2 I’ve pretty much reviewed previously, and have no further comments on.
• Section 3 is interesting. I agree that we need ways to negotiate and discover service commitments. I am not sure if the flows or data structures here are going to be quite the right fit (and in some cases the data structures are pretty abstract, so it’s not clear exactly what is intended). I don’t think it makes sense to deeply revise this part now, but we should mark it as a topic to discuss when considering subsequent versions of the report, changes to the specs, or other matters.