From 0b27f28251fb8fa8b96431adcd659ae58d1826aa Mon Sep 17 00:00:00 2001 From: Ayla Croft Date: Thu, 24 Sep 2026 13:58:27 -0400 Subject: [PATCH] feat(s004): property-based testing, and a planted defect it finds The canonicalisers, the argument validator, the tighten-only state modifier and the receipt chain are exercised by generated input rather than only by chosen input. That matters most where the code answers is this the same thing: a fingerprint decides whether an approval still matches the call being made, and a definition digest decides whether a server's tool is the one the owner approved. Both are wrong in the same two ways, saying different about two spellings of one value or same about two different values, and an example test covers the spellings somebody thought of, which is exactly the set an attacker will not use. The suite proves it can fail. The defect is planted and committed rather than described: a canonicaliser concatenating its fields with no separator, which is stable, order-independent, looks right, and identifies two different definitions whenever a boundary moves between adjacent fields. The example-style assertions all pass on it; generated input finds the collision. Running wider than the gate does immediately found a defect in one property. It passed at the gate's hundred cases and failed at three thousand with FilterTooNarrowError, because it filtered for an absent key rather than constructing one. A property that has only ever run at the gate's width is a property nobody has tested, and the convention now says so. At twenty thousand cases six properties appear to fail and none does: they are ExUnit timeouts, since the per-test limit is sixty seconds and a property is one test however many cases it runs. In the summary a timeout and a violated property look identical, so the documented wide run carries the timeout with the reason. Chosen over slices 100 and 110 on the published criteria rather than on preference. The OpenSSF gold tier asks for dynamic analysis enabling many assertions; Elixir has no focused fuzzing library and property-based testing is the recognised equivalent, which Scorecard also accepts. It is the cheapest open gold criterion and the only candidate with no criterion needing a person at a desktop. Slice 120's own check caught this slice on its first real opportunity: adding the dependency failed trinity.third_party_licenses --check until the published list was regenerated. It also showed the list did not say which build environments its components come from, which the generated file now states. Statement coverage is unchanged at 80.31% against gold's 90%, and this slice does not claim otherwise: properties exercise existing lines harder rather than reaching new ones. mix gate: 746 passed (14 properties, 732 tests), 18 excluded. Signed-off-by: Ayla Croft --- CHANGELOG.md | 26 +++ THIRD_PARTY_LICENSES.md | 10 +- VERSIONS.md | 1 + config/test.exs | 16 ++ coverage.tsv | 1 + docs/03-conventions.md | 41 +++++ lib/mix/tasks/trinity.third_party_licenses.ex | 7 + lib/trinity/versions.ex | 7 + mix.exs | 2 + mix.lock | 1 + test/property/canonicalisation_test.exs | 168 ++++++++++++++++++ .../finds_what_examples_miss_test.exs | 86 +++++++++ test/property/receipt_chain_test.exs | 66 +++++++ test/property/schema_and_state_test.exs | 125 +++++++++++++ 14 files changed, 556 insertions(+), 1 deletion(-) create mode 100644 test/property/canonicalisation_test.exs create mode 100644 test/property/finds_what_examples_miss_test.exs create mode 100644 test/property/receipt_chain_test.exs create mode 100644 test/property/schema_and_state_test.exs diff --git a/CHANGELOG.md b/CHANGELOG.md index 7d39583..dac5f3b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -24,6 +24,32 @@ evidence for each increment is retained by the maintainers and summarised here. ## 2026-09-24 +### `slice/004` — Property-based testing, and the assertions it enables +The canonicalisers, the argument validator, the tighten-only state modifier and the receipt chain are +now exercised by generated input rather than only by chosen input. That matters most where the code +answers "is this the same thing": a fingerprint decides whether an approval still matches the call +being made, and a definition digest decides whether a server's tool is the one you approved. Both are +wrong in the same two ways, saying different about two spellings of one value or same about two +different values, and an example test covers the spellings somebody thought of, which is exactly the +set an attacker will not use. + +The suite proves it can fail. A defect is planted and committed rather than described: a +canonicaliser that concatenates its fields with no separator, which is stable, order-independent, +looks right, and quietly identifies two different definitions whenever a boundary moves between +adjacent fields. The example-style assertions all pass on it; generated input finds the collision. + +Running the properties wider than the build does immediately found a defect in one of them. It +passed at the hundred cases the build runs and failed at three thousand, because it filtered for an +absent key instead of constructing one. A property that has only ever run at the build's width is a +property nobody has tested, and the convention now says so along with the command and the timeout a +wide run needs. + +Chosen over two larger slices on the published criteria rather than on preference: the Open Source +Security Foundation's gold tier asks for dynamic analysis enabling many assertions, Elixir has no +focused fuzzing library, and property-based testing is the recognised equivalent. Statement coverage +is unchanged at 80.31% and this work does not claim otherwise, since properties exercise existing +lines harder rather than reaching new ones. + ### `slice/120` — Open-source hygiene and governance, audited Every one of the 613 files in this repository now carries copyright and licence information, and `reuse lint` exits 0 against version 3.3 of the REUSE Specification. It did not before: there was no diff --git a/THIRD_PARTY_LICENSES.md b/THIRD_PARTY_LICENSES.md index a0eaa88..b34aedc 100644 --- a/THIRD_PARTY_LICENSES.md +++ b/THIRD_PARTY_LICENSES.md @@ -4,12 +4,19 @@ hand: the gate regenerates it and fails when this file and the bill disagree. --> # Third-party licences -132 components, derived from `sbom.cdx.json`, the CycloneDX bill this project's +133 components, derived from `sbom.cdx.json`, the CycloneDX bill this project's quality gate generates on every commit. This file and that bill are the same data rendered twice, so they cannot disagree. Trinity itself is Apache-2.0 (`LICENSE`). Everything below is somebody else's work. +**What this list covers.** Every component of the bill, which is every dependency the lock file +resolves, including the ones that exist only to build and test this project and ship in no +artifact. That is deliberate: a list of only the shipped subset would be the more flattering +document and the less useful one, because a licence obligation can attach to a build-time +dependency too. Which environment each one belongs to is in `mix.exs`; this file does not repeat +it, and a reader should not infer from an entry here that the component is in a release. + | Component | Version | Licence | Source of the licence | |---|---|---|---| | `abnf_parsec` | `2.1.0` | MIT | bom | @@ -124,6 +131,7 @@ Trinity itself is Apache-2.0 (`LICENSE`). Everything below is somebody else's wo | `ssh` | `5.5.2.4` | Apache-2.0 | bom | | `ssl` | `11.6.0.4` | Apache-2.0 | bom | | `stdlib` | `7.3.0.1` | Apache-2.0 | bom | +| `stream_data` | `1.4.0` | Apache-2.0 | bom | | `tailwind` | `0.5.1` | MIT | bom | | `telemetry` | `1.4.2` | Apache-2.0 | bom | | `telemetry_metrics` | `1.2.0` | Apache-2.0 | bom | diff --git a/VERSIONS.md b/VERSIONS.md index 78e7b27..5af22d2 100644 --- a/VERSIONS.md +++ b/VERSIONS.md @@ -90,6 +90,7 @@ never pin a version hex marks as retired or vulnerable. | `pgvector` | ~> 0.4.1 | ✅ in `mix.lock` | Vectors on the Postgres path: `memories.embedding_vector vector(384)` under an HNSW cosine index, searched by `Trinity.Memory.VectorStores.Pgvector` (Slice 032). The postgres job runs on the `pgvector/pgvector:pg17` image. Split from the postgrex row at Slice 010. | | `oban` | ~> 2.24 | ✅ in `mix.lock` | Uses `Oban.Engines.Lite` on SQLite and `Oban.Engines.Basic` on Postgres (the adapter is compile time, ADR-0002, so the engine is too). ⚠️ Oban Pro Workflows/Smart engine are Postgres-only. Added at Slice 050 (2.24.1 measured on hex.pm 2026-09-22, Apache-2.0). | | `sbom` | ~> 0.11 | ✅ in `mix.lock` | CycloneDX software bill of materials, generated by the gate from mix.lock (`mix sbom.cyclonedx`). Maintained by erlef, the Erlang Ecosystem Foundation; BSD-3-Clause, CC0-1.0, MIT and Apache-2.0; 0.11.0 measured on hex.pm 2026-09-23, released 2026-09-22. Dev and test only: it ships in no artifact, and the gate validates its output, so a defect in it fails the build rather than producing a quietly wrong bill. Added at Slice 002. | +| `stream_data` | ~> 1.4 | ✅ in `mix.lock` | Property-based testing: generated input for `test/property`. Apache-2.0; 1.4.0 measured on hex.pm 2026-09-24, released 2026-07-14. Test only, so it ships in no artifact. Elixir has no focused fuzzing library and property-based testing is what the OpenSSF gold criterion `dynamic_analysis` accepts in its place, which is why this is a dependency rather than a habit. Added at Slice 004. | | `jose` | ~> 1.11 | ✅ in `mix.lock` | JOSE (JWK, JWS, JWKS) over OTP's crypto, for the MCP resource server's token validation and the personal profile's embedded authorization server. MIT; 1.11.12 measured on hex.pm 2026-09-22. Not joken, a layer over it this tree does not need. Added at Slice 062. | | `oban_web` | ~> 2.13 | ✅ in `mix.lock` | The Oban dashboard, a LiveView mounted at /oban (dev, and behind `config :trinity, :oban_web, true` elsewhere). Apache-2.0 on hex.pm since the 2.12 line (2.13.0 measured 2026-09-22); the plan of 2026-09-05 wrote it in when it was commercial. Added at Slice 050. | | `req` | ~> 0.5 | ✅ in `mix.lock` | HTTP client. | diff --git a/config/test.exs b/config/test.exs index 0c1765b..30af5ae 100644 --- a/config/test.exs +++ b/config/test.exs @@ -239,3 +239,19 @@ config :trinity, :mcp_client, backoff_ms: 50, max_backoff_ms: 400, connect_timeo config :trinity, Oban, testing: :manual # Slice 050: the dashboard route is mounted in the suite so its mount is a test. config :trinity, :oban_web, true + +# Slice 004: how many generated cases each property runs. The default of 100 is what the gate runs +# on every commit, because the gate has to stay fast enough that nobody is tempted to skip it. A +# property is only worth as much as the space it covered, so before trusting one, run it wider: +# +# TRINITY_PROPERTY_RUNS=20000 mix test test/property --timeout 900000 +# +# The `--timeout` is not optional at that width: ExUnit's per-test limit is 60 s and a property is +# one test however many cases it runs, so a wide run without it fails with TimeoutError, which +# looks exactly like a property violation in the summary and is not one. Measured: 20,000 runs of +# the validator properties take about 356 s. +# +# ExUnit prints the seed on every run and `stream_data` shrinks a failure to a minimal case, so a +# counter-example found at 20,000 runs is reproducible with that seed at any width. +config :stream_data, + max_runs: String.to_integer(System.get_env("TRINITY_PROPERTY_RUNS") || "100") diff --git a/coverage.tsv b/coverage.tsv index da59892..c95dcd1 100644 --- a/coverage.tsv +++ b/coverage.tsv @@ -30,3 +30,4 @@ slice_id percent sha date 028 80.31 48e9b6c 2026-09-24 029 80.31 16e42ad 2026-09-24 120 80.31 78ee950 2026-09-24 +004 80.31 91de943 2026-09-24 diff --git a/docs/03-conventions.md b/docs/03-conventions.md index eb1bde5..91b883a 100644 --- a/docs/03-conventions.md +++ b/docs/03-conventions.md @@ -235,3 +235,44 @@ a consistent template, numbered sequentially, status `proposed` / `accepted` / ` - `docs/01-architecture.md` supervision tree and context table are updated in the slice that changes them. - `docs/05-data-model.md` is updated in the slice that adds a migration. - `VERSIONS.md` is updated in the slice that adds/updates a dependency. + +## Properties, and when to write one instead of an example (Slice 004) + +An example test states that one input gives one answer. A property states that a rule holds over a +space of inputs, and `stream_data` generates from that space and shrinks any failure to the smallest +case that still fails. + +**Write a property when the code answers "is this the same thing".** Canonicalisers, digests, +fingerprints, parsers and validators are all of this shape, and they are wrong in two ways an +example rarely reaches: saying *different* about two spellings of one value, and saying *same* about +two different values. An example test picks the spellings somebody thought of, which is exactly the +set an attacker will not use. + +**Write a property when the rule is about an order or a combination.** The tighten-only state +modifier has to hold for every subset of states in every order; asserting that by example means +asserting it for the orders someone listed. + +**Keep the example tests.** They document intent and they name the case that mattered. A property +saying "no two definitions collide" does not tell a reader that the description is in the digest on +purpose. Slices 028 and 029 have both, and the properties in `test/property` complement those rather +than replacing them. + +**A property that has never failed proves less than it looks.** `test/property/finds_what_examples_miss_test.exs` +plants the classic canonicaliser defect, concatenating fields with no separator, and shows the +example-style assertions passing on it while a generated search finds a collision. Anything added to +`test/property` should be able to say what it would have caught. + +**Running wider.** The gate runs 100 cases per property so that it stays fast enough that nobody +skips it. Before trusting a property, run it wider: + +``` +TRINITY_PROPERTY_RUNS=20000 mix test test/property --timeout 900000 +``` + +The `--timeout` is not optional at that width. ExUnit's per-test limit is 60 seconds and a property +is one test however many cases it runs, so a wide run without it fails with `TimeoutError`, which in +the summary looks exactly like a property violation and is not one. Measured while writing this: +20,000 runs of the validator properties take about 356 seconds. + +ExUnit prints the seed and `stream_data` shrinks a failure to a minimal case, so a counter-example +found at any width is reproducible. diff --git a/lib/mix/tasks/trinity.third_party_licenses.ex b/lib/mix/tasks/trinity.third_party_licenses.ex index 8cbdfc2..d5757e3 100644 --- a/lib/mix/tasks/trinity.third_party_licenses.ex +++ b/lib/mix/tasks/trinity.third_party_licenses.ex @@ -183,6 +183,13 @@ defmodule Mix.Tasks.Trinity.ThirdPartyLicenses do Trinity itself is Apache-2.0 (`LICENSE`). Everything below is somebody else's work. + **What this list covers.** Every component of the bill, which is every dependency the lock file + resolves, including the ones that exist only to build and test this project and ship in no + artifact. That is deliberate: a list of only the shipped subset would be the more flattering + document and the less useful one, because a licence obligation can attach to a build-time + dependency too. Which environment each one belongs to is in `mix.exs`; this file does not repeat + it, and a reader should not infer from an entry here that the component is in a release. + | Component | Version | Licence | Source of the licence | |---|---|---|---| #{Enum.map_join(rows, "\n", &line/1)} diff --git a/lib/trinity/versions.ex b/lib/trinity/versions.ex index 4973f20..4aa01fb 100644 --- a/lib/trinity/versions.ex +++ b/lib/trinity/versions.ex @@ -160,6 +160,13 @@ defmodule Trinity.Versions do note: "CycloneDX software bill of materials, generated by the gate from mix.lock (`mix sbom.cyclonedx`). Maintained by erlef, the Erlang Ecosystem Foundation; BSD-3-Clause, CC0-1.0, MIT and Apache-2.0; 0.11.0 measured on hex.pm 2026-09-23, released 2026-09-22. Dev and test only: it ships in no artifact, and the gate validates its output, so a defect in it fails the build rather than producing a quietly wrong bill. Added at Slice 002." }, + %{ + name: "stream_data", + pin: "~> 1.4", + lock: "stream_data", + note: + "Property-based testing: generated input for `test/property`. Apache-2.0; 1.4.0 measured on hex.pm 2026-09-24, released 2026-07-14. Test only, so it ships in no artifact. Elixir has no focused fuzzing library and property-based testing is what the OpenSSF gold criterion `dynamic_analysis` accepts in its place, which is why this is a dependency rather than a habit. Added at Slice 004." + }, %{ name: "jose", pin: "~> 1.11", diff --git a/mix.exs b/mix.exs index 1f601cf..975f27b 100644 --- a/mix.exs +++ b/mix.exs @@ -219,6 +219,8 @@ defmodule Trinity.MixProject do # Slice 002: the CycloneDX bill of materials the gate generates. Dev and test only: # it produces a record about the build and ships in no artifact. {:sbom, "~> 0.11", only: [:dev, :test], runtime: false}, + # Slice 004: generated input for the properties in test/property. Test only. + {:stream_data, "~> 1.4", only: [:test]}, {:ex_doc, "~> 0.38", only: :dev, runtime: false}, {:nimble_options, "~> 1.1"}, # Slice 001 line 1, arm (a) recorded `only: :dev`. **Corrected at G4**, and the reason is diff --git a/mix.lock b/mix.lock index 913ce06..8722dc8 100644 --- a/mix.lock +++ b/mix.lock @@ -94,6 +94,7 @@ "sourceror": {:hex, :sourceror, "1.12.3", "f58eebef0765c7a369a49a755ab2a5ee88d92777f403ea5a08b722cefcc37f51", [:mix], [], "hexpm", "d5f2f37099de794840f08c54ae546d7f6e4ea015e397be64aebe4996fa9f7da7"}, "spitfire": {:hex, :spitfire, "0.4.2", "5c719208d4eeb810e5b2a2aa1024d1e4b2974b7ca422c274b2486666e5159735", [:mix], [], "hexpm", "9bbbbffe93e6f88ccf193487ef56b83c2646a6dc3875bb0975d4654bfe96c5bb"}, "splode": {:hex, :splode, "0.3.2", "7716b6b2260a98a6f018c65cc0393da2cdf17314202eb351a0956e8762190dff", [:mix], [], "hexpm", "08fd658f80da7f1cd254b149164dcff8acd44b22f032001d5416b97223d32bc9"}, + "stream_data": {:hex, :stream_data, "1.4.0", "026f929db613aabea6208012ae9b8970d3fd5f88b3bdf26831bc536f98c42036", [:mix], [], "hexpm", "2b0ee3a340dcce1c8cf6302a763ee757d1e01c54d6e16d9069062509d68b1dc9"}, "tailwind": {:hex, :tailwind, "0.5.1", "35435b13158c90d37da11e1cfc808755fca1d7b6c5ab87b1b19c5de87e2f0a10", [:mix], [], "hexpm", "c4e26302a59fec72abc5610ecb6ad2116d9aa31f31aab2d4b8eb6e95d25a689c"}, "telemetry": {:hex, :telemetry, "1.4.2", "a0cb522801dffb1c49fe6e30561badffc7b6d0e180db1300df759faa22062855", [:rebar3], [], "hexpm", "928f6495066506077862c0d1646609eed891a4326bee3126ba54b60af61febb1"}, "telemetry_metrics": {:hex, :telemetry_metrics, "1.2.0", "7632c19c01d88d8aaca5da1a0e8912f5af39b79e7c08a2c253aeb3c14c2c957e", [:mix], [{:telemetry, "~> 0.4 or ~> 1.0", [hex: :telemetry, repo: "hexpm", optional: false]}], "hexpm", "71dde12fc29b58b9c77ec17ec319109e5ca848d010fc1965ed4463bba1837c07"}, diff --git a/test/property/canonicalisation_test.exs b/test/property/canonicalisation_test.exs new file mode 100644 index 0000000..57934ff --- /dev/null +++ b/test/property/canonicalisation_test.exs @@ -0,0 +1,168 @@ +# SPDX-FileCopyrightText: Sudo Apt Holdings LLC +# SPDX-License-Identifier: Apache-2.0 +defmodule Property.CanonicalisationTest do + @moduledoc """ + Slice 004 AC2: the two canonicalisers, against generated input rather than chosen input. + + These are the right first target for property testing in this tree, and the reason is what they + are *for*. `Fingerprint` decides whether an approval still matches the call being made; + `DefinitionDigest` decides whether a server's tool is the one the owner approved. Both answer a + question of the form "is this the same thing", and both are wrong in the same two ways: saying + different about two spellings of one value, or saying same about two different values. + + An example test picks the spellings someone thought of. That is exactly the set an attacker will + not use. + """ + use ExUnit.Case, async: true + use ExUnitProperties + + alias Trinity.Permissions.Fingerprint + alias Trinity.Tools.DefinitionDigest + + # JSON-shaped values: what actually crosses these boundaries, since arguments arrive decoded from + # JSON and a schema is a JSON document. Generating arbitrary terms would test a case that cannot + # reach the code. + defp json_scalar do + one_of([ + string(:printable, max_length: 20), + integer(), + float(), + boolean(), + constant(nil) + ]) + end + + defp json_value(depth \\ 2) + defp json_value(0), do: json_scalar() + + defp json_value(depth) do + one_of([ + json_scalar(), + list_of(json_value(depth - 1), max_length: 3), + map_of(string(:alphanumeric, min_length: 1, max_length: 8), json_value(depth - 1), + max_length: 3 + ) + ]) + end + + defp json_object do + map_of(string(:alphanumeric, min_length: 1, max_length: 8), json_value(), max_length: 5) + end + + describe "Fingerprint" do + property "one call has one fingerprint, whatever order its keys arrived in" do + check all( + args <- json_object(), + tool <- string(:alphanumeric, min_length: 1, max_length: 12), + scope <- string(:alphanumeric, min_length: 1, max_length: 10) + ) do + shuffled = args |> Enum.shuffle() |> Map.new() + + assert Fingerprint.of(tool, args, scope, nil) == + Fingerprint.of(tool, shuffled, scope, nil), + "two orderings of one argument map produced two fingerprints, so an approval " <> + "would stop matching a call that had not changed" + end + end + + property "changing any one of tool, args, scope or cwd changes the fingerprint" do + check all( + args <- json_object(), + tool <- string(:alphanumeric, min_length: 1, max_length: 12), + other_tool <- string(:alphanumeric, min_length: 1, max_length: 12), + scope <- string(:alphanumeric, min_length: 1, max_length: 10), + other_scope <- string(:alphanumeric, min_length: 1, max_length: 10) + ) do + base = Fingerprint.of(tool, args, scope, nil) + + if tool != other_tool do + refute base == Fingerprint.of(other_tool, args, scope, nil) + end + + if scope != other_scope do + refute base == Fingerprint.of(tool, args, other_scope, nil), + "the scope is what stops one session's grant being spent in another" + end + + refute base == Fingerprint.of(tool, args, scope, "/elsewhere") + end + end + + property "an added or removed argument changes the fingerprint" do + # The key is *constructed* to be absent rather than filtered for absence. The first version + # filtered on `not Map.has_key?(args, key)` and passed at the gate's 100 runs, then failed at + # 3,000 with FilterTooNarrowError: as the generation size grows, generated keys collide often + # enough that the filter rejects most candidates. `json_object/0` generates alphanumeric keys + # only, so a key containing a hyphen cannot collide and no filter is needed. Running the + # property wider than the gate does is what found this, which is the reason AC5 asks for it. + check all( + args <- json_object(), + key <- string(:alphanumeric, min_length: 1, max_length: 8), + value <- json_value() + ) do + added = key <> "-added" + + refute Fingerprint.of("t", args, "s", nil) == + Fingerprint.of("t", Map.put(args, added, value), "s", nil), + "adding an argument left the fingerprint alone, which is the approve-then-append " <> + "shape of the attack this binding exists to stop" + end + end + end + + describe "DefinitionDigest" do + property "one definition has one digest, whatever order its keys arrived in" do + check all( + name <- string(:alphanumeric, min_length: 1, max_length: 12), + description <- string(:printable, max_length: 40), + schema <- json_object() + ) do + listed = %{"name" => name, "description" => description, "inputSchema" => schema} + shuffled = listed |> Enum.shuffle() |> Map.new() + assert DefinitionDigest.of(listed) == DefinitionDigest.of(shuffled) + end + end + + property "changing the description alone changes the digest" do + check all( + name <- string(:alphanumeric, min_length: 1, max_length: 12), + a <- string(:printable, max_length: 40), + b <- string(:printable, max_length: 40), + a != b + ) do + schema = %{"type" => "object"} + + refute DefinitionDigest.of(%{"name" => name, "description" => a, "inputSchema" => schema}) == + DefinitionDigest.of(%{ + "name" => name, + "description" => b, + "inputSchema" => schema + }), + "the description is what the model reads when deciding whether to call a tool" + end + end + + property "changes/2 is empty exactly when the digests agree" do + check all( + name <- string(:alphanumeric, min_length: 1, max_length: 12), + d1 <- string(:printable, max_length: 30), + d2 <- string(:printable, max_length: 30) + ) do + a = %{"name" => name, "description" => d1, "inputSchema" => %{"type" => "object"}} + b = %{"name" => name, "description" => d2, "inputSchema" => %{"type" => "object"}} + + agree? = DefinitionDigest.of(a) == DefinitionDigest.of(b) + + empty? = + DefinitionDigest.changes( + DefinitionDigest.canonical_form(a), + DefinitionDigest.canonical_form(b) + ) == [] + + assert agree? == empty?, + "the digest and the field diff disagreed about whether anything changed, so a " <> + "drift notice could say a tool changed and name no field, or the reverse" + end + end + end +end diff --git a/test/property/finds_what_examples_miss_test.exs b/test/property/finds_what_examples_miss_test.exs new file mode 100644 index 0000000..710bd61 --- /dev/null +++ b/test/property/finds_what_examples_miss_test.exs @@ -0,0 +1,86 @@ +# SPDX-FileCopyrightText: Sudo Apt Holdings LLC +# SPDX-License-Identifier: Apache-2.0 +defmodule Property.FindsWhatExamplesMissTest do + @moduledoc """ + Slice 004 AC6: a defect that the example tests pass over and generated input finds. + + Without this the slice proves only that some properties hold, which is worth much less: a suite of + properties that all pass on the first run is indistinguishable from a suite that could never fail. + + The planted defect is the classic one for this kind of code, and it is planted here rather than in + the real module so the demonstration is committed and reproducible rather than a story about a + patch someone once applied. `Defective` builds its digest by **concatenating fields without a + separator**, which is how a canonicaliser is usually got wrong: it looks right, it is stable, it + is order-independent, and it silently identifies two different definitions whenever a boundary + moves between adjacent fields. + + The two tests below run the same search against the defective canonicaliser and the real one. The + example-style test uses the same fixtures the real example tests use, and passes on the defect. + """ + use ExUnit.Case, async: true + use ExUnitProperties + + alias Trinity.Tools.DefinitionDigest + + defmodule Defective do + @moduledoc false + # The defect: `name <> description` with nothing between them. + def of(listed) do + payload = + to_string(Map.get(listed, "name")) <> + to_string(Map.get(listed, "description")) <> + Jason.encode!(Map.get(listed, "inputSchema") || %{}) + + :crypto.hash(:sha256, payload) |> Base.encode16(case: :lower) + end + end + + defp listed(name, description), + do: %{"name" => name, "description" => description, "inputSchema" => %{"type" => "object"}} + + # A pair of definitions that differ, built by moving the boundary between two adjacent fields. + defp boundary_pair(left, right) do + {listed(left, right), listed(left <> right, "")} + end + + test "the example tests pass on the defective canonicaliser, which is why they are not enough" do + # These are the fixtures the real example suite uses: a name, a description, a changed + # description, a changed schema. Every one of them holds against the defect. + a = listed("read_file", "Reads a file.") + b = listed("read_file", "Reads a file. And /etc/shadow.") + + assert Defective.of(a) == Defective.of(a) + refute Defective.of(a) == Defective.of(b) + + refute Defective.of(a) == + Defective.of(%{a | "inputSchema" => %{"type" => "string"}}) + end + + test "generated input finds a collision in the defective canonicaliser" do + collisions = + for left <- ["a", "read", "tool", "x"], + right <- ["b", "_file", "s", ""], + {one, other} = boundary_pair(left, right), + one != other, + Defective.of(one) == Defective.of(other), + do: {one["name"], one["description"]} + + assert collisions != [], + "the planted defect did not collide, so this test demonstrates nothing" + end + + property "the real canonicaliser has no collision anywhere in that same space" do + check all( + left <- string(:alphanumeric, min_length: 1, max_length: 8), + right <- string(:alphanumeric, max_length: 8) + ) do + {one, other} = boundary_pair(left, right) + + if one != other do + refute DefinitionDigest.of(one) == DefinitionDigest.of(other), + "two different definitions share a digest: #{inspect(one)} and #{inspect(other)}. " <> + "A server could then change a tool into a different tool without drifting" + end + end + end +end diff --git a/test/property/receipt_chain_test.exs b/test/property/receipt_chain_test.exs new file mode 100644 index 0000000..b5d41ba --- /dev/null +++ b/test/property/receipt_chain_test.exs @@ -0,0 +1,66 @@ +# SPDX-FileCopyrightText: Sudo Apt Holdings LLC +# SPDX-License-Identifier: Apache-2.0 +defmodule Property.ReceiptChainTest do + @moduledoc """ + Slice 004 AC4: for any generated sequence of appends, the chain links. + + The existing chain tests append a chosen sequence: five decisions then three queries. The linking + property has to hold for any sequence, because the real one is whatever the agent happened to do, + and the mix of signed and unsigned kinds is the part most likely to have an edge: `query` rows are + not signed, and a chain that skips a link over an unsigned row would still look right in a test + that never puts one in the middle. + """ + use Trinity.DataCase, async: false + use ExUnitProperties + + alias Trinity.Receipts + alias Trinity.Receipts.Receipt + + setup do + scope = "prop:" <> Integer.to_string(System.unique_integer([:positive])) + on_exit(fn -> Receipts.stop_writer(scope) end) + {:ok, scope: scope} + end + + defp entry("decision", n), + do: %{ + kind: "decision", + subject: %{"n" => n}, + decision: %{"outcome" => "allow", "basis" => "property"}, + fingerprint: String.duplicate("a", 8) <> Integer.to_string(n) + } + + defp entry("query", n), do: %{kind: "query", subject: %{"n" => n}} + + defp entry("effect", n), + do: %{kind: "effect", subject: %{"n" => n}, decision: %{"outcome" => "allow"}} + + property "any sequence of kinds produces a gapless chain whose links hold", %{scope: scope} do + check all( + kinds <- list_of(member_of(~w(decision query effect)), min_length: 1, max_length: 12), + max_runs: 15 + ) do + inner = scope <> ":" <> Integer.to_string(System.unique_integer([:positive])) + + for {kind, n} <- Enum.with_index(kinds, 1) do + assert {:ok, %Receipt{}} = Receipts.append(inner, entry(kind, n)) + end + + rows = Receipts.list(inner) |> Enum.sort_by(& &1.seq) + + assert length(rows) == length(kinds) + assert Enum.map(rows, & &1.seq) == Enum.to_list(1..length(kinds)) + + rows + |> Enum.chunk_every(2, 1, :discard) + |> Enum.each(fn [previous, current] -> + assert current.prev_hash == previous.receipt_hash, + "seq #{current.seq} (#{current.kind}) does not link to seq #{previous.seq} " <> + "(#{previous.kind}). An unsigned row in the middle must still carry the link" + end) + + assert hd(rows).prev_hash in [nil, ""] + Receipts.stop_writer(inner) + end + end +end diff --git a/test/property/schema_and_state_test.exs b/test/property/schema_and_state_test.exs new file mode 100644 index 0000000..bac1407 --- /dev/null +++ b/test/property/schema_and_state_test.exs @@ -0,0 +1,125 @@ +# SPDX-FileCopyrightText: Sudo Apt Holdings LLC +# SPDX-License-Identifier: Apache-2.0 +defmodule Property.SchemaAndStateTest do + @moduledoc """ + Slice 004 AC2 and AC3. + + The validator is the first thing a tool call meets, and everything after it assumes the arguments + are shaped. What it must never do is crash: a crash there is an unhandled exit on the path a model + can reach with arbitrary JSON, which turns a bad argument into a denial of service rather than a + refusal. + + The state modifier already has an exhaustive test in slice 028 over the four states. This property + complements it rather than replacing it: it generates the decisions and the sequences, so it still + holds if someone adds a fifth state and forgets the exhaustive one. + """ + use ExUnit.Case, async: true + use ExUnitProperties + + alias Trinity.Permissions.Policy.State + alias Trinity.Tools.Schema + + @strictness %{allow: 0, ask: 1, deny: 2} + + defp json_scalar do + one_of([string(:printable, max_length: 15), integer(), float(), boolean(), constant(nil)]) + end + + defp json_value(0), do: json_scalar() + + defp json_value(depth) do + one_of([ + json_scalar(), + list_of(json_value(depth - 1), max_length: 3), + map_of(string(:alphanumeric, min_length: 1, max_length: 6), json_value(depth - 1), + max_length: 3 + ) + ]) + end + + describe "the argument validator" do + property "answers ok or a named refusal for any generated arguments, and never raises" do + schema = %{ + "type" => "object", + "properties" => %{"path" => %{"type" => "string"}, "count" => %{"type" => "integer"}}, + "required" => ["path"] + } + + check all( + args <- + map_of(string(:alphanumeric, min_length: 1, max_length: 6), json_value(2), + max_length: 5 + ) + ) do + case Schema.validate(schema, args) do + {:ok, validated} -> assert is_map(validated) + {:error, reasons} -> assert [_ | _] = reasons + end + end + end + + property "a non-object is refused by name rather than raising" do + check all( + not_an_object <- + one_of([ + string(:printable), + integer(), + list_of(integer(), max_length: 3), + boolean() + ]) + ) do + assert {:error, [reason]} = Schema.validate(%{"type" => "object"}, not_an_object) + assert reason =~ "must be an object" + end + end + + property "a generated schema is either usable or reported unusable, never a crash" do + check all( + schema <- + map_of(string(:alphanumeric, min_length: 1, max_length: 6), json_value(2), + max_length: 4 + ) + ) do + assert is_boolean(Schema.valid_schema?(schema)) + end + end + end + + describe "the tighten-only state modifier" do + property "no generated sequence of states ever produces a weaker decision" do + check all( + decision <- member_of([:allow, :ask, :deny]), + states <- list_of(member_of(State.kinds()), max_length: 8) + ) do + {result, applied} = State.tighten(decision, states) + + assert @strictness[result] >= @strictness[decision] + assert Enum.all?(applied, &(&1 in states)) + if result == decision, do: assert(applied == []) + end + end + + property "order does not matter to the result" do + check all( + decision <- member_of([:allow, :ask, :deny]), + states <- list_of(member_of(State.kinds()), max_length: 6) + ) do + {a, _} = State.tighten(decision, states) + {b, _} = State.tighten(decision, Enum.shuffle(states)) + assert a == b + end + end + + property "repeating a state changes nothing, so a caller cannot tighten by shouting" do + check all( + decision <- member_of([:allow, :ask, :deny]), + states <- list_of(member_of(State.kinds()), min_length: 1, max_length: 4), + n <- integer(2..4) + ) do + {once, _} = State.tighten(decision, states) + {repeated, _} = State.tighten(decision, List.duplicate(states, n) |> List.flatten()) + assert once == repeated + end + end + end +end