Architecture

deducible is a pure-Rust compiler. The contribution is the front end and the invariant engine; solc (via Hardhat) and the Hedera SDK (Node) are orchestrated as subprocesses, never linked.

Pipeline

                     ┌──────────────────────── deducible (Rust) ─────────────────────────┐
source .fiqh ──▶ lexer ──▶ parser ──▶ AST ──▶ sema (invariant engine) ──▶ codegen ──┐
                                                  │ (rule-base, regime)              │
                                                  ▼                                  ▼
                                            diagnostics                    ┌─ Solidity (+ Hardhat test)
                                            (code, span, citation)         ├─ deploy descriptor (JSON)
                                                                           ├─ invariant manifest (JSON)
                                                                           └─ ZK circuit + manifest (Circom)

check stops after sema. build continues into codegen only if sema produced no errors — a contract that is not provably consistent is never emitted.

Crate layout

A Cargo workspace (Rust 1.96):

crates/
  deducible/            # lib + bin
    src/
      lexer.rs      # tokeniser
      parser.rs     # recursive-descent → AST   (parse_unit / parse_bundle / parse_legs)
      ast.rs        # Spec, Bundle, Section, Kv, Value, Span
      sema.rs       # the invariant engine + RuleSet (data-driven rule modules)
      codegen.rs    # Solidity + Hardhat test + descriptor + manifest
      composite.rs  # asset-flow graph + cycle detection (al-'uqud al-murakkabah)
      zakat.rs      # exact u128-widened zakat arithmetic
      faraid.rs     # Islamic inheritance as exact integer fractions
      zk.rs         # sigma-protocol PoC (Pedersen / Schnorr / Fiat–Shamir)
      nl.rs         # natural-language drafting (LLM) → re-checked by sema
      lsp.rs        # stdio JSON-RPC language server
      fuzz.rs       # dependency-free fuzz/property harness
  fiqhc-ffi/        # cdylib → wasm32 + native .so (C-ABI)
rules/              # *.rules.json  (aaoifi, dsn-mui)
specs/              # *.fiqh

Diagnostics & spans

A diagnostic is { severity, code, message, citation, span }. Diagnostic::error blocks codegen; Diagnostic::warn is advisory. Citations carry a [scholar-verify] marker for scriptural/fiqh references and [verify] for common-law cases — the engine asserts consistency, never legitimacy (see the epistemic boundary).

Spans are byte ranges into the source. The LSP maps them to LSP 0-based line/col ranges and emits textDocument/publishDiagnostics with code set and the daleel (citation) in the message. Span precision is complete for the musharakah path (e.g. a capital_guarantee clause underlines exactly that kv); check_with_ruleset and some other instruments still attach the contract header span and are being threaded.

Determinism

The engine is a pure function of (source, regime, rule-module). There is no clock, no RNG, no I/O in the check path. This is what makes “every time, identically, for anyone to verify” a literal property rather than a slogan:

• The same spec under the same module yields byte-identical diagnostics.
• codegen is deterministic: the four base generators are byte-stable across releases, which the codegen-safety test enforces (see Codegen & manifest).

The one impure verb is deducible nl, which calls an LLM — but its output is fed straight back through the deterministic check, so the model can only propose, never certify.

Test surface

• Unit + integration: per-module tests (tests/composite.rs, tests/zakat.rs, tests/contingency.rs, tests/consensus.rs, tests/pluggable.rs, …) assert each diagnostic fires on its negative control and stays silent on the positive one.
• Fuzz (deducible fuzz [N], fuzz.rs): an xorshift64* PRNG feeds random bytes, token soup, and structured mutations of seed specs through compile_check inside catch_unwind. The engine must never panic. 200k iterations run clean.
• Codegen-safety (tests/codegen_safety.rs): a uniform property over all generated contracts — every external/public function that moves value (.call{value:}) must carry nonReentrant; role modifiers, the @dev INVARIANT annotations, and a pinned pragma must be present. This pass originally surfaced five unguarded value-movers, now fixed.
• Generated Hardhat tests: each instrument ships a generated test that runs on a local EVM (and, for some, live on Hedera testnet).

Honest scope

The Rust front end and invariant engine are the research contribution. The ZK layer is a real sigma protocol but its modulus is illustrative (~61-bit), not production. Formal verification of the engine itself is future work; today the guarantees are: a typed, total parser; deterministic checks; fuzz-tested non-panicking; and a machine-checked safety property over codegen output.