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/
  fiqhc/                # lib crate (internal name) + the `deduce` binary
    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
      maqasid.rs    # the maqasid / hiyal-risk surfacing layer (warnings only)
      composite.rs  # asset-flow graph + cycle detection (al-'uqud al-murakkabah)
      zakat.rs      # exact u128-widened zakat arithmetic (genus rates + the eight asnaf)
      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, hanafi, maliki, shafii, hanbali)
specs/              # *.fiqh  (one positive + one negative control per instrument)

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 deduce nl, which calls an LLM. 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 (deduce 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, and 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.