The Coq mailing list

[Mario Frank <mafrank AT uni-potsdam.de>]

    Dear Andrew,
    
    in fact, I already stumbled over VeriFFI yesterday. But nevertheless
    I want to thank you for
    confirming that I found the right spot to search for a solution for
    my use case.
    
    Sadly, the examples did not enlighten me, since the main.c files in
    the respective folders
    do not provide args to the thread_info. In my use case, I do not
    have a main. Rather,
    I catch some event with some integral parameters which I need to
    pass to the Coq code.
    So, I hope someone of the VeriFFI team can enlighten me a bit.
    
    Best regards,
    Mario
---
Dipl.-Inform Mario Frank
Wissenschaftlicher Mitarbeiter
Universität Potsdam
Institut für Informatik und Computational Science
 - Lehrstuhl Theoretische Informatik -
 - Konsortialprojekt VERSECLOUD -
eMail: mario.frank AT uni-potsdam.de
fon: 0331 977 3069

Am 06.10.23 um 14:16 schrieb Andrew Appel:

      Dear
        Mario:

The Verified Foreign Function Interface for CertiCoq, or VeriFFI for short, addresses exactly these issues:

How to interface Coq code (compiled by CertiCoq) to C code, and how to connect Coq proofs of the Coq code to VST proofs of the C code (and the garbage collector) across the interface.

https://github.com/CertiCoq/VeriFFI#readme

Two of the VeriFFI research team are traveling or otherwise unavailable this week, but I hope someone can respond to you about this in the next week or two.

Sincerely,

Andrew Appel

On Oct 6, 2023, at 5:15 AM, Mario Frank <mafrank AT uni-potsdam.de> wrote:

Dear Coq community,

I am working on integrating a synthesised portion of CLight code into a
C application.
Namely, I do have the following C and Coq function definitions :

int my_fun(unsigned int val1, unsigned int val2, int val3, unsigned int
val4)

Definition coq_fun (val1  : nat) (val2  : nat) (val3  : Z) (val4  : nat)
: Z := ...

my_fun shall call coq_fun, providing the parameters and return either
an error value or success.

The Coq function was compiled with

CertiCoq Compile -args 4 "my_fun" my_fun ...

and I use the following implementation for my_fun.

int my_fun(unsigned int val1, unsigned int val2, int val3, unsigned int
val4)
{
  struct thread_info *ti;
  ti = make_tinfo();
  if (ti == 0)
    return -1;

  ti->args[1]=val1; // Wrapping val into Val_int does not change anything
  ti->args[2]=val2; // Wrapping val into Val_int does not change anything
  ti->args[3]=val3; // Wrapping val into Val_int does not change anything
  ti->args[4]=val4; // Wrapping val into Val_int does not change anything

  value ret_val = body(ti);

  if (Int_val(ret_val) == -1)
  {
    return -1;
  }
  else
  {
    return 0;
  }
}

The conglomerate of native C code and synthesised C code compiles fine,
apart from some.
Also, the body function is called, but always returns 0, even when being
called
with invalid values. First it seemed that the parameters were not
properly handed over
to the function. But after tracing what happens in the CLight code, I
found out, that
the body function indeed is entered and left. But the closure to coq_fun
seemingly is not called.
At least, the tracing output does not show up.
But I am not able to find a resource or example describing how to
provide arguments from C to
synthesised code.

Does anyone have experience with this use case or a pointer to some example?

Best regards,
Mario