cubical-transport-hott-lean4/native/cubical/test/wasm_harness.mjs

// wasm_harness.mjs — Node.js validation harness for topolei-cubical wasm.
//
// Proves the wasm ABI surface works by implementing a *minimal* subset of
// Lean's runtime in JS (bump allocator + object header layout) and
// exercising both scalar-passthrough and heap-allocating cubical
// functions.  A real Lean-wasm runtime will provide the shim imports
// natively; see `WASM.md` for integration details.
//
// Run: node test/wasm_harness.mjs

import fs from 'fs';
import path from 'path';
import { fileURLToPath } from 'url';

const __dirname = path.dirname(fileURLToPath(import.meta.url));
const wasmPath = path.resolve(
  __dirname,
  '../target/wasm32-unknown-unknown/release/topolei_cubical.wasm'
);

// ── Lean object layout (wasm32) ────────────────────────────────────────────
// struct lean_object {
//     uint32_t m_rc;         // offset 0, 4 bytes
//     uint16_t m_cs_sz;      // offset 4, 2 bytes (bitfield 16)
//     uint8_t  m_other;      // offset 6, 1 byte  (bitfield 8)
//     uint8_t  m_tag;        // offset 7, 1 byte  (bitfield 8)
//     // ctor fields: 4-byte pointers at offsets 8, 12, 16, ...
// };
//
// Scalar pointer encoding: (value << 1) | 1.  low-bit-set → scalar.

const HEADER_SIZE = 8;
const FIELD_SIZE  = 4;  // wasm32: pointer is 4 bytes.

const isScalar = (o) => (o & 1) === 1;
const unbox    = (o) => o >>> 1;
const boxTag   = (tag) => (tag << 1) | 1;

// ── Bump allocator + shim ──────────────────────────────────────────────────

// The wasm module is instantiated with our shim; we read `__heap_base`
// after instantiation to find where we can start allocating.

let memory = null;
let heapPtr = 0;
let view = null;

function align(p, a) { return (p + (a - 1)) & ~(a - 1); }

function alloc(bytes) {
  heapPtr = align(heapPtr, 8);
  const p = heapPtr;
  heapPtr += bytes;
  return p;
}

function setHeader(o, tag, num_objs) {
  view.setUint32(o, 1, true);          // m_rc = 1
  view.setUint16(o + 4, 0, true);      // m_cs_sz = 0
  view.setUint8(o + 6, num_objs);      // m_other = num_objs
  view.setUint8(o + 7, tag);           // m_tag = tag
}

function getTag(o) {
  if (isScalar(o)) return unbox(o);
  return view.getUint8(o + 7);
}

function getField(o, i) {
  return view.getUint32(o + HEADER_SIZE + i * FIELD_SIZE, true);
}

function setField(o, i, v) {
  view.setUint32(o + HEADER_SIZE + i * FIELD_SIZE, v, true);
}

const shim = {
  topolei_shim_obj_tag: getTag,
  topolei_shim_ctor_get: getField,
  topolei_shim_ctor_set: setField,
  topolei_shim_alloc_ctor: (tag, num_objs, scalar_sz) => {
    const size = HEADER_SIZE + num_objs * FIELD_SIZE + scalar_sz;
    const p = alloc(size);
    setHeader(p, tag, num_objs);
    return p;
  },
  topolei_shim_inc: () => {},  // refcount — harness doesn't GC
  topolei_shim_dec: () => {},
  topolei_shim_string_eq: (a, b) => {
    // For tests that don't exercise strings; panic if called.
    throw new Error('string_eq: harness does not implement string content comparison');
  },
  topolei_shim_mk_string: () => {
    throw new Error('mk_string: harness does not implement string allocation');
  },
};

// ── Instantiate ────────────────────────────────────────────────────────────

const wasmBuffer = fs.readFileSync(wasmPath);
const { instance } = await WebAssembly.instantiate(wasmBuffer, { env: shim });
memory = instance.exports.memory;
view = new DataView(memory.buffer);
heapPtr = instance.exports.__heap_base.value;

// ── Test cases ─────────────────────────────────────────────────────────────

// DimExpr constructor tags (from native/cubical/src/tags.rs):
const DIM_ZERO = 0, DIM_ONE = 1, DIM_VAR = 2, DIM_INV = 3, DIM_MEET = 4, DIM_JOIN = 5;
const FACE_BOT = 0, FACE_TOP = 1, FACE_EQ0 = 2, FACE_EQ1 = 3, FACE_MEET = 4, FACE_JOIN = 5;

const scalarZero = boxTag(DIM_ZERO);  // 0x1
const scalarOne  = boxTag(DIM_ONE);   // 0x3

// Build (.inv .zero) — heap-allocated ctor with one field pointing at .zero scalar.
function mkInv(inner) {
  const p = alloc(HEADER_SIZE + FIELD_SIZE);
  setHeader(p, DIM_INV, 1);
  setField(p, 0, inner);
  return p;
}

function mkMeet(a, b) {
  const p = alloc(HEADER_SIZE + 2 * FIELD_SIZE);
  setHeader(p, DIM_MEET, 2);
  setField(p, 0, a);
  setField(p, 1, b);
  return p;
}

function mkFaceMeet(a, b) {
  const p = alloc(HEADER_SIZE + 2 * FIELD_SIZE);
  setHeader(p, FACE_MEET, 2);
  setField(p, 0, a);
  setField(p, 1, b);
  return p;
}

const tests = [];

// Scalar passthrough (no allocation).
tests.push(['DimExpr.normalize(.zero) → .zero',
  () => instance.exports.topolei_cubical_dimexpr_normalize(scalarZero),
  scalarZero]);
tests.push(['DimExpr.normalize(.one) → .one',
  () => instance.exports.topolei_cubical_dimexpr_normalize(scalarOne),
  scalarOne]);

// Heap-object reductions.
tests.push(['DimExpr.normalize(.inv .zero) → .one',
  () => instance.exports.topolei_cubical_dimexpr_normalize(mkInv(scalarZero)),
  scalarOne]);
tests.push(['DimExpr.normalize(.inv .one) → .zero',
  () => instance.exports.topolei_cubical_dimexpr_normalize(mkInv(scalarOne)),
  scalarZero]);
tests.push(['DimExpr.normalize(.inv (.inv .zero)) → .zero',
  () => instance.exports.topolei_cubical_dimexpr_normalize(mkInv(mkInv(scalarZero))),
  scalarZero]);

// FaceFormula scalar passthrough.
tests.push(['FaceFormula.normalize(.bot) → .bot',
  () => instance.exports.topolei_cubical_face_normalize(boxTag(FACE_BOT)),
  boxTag(FACE_BOT)]);
tests.push(['FaceFormula.normalize(.top) → .top',
  () => instance.exports.topolei_cubical_face_normalize(boxTag(FACE_TOP)),
  boxTag(FACE_TOP)]);

// FaceFormula absorption laws.
tests.push(['FaceFormula.normalize(.meet .top .bot) → .bot',
  () => instance.exports.topolei_cubical_face_normalize(
    mkFaceMeet(boxTag(FACE_TOP), boxTag(FACE_BOT))),
  boxTag(FACE_BOT)]);
tests.push(['FaceFormula.normalize(.meet .bot .top) → .bot',
  () => instance.exports.topolei_cubical_face_normalize(
    mkFaceMeet(boxTag(FACE_BOT), boxTag(FACE_TOP))),
  boxTag(FACE_BOT)]);

// DimExpr meet reductions (recursive).
tests.push(['DimExpr.normalize(.meet (.inv .zero) (.inv .one)) → .meet .one .zero',
  () => {
    // inv .zero normalizes to .one; inv .one normalizes to .zero.
    // Our normalize recurses on meet's children, so result is .meet .one .zero.
    // In our encoding: a heap .meet ctor (tag 4) with fields (0x3, 0x1).
    const result = instance.exports.topolei_cubical_dimexpr_normalize(
      mkMeet(mkInv(scalarZero), mkInv(scalarOne)));
    if (isScalar(result)) return `scalar 0x${result.toString(16)}`;
    const tag = getTag(result);
    if (tag !== DIM_MEET) return `tag=${tag} (expected ${DIM_MEET})`;
    const a = getField(result, 0);
    const b = getField(result, 1);
    return `meet 0x${a.toString(16)} 0x${b.toString(16)}`;
  },
  `meet 0x${scalarOne.toString(16)} 0x${scalarZero.toString(16)}`]);

// ── Run ────────────────────────────────────────────────────────────────────

let fails = 0;
console.log('── Topolei cubical wasm harness ──');
for (const [desc, fn, expected] of tests) {
  try {
    const got = fn();
    if (got === expected) {
      console.log(`  ✅ ${desc}`);
    } else {
      console.log(`  ❌ ${desc}`);
      console.log(`       expected: ${typeof expected === 'number' ? '0x' + expected.toString(16) : expected}`);
      console.log(`       actual:   ${typeof got === 'number' ? '0x' + got.toString(16) : got}`);
      fails++;
    }
  } catch (e) {
    console.log(`  ❌ ${desc}  threw: ${e.message}`);
    fails++;
  }
}
console.log(`── ${tests.length - fails} / ${tests.length} tests passed ──`);
process.exit(fails > 0 ? 1 : 0);