|
| 1 | +# SPDX-License-Identifier: PMPL-1.0-or-later |
| 2 | +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> |
| 3 | +# |
| 4 | +# Phronesis — Property-Based (P2P) Tests |
| 5 | +# |
| 6 | +# Uses StreamData to generate inputs and verify invariants that must |
| 7 | +# hold across all possible inputs, not just the specific cases in unit tests. |
| 8 | +# |
| 9 | +# Properties tested: |
| 10 | +# 1. Lexer panic-freedom on arbitrary printable strings |
| 11 | +# 2. Lexer always returns a tagged tuple {:ok, _} or {:error, _} |
| 12 | +# 3. Compiler output type consistency: always returns {:ok, bytecode} or {:error, _} |
| 13 | +# 4. Integer constants compile to bytecode with non-empty instructions |
| 14 | +# 5. Determinism: same source always produces the same compiler result |
| 15 | + |
| 16 | +defmodule Phronesis.PropertyTest do |
| 17 | + use ExUnit.Case |
| 18 | + use ExUnitProperties |
| 19 | + |
| 20 | + alias Phronesis.Lexer |
| 21 | + alias Phronesis.Compiler |
| 22 | + |
| 23 | + # ==================================================================== |
| 24 | + # P2P Property 1: Lexer never crashes on arbitrary printable strings |
| 25 | + # ==================================================================== |
| 26 | + |
| 27 | + @doc """ |
| 28 | + The lexer must not raise an exception on any printable ASCII string. |
| 29 | + It must return a tagged tuple — either {:ok, tokens} or {:error, _}. |
| 30 | + A crash or bare exception is always a bug. |
| 31 | + """ |
| 32 | + property "lexer does not crash on arbitrary printable strings" do |
| 33 | + check all(s <- string(:printable)) do |
| 34 | + result = Lexer.tokenize(s) |
| 35 | + assert match?({:ok, _}, result) or match?({:error, _}, result), |
| 36 | + "Lexer returned unexpected value for input #{inspect(s)}: #{inspect(result)}" |
| 37 | + end |
| 38 | + end |
| 39 | + |
| 40 | + # ==================================================================== |
| 41 | + # P2P Property 2: Lexer result is always a tagged tuple |
| 42 | + # ==================================================================== |
| 43 | + |
| 44 | + @doc """ |
| 45 | + For any alphanumeric string, the lexer must return exactly a 2-tuple |
| 46 | + whose first element is :ok or :error. No other return shapes are valid. |
| 47 | + """ |
| 48 | + property "lexer always returns a tagged tuple" do |
| 49 | + check all(s <- string(:alphanumeric)) do |
| 50 | + result = Lexer.tokenize(s) |
| 51 | + assert is_tuple(result) and tuple_size(result) >= 2, |
| 52 | + "Expected a tuple, got: #{inspect(result)}" |
| 53 | + assert elem(result, 0) in [:ok, :error], |
| 54 | + "Expected :ok or :error as first element, got: #{inspect(elem(result, 0))}" |
| 55 | + end |
| 56 | + end |
| 57 | + |
| 58 | + # ==================================================================== |
| 59 | + # P2P Property 3: Compiler output is always a tagged tuple |
| 60 | + # ==================================================================== |
| 61 | + |
| 62 | + @doc """ |
| 63 | + The compiler must return {:ok, bytecode} or {:error, reason} for any |
| 64 | + string input. The shape of the return must not depend on the specific |
| 65 | + content — only on whether it is valid Phronesis syntax. |
| 66 | + """ |
| 67 | + property "compiler always returns a tagged tuple" do |
| 68 | + check all(s <- string(:printable, max_length: 200)) do |
| 69 | + result = Compiler.compile(s) |
| 70 | + assert is_tuple(result) and tuple_size(result) == 2, |
| 71 | + "Compiler must return a 2-tuple, got: #{inspect(result)}" |
| 72 | + assert elem(result, 0) in [:ok, :error], |
| 73 | + "Compiler first element must be :ok or :error, got: #{inspect(elem(result, 0))}" |
| 74 | + end |
| 75 | + end |
| 76 | + |
| 77 | + # ==================================================================== |
| 78 | + # P2P Property 4: Integer constants always produce non-empty bytecode |
| 79 | + # ==================================================================== |
| 80 | + |
| 81 | + @doc """ |
| 82 | + Any valid integer constant declaration must compile to bytecode with |
| 83 | + at least one instruction. A constant with no instructions is a |
| 84 | + compiler bug: there must always be at least a LOAD or STORE instruction. |
| 85 | + """ |
| 86 | + property "valid integer constants always compile to non-empty instruction list" do |
| 87 | + check all(n <- integer()) do |
| 88 | + source = "CONST x = #{n}" |
| 89 | + case Compiler.compile(source) do |
| 90 | + {:ok, bytecode} -> |
| 91 | + assert is_list(bytecode.instructions), |
| 92 | + "bytecode.instructions must be a list" |
| 93 | + assert length(bytecode.instructions) > 0, |
| 94 | + "Compiling 'CONST x = #{n}' produced empty instruction list" |
| 95 | + {:error, _} -> |
| 96 | + # Compile errors are acceptable — only assert the shape |
| 97 | + :ok |
| 98 | + end |
| 99 | + end |
| 100 | + end |
| 101 | + |
| 102 | + # ==================================================================== |
| 103 | + # P2P Property 5: Compiler determinism |
| 104 | + # ==================================================================== |
| 105 | + |
| 106 | + @doc """ |
| 107 | + Compiling the same source twice must produce structurally identical |
| 108 | + bytecode. This guards against hidden mutable state in the compiler |
| 109 | + (e.g. global counters, non-deterministic map iteration). |
| 110 | + """ |
| 111 | + property "compiler is deterministic for the same source" do |
| 112 | + check all(n <- integer(-1_000_000..1_000_000)) do |
| 113 | + source = "CONST deterministic_value = #{n}" |
| 114 | + result_a = Compiler.compile(source) |
| 115 | + result_b = Compiler.compile(source) |
| 116 | + |
| 117 | + case {result_a, result_b} do |
| 118 | + {{:ok, bc_a}, {:ok, bc_b}} -> |
| 119 | + assert length(bc_a.instructions) == length(bc_b.instructions), |
| 120 | + "Non-deterministic instruction count for source: #{source}" |
| 121 | + assert map_size(bc_a.constants) == map_size(bc_b.constants), |
| 122 | + "Non-deterministic constant count for source: #{source}" |
| 123 | + {{:error, _}, {:error, _}} -> |
| 124 | + # Both fail consistently — determinism preserved |
| 125 | + :ok |
| 126 | + _ -> |
| 127 | + flunk("Non-deterministic result (one ok, one error) for source: #{source}") |
| 128 | + end |
| 129 | + end |
| 130 | + end |
| 131 | +end |
0 commit comments