Support for efficient primitives

[annenkov]

I have the following questions:

• Will CertiCoq support the use of Coq's primitive integers in a way that they compile to efficient C representation?

• More generally, would it be possible to tell the CertiCoq compiler what is considered a "primitive"? I.e., similarly to Extract Constant of Coq's extraction, allow for remapping certain functions and data types to "library" implementations of these (e.g. lists to arrays and operations on lists to operations on arrays).
  I understand that this would be way harder (if possible) than Extract Constant, but maybe you have some thoughts about that.

[zoep]

Hi Danil,

• We have not yet ported CertiCoq to Coq 8.12, but once we move to 8.12 we should be able to support primitive integers (at least without proofs at first). That seems to be more relevant to the CertiCoq FFI, so maybe @joom, @KatStark or @andrew-appel could elaborate more.

• Again, @joom is working on something similar and currently he's able to do i/o from Coq programs by providing C implementations of typeclasses (and perhaps he can say more about it). Maybe something similar could be used to parameterize with an array implementation and then link the compiled program with a native C array implementation.

I do not think that we'll be able to remap implementations in the same way Extract Constant does it because we need some abstraction barrier for this to be sound. So I think what we are targeting is letting the user provide C implementations for abstract/opaque interfaces.

Zoe

[annenkov]

Hi Zoe,

Thanks a lot for your answer!

I do not think that we'll be able to remap implementations in the same way Extract Constant does it because we need some abstraction barrier for this to be sound. So I think what we are targeting is letting the user provide C implementations for abstract/opaque interfaces.

This sounds very reasonable to me. How the interfaces will be specified at the Coq level? Typeclasses, modules?

[zoep]

Right now with typeclasses (@joom has some neat examples in becnhmarks/io and becnhmarks/hash). Because they're first class, we can parameterize the program with the interface and then, after compilation, apply it to the C implementation.

There is a problem with that: because the functions of the interface are parameters of the top-level program, they are not treated as global variables/top-level known functions. That means that the C functions need to be wrapped in closures at the C level, before being passed to the CertiCoq-generated program. Therefore, whenever they are applied the code pointer is fetched from the closure record (1st source of inefficiency) and also they are considered free variables of the functions that use them (unless they are always invoked at the top-level) so they need to be propagated to their call sites through closure environments (2nd source of inefficiency) .

For Coq's primitive objects, we should be able to do better and treat calls to primitive functions as calls to known functions, which will be much more efficient.

[joom]

• Will CertiCoq support the use of Coq's primitive integers in a way that they compile to efficient C representation?

That is within our plans. CertiCoq's first step is to reify the term you're compiling, and MetaCoq currently doesn't support reifying terms containing primitive ints, floats or arrays:
https://github.com/MetaCoq/metacoq/blob/613bfd9d70699986eb78463b03f6860b0ce98853/template-coq/src/quoter.ml#L267-L269

We can start working on CertiCoq support for them once they are added to MetaCoq, but even that might take some time, since some proofs may depend on assumptions on how data types are represented. Currently only 0-ary constructors are unboxed in CertiCoq, but support for Int63 and such will change that.

Also, one of the goals of the FFI project is to define a new integer type, that uses Int63 for the integers that fit, and a big integer type for the ones that don't, but with both constructors unboxed. Even if we had primitive integers, this is not immediately possible since 1-ary constructor are always boxed. Having both constructors unboxed would help us avoid pointer indirection and make using the new safe integer type computationally cheaper.

How the interfaces will be specified at the Coq level? Typeclasses, modules?

Currently type classes:
https://github.com/PrincetonUniversity/certicoq/blob/d7984465c2fb240d5328c92c633d5a1e695ac0e4/benchmarks/io/io.v

And then the FFI user creates instances of those type classes in C, using the glue functions generated by CertiCoq:
https://github.com/PrincetonUniversity/certicoq/blob/d7984465c2fb240d5328c92c633d5a1e695ac0e4/benchmarks/io/prog_main.c#L139-L157

But it seems there are a few issues with this so we might explore different avenues.

(We cannot do modules because MetaCoq doesn't support modules in the way we need.)

[annenkov]

Thank you @joom for the clarification.

MetaCoq currently doesn't support reifying terms containing primitive ints, floats or arrays

Indeed. So I asked at Coq Zulip about this: https://coq.zulipchat.com/#narrow/stream/237658-MetaCoq/topic/Primitive.20types.20in.20MetaCoq

I'll take a closer look at the FFI, thanks for the pointer.

We cannot do modules because MetaCoq doesn't support modules in the way we need

Yes, fair enough.

[intoverflow]

Looping back here to share some updates:

1. The CertiCoq prims branch provides support for binding Coq definitions/axioms to C functions. @joom and @zoep have demo code for some Int63 and bytestring functions. I have confirmed that this works and have been consolidating/extending these libraries. End-to-end proofs will take a minute, but the (unverified) functionality will be done Real Soon Now.
2. Since the proof story is still in development, certain aspects of (1) are subject to change
3. MetaCoq now has support for Primitive definitions, but CertiCoq does not yet handle them (if I understand correctly). See Quoting + erasure of primitive objects MetaCoq/metacoq#527 . This currently blocks us from being able to provide seamless support for Int63. This is expected to be an easy fix once someone gets a chance to do it (currently unassigned)

[mattam82]

With PR #39 we will now have access to the primitive ints and floats in the erased code.

[spitters]

@mattam82 I understand that these pimitives have been disabled again?
@joom any updates on https://github.com/CertiCoq/VeriFFI ?

[yforster]

I understand that these pimitives have been disabled again?

Yes, the primitives have been disabled for the moment. The problem is that we don't have a good story how to include them in the type system and type checker yet, meaning programs containing primitives were anyways not supported by MetaCoq's erasure (i.e. the first phase of CertiCoq). We disabled them because like this CertiCoq (seen as a program from TemplateCoq AST to C light AST) can compile itself. On the MetaCoq side we are commited to include them again, but it will take some time / some more humanpower in the team. It would probably make for a good self-contained but potentially challenging internship / Bachelor's / Master's thesis project to introduce proper support for primitives on the various levels.

[mattam82]

See PR #57 for working support for primitive types (int63 for now, floats and arrays are not yet implemented)

[spitters]

@mattam82 I could not directly find the answer in the code. How are Int63 translated to C? Are you using 64 bit integers? Did you prove correctness of this translation, which seems somewhat daunting...

[mattam82]

(Unsigned) Int63 are translated to immediate ints, just like in ocaml. We verify the basic operational semantics: if something evaluates to a primitive int in Coq, it evaluates to the same in C, provided the primitives implementations I coded in C are equivalent to those linked in the Coq kernel. So the hard part is unverified for now. With VeriFFi it will be easy to setup the necessary obligations.

[spitters]

Thanks!
I wasn't aware of:
https://github.com/CertiCoq/VeriFFI
It seems somewhat related to https://gallium.inria.fr/~agueneau/publis/melocoton.pdf , which treats the ocaml-C FFI.