/* test_foundation.c -- the first DECOMPOSITION.md definitions, executed.
 *
 * Section 4 says of its colon definitions that each "has been traced by hand,
 * but none has been executed".  This file assembles the helpers, the sign and
 * zero tests, U< and UM* exactly as written there (plus 2DUP and - from
 * section 5, which U< needs) and runs them on the golden model against the C
 * operation each one stands for.
 *
 * Every call is made with a canary under the arguments, and the canary must
 * still be directly under the results afterwards: a definition that leaves
 * the right answer but an unbalanced stack is wrong.
 */
#include "v4/asm.h"
#include "v4/testcode.h"
#include "v4/umul.h"
#include <stdio.h>

static int failures = 0, checks = 0;
#define CHECK(c,...) do{checks++; if(!(c)){failures++; printf("FAIL %s:%d: ",__FILE__,__LINE__); printf(__VA_ARGS__); printf("\n");}}while(0)

#define CANARY ((v4_cell)0x0C0FFEE5)
#define MAXU   ((v4_ucell)~(v4_ucell)0)
#define FLAG(c) ((c) ? V4_ALL_ONES : (v4_cell)0)

static v4_node       n;
static v4_exec_state es;
static v4_heat       h;
static v4_asm        as;

static v4_cell w_nip, w_swap, w_or, w_negate, w_rot, w_zless, w_zequal,
               w_2dup, w_minus, w_uless, w_umstar;

#define O(name)  v4_asm_op(&as, V4_OP_##name)
#define LIT(v)   v4_asm_lit(&as, (v4_cell)(v))
#define CALL(w)  v4_asm_branch(&as, V4_OP_CALL, (w))

static void build(void)
{
    v4_asm_ref ref;

    v4_node_reset(&n);
    v4_asm_begin(&as, &n, 16);

    /* : NIP  push drop pop ; */
    w_nip = v4_asm_label(&as);
    O(PUSH); O(DROP); O(RPOP); O(SEMI);

    /* : SWAP  over push push drop pop pop ; */
    w_swap = v4_asm_label(&as);
    O(OVER); O(PUSH); O(PUSH); O(DROP); O(RPOP); O(RPOP); O(SEMI);

    /* : OR  over inv and xor ; */
    w_or = v4_asm_label(&as);
    O(OVER); O(INV); O(AND); O(XOR); O(SEMI);

    /* : NEGATE  inv 1 + ; */
    w_negate = v4_asm_label(&as);
    O(INV); LIT(1); O(ADD); O(SEMI);

    /* : ROT  push SWAP pop SWAP ; */
    w_rot = v4_asm_label(&as);
    O(PUSH); CALL(w_swap); O(RPOP); CALL(w_swap); O(SEMI);

    /* : 0<  -if L1  drop -1 ;   L1: drop 0 ; */
    w_zless = v4_asm_label(&as);
    ref = v4_asm_branch_fwd(&as, V4_OP_MINUS_IF);
    O(DROP); LIT(-1); O(SEMI);
    v4_asm_resolve(&as, ref, v4_asm_label(&as));
    O(DROP); LIT(0); O(SEMI);

    /* : 0=  if L1  drop 0 ;   L1: drop -1 ; */
    w_zequal = v4_asm_label(&as);
    ref = v4_asm_branch_fwd(&as, V4_OP_IF);
    O(DROP); LIT(0); O(SEMI);
    v4_asm_resolve(&as, ref, v4_asm_label(&as));
    O(DROP); LIT(-1); O(SEMI);

    /* : 2DUP  over over ;        (section 5.1) */
    w_2dup = v4_asm_label(&as);
    O(OVER); O(OVER); O(SEMI);

    /* : -  NEGATE + ;            (section 5.4), NEGATE in line */
    w_minus = v4_asm_label(&as);
    O(INV); LIT(1); O(ADD); O(ADD); O(SEMI);

    /* : U<  2DUP xor 0< IF NIP 0< ELSE - 0< THEN ;
     * with section 2's IF: the flag is dropped on both arms. */
    w_uless = v4_asm_label(&as);
    CALL(w_2dup); O(XOR); CALL(w_zless);
    ref = v4_asm_branch_fwd(&as, V4_OP_IF);
    O(DROP); CALL(w_nip); CALL(w_zless); O(SEMI);
    v4_asm_resolve(&as, ref, v4_asm_label(&as));
    O(DROP); CALL(w_minus); CALL(w_zless); O(SEMI);

    /* : UM*  a!  0  31 FOR +* UNEXT  push drop a pop ;
     * 31 is the cell width less one; written for a 32-bit cell in section 4.
     * The loop body is the start of its own word so that unext restarts it. */
    w_umstar = v4_asm_label(&as);
    O(BANG_A); LIT(0); LIT(V4_CELL_BITS - 1); O(PUSH);
    (void)v4_asm_label(&as);
    O(MUL_STEP); O(UNEXT); O(PUSH); O(DROP); O(PUSH_A); O(RPOP);
    O(SEMI);

    CHECK(v4_asm_ok(&as), "foundation words assemble");
}

/* Call `word` with a canary and up to three arguments on fresh stacks. */
static int call(v4_cell word, unsigned argc, v4_cell a, v4_cell b, v4_cell c)
{
    v4_dstack_reset(&n.ds);
    v4_rstack_reset(&n.rs);
    v4_exec_reset(&es);
    v4_heat_reset(&h);
    v4_dstack_push(&n.ds, CANARY);
    if (argc > 0) v4_dstack_push(&n.ds, a);
    if (argc > 1) v4_dstack_push(&n.ds, b);
    if (argc > 2) v4_dstack_push(&n.ds, c);
    return v4_test_call(&n, &es, &h, word, 1000) > 0;
}

/* The results, top first, then the canary. */
static int left1(v4_cell t)
{
    return n.ds.t == t && n.ds.s == CANARY;
}
static int left2(v4_cell s, v4_cell t)
{
    if (n.ds.t != t || n.ds.s != s) return 0;
    (void)v4_dstack_pop(&n.ds);
    return n.ds.s == CANARY;
}
static int left3(v4_cell third, v4_cell s, v4_cell t)
{
    if (n.ds.t != t) return 0;
    (void)v4_dstack_pop(&n.ds);
    return left2(third, s);
}

static const v4_cell vec[] = {
    0, 1, 2, 3, -1, -2, 12345, -12345,
    (v4_cell)(V4_MSB - 1u), (v4_cell)V4_MSB, (v4_cell)(V4_MSB + 1u),
    (v4_cell)(V4_MSB >> 1), (v4_cell)((V4_MSB >> 1) - 1u),
    (v4_cell)(MAXU / 3u), (v4_cell)(MAXU / 3u * 2u)
};
#define NVEC (sizeof vec / sizeof vec[0])

/* Does UM* as written give the true product? */
static int umstar_exact(v4_ucell u1, v4_ucell u2)
{
    v4_ucell lo, hi;
    v4_umul(u1, u2, &lo, &hi);
    return call(w_umstar, 2, (v4_cell)u1, (v4_cell)u2, 0) && left2((v4_cell)lo, (v4_cell)hi);
}

int main(void)
{
    printf("v4 foundation tests: V4_CELL_BITS=%d\n", V4_CELL_BITS);

    build();

    for (unsigned i = 0; i < NVEC; i++) {
        v4_cell a = vec[i];
        v4_ucell ua = (v4_ucell)a;

        CHECK(call(w_negate, 1, a, 0, 0) && left1((v4_cell)(0u - ua)), "NEGATE [%u]", i);
        CHECK(call(w_zless, 1, a, 0, 0) && left1(FLAG(ua & V4_MSB)), "0< [%u]", i);
        CHECK(call(w_zequal, 1, a, 0, 0) && left1(FLAG(a == 0)), "0= [%u]", i);

        for (unsigned j = 0; j < NVEC; j++) {
            v4_cell b = vec[j];
            v4_ucell ub = (v4_ucell)b;

            CHECK(call(w_nip, 2, a, b, 0) && left1(b), "NIP [%u,%u]", i, j);
            CHECK(call(w_swap, 2, a, b, 0) && left2(b, a), "SWAP [%u,%u]", i, j);
            CHECK(call(w_or, 2, a, b, 0) && left1((v4_cell)(ua | ub)), "OR [%u,%u]", i, j);
            CHECK(call(w_2dup, 2, a, b, 0) && n.ds.t == b && n.ds.s == a
                  && (v4_dstack_pop(&n.ds), v4_dstack_pop(&n.ds), left2(a, b)),
                  "2DUP [%u,%u]", i, j);
            CHECK(call(w_minus, 2, a, b, 0) && left1((v4_cell)(ua - ub)), "- [%u,%u]", i, j);
            CHECK(call(w_uless, 2, a, b, 0) && left1(FLAG(ua < ub)), "U< [%u,%u]", i, j);

            for (unsigned k = 0; k < NVEC; k++) {
                v4_cell c = vec[k];
                CHECK(call(w_rot, 3, a, b, c) && left3(b, c, a), "ROT [%u,%u,%u]", i, j, k);
            }

            /* UM* as written is exact whenever the multiplicand (u1, which
             * stays in S) is at most 2^(n-2): T is then always below S, so
             * T+S stays below 2^(n-1) and neither the lost carry nor +*'s
             * sign-keeping shift can touch the result.  u2 is unrestricted. */
            if (ua <= (V4_MSB >> 1))
                CHECK(umstar_exact(ua, ub), "UM* [%u,%u]", i, j);
        }
    }

    /* KNOWN LIMITS of UM* as written, recorded so they cannot be forgotten.
     * Section 4 marks UM* "NEEDS REVISION" and gives the limit as "operands
     * below 2^31".  The measured limit is tighter and is on u1 only.  These
     * two checks assert that the definition is still wrong where it is known
     * to be wrong; when UM* is rewritten they must be turned into ordinary
     * exactness checks. */
    CHECK(!umstar_exact(MAXU, MAXU), "UM* limit: carry out of T is lost (D-3)");
    CHECK(!umstar_exact(V4_MSB - 1u, 3u), "UM* limit: u1 below 2^(n-1) still fails");

    CHECK(v4_node_guards_intact(&n), "guards intact");

    printf("  %d checks, %d failures\n", checks, failures);
    return failures ? 1 : 0;
}