cryptol-3.4.0: lib/cry_ffi.h
#pragma once
#include <stdlib.h>
#include <stdint.h>
// A convenince macro to call a method on an object.
#define CRY_FFI(obj, f, args...) ((obj)->f((obj)->self, args))
/** Imports foreign values into Cryptol.
This should be used when a foreign function needs to return a result
to the Cryptol interpreter. Cryptol values are imported as follows:
Bit:
send_bool(value);
Float32, Float64:
send_double(value);
Integer, Z:
uint64_t* digits = send_new_large_int(size);
// write value into `digits`
send_sign(sign);
[n]
| n <= 64 send_small_uint(value) or
send_small_sint(value)
| otherwise send Integer (as above)
(like receiving an Integer, but without a sign)
[n] a
send `n` values of type `a`
Rational:
send 2 Integers (as above): 1st is numerator, 2nd denominator.
Tagged sum:
send_tag(&tag); send fields based on the tag;
The constructor number corresponds to the order of the declaration.
Tuple, record, newtype:
send the elements one after the other.
The fields of records and newtypes are sent in alphabetical order.
*/
struct CryValImporter {
/** This should be passed to all the function pointers.
It captures the current state of the importing process.
*/
void* self;
/** Make a boolean value: 0: false, > 0: true.
This is used to send Bit values.
*/
void (*send_bool)(void*, uint8_t);
/** Make a small unsigned integer, which fits in an uint64_t.
This is used to send words [n] (n <= 64).
*/
void (*send_small_uint)(void*, uint64_t);
/** Make a small signed integer, which fits in an int64_t.
This is used to send words [n] (n <= 64).
*/
void (*send_small_sint)(void*, int64_t);
/** Make a floating point value.
This is used to send Float32 and Float64 values.
*/
void (*send_double)(void*, double);
/** Start building a sum type.
The size_t argument is the number of the constructor.
*/
void (*send_tag)(void*, size_t);
/** Start building an Integer, a Z value, or a large word [n] (n > 64).
The size argument is the number of uint64_t digits we need.
The result is a buffer where the digits should be placed,
least significant first.
*/
uint64_t* (*send_new_large_int)(void*, size_t);
/** Finish bulding an Integer, a Z value, or a large word [n] (n > 64).
The sign argument is 1 for negative, and 0 for non-negative.
*/
void (*send_sign)(void*, uint8_t);
};
/** Exports Cryptol values into a foreign environment.
This should be used to get a foreign function's arguments from the
Cryptol interpreter. Cryptol values are exported as follows:
Bit:
recv_u8(&value);
Float32, Float64:
recv_double(&value);
Integer, Z:
recv_u8(&sign); recv_u64(&size); recv_u64_digits(value);
numeric type parameter:
recv_u64(&value);
if (value == (maxBound :: uint64_t)) then receive an Integer (as above).
[n]
| n <= 8 recv_u8(&value)
| 8 < n && n <= 64 recv_u64(&value)
| otherwise recv_u64(&size); recv_u64_digits(value);
(like receiving an Integer, but without a sign)
[n] a
receive `n` values of type `a`
Rational:
receive 2 Integers (as above): 1st is numerator, 2nd denominator.
Tagged sum:
recv_u64(&tag); receive fields based on the tag;
The constructor number corresponds to the order of the declaration.
Tuple, record, newtype:
Receive the elements one after the other.
The fields of records and newtypes are received in alphabetical order.
*/
struct CryValExporter {
/** This should be passed to all function pointers.
It captures the current state of the exporting process.
*/
void *self;
/** Get a uint8_t. This is used to receive:
* The value of a Bit
* The value of a small words [n] (n <= 8)
* The sign of an Integer or Z value
Returns 0 on success.
*/
uint32_t (*recv_u8)(void*, uint8_t*);
/** Get a double. This is used to receive the value of a Float32 or Float64.
Returns 0 on success.
*/
uint32_t (*recv_double)(void*, double*);
/* Get a uint64_t. This is used to receive:
* The value of a small numeric type parameter
* The value of a word [n] (8 < n && n <= 64)
* The size of an Integer or Z value
* The size of a large numeric type parameter
* The tag of a sum type
Returns 0 on success.
*/
uint32_t (*recv_u64)(void*, uint64_t*);
/** Receive the uint64_t digits of an Integer, a Z value, a large numeric type
parameter, or a large word [n] (n > 64). These are placed in the provided
buffer, starting with the least significant one. The buffer should be big
enough to fit the digits.
Returns 0 on success.
*/
uint32_t (*recv_u64_digits)(void*, uint64_t*);
};