FFI using type argument as array length

[qsctr]

A Cryptol user reports:

I ran into some surprising behavior in the Cryptol FFI yesterday. Let's say you have a foreign function that takes an array whose length is defined as an expression involving a type parameter:

foreign myfunc :
  {n} (fin n)
  => [n + 1][32] -> [32]

The array gets passed to the FFI function as a length followed by a pointer.

#[no_mangle]
#[export_name = "myfunc"]
pub extern "C" fn myfunc(n: usize, v: *const u32) -> u32 {
    eprintln!("In FFI: n = {n}");
    n as u32
}

It looks like Cryptol is passing in the value of the type parameter as the array length, instead of using the value of the expression. Example output:

Cryptol> :l /home/cryptol/ffi_test.cry
Loading module Cryptol
Loading module Main
Loading dynamic library ffi_test.so
Main> let v = [1, 2] : [2][32]
Main> myfunc v
In FFI: n = 1
0x00000001

This is actually the intended behavior. Sequences are not passed as a pair of length and pointer, but rather the pointer only. Additionally, numeric type arguments are passed as size_t's at the beginning of the argument list. Therefore, myfunc receiving n as the first argument rather than n+1 is correct. The size of any array can always be determined since it is some arithmetic expression built from some type arguments which are always passed explicitly. You can read more here and here.

cc @eddywestbrook @weaversa