(I am working from the prims branch; apologies if this has been fixed in a later commit.)

The issue is best illustrated by an example:

From CertiCoq.Plugin Require Import CertiCoq.

Axiom my_fast_add: nat -> nat.

Definition foo: nat := 0.

(* This works: *)
CertiCoq Compile
    foo
    Extract Constants [
    ]
    Include [
    ].

Definition bar: nat := my_fast_add foo.

(* This also works: *)
CertiCoq Compile
    bar
    Extract Constants [
        my_fast_add => "my_primitive_fast_add"
    ]
    Include [
    ].

(* This does not work: *)
CertiCoq Compile
    foo
    Extract Constants [
        my_fast_add => "my_primitive_fast_add"
    ]
    Include [
    ].
(* Error message:
Could not compile: Constant example.my_fast_add not found in environment
*)

The error is raised by find_prim_arrity during register_prims in theories/Compiler/pipeline.v.

I suspect the environment for the extraction target does not include unused axioms/definitions.

The fix: if a constant is not used, it is safe to give it any arity we want (is this right? I'm only guessing here). The attached patch exploits this by modifying find_prim_arrity to return 0 for primitives that cannot be found in the environment.

tcarstens@pop-os:~/formal_methods/certicoq$ git diff
diff --git a/theories/Compiler/pipeline.v b/theories/Compiler/pipeline.v
index 85d7990d..ad4ee543 100644
--- a/theories/Compiler/pipeline.v
+++ b/theories/Compiler/pipeline.v
@@ -40,9 +40,10 @@ Definition find_global_decl_arrity (gd : Ast.global_decl) : error nat :=
 
 Fixpoint find_prim_arrity (env : Ast.global_env) (pr : kername) : error nat :=
   match env with
-  | [] => Err ("Constant " ++ string_of_kername pr ++ " not found in environment")
+  (* | [] => Err ("Constant " ++ string_of_kername pr ++ " not found in environment") *)
+  | [] => Ret 0
   | (n, gd) :: env =>
-    if eq_kername pr n then find_global_decl_arrity  gd
+    if eq_kername pr n then find_global_decl_arrity gd
     else find_prim_arrity env pr
   end.

tcarstens@pop-os:~/formal_methods/certicoq$ 

Hi all,

trying to install CertiCoq me + others spent time with the fact that it is required to have make install and not sudo make install (as everything is installed via Opam).
Maybe one could either adapt the make files or mention this in the instructions? -- Thanks!

Kathrin

Environment

certicoq commit a426ffe
Alpine linux 3.16.2

Steps to reproduce

(This actual test input is not relevant, CertiCoq FFI generates incorrect output on any type class I tried.)

(* Test.v *)
Class Test : Type := { test : unit -> unit }.

From CertiCoq.Plugin Require Import CertiCoq.
CertiCoq FFI Test.

coqc Test.v

gcc -w -c ffi.Test.Test.c

Expected behavior

The generated C file compiles without errors.

Actual behavior

ffi.Test.Test.c:15:3: error: '$result' undeclared (first use in this function); did you mean 'result'?
   15 |   $result = test(tinfo, $arg);
      |   ^~~~~~~
      |   result
ffi.Test.Test.c:15:3: note: each undeclared identifier is reported only once for each function it appears in
ffi.Test.Test.c:15:18: error: 'tinfo' undeclared (first use in this function); did you mean '$tinfo'?
   15 |   $result = test(tinfo, $arg);
      |                  ^~~~~
      |                  $tinfo

Some variable definitions are wrong. An excerpt from ffi.Test.Test.c:

void test_1(struct thread_info *$tinfo, unsigned long long $env, unsigned long long $arg)
{
  unsigned long long result;
  $result = test(tinfo, $arg);
  *((unsigned long long *) (*$tinfo).args + 1LLU) = $result;
  return;
}

The variable should be declared as $result instead of result. tinfo is also wrong, but the other way around.

Workaround

This is what I came up with for now, seems to be working so far:
sed -i 's/\$\(result\|arg[0-9]\?\|pair\|new_env\|new_clo\|tinfo\|env\)/\1/g' ffi.*.c

I'm aware that the primitive operations are not verified, but I believe that there are some bugs in the C code for the Coq primitive Uint63 operations (in plugin/runtime/prim_int63.c)

The specification for Uint63.div x y defines the result to be 0 if the y is 0 (and this is also the result of evaluating the expression in Coq with e.g. Compute).
Currently the function prim_int63_div doesn't check the value of y, leading to a division-by-zero/ segfault if y is 0.

Similarly, the specification for Uint63.mod x y defines the result to be x if the y is zero, but prim_int63_mod doesn't check the value of y, and so also segfaults if it is 0.

The above also has implications for Uint63.diveucl x y. It's defined to return (Uint63.div x y, Uint63.mod x y), but the function prim_int63_diveucl returns (0, 0) for inputs x and y if y is 0 while it should be (0, x).

The specification for logical shifts Uint63.lsl x y and Uint63.lsr x y implies that the result is 0 if 63 <= y (and this is also the actual result of evaluating such an expression), but in C the expressions x << y and x >> y have undefined behavior if 64 <= y.
For example, the result of Compute Uint63.lsl 1 64. is 0, but using CertiCoq to compile the expression to C and then compiling it with both clang (v 17.0.6), gcc (v 13.2.1) and ccomp (v 3.12) and then pretty printing the resulting value (I used the function Unsigned_long_val in plugin/runtime/values.h on the value I get back from the main/ body function and then did printf("%llu\n", x)) gives me 1.
The story is similar for right shift.

Finally, I think there is a mistake in the implementation of Uint63.mulc.

First, I think some of the expressions in mulc_aux should be taken modulo 2^63 (it seems like the C code is translated from the ml code in the Coq kernel, which assumes 63-bit integers).

For instance, I think the statement l = (l + hl2); on line 292 should be l = (l + hl2) & maxuint63;, because l is used in a comparison on the next line to check for a carry, which could get lost if the result of the addition is greater than 2^63-1 but not greater than 2^64-1.
For example, the result of Compute Uint63.mulc 12188099900 12188099900. is (16, 975826582703597072), but using CertiCoq to compile the expression to C and pretty print the result with glue code for prod gives me (pair 15 975826582703597072).
It should probably also be done for the statement unsigned long long hl = hxly + lxhy; on line 289, since hl is also used in the next line to check for a carry.

Secondly, I think there is a dereference missing in the else branch in prim_int63_mulc, when extracting the arguments from the pair, line 308 and 309, I believe it should be

unsigned long long h = Unsigned_long_val(*((unsigned long long*) p + 0));
unsigned long long l = Unsigned_long_val(*((unsigned long long*) p + 1));

Without the above dereference, the result of e.g. Compute Uint63.mulc 8500964271916320249 8500964271916320249 is (7835138088720211561, 6616587037742705713), but using CertiCoq to compile and run with pretty printing as above gives me different results on each execution.

Hi,
There seems to be a compilation error in files AstCommon.v as Prototype.v, as the following error messages pop up:

File "./common/AstCommon.v", line 10, characters 0-37:
Error: Notation "_ >>= _" is already defined at level 50 with arguments
constr at level 50, constr at next level while it is now required to be
at level 58 with arguments constr at level 58, constr at next level.

File "./L6_PCPS/Prototype.v", line 70, characters 0-1758:
Error: Non exhaustive pattern-matching: no clause found for pattern tInt _

I'm using opam 4.07.1, coq 8.12.0, coq-equations 1.2.3+8.12, coq-ext-lib 0.11.2 and coq-metacoq 1.0~beta2+8.12

Thanks in advance,
Felipe

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.

coq-ext-lib normally checks all dependants in its CI, but coq-certicoq takes too long to build, and exhausts the time budget.
coq-community/coq-ext-lib#135 skips the compatibility checking with CertiCoq.
Before we figure out how to add it back (e.g. by switching to GitHub Actions), please be aware of potential incompatibilities with newer versions of ExtLib, and submit complaints via GitHub Issues.

Dear developers of Certicoq,

I've tried compiling Certicoq master in order to play with the plugin; but I wasn't able to proceed, maybe because of some linking issue…
I've tried using the dependencies from the Git submodules with different versions of OCaml and Coq in ({4.05.0, 4.06.1, 4.07.0+flambda} × {8.8.1, 8.8.2}), but ended up with the error:

File "./CertiCoq.v", line 3, characters 0-33:
Error:
Anomaly "cannot find tmExistingInstance in module Template.TemplateMonad.Extractable."
Please report at http://coq.inria.fr/bugs/.

I've not investigated further, but FYI I paste below a sample Dockerfile I've been using, with OCaml version 4.06.1 and Coq version 8.8.1 (as suggested in the README.md).
Do you think this issue is easy to solve?

Kind regards, Erik

FROM coqorg/base:bare

ENV COMPILER="4.06.1"
ENV COQ_VERSION="8.8.1"
ENV NJOBS="2"

WORKDIR /home/coq

RUN ["/bin/bash", "--login", "-c", "set -x \
  && opam init --auto-setup --yes --jobs=${NJOBS} --compiler=${COMPILER} --disable-sandboxing \
  && eval $(opam env) \
  && opam repository add --all-switches --set-default coq-released https://coq.inria.fr/opam/released \
  && opam repository add --all-switches --set-default coq-extra-dev https://coq.inria.fr/opam/extra-dev \
  && opam repository add --all-switches --set-default coq-core-dev https://coq.inria.fr/opam/core-dev \
  && opam update -y \
  && opam pin add -n -y -k version coq ${COQ_VERSION} \
  && opam install -y -v -j ${NJOBS} coq \
  && opam clean -a -c -s --logs \
  && opam config list && opam repo list && opam list && coqc --version"]

ENV CERTICOQ_VERSION="abd82fd"

RUN ["/bin/bash", "--login", "-c", "set -x \
  && git clone https://github.com/PrincetonUniversity/certicoq.git \
  && cd certicoq && git checkout ${CERTICOQ_VERSION} \
  && git submodule update --init \
  && for dir in paramcoq coq-ext-lib SquiggleEq Template-Coq; \
  do \
  ( cd \"submodules/${dir}\" && make -j ${NJOBS} && make install ); \
  done"]

WORKDIR /home/coq/certicoq

RUN ["/bin/bash", "--login", "-c", "set -x \
  && make -j ${NJOBS} && make install"]

Our opam file will require clang for now (see PR #62 ) , as gcc is usually too slow and we barely tested CompCert's ccomp AFAIK.
We should add a Coq option to choose which C compiler to use (for Eval/Run) and use the same one in the Makefiles.
Probably we need CI tests for all three as well.

The current CI checks the build but does not check the benchmarks/examples.

Adding the benchmarks/examples to the CI will help in two ways:

• It will ensure the benchmarks/examples are being maintained
• It will automatically test the behavior of new PRs

Of course, the benchmarks/examples were not designed to be used for this purpose. However, follow-on work could update them in light of this use case.

The proof of correctness for Codegen doesn't compile with Coq 8.14.1
it is also not included in the CI build (has never been?)

for now it would help to know if there is a version of Coq, CertiCoq for which it is known to compile?

(I tried an older version with Coq 8.9 and had some issues installing the dependencies. )

thanks!

Some background:

I'm working on a backend to WebAssembly (together with Jean Pichon-Pharabod and Bas Spitters).
When translating indirect function calls I'd like to use the function tags of LambdaANF function definitions to distinguish functions.

From the comment here I assumed that they would be unique, but they are not, e.g. vs_easy from the benchmarks.

Am I missing something?

For the C-backend, that is not an issue since indirect calls work by passing the function pointer directly. However, WebAssembly doesn't have function pointers (that may be the case for other potential target languages as well.)