|
| 1 | +// SPDX-License-Identifier: MPL-2.0 |
| 2 | +// EchoRuntimeTest.res — semantic / runtime decomposition plane for Echo types. |
| 3 | +// |
| 4 | +// Proves the runtime half of "decomposition must be visible": |
| 5 | +// - echo(x, y) builds VEcho{input, output} |
| 6 | +// - echo_input works on VEcho, FAILS on a residue (witness genuinely gone) |
| 7 | +// - echo_output works on BOTH VEcho and VResidue (output survives) |
| 8 | +// - echo_to_residue yields VResidue and debits stability EXACTLY ONCE |
| 9 | +// - projection (echo_input / echo_output) never debits stability |
| 10 | + |
| 11 | +open Bytecode |
| 12 | +open TestHelpers |
| 13 | + |
| 14 | +let dummyLoc: Types.location = { |
| 15 | + start: {line: 1, column: 1, offset: 0}, |
| 16 | + end_: {line: 1, column: 1, offset: 0}, |
| 17 | + file: "<echo-runtime-test>", |
| 18 | +} |
| 19 | + |
| 20 | +// Build a chunk from a bare opcode list (locations unused by these opcodes). |
| 21 | +let chunkOf = (code: array<opcode>): chunk => { |
| 22 | + code, |
| 23 | + constants: [], |
| 24 | + locations: [], |
| 25 | +} |
| 26 | + |
| 27 | +// Run a chunk; return (result, final stability score). |
| 28 | +let runChunk = (code: array<opcode>): (result<value, string>, float) => { |
| 29 | + let vm = VM.make(chunkOf(code)) |
| 30 | + let r = VM.run(vm) |
| 31 | + (r, vm.stabilityScore) |
| 32 | +} |
| 33 | + |
| 34 | +// echo(1, "a") — input pushed first, output second (OpEcho pops output then input). |
| 35 | +let echoProgram: array<opcode> = [OpPush(VInt(1)), OpPush(VString("a")), OpEcho] |
| 36 | + |
| 37 | +let testEchoConstructsWitness = () => { |
| 38 | + suite("Echo runtime: construction") |
| 39 | + let (r, _) = runChunk(Array.concat(echoProgram, [OpHalt])) |
| 40 | + assertEqual("echo(1, \"a\") builds VEcho{input:1, output:\"a\"}", r, Ok(VEcho({input: VInt(1), output: VString("a")}))) |
| 41 | +} |
| 42 | + |
| 43 | +let testProjections = () => { |
| 44 | + suite("Echo runtime: projection") |
| 45 | + let (inp, _) = runChunk(Array.concat(echoProgram, [OpEchoInput, OpHalt])) |
| 46 | + assertEqual("echo_input recovers the witness", inp, Ok(VInt(1))) |
| 47 | + |
| 48 | + let (out, _) = runChunk(Array.concat(echoProgram, [OpEchoOutput, OpHalt])) |
| 49 | + assertEqual("echo_output recovers the output", out, Ok(VString("a"))) |
| 50 | +} |
| 51 | + |
| 52 | +let testToResidue = () => { |
| 53 | + suite("Echo runtime: decomposition to residue") |
| 54 | + let (res, _) = runChunk(Array.concat(echoProgram, [OpEchoToResidue, OpHalt])) |
| 55 | + assertEqual("echo_to_residue yields VResidue{output:\"a\"}", res, Ok(VResidue({output: VString("a")}))) |
| 56 | + |
| 57 | + // Output still recoverable from the residue. |
| 58 | + let (out, _) = runChunk(Array.concat(echoProgram, [OpEchoToResidue, OpEchoOutput, OpHalt])) |
| 59 | + assertEqual("echo_output survives erasure", out, Ok(VString("a"))) |
| 60 | + |
| 61 | + // residue_strictly_loses reports non-recoverability for a residue, not for an echo. |
| 62 | + let (lossR, _) = runChunk(Array.concat(echoProgram, [OpEchoToResidue, OpResidueStrictlyLoses, OpHalt])) |
| 63 | + assertEqual("residue_strictly_loses(residue) = true", lossR, Ok(VBool(true))) |
| 64 | + let (lossE, _) = runChunk(Array.concat(echoProgram, [OpResidueStrictlyLoses, OpHalt])) |
| 65 | + assertEqual("residue_strictly_loses(echo) = false", lossE, Ok(VBool(false))) |
| 66 | +} |
| 67 | + |
| 68 | +let testWitnessActuallyGone = () => { |
| 69 | + suite("Echo runtime: witness is genuinely unavailable after erasure") |
| 70 | + // echo_input on a residue must be a runtime error, not silently nil. |
| 71 | + let (r, _) = runChunk(Array.concat(echoProgram, [OpEchoToResidue, OpEchoInput, OpHalt])) |
| 72 | + switch r { |
| 73 | + | Error(_) => assertTrue("echo_input on residue fails at runtime", true) |
| 74 | + | Ok(_) => assertTrue("echo_input on residue fails at runtime", false) |
| 75 | + } |
| 76 | +} |
| 77 | + |
| 78 | +let testStabilityDebitedExactlyOnce = () => { |
| 79 | + suite("Echo runtime: stability debit is visible and charged exactly once") |
| 80 | + // No erasure → no debit. |
| 81 | + let (_, sPlain) = runChunk(Array.concat(echoProgram, [OpEchoOutput, OpHalt])) |
| 82 | + assertEqual("projection alone does not debit stability", sPlain, 100.0) |
| 83 | + |
| 84 | + // One erasure → exactly one debit (echoEraseCost = 15.0). |
| 85 | + let (_, sErase) = runChunk(Array.concat(echoProgram, [OpEchoToResidue, OpHalt])) |
| 86 | + assertEqual("echo_to_residue debits stability once", sErase, 100.0 -. VM.echoEraseCost) |
| 87 | + |
| 88 | + // Erasure then projection → still exactly one debit (projection is free). |
| 89 | + let (_, sEraseThenProj) = runChunk(Array.concat(echoProgram, [OpEchoToResidue, OpEchoOutput, OpHalt])) |
| 90 | + assertEqual("projection after erasure adds no further debit", sEraseThenProj, 100.0 -. VM.echoEraseCost) |
| 91 | +} |
| 92 | + |
| 93 | +let runAll = () => { |
| 94 | + Console.log("\n========================================") |
| 95 | + Console.log(" ERROR-LANG ECHO RUNTIME TESTS") |
| 96 | + Console.log("========================================") |
| 97 | + testEchoConstructsWitness() |
| 98 | + testProjections() |
| 99 | + testToResidue() |
| 100 | + testWitnessActuallyGone() |
| 101 | + testStabilityDebitedExactlyOnce() |
| 102 | + summarize() |
| 103 | +} |
| 104 | + |
| 105 | +let _ = runAll() |
0 commit comments