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