https://github.com/mit-plv/fiat-crypto/issues/707

main.c

#include <stdio.h>

#include "curve25519_32_p.h"

// for hex2bin
#include "o1c.h"

int main() {
    uint8_t a[32], b[32], c[32];
    for (unsigned i = 0; i < 32; ++i) {
        a[i] = i;
        b[i] = i + 32;
    }
    uint32_t af[10], bf[10], cf[10];
    fiat_25519_from_bytes(af, a);
    fiat_25519_from_bytes(bf, b);
    fiat_25519_carry(af, af);
    fiat_25519_carry(bf, bf);
    fiat_25519_carry_mul(cf, af, bf);
    fiat_25519_to_bytes(c, cf);

    char A[65], B[65], C[65];
    unsigned i;
    o1c_bin2hex(A, a, 32);
    o1c_bin2hex(B, b, 32);
    o1c_bin2hex(C, c, 32);
    printf("%s * %s = %s\n", A, B, C);
    return 0;
    // result: 000102030405060708090a0b0c0d0e0f101112131415161718191a1b1c1d1e1f * 202122232425262728292a2b2c2d2e2f303132333435363738393a3b3c3d3e3f = 1f8a85cd3caefc029ca2f163d41d1ba79cd62f83ab83e6aeb7dbf5e077951450

}

Main.java

public class Main {
    public static void main(String[] args) {
        int[] a = new int[32];
        int[] b = new int[32];
        int[] c = new int[32];
        for (int i = 0; i < 32; i++) {
            a[i] = i;
            b[i] = i;
        }
        int[] af = new int[10];
        int[] bf = new int[10];
        int[] cf = new int[10];
        FiatCurve25519.fiat_Curve25519_from_bytes(af, a);
        FiatCurve25519.fiat_Curve25519_from_bytes(bf, b);
        FiatCurve25519.fiat_Curve25519_carry(af, af);
        FiatCurve25519.fiat_Curve25519_carry(bf, bf);
        FiatCurve25519.fiat_Curve25519_carry_mul(cf, af, bf);
        FiatCurve25519.fiat_Curve25519_to_bytes(c, cf);
        for (int i = 0; i < 32; i++) {
            System.out.printf("%02x", a[i]);
        }
        System.out.print(" * ");
        for (int i = 0; i < 32; i++) {
            System.out.printf("%02x", b[i]);
        }
        System.out.print(" = ");
        for (int i = 0; i < 32; i++) {
            System.out.printf("%02x", c[i]);
        }
        System.out.println();
        // result: 000102030405060708090a0b0c0d0e0f101112131415161718191a1b1c1d1e1f * 000102030405060708090a0b0c0d0e0f101112131415161718191a1b1c1d1e1f = 58ed2c5a5eff1caf600cfd65496a24514bb1981d2275f18dfb1e0d4195c45a01
    }
}