Add primitive string type.

[rlepigre]

Since refactoring Constr.t to combine primitive values into an intermediate type is not a clear win (see #17951), here is an attempt to add primitive char and string types by simply extending Constr.t with corresponding primitive value constructors a primitive string type by simply extending Constr.t with a corresponding value constructor.

Check list:

• Added / updated test-suite.
• documentation
• Added changelog.
• Opened overlay pull requests.

[silene]

Two preliminary remarks:

• Do not add new VM opcodes (especially some that will cause an instant segfault). Use existing opcodes instead. For example, PString.cat can directly be mapped to CHECKCAMLCALL2.
• It seems we do not gain much from having a primitive type char. It seems like using int would work just as well, if not better.

[rlepigre]

@silene I don't understand the code related to VM opcodes, so I'd really appreciate help here. By the way, why are many of these opcode named CHECK*? Are they not meant to correspond to specific instructions? (Your suggestion makes me think they are not.)

About your second point (using int as char), I'm not sure that this is the right thing, since char builds in the fact that the integer value is less than 256. Also, having a specific char type would probably be better when it comes to extraction? In any case, let's see what others think.

[silene]

The CHECK part means that they support open terms as input. (It happens that this is the most common behavior, and it would have been better to use a NOCHECK prefix for their uncommon counterparts, but what is done is done.) Some of them correspond to specific instructions, e.g., CHECKADDINT63; some of them work with arbitrary code, e.g., CHECKCAMLCALL.

In your case, the starting point would be to modify Vmbytegen.get_caml_prim, and from there, the other needed changes should flow naturally.

[silene]

since char builds in the fact that the integer value is less than 256

Note that this is not even an intrinsic property of your type. It is just a consequence of axiom chr_code_id. If you were to replace char by int, then this axiomatic property would just move from axiom chr_code_id to axiom make_get_spec.

[JasonGross]

What is the benefit of having primitive strings over using array int? The downside I'm concerned about is ad-hoc complication of the kernel and tcb. (If the primary upside is extraction of literals, maybe something can be added to extraction in general?)
On the performance side:

• Are any of the operations asymptotically more efficient?
• What are the constant factor speedups that we see for each operation?

[SkySkimmer]

Strings are more space efficient (1 byte / character instead of 1 word / character).
You could recover some efficiency by using all the bits in an int instead of just the lower 8 but since primitive ints are 63 bits it doesn't fit well.

[rlepigre]

@JasonGross using arrays of integers, you are either space-inefficient (by storing one character per word) or you need to work with an encoding which requires computation. We have several use-cases where what we want is a compact representation of names (for variables, functions, ...) from a source program. These names would typically be string literals in a (generated) Coq source file, and they would only be carried around during program verification (and also used as keys for lookups in a maps).

[silene]

What are the constant factor speedups that we see for each operation?

I performed a small test by repetitively concatenating strings of various size until the total size reaches 100,000 characters. For native_compute, the speedup of having native strings would be between 300x and 400x. For vm_compute, it would be between 1000x and 3000x.

To improve the situation when working with strings, we could add a primitive concatenation operation on arrays. This time, the speedup for native_compute would only be between 40x and 50x, while for vm_compute, it would be between 25x and 50x.

So, in addition to the fact that arrays occupy 8x more memory than strings (but this is hardly relevant performance-wise, unless you are actually filling your memory with strings), the things to remember are the following ones:

1. Arrays in Coq are persistent, so mutating them leaves a trail, which has a non-negligible cost.
2. Mutating/copying arrays in OCaml triggers the GC barrier, contrarily to strings (and floating-point arrays), which again has a non-negligible cost.
3. Iterating in the VM is damn slow.

Obviously, these numbers are only meaningful under the assumption that no mutating operations are ever added to a native Coq string type. If strings start offer mutations like arrays do, then the performance gains would be a lot less dramatic.

[silene]

I am pretty sure one can derive False from this axiom.

Needless to say, this axiom is way too complicated for its own good.

[rlepigre]

I can't say I'm too happy about this axiom, but do you have an alternative in mind?

[SkySkimmer]

I think the axiom should be on the primitive compare not the derived lt.
Then maybe define to_list : string -> list char and the axiom says forall s s', compare_string s s' = compare_list compare_int (to_list s) (to_list s') (not sure if we have compare_list already defined)

[silene]

I am not sure whether we have compare_list, but we do have String.compare. More generally, I think we should strive to express all our axioms in terms of fully-defined inductive functions. (This is something we had in the old days of retroknowledge and that we unfortunately lost.) And then, properties like transitivity would be trivial corollaries.

[rlepigre]

The axiom was indeed wrong, but it should be fixed now. I'll look into the other possibilities when I have a minute.

[proux01]

A few comments. About the specification, I concur with Guillaume that it would be better to have it in terms of equivalence with an inductive implementation, like it's done for int and float.

[proux01]

One could also have tests for simpl and hnf.

[proux01]

C.f. above comment

[proux01]

C.f. above comment

[proux01]

Please split this file into multiple ones (primitives, specs, axioms, lemmas) with minimal requirements otherwise it will be a nightmare the day we'll have to run primitive strings through the debuger.

[rlepigre]

I split the primitives to their own files, and same for the axioms. The rest is still in a single for for now, but still a work in progress.

[proux01]

BTW, this is fine when it comes to testing the parsing but a printing test is probably also in order in test-suite/output (c.f. test-suite/output/FloatNumberSyntax.v for instance).

[proux01]

So if I understand correctly, the only missing things here are the executable spec and the doc. FWIW if we want it into upcoming 8.20, this must be merged before June 17th.

[rlepigre]

To make the notation work, I had to use this coercion. Is that OK, or is there a better approach here?

[proux01]

Do you have an example of something that doesn't work? I can't reproduce.

[rlepigre]

For example, the test file I added has failures. Basically, using the notation gives a type error for me.

You can also try Check make 2 "c". at the very end of PrimString.v.

[proux01]

So that's not a printing issue, rather a parsing one. The coercion is probably fine, otherwise you can copy what's done in number notation to string notation so that you can register the string notation for type int rather than int_wrapper.