Finite Policy Difference

Compare two bounded, finite first-match rule tables. A reduced ordered multi-valued decision diagram counts every outcome-pair region exactly, without listing the Cartesian domain. A difference includes the first assignment in the declaration order, checked by a separate direct rule replay.

Version 0.2.0 changes the 0.1 contract. Read the migration guide before upgrading. This is an offline comparison library and stdin/stdout tool for explicit categorical tables. A complete result concerns that finite model; it does not certify an authorization deployment.

Português · Exact contract · Owned wire · Third-party notices

{"schema_version":1,"variables":[{"name":"tier","values":["zeta","alpha"]}],"outcomes":["permit","review"],"left":{"default":"permit","rules":[]},"right":{"default":"permit","rules":[{"when":{"tier":["zeta"]},"outcome":"review"}]}}

The example returns DIFFERENT, domain size "2", one assignment in each outcome-pair region and witness {"values":["zeta"],"left":"permit","right":"review"}. Counts are decimal strings. zeta comes first because the caller declared it first.

Semantics and bounds

• Declare 0–16 variables, each with 1–8 distinct values, and 1–16 distinct outcomes. Zero variables describe one assignment {}. Names are ASCII identifiers of 1–32 bytes; values/outcomes are literal, nonempty UTF-8 labels of at most 64 bytes without NUL.
• Each table has a required default and 0–128 ordered rules. The first matching rule wins. An omitted variable is unrestricted; an empty subset makes the rule unsatisfiable; condition {} always matches. Unknown names/values, duplicate array labels and extra schema fields are invalid.
• The Crystal JSON parser is the only decoder. Duplicate object members use last-member-wins; repeated declaration/subset array entries are rejected. There is no trimming, Unicode normalization or lexical reordering.
• Input is at most 524,288 bytes. Exact UInt64 counts sum to the domain product, at most 2^48. Nonzero pairs follow the declared outcome indices. The witness follows variable/value indices, with the first variable most significant.
• Limits.new(max_nodes: 65_536, max_visits: 1_000_000) accepts named Int32/Int64 limits from zero through those caps. A visit is charged before compile, condition, ITE, count, witness and replay work, including cache/base/reduction work and declared rules. Nodes include retained terminals and auxiliary nodes. Exhaustion exposes no partial counts, witness or reusable compiled policy.

The source uses shared suffix memoization for rule conditions and value-owned keys for decision nodes. The independent fixture checker uses direct Cartesian enumeration only for small cases, plus elementary constant-count proofs for a 2^48 domain; it does not import the diagram algorithm.

Library and CLI

The qualified stack is Linux x86_64, Debian 13, Crystal 1.14.0+dfsg-1, Shards 0.19.0-1. The shard constraint accepts the 1.14 minor series; only the exact distro versions above were tested. There are no external Crystal shard dependencies. The genuine empty shard.lock is retained.

require "finite_policy_difference"

result = FinitePolicyDifference.compare_json(document)
STDOUT.write(result.json_frame.to_slice)
# Typed construction: Variable, Rule, Policy, Problem; compare(problem, limits).
# decode_json(bytes_or_string) returns Problem | Failure.

Result and Failure are non-inheritable value types with private constructors. Public comparison operations compute from admitted input. Successful comparisons privately stage compact JSON plus LF within 65,536 bytes before returning a complete result. Result#report and its arrays are detached copies; changing them cannot change json_frame. There is no public report-to-result or arbitrary-frame constructor. Crystal unsafe memory operations and deliberate source/type reopening are outside this API boundary.

shards install --local
crystal build src/main.cr --release -o finite-policy-difference
./finite-policy-difference < examples/declared-order.json
./finite-policy-difference demo --max-visits 1000000
./finite-policy-difference --help

The CLI reads one bounded stdin document and writes the exact owned frame. It has no filename, endpoint, expression, executable or configuration-file argument. compare is the default command; demo computes the synthetic example. Options are --max-nodes N and --max-visits N, each once, using unsigned decimal syntax. --help and --version are standalone.

Failures contain only schema_version, status and code. Input read failures can emit an IO_READ frame if stdout works. Output failure returns 3 and attempts a bounded diagnostic; a secondary stderr failure is suppressed. Output is staged before writing, but operating-system writes are not rollback transactions and a broken destination can contain a prefix. No trace or exception details enter the protocol.

Reproduce the qualification

sh scripts/ci.sh explicitly prepares the fixed SDK artifacts, then builds the SDK and product with --network none; the offline stages never execute a downloader. Dockerfile.prepare is the only network preparation stage. It fetches the 62 actual Debian binary packages and 7 matching source artifacts from fixed official HTTPS URLs with exact byte counts and SHA-256 checks. No compiler/package archives, credentials or home directories are committed or mounted.

The product build runs the native specs, packages all source/docs/notices with a per-file inventory, extracts the real archive outside the checkout, builds an independent library consumer, checks 127 frozen semantic/invalid/budget cases and rejects five external result-construction/serialization probes. The final runtime contains the compiled CLI/consumer, actual shared-library closure, original synthetic examples and complete notices. It contains no source checkout/archive, Crystal, Shards or C compiler. Qualification runs without host binds, network, root privileges or writable root, with dropped capabilities, no-new-privileges, 256 PIDs, 1 GiB memory and 2 CPUs.

qualification/runtime_checks.sh exercises the real demo/stdin/help/version, invalid bytes, oversized input and actual /dev/full output/diagnostic failures. These are native Linux technical checks. No browser, cross-platform, benchmark, security certification or native compiler reproducibility claim is made. Actual ELF/transitive-library ownership and hashes are captured; a linker trace is not proof of retained archive members.

Original source is MIT licensed. Gemini 4 Argon authored the original six-file core; Codex support made recorded native compile, ownership and memo fixes and the transport/package/documentation layer. The maintained compiler/stdlib/native components retain their complete upstream terms. Published by Lofrano Tecnologia.