Literal byte arrays

[vbgl]

Description

This adds literal (byte) arrays to the language of expressions. In source code they can be written using string syntax (e.g., "data") or array syntax (e.g., { x, y + z }). Both syntax were already accepted for top-level definitions of global variables.

Fixes #510

This PR is marked as draft as it needs a bit of polishing (see checklist below).

Future work (not for this PR): generalize the type of cells (currently limited to u8).

Checklist

• Add a changelog entry in changes if the PR is a user-visible change
• Add one or several tests to compiler/tests if it makes sense, especially if it is a bug fix
• Update the documentation if needed

[vbgl]

The first commit is unrelated: documentation of expressions still made use of the legacy syntax for memory accesses.

Then we have:

1. the uincl relation for arrays can be decided
2. addition of the new constructor for expressions (syntax & semantics) and fix the compiler accordingly
3. extend the remove-global pass to handle global variables whose value is an array
4. change the concrete syntax (a few things become simpler as an array is now a usual expression), add tests and documentation

[vbgl]

I’ve doubts about the rev in the semantics: which operator does cancel it? Either curry or WArray.fill.

[eponier]

Out of curiosity, is there a specific usecase you have in mind?

[vbgl]

1. PR Safety assert2 #1170 uses them.
2. “scoped globals” (the one declared within an inline function) are currently restricted to word

[eponier]

What should happen in these cases? reg u8[3] r = { 1, 2, 3 }; and stack u8[3] s = { 1, 2, 3 }? For now, we get an error in array expansion for the first one, and an assert false for the second one.

[vbgl]

For now, I think it is fine for the compiler to reject these programs. I’ve just changed the assertion failure in a better error message.

[eponier]

To be sure I understand, this is dead code and would typically be an assert false if it were possible?

[vbgl]

Yes, this is dead code. I’m not sure there is a more elegant way to write the same code (here, there are two nested pattern-matching twice on the same value).

[eponier]

Actually, Rocq is able to elaborate a bit. So you could write

Definition s_opN (op:opN) (es:pexprs) : pexpr :=
  match op, app_sopn _ (sem_opN_typed op) es with
  | Opack ws _, Ok w => Papp1 (Oword_of_int ws) (Pconst (wunsigned w))
  | Ocombine_flags _, Ok b => Pbool b
  | _, _ => PappN op es
  end.

[eponier]

(and this has no impact on the proof it seems)

[vbgl]

Thanks. I’ll apply your suggestion.

[vbgl]

Done.

[eponier]

I made suggestions for the doc. Also I'm surprised that global_in_global_def.jazz now passes. Shouldn't it complain that we're going u8 -> u16 conversion at some point?

Apart from that, this seems good to go.

[eponier]

I’ve doubts about the rev in the semantics: which operator does cancel it? Either curry or WArray.fill.

It looks like curry is indeed reverting its arguments.

Example curry2 A B (f : seq (sem_t A) -> B) a b :
  curry 2 f a b = f [:: b; a].
Proof. by reflexivity. Qed.

[vbgl]

Right. curry is fishy. It is only used (so far) in the semantics of packs, so that’s fine.

[vbgl]

I made suggestions for the doc. Also I'm surprised that global_in_global_def.jazz now passes. Shouldn't it complain that we're going u8 -> u16 conversion at some point?

You’re perfectly right. Thanks. I’ve added the missing check in pretyping and now the test case fails again, as expected.

[eponier]

This is good, and I don't want to delay it further. I made one suggestion about the definition of s_opN. Just tell me if you want to integrate it. In any case, I'll merge the PR.

[eponier]

Let's merge!