openfga-to-z3

openfga-to-z3 is an early verification-oriented compiler based on OpenFGA Server v1.20.0 (commit 73591ef16ce508623920d5b706286ffcdfb6841b) and its pinned API protobuf revision. It compiles finite property queries to portable SMT-LIB v2 and DIMACS, runs a Z3/cvc5/CaDiCaL solver portfolio, and cross-checks solver answers against an independent executable semantics.

This repository does not yet claim a formally verified end-to-end pipeline. The Rocq files have no Admitted, are accepted by the Rocq 9.3 kernel, and 726 exported theorems report no assumptions. These cover concrete tuple semantics, monotone fixed-point evaluation with finite convergence, stratified negation, condition-context precedence, a typed CEL core, conditional-tuple filtering, structural normalization, property queries, equisatisfiable Tseitin CNF, SMT AST preservation and DIMACS body round-tripping. The remaining boundaries are tracked in docs/proof-obligations.md.

The implementation is OCaml extracted from Rocq: the theory in theories/, the extracted kernel in extraction/, the library in src/ and the satisfgable executable in bin/, all built by dune. The former Rust implementation was removed; its final state is the git tag rust-final. Behavior is defined by OpenFGA v1.20.0 itself, reached through the fga-oracle test oracle, under the rule exact or refuse: the executable either answers like OpenFGA or refuses the input. The Rocq CEL evaluator still has known wrong answers; they are recorded in test/exactness/divergences.jsonl. At runtime the CLI cross-checks every concrete condition outcome against OpenFGA (fga-oracle evaluate) and refuses on a mismatch, which turns those condition-level wrong answers into refusals. Graph semantics are guarded by interim refusals, not by a runtime cross-check; see docs/exactness.md. Its CEL syntax target is the v0.25.3 release, pinned by commit and source digests; the executable accepts only a documented fragment. See the migration guide for the accepted inputs and current proof boundary.

compile and prove generate the Rocq certificate contract for that fragment. prove runs the solver portfolio, checks a separate table evaluator, reports and replays named witnesses, and supports --lrat-proof.

Two autonomous frozen corpora run without any other toolchain: the verifier corpus (143 adversarial verifier calls) and the kernel corpus (240 exact compile calls). Both were captured from the former Rust test suite and run with dune build -j 2 @corpora.

Implemented fragment

Supported now:

• canonical OpenFGA JSON schemas 1.1 and 1.2; modular source files are composed only by the official fga frontend;
• concrete subjects, type#relation usersets and typed wildcards type:*;
• direct, computed userset, union, intersection, difference;
• tuple-to-userset with a direct concrete tupleset;
• positive recursive usersets and recursive tuple-to-userset over finite scopes, interpreted by least iteration from the empty relation;
• stratified difference over recursive relations, evaluated and encoded one finite least fixed point per stratum;
• conditional direct tuples evaluated on a closed request/tuple context, with tuple-local values taking precedence as in OpenFGA 1.20;
• CEL bool/string/int/uint/double/duration/timestamp/list/map parameters via a fail-closed evaluator (ipaddress remains outside the fragment);
• request-scoped contextual tuple files merged into the closed tuple store;
• finite closed-world implication, equivalence and reachability queries;
• portable SMT-LIB v2 and proposition-only CNF/DIMACS;
• parallel Z3/cvc5/CaDiCaL execution with fail-closed disagreement handling;
• replay of SAT witnesses with the reference evaluator.

Rejected before solver invocation:

• CEL ipaddress parameters, missing condition parameters, ill-typed values, undefined or mismatched tuple conditions;
• unstratifiable negative cycles through difference;
• unknown JSON fields and ambiguous userset variants.

See the research and soundness analysis for the complete scope and trust model. The live theorem ledger is docs/proof-obligations.md.

Build and test

docker/Dockerfile has three targets; no host Rocq, OCaml, Go or solver is needed:

• toolchain: OCaml 5.5.1, dune, Rocq 9.3, Z3/cvc5/CaDiCaL, the pinned fga CLI and fga-oracle;
• build: runs every suite (dune build -j 2 @install @runtest @live @corpora @cel-spec, with a pinned cel-spec checkout), then installs the executable and the OpenFGA theory;
• app: the toolchain plus the installed satisfgable (entrypoint) and theory.

docker build --target app -f docker/Dockerfile -t satisfgable .
docker run --rm satisfgable --help

To work inside the toolchain:

docker build --target toolchain -f docker/Dockerfile -t satisfgable-toolchain:ocaml5.5-rocq9.3 .
docker run --rm -v "$PWD":/src:ro satisfgable-toolchain:ocaml5.5-rocq9.3 sh -c \
  'cp -R /src /tmp/work && cd /tmp/work && dune build -j 2 && dune runtest -j 2'

The dune aliases are:

• dune build -j 2: the theory, the audit gate (a closed Print Assumptions transcript and an independent rocqchk replay of every compiled module), the extracted kernel and satisfgable; a failing gate blocks the kernel, so also @install and opam install;
• dune runtest -j 2: unit, cram and command-line tests and the closed reference Print Assumptions audit (Audit.expected);
• dune build -j 2 @live: the same certificate, planner, scale and LRAT tests with the real solvers;
• dune build -j 2 @corpora: the frozen kernel and verifier corpora. Run it before installing the theory into the switch: an installed OpenFGA theory would shadow the built one, so the rule fails closed;
• dune build -j 2 @cel-spec: the official CEL v0.25.3 conformance suite against test/cel-spec/known-failures.jsonl (see docs/cel-full-conformance.md). It needs CEL_SPEC_CHECKOUT, protoc and Python protobuf, and is skipped when the variable is unset unless SATISFGABLE_REQUIRE_CEL_SPEC=1 (set in the Docker build).

Always pass -j 2: compiling BooleanCELSlice.v alone peaks around 16.5 GB of memory, and more parallel jobs can exhaust a 32 GB host.

Without Docker

opam switch create . 5.5.1 --no-install
eval $(opam env)
export OPAMJOBS=2                     # memory: see the -j 2 note above
opam install . --deps-only --locked   # reads satisfgable.opam.locked
dune build -j 2
dune runtest -j 2
opam install .                        # satisfgable and the OpenFGA theory

opam install . builds with dune build -p satisfgable -j $OPAMJOBS @install, so it needs OPAMJOBS=2 as much as the dependency install does (dune install -j 2 installs the same files from the existing _build). In a git checkout it installs the committed tree; add --working-dir to include uncommitted changes. satisfgable.opam.locked is Linux-only: it was solved in the Debian 13 image and locks conf-linux-libc-dev; elsewhere drop --locked.

dune runtest and opam install . --with-test run the command-line and frontend tests, so fga-oracle and fga must be on PATH; dune build @live also needs z3, cvc5 and cadical.

Runtime tools, found on PATH (or through the matching option):

• fga-oracle (always; see oracle/README.md), --fga-oracle or $FGA_ORACLE_BIN;
• z3, cvc5 and cadical (with textual LRAT support) for prove;
• the pinned fga CLI for DSL models (--fga);
• rocq (9.3) for verify-certificate (--rocq). It finds the installed theory in $(rocq c -where)/user-contrib/OpenFGA, else in the first ROCQPATH entry holding OpenFGA, unless --rocq-library is given.

The same -j 2 memory note applies.

Oracle image (OpenFGA v1.20.0 behavioral reference, see oracle/README.md):

docker build -t satisfgable-fga-oracle:v1.20.0 oracle
sh oracle/test.sh

Exactness tooling (official verdicts, divergence ledger) is described in docs/exactness.md.

The examples below call the binary through the app image:

satisfgable() { docker run --rm -v "$PWD":/work -w /work satisfgable "$@"; }

Every model-accepting command validates the model with the official fga-oracle validate (--fga-oracle PATH or $FGA_ORACLE_BIN), in addition to the pinned fga CLI for DSL input (--fga PATH; --require-official-validation makes an unavailable frontend an error).

compile and prove accept JSON or YAML tuple, context and scope files. They retain the JSON actually passed to Rocq as model.json, tuples.json, context.json, optional scope.json and ordered contextual-tuples-<index>.json files alongside the solver artifacts. Use these snapshots for the explicit certificate source audits. The YAML conversion is an external frontend; those audits certify the JSON snapshots, not the original YAML parser or file.

The autonomous OCaml frontend test also runs OpenFGA assertions from the official conformance fixtures (test/fixtures/*.fga.yaml), including modular schema 1.2 composition, recursion, conditions, overflow masking and duration precision. Several test/fixtures/*-compatibility.jsonl files hold frozen results of the former Rust implementation; they are kept as regression data. The exactness ledger compares OCaml with OpenFGA on every one of them: the Rocq condition evaluator (without the runtime cross-check), the Rocq context conversions and the CLI's model-acceptance decision. Its wrong answers are all condition outcomes or parameter conversions feeding one, so the CLI's runtime cross-check refuses any that would change an answer; the model rows are refusals only, since OpenFGA itself validates every model.

Build the pinned rocq-comparator image and compare eight FiniteFormula.v theorems, three context selection/ priority laws from CELContextInputs.v and two public double comparison laws from CEL.v at HEAD with the current proofs. The check includes axiom closure and rocqchk replay:

docker build -f docker/rocq-comparator.Dockerfile -t satisfgable-rocq-comparator:9.2 .
sh scripts/check_rocq_comparator.sh

The comparator uses Rocq 9.2 and OCaml 5.3 in its own Docker image, independent of the Rocq 9.3 toolchain used for the build. The comparator script runs in a read-only container with network access disabled.

For solving, the app image provides Z3, cvc5 and CaDiCaL. The safe default requires consensus from every applicable solver. Missing solvers produce INCONCLUSIVE; the diagnostic --allow-single-solver-result mode is explicit and never presented as consensus.

Usage

Inspect the compatibility target:

satisfgable about

Validate a canonical model:

satisfgable validate test/fixtures/model.json

Compile a finite counterexample query without invoking solvers:

satisfgable compile test/fixtures/model.json \
  --tuples test/fixtures/tuples.yaml \
  --property 'document#viewer => document#editor' \
  --output-dir artifacts

For a conditional model, provide request context separately. Tuple-local context lives on each tuple and overrides matching request fields:

satisfgable compile test/fixtures/conditional-model.fga \
  --tuples test/fixtures/conditional-tuples.yaml \
  --context test/fixtures/conditional-context.yaml \
  --property 'reachable(document#viewer)'

--contextual-tuples path.yaml may be repeated to add request-scoped tuples; the files form one request tuple set. Matching object/relation/subject identities replace persistent tuples before condition evaluation. A false contextual condition suppresses its persistent counterpart; a replaced persistent condition is never evaluated. Duplicate identities within the persistent set or the request set are rejected. Selected tuples are validated and filtered before the finite scope and formula are built.

This also emits artifacts/QueryCertificate.v. It embeds the normalized OpenFGA model, facts, finite scope and property; proves the query equivalent to the verified layered compiler; and proves the exact CNF equal to the verified Tseitin output. For conditions in the certified CEL core it also reconstructs every merged environment, proves each true/false CEL result, and proves that filtering those results yields exactly the active tuple store. It retains selected input tuples before filtering, including unconditional and inactive tuples, so this equality checks their conservation as well. It also checks a precedence-aware typed source tree against the exact CEL text and proves that this tree maps to the expression evaluated by Rocq. Query equivalence no longer enumerates every Boolean valuation: a generic Rocq theorem combines the exact closed-store assertion shape, variable bounds and equality under the all-facts-true valuation to prove equality for every valuation. This retains the original complete-query guarantee while avoiding an exponential case split. Kernel regressions cover 12 and 32 tuple facts. CNF allocation follows the compiler's tuple order, keeping tuple_10 aligned with its SMT identifier instead of placing it before tuple_2 lexicographically. Verify it with the strict core-contract verifier:

satisfgable verify-certificate artifacts/QueryCertificate.v

It requires the neighboring query.smt2 and query.cnf (override with --smtlib/--dimacs), checks a mandatory typed contract in a separate Rocq process, audits its assumptions, and proves equality with the supplied solver file snapshots. Missing contracts, axiomatic substitutes and changed files fail. The reported claim distinguishes compilation-only, no witness and a scoped counterexample. CORE_CERTIFICATE_VERIFIED concerns the normalized mathematical model, prepared facts, declared scope and embedded property; input-conversion extensions are not included in this contract's assumption audit. LRAT requires an explicit --lrat-proof path on verification; it is not inferred from statements already present in the candidate certificate.

To bind the certificate to the question you actually want checked:

satisfgable verify-certificate artifacts/QueryCertificate.v \
  --model-json model.json --expected-property 'document#editor => document#viewer'

--expected-property requires the model audit. Rocq independently parses the original argument, resolves type/relation names, and checks the exact target, operator and operand order in the core contract. reachable(...), =>, <=> and the == alias are supported. End whitespace is trimmed without joining identifier fragments; the UTF-8 whitespace table is tested against every Unicode scalar accepted by the Rust standard library's char::is_whitespace (checked historically). PROPERTY_SOURCE_VERIFIED connects that parsed question to the complete compiled formula for every valuation. A consistent certificate for another true property is rejected. This does not upgrade a compilation-only claim into a proof of validity, and general parser equivalence remains unproved. Without this flag only the embedded property is audited, not its correspondence with your question.

To check the model's structure against a separately supplied JSON input:

satisfgable verify-certificate artifacts/QueryCertificate.v --model-json model.json

The additional MODEL_STRUCTURE_VERIFIED status means Rocq independently decoded that file snapshot and checked the core contract's type/relation names, normalized rewrites, and restrictions on every selected tuple (including inactive ones). This works even without the old optional source theorems; a different rewrite, invalid restriction or substituted name table is rejected. JSON formatting may differ. This status does not certify condition expressions or their evaluation, raw tuple/scope files, full model validity or DSL translation. For DSL input, supply the official frontend's canonical JSON output, not the DSL. --model-json and --lrat-proof can be combined, including in the shell helper.

To additionally bind and check original tuple JSON documents:

satisfgable verify-certificate artifacts/QueryCertificate.v \
  --model-json model.json --tuples-json tuples.json \
  --contextual-tuples-json request-tuples.json

--tuples-json requires --model-json. Repeat --contextual-tuples-json in compilation order when needed, retaining empty documents too. Rocq checks exact document bytes, complete unique selection after contextual override, each tuple header/condition name and equality with the core's pre-filter input facts. It also checks every object-table entry has a defined type and that all rendered object texts are distinct. A generic theorem proves injectivity for every representable object, including entries unused by the query. This compares actual text, so delimiter-induced collisions are rejected too. Subject checks additionally require unique relation/wildcard names, no # in object/wildcard texts and no collision between objects and wildcard texts. A verified first-# split establishes that equal subject text implies the same concrete, userset or wildcard subject. Together these checks prove uniqueness of the full (user, relation, object) tuple identity, without enumerating the object × relation product. They cover the whole symbol table, including unused entries; neither check claims complete OpenFGA identifier-syntax validation. TUPLE_SOURCES_VERIFIED does not certify conditional outcomes, request-context conversion or full JSON grammar conformance. The active-fact theorem is conditional on the embedded outcomes. YAML/programmatic sources are not silently converted for this audit: JSON provenance declarations must exist. The verifier permits at most 128 tuple documents totaling 64 MiB.

To audit selected CEL outcomes against the supported formal core as well:

satisfgable verify-certificate artifacts/QueryCertificate.v \
  --model-json model.json --tuples-json tuples.json \
  --verify-cel --context-json context.json

--verify-cel requires the tuple/model audits. --context-json is optional and defaults to {}; when supplied, it requires --verify-cel. A fresh Rocq audit checks every selected conditional binding against its source-located trace, model condition expression/complete parameter table, formal evaluation, and the decoded request context (with tuple-local parameter precedence). It reports CEL_TRACES_VERIFIED only after auditing the contract and its selected/active-fact corollaries. Missing or unsupported traces fail the requested audit, rather than silently reducing coverage. All selected conditions are checked, including denied ones; unused model conditions are not certified. Context JSON formatting may differ, but its full decoded value must match every trace. Even an empty selection requires valid context JSON. This is not a claim of general CEL/JSON parser conformance or complete CEL language support.

To bind the finite scope to requested JSON additions:

satisfgable verify-certificate artifacts/QueryCertificate.v \
  --model-json model.json --tuples-json tuples.json \
  --verify-scope --scope-json scope.json

--verify-scope requires the tuple/model audits. Its default, when --scope-json is omitted, is {"objects":[]}. The JSON wrapper must contain only an objects array of concrete object strings. Order and duplicate entries do not change the set. Rocq checks both directions of the additions/name-table correspondence and then checks that the actual core scope is exactly active tuple objects plus those additions. SCOPE_SOURCE_VERIFIED also audits the transfer to the complete compiled query for every valuation, including its closed-store fact assertions. A consistent certificate for a different scope is rejected. This checks the supplied snapshot's decoded set, not historical file-byte identity. Conditional activation requires --verify-cel separately; full JSON/DTO rejection conformance remains open.

Rocq source can execute code: the verifier is not a sandbox for arbitrary unreviewed .v files. It uses a private temporary directory, a per-process timeout (60 seconds by default) and a 64 MiB limit per input file. The Rocq executable and compiled formal library must be trusted. --rocq, --rocq-library and --timeout-ms configure those paths and timeout.

Run the portfolio:

satisfgable prove test/fixtures/model.json \
  --tuples test/fixtures/tuples.yaml \
  --property 'document#can_delete => document#editor'

To request a solver refutation as well, add --lrat-proof (--rup-proof is a compatible alias). CaDiCaL writes query.lrat while Z3 and cvc5 still run in parallel. After an accepted UNSAT portfolio result, the LRAT trace is included in QueryCertificate.v:

satisfgable prove test/fixtures/model.json \
  --tuples test/fixtures/tuples.yaml \
  --property 'document#can_delete => document#editor' --lrat-proof
satisfgable verify-certificate artifacts/QueryCertificate.v --lrat-proof artifacts/query.lrat

The kernel checks each hinted unit propagation against the actual generated CNF, proves it unsatisfiable, and transfers that result to the query through the verified Tseitin equality. Textual LRAT supports RUP additions, RAT additions with checked resolvents, and clause deletions. A generic theorem proves that RAT preserves satisfiability by adjusting the pivot variable; every active clause containing the opposite pivot must be justified. Parsing the trace alone does not certify UNSAT: the kernel check is required. With verify-certificate --lrat-proof artifacts/query.lrat, the verifier reads that file again, constructs a fresh untrusted proof witness, and kernel-checks it against the CNF already bound to the core contract. A separate audit checks the refutation and its transfer to the compiled query without assumptions. Only then is LRAT_REFUTATION_VERIFIED reported. Without this flag, appended solver statements are not assumption-audited. Parsing need not be trusted for UNSAT: whatever steps the parser produces must pass the sound checker for that CNF.

An optional scope file extends the active domain:

objects:
  - user:anne
  - document:1

The result HOLDS_IN_FINITE_SCOPE refers only to the displayed finite scope and closed tuple store. Kernel-checking QueryCertificate.v proves absence of a witness in the generated layered query. The kernel now also compares the chosen layer with its successor on every declared relation/object/subject atom in the scope, and separately checks every stratum using its actual lower-layer prefix. A false depth is rejected even when it leaves the requested property's answer unchanged. The kernel checks closure of computed/userset/tuple-to-userset dependencies as well, and proves that the stable value persists at every later iteration (for each stratum with its lower prefix fixed). For syntactically positive models, an additional positivity check and generic projection theorem connect the actual membership encoding to the least fixed point of the bounded operator. Models containing difference instead receive signed-rank checks: positive dependencies may stay at the same or a lower level, while negative dependencies must be strictly lower. Each stabilized stratum is proved to be the least fixed-point extension of its frozen lower interpretation. The final membership encoding is connected to those extensions, and its projection is proved to satisfy the original bounded model equations. This is stratified leastness, not a claim of a global least fixed point for a nonmonotone operator. This is not an unbounded proof over future objects or tuple stores.

The formal query now enumerates all subject/object pairs directly from one embedded scope, filtering targets by type. For scopes built from active tuples, Rocq checks exact membership in the active tuple objects plus explicitly declared additions, with no duplicates. Inactive tuple objects do not enter automatically; wildcards do not create concrete users. SAT witnesses must belong to that scope. Independently supplied scopes retain the enumeration guarantee but do not claim active-store derivation in their generated loose proofs. --verify-scope can independently establish the active-store-plus-additions contract from the supplied JSON snapshot when the required addition data is present. The strict tuple audit also proves textual object/subject/tuple injectivity. General parser conformance and external file authenticity remain separate boundaries.

Formalization

UTF8.v proves the byte validator sound and complete for the RFC 3629 UTF-8 grammar. The JSON entry point now requires this check before parsing: invalid bytes are rejected even inside unused or overwritten strings. This fixes a reproduced mismatch where the former byte-oriented decoder accepted a quoted 0xFF that serde_json rejected. Overlong encodings, encoded surrogates, truncated sequences and values above U+10FFFF are covered by the grammar and boundary regressions. Successful JSON/context decoding therefore entails valid UTF-8 source bytes. This source-encoding guarantee is separate from decoding escapes and proving UTF-8 preservation for a complete string.

JSONUnicode.v proves hexadecimal word decoding and Unicode-escape decoding sound and complete, with exact suffix preservation. It covers scalar BMP words and high/low surrogate pairs under the existing strict scalar-value policy: unpaired surrogates are rejected. For every scalar, the UTF-8 encoder is total, its output satisfies the byte grammar, and its payload reconstructs exactly the original code point; the encoder is therefore injective. The proofs use integer arithmetic and byte bounds, not an exhaustive scalar enumeration. Tests compare all hexadecimal input bytes and Unicode boundary cases against serde_json (historical comparison). JSONStringGrammar.v now composes those results with short escapes and raw bytes. For UTF-8 input, the existing string-body decoder (starting after the opening quote) is sound and complete for the strict scalar string grammar, preserves decoded UTF-8 and the exact suffix after the closing quote, and has a sufficient fuel bound. More fuel cannot change a successful result; the grammar's decoded value and suffix are deterministic. UTF-8 preservation uses an arbitrary-prefix invariant, not the false assumption that the tail after one byte of a multibyte character is valid UTF-8. Full value/container parsing and DTO conformance remain separate obligations.

JSONNumberGrammar.v proves the existing JSON numeric lexer sound and complete for the RFC 8259 number grammar. Successful decoding preserves the exact consumed lexeme and remaining suffix; every grammatical number is accepted in full, including before a suffix that cannot extend it. This is a generic proof over arbitrary finite strings, not only a test corpus. It covers signs, leading-zero restrictions, fractions and exponents. Numeric range/conversion is separate: 1e400 is grammatically valid even though serde_json's default finite-f64 representation rejects it. This does not yet prove the full JSON value/string/container parser or DTO validation.

The formal theory is under theories/ (logical path OpenFGA). dune build -j 2 compiles it and gates the kernel on a closed assumptions audit and a rocqchk replay; dune runtest -j 2 also checks the reference audit. The kernel corpus (dune build -j 2 @corpora) also runs kernel regression examples for timestamp boundaries, invalid dates, fractional seconds, time-zone offsets, large numeric literals and incorrect parameter bindings. Epoch arithmetic uses binary integers, including for dates before 1970.

Exercise the generated certificates themselves:

dune runtest -j 2           # certificate tests without solvers
dune build -j 2 @live       # adds the real solvers and LRAT

These tests need rocq and a CaDiCaL binary supporting textual LRAT (all in the toolchain image). They check the temporal and attribute fixtures and require the kernel to reject deliberately altered timestamps, double bits, parameter identifiers and Boolean results. Double literal checking uses exact decimal rationals and binary64 midpoint comparisons with ties to even. It includes normal/subnormal boundaries, signed zero, halfway cases, and a deterministic corpus of 256 finite values with adjacent-bit mutations.

Canonical double-quoted strings are independently decoded by Rocq, including escaped quotes, backslashes, control bytes and literal UTF-8 text. A general round-trip theorem and injectivity theorem cover this encoder. Integration tests compare all ASCII characters and selected Unicode strings and reject an altered decoded value with an unchanged lexeme.

The typed CEL core checks signed/unsigned 64-bit values and the results of signed addition/subtraction and unsigned addition. Overflow produces an error. Boolean && and || let a decisive operand mask an error on either side. Kernel integration tests compare 114 integer boundary calculations against frozen reference results; the OpenFGA fixture checks the Boolean masking behavior.

Conditional certificates also embed the decoded request and tuple contexts separately. For each parameter represented by the certified core, Rocq checks tuple precedence and conversion against the actual typed environment. Tests reject swapped context priority and altered environment values, and accept an invalid request value when a valid tuple value overrides it. For request contexts loaded from a .json file, the exact source text is retained and decoded inside Rocq; the parameter obligations use that decoded result. Tuples loaded from JSON also retain the original document and array index. For certified conditional tuples, Rocq checks the original identity and condition name, then decodes the tuple context from that record. Unconditional JSON tuples have identity obligations too. Both array and { "tuples": [...] } formats are supported. For entirely JSON-backed file loads, certificates also retain every tuple document, including empty files. Rocq independently selects the persistent and contextual record positions, rejects duplicate identities within either set, and checks that the retained position list has exactly the same members and length. A single list of source/fact bindings now supplies the conditional facts used by the compiler. Rocq checks complete, nonduplicated position coverage and re-renders each numeric tuple through embedded name tables to compare its subject, relation, object and condition name with the source. A generic theorem connects active facts to these source bindings. Tests reject omitted, duplicated, fabricated and shadowed positions, changed numeric identities and altered unconditional outcomes; inactive inputs are checked too. Concrete, userset and wildcard subjects and multiple contextual files are covered. For all-JSON loads whose selected conditions have certified source trees and supported parameter types, an additional theorem links fact outcomes to source-located CEL traces. It reads each tuple context from the dataset, checks parameter conversion against that context and the request, validates the source tree and bindings, and compares the complete condition outcome with the evaluation of that tree. Swapped environments are rejected even when both outcomes are false. Unsupported conditions explicitly omit this stronger claim. The CLI also retains the exact canonical model JSON. For each supported condition used in an evaluation, Rocq looks up its original declaration and checks the condition name, CEL text and complete typed parameter table (including generic list/map types and parameter identifiers). For all-JSON stores this composes with the source/fact/CEL trace theorem. A consistently recompiled different condition is rejected when paired with the original source. DSL inputs retain the official frontend's JSON output, not a proof of the DSL transformation. Rocq also reconstructs all type/relation names and relation rewrites from that JSON. The generated model is a lookup into one shared relation table, checked equal to the independently decoded table after verified structural normalization. An equality theorem connects the actual model function used by the query compiler to this source-derived model. Tests cover all operators, nested union/intersection flattening, JSON aliases and null optional variants, recursion, stratified negation and schema 1.2. Source-only and consistently recompiled rewrite mutations fail, as do omitted relations and added empty types. Selected tuples, including inactive ones, are additionally checked against the original model's directly_related_user_types metadata. The checker distinguishes concrete subjects, usersets and wildcards, requires the exact condition name and a direct branch in the relation rewrite, and transfers these checks to active facts. Metadata-only and consistently widened-restriction mutations fail. With JSON tuples, these inputs are projected from the existing source bindings; with YAML/programmatic tuples, the model restrictions are checked but tuple-input provenance remains external. Closed-store fact variables are retained in CNF even when the witness query is constant false, so this case remains certifiable. These guarantees are relative to embedded documents; file-manifest authenticity, validation of unused declarations, complete reference-validation conformance, object/scope correspondence and general CEL parser conformance remain open. Mixed JSON/YAML loads, programmatic stores and already-evaluated store overlays do not claim this dataset-level check. YAML input and full model-validation conformance also remain open boundaries. General conformance of the new JSON decoder remains an open proof obligation, with positive, malformed-input and source-mutation tests. Object normalization has generic proofs: every key retains its final input value and the normalized object has no duplicate keys.

For example, the following context fixture includes duplicate keys and Unicode escapes; its original text is included in the generated certificate:

satisfgable compile test/fixtures/attribute-model.json \
  --tuples test/fixtures/attribute-request-tuples.yaml \
  --context test/fixtures/attribute-context.json \
  --property 'reachable(document#viewer)'

Duration inputs follow OpenFGA's Go behavior: integral nanoseconds stay exact (9007199254740993ns differs from 9007199254740992ns), µs/μs are accepted, and fractional parts use Go's rounding, reproduced with exact rational calculations in Rocq. OpenFGA v1.20.0 (cel-go v0.31.0), reached through fga-oracle, is the behavioral reference for CEL parsing and execution; differences are ledgered, not assumed away. Free-variable validation respects lexical scope in macro-expanded comprehensions. The extracted core certifies typed all, exists and exists_one with scoped bindings; other comprehension forms remain outside that core.

verify-certificate fails with a nonzero exit code when Rocq or the theory is unavailable; it never turns a missing prover into a successful verification.

License

Apache-2.0.