Rule modules

The single most important architectural choice in Deducible: the engine is separate from the rule-base. The compiler knows how to check a contract. What counts as compliant is supplied by a rule module, plain JSON that a scholar or standards body can author and ratify without touching Rust.

This is what closes the authority gap. Ratification becomes a module, not a fork.

Shape of a module

rules/aaoifi.rules.json

{
  "authority": "AAOIFI", "version": "2017",
  "regimes": { "islamic": { "classes": {
    "musharakah_mutanaqisah": {
      "required_invariants": ["ownership_conserved", "rent_on_living_share", "loss_follows_capital", "price_attested"],
      "constraints": [
        { "code": "RIBA-1", "field": "risk.capital_guarantee", "op": "eq", "value": "none",
          "citation": "al-Baqarah 2:275; AAOIFI SS No. 12 [scholar-verify]" }
      ]
    }
  } } }
}

A module declares, per class, the invariants that must hold and the constraints that encode them. Each constraint is a { code, field, op, value, citation } tuple, where field is a dotted path resolved against the spec (risk.*, returns.<mechanism>.<key>, returns.buyout.priceSource, dispute.*, zakat.*) and op is eq, ne, or gt (nothing else exists yet; see “What the engine cannot enforce” below). The engine loads the module and checks the spec against it. It is data-driven and regime-neutral. RULES-1 fires when a module has no entry for the class.

Two things worth being exact about, since they shape everything below. First, required_invariants checks only that an invariant’s name is declared in the spec, never its assertion body; the real substance comes entirely from constraints, which is why every class in this reference carries at least one genuinely enforceable field check, never a bare name-presence rubber stamp. Second, a rule module is fully self-contained: nothing the compiler’s own built-in check_* functions enforce natively is inherited “for free.” A module that omits a check does not get it back from the engine.

Selecting a module

deduce check home.fiqh --rules aaoifi      # or dsn-mui, hanafi, maliki, shafii, hanbali

meta { rules: "dsn-mui"; }                 # or pin it in the spec

Modules are discovered in ./rules or $FIQHC_RULES_DIR. Since the foundations work, --rules governs both check and build: a spec a chosen authority refuses will not generate a contract, so the authority governs whether code is emitted, not only whether it checks. Without --rules, the built-in universal core applies.

Coverage: all 26 classes, six modules

Every module now carries an entry for every class in its regime; RULES-1 (no entry for the class) no longer fires anywhere it shouldn’t. Two labels distinguish what kind of coverage a cell holds:

• S: substantive. Real field constraints, and either a dedicated standard or fatwa number from that authority, or, for a madhhab, an actual documented divergence from the base position.
• M: mirror-base. Real field constraints too, the same genuine, enforceable checks as an S entry, but no dedicated standard/fatwa exists for that class under that authority (so the citation falls back to classical basis), or, for a madhhab, no confidently-citable divergence was found for that class beyond a different citation on the same requirement.
• N/A: regime mismatch by design. commercial_escrow is a common_law class; the four madhāhib and DSN-MUI carry no common_law block at all, so they have nothing to say about it. That absence is correct, not a gap.

Class	AAOIFI	DSN‑MUI	Ḥanafī	Mālikī	Shāfiʿī	Ḥanbalī
musharakah_mutanaqisah	S	S	M	S (khilāf)	S (khilāf)	M
mudarabah	S	S	M	M	M	M
ijarah_imbt	S	S	M	M	M	M
murabahah	S	S	M	M	M	M
salam	S	S	M	M	M	M
istisna	S	S	M	M	M	M
sarf	S	S	M	M	M	M
tawarruq	S	M	M	M	M	M
qard_hasan	S	S	M	M	M	M
rahn	S	S	S (khilāf)	M	M	M
kafala	S	S	M	M	M	M
hawala	S	S	M	M	M	M
wadia	M	S	M	M	M	M
wakala	S	S	M	M	M	M
ijarah	S	S	M	M	M	M
juala	S	S	M	M	M	M
ariyah	M	M	M	M	M	M
musharakah	S	S	M	M	M	M
muzaraah	M	M	M	M	M	M
sukuk	S	S	M	M	M	M
takaful	S	S	M	M	M	M
mudarabah_pool	S	M	M	M	M	M
waqf	S	S	M	M	M	M
hibah	M	M	M	M	M	M
wasiyya	M	M	M	M	M	M
commercial_escrow	S	N/A	N/A	N/A	N/A	N/A

Counts: AAOIFI 21 S / 5 M, 26/26 classes, zero RULES-1. DSN‑MUI 19 S / 6 M / 1 N/A, 25/25 islamic classes, zero RULES-1. Ḥanafī 1 S / 24 M / 1 N/A. Mālikī 1 S / 24 M / 1 N/A. Shāfiʿī 1 S / 24 M / 1 N/A. Ḥanbalī 0 S / 25 M / 1 N/A. Every madhhab module covers all 25 islamic classes; the one substantive entry each carries is exactly its khilāf, not an accident of counting.

A mirror-base entry is not a weaker check. wasiyya under every module still refuses a bequest to an heir and demands a positive share; it simply has no AAOIFI Shari’ah Standard number to cite, since wasiyya belongs to inheritance law (farā’iḍ), outside AAOIFI’s commercial-instrument standard set. “Mirror-base” describes the citation and the divergence question, never the strength of the constraint itself.

The four madhāhib: khilāf made executable

Deducible ships six modules. Two are standards bodies (AAOIFI, DSN-MUI) and four are the classical schools (ḥanafī, mālikī, shāfiʿī, ḥanbalī). The schools are where the design earns its keep, because they disagree, and the engine lets them disagree in code. Two divergences are encoded so far, each promoted from a citation already sitting in the engine’s own source, never invented fresh for this reference.

Musharakah mutanaqisah: does profit have to track capital?

The Mālikīs (with the Shāfiʿīs) hold that a partner’s profit share must track his capital share; he may not take profit beyond his capital ratio by mere stipulation. The Ḥanafīs (with the Ḥanbalīs) permit profit by free stipulation, with loss alone fixed to capital. The Mālikī and Shāfiʿī modules encode this as an extra required invariant, profit_tracks_capital. The Ḥanafī and Ḥanbalī modules omit it.

$ deduce check specs/musharakah_mutanaqisah.fiqh --rules hanafi
✓ consistent

$ deduce check specs/musharakah_mutanaqisah.fiqh --rules maliki
✗ INV-1  required invariant "profit_tracks_capital" is not declared for this class.
         Malik, al-Muwatta; Ibn Rushd, Bidayat al-Mujtahid [scholar-verify]

Module	Stance on profit in this partnership
hanafi	profit by free stipulation (no profit_tracks_capital); al-Sarakhsī, al-Kāsānī.
hanbali	profit by free stipulation; aligns with the Ḥanafī rule here.
maliki	profit must track capital (profit_tracks_capital required); Mālik, Ibn Rushd.
shafii	profit must track capital; aligns with the Mālikī rule here.
aaoifi	the contemporary standard (SS No. 12).
dsn-mui	the Indonesian fatwa body; adds an explicit nisbah requirement.

This divergence does not currently extend to musharakah (the plain full partnership, a separate class). It is textually the same fiqh position, but there is no regression fixture for it yet; extending profit_tracks_capital to musharakah needs a dedicated musharakah_khilaf2.fiqh (mirroring how musharakah_khilaf.fiqh already fixtures the diminishing class) before the divergence is added there too. A well-sourced contribution, not an oversight.

Rahn: is the pledge held in trust, or as security for the debt?

A rahn (pledge/collateral) is held by the creditor while the debt is outstanding. The majority, Mālikī, Shāfiʿī, Ḥanbalī, and the two standards bodies, hold it as amāna, a pure trust: the creditor is not liable for its loss absent negligence, and gains nothing from holding it beyond the security itself. The Ḥanafīs hold it as ḍamān, guaranteed up to the value of the debt: if the pledge is lost, the debt is reduced by its value regardless of fault. Both positions keep the creditor from profiting off the pledge; they differ on who bears an accidental loss.

$ deduce check specs/rahn.fiqh --rules aaoifi
✓ consistent

$ deduce check specs/rahn.fiqh --rules hanafi
✗ RAHN-4  pledge liability is declared "amanah"; the Hanafi position holds a rahn as
          daman (guaranteed up to the debt's value), not pure amana.
          al-Kasani, Bada'i' al-Sana'i' [scholar-verify]

Module	Stance on the pledge’s liability
hanafi	ḍamān, guaranteed up to the debt’s value; al-Kāsānī, Badā’i’ al-Ṣanā’i’.
maliki	amāna, a trust; Ibn Rushd, Bidāyat al-Mujtahid.
shafii	amāna; al-Nawawī, al-Majmūʿ.
hanbali	amāna; Ibn Qudāma, al-Mughnī.
aaoifi	the majority position (SS No. 39).
dsn-mui	the majority position (Fatwa No. 25/DSN-MUI/2002).

The canonical rahn.fiqh spec declares liability: amanah, so it deliberately fails under the Ḥanafī module, the same shape as the Mālikī/Shāfiʿī flip on musharakah_mutanaqisah above, not a bug to be quietly fixed. This one is newer and carries a heavier caveat than the diminishing- partnership khilāf: amāna versus ḍamān in rahn is a genuine, live classical disagreement, and promoting it from a code comment (C_RAHN already said this, unencoded, before this pass) into an executable constraint is not the same thing as a scholar’s takhrīj. Ratify before relying on it for anything real.

Honest gaps: when no dedicated standard exists

Several classes have no dedicated AAOIFI Shari’ah Standard or DSN-MUI fatwa, because the contract predates modern standard-setting or sits outside a standards body’s commercial-instrument mandate (inheritance law, gratuitous transfers). Rather than invent a plausible-looking standard number, these carry a classical citation instead, said plainly:

• AAOIFI, no dedicated Standard: wadia (though DSN-MUI does have one: its two 2000 fatwas on giro and tabungan), ariyah (the Prophet ﷺ borrowing armour from Ṣafwān, Sunan Abī Dāwūd), muzaraah (the Khaybar precedent, Ṣaḥīḥ al-Bukhārī/Muslim), hibah (qabḍ completes a gift; the “returns to his vomit” hadith on reclaiming one, al-Bukhārī/Muslim), wasiyya (“the third, and the third is much”; “no bequest to an heir,” Abū Dāwūd, al-Tirmidhī; this is farā’iḍ, outside AAOIFI’s commercial-standard remit by nature, not by omission).
• DSN-MUI, no dedicated fatwa: the same five, plus tawarruq (no dedicated fatwa on tawarruq by name; the nearest structural analogue is Fatwa No. 82/DSN-MUI/2011 on commodity trading, cited as an analogue, not a match) and mudarabah_pool (the base Mudharabah fatwa, No. 07/2000, applied by extension; a real different structure, Mudharabah Musytarakah under Fatwa No. 50/2006, is deliberately not cited here, since it has the muḍārib contribute capital too, which this pooled class does not model).

A handful of further madhhab divergences were considered and explicitly declined, for either of two reasons: no citation held with enough confidence to attribute to a specific school as a school position, or the DSL has no field to express the divergence even with a firm citation. Named briefly, so a future contributor does not have to rediscover them: salam with immediate delivery (salam ḥāll), whether muzāra’a is independently valid without an accompanying musāqāh (a Shāfiʿī validity-level question, not a terms question), Mālikī temporary waqf (waqf mu’aqqat), a borrower’s liability for an ’āriyya destroyed by ordinary use, and a father’s right to revoke a gift to his own child. Each would need either a firmer citation, a new DSL field, or both.

What the engine cannot yet enforce

eval_op supports exactly eq, ne, gt. Several substantive requirements are consequently not expressible as a rule-module constraint today, held back by the checker’s grammar rather than by any gap in the fiqh. Reported honestly rather than faked with a constraint that looks like it works and does not:

Gap	Blocks	What closing it needs
No lt/le	wasiyya’s one-third cap (share_bps <= 3333); a constraint can only assert gt 0, never the ceiling.	add lt/le to eval_op
No cross-field equality	hawala’s transfer.amount == transfer.debt; value in a constraint is always a literal, never another field path.	a new constraint shape, e.g. {field_a, op, field_b}
No OR-of-values	sukuk.income.basis (asset_rental or asset_profit), hibah.gift.transfer (immediate or irrevocable); would also block a Mālikī waqf-mu’aqqat constraint if the citation is ever firmed up.	a {field, op: "in", value: [...]} shape
No pool.* path	sukuk, takaful, mudarabah_pool all declare a pool { ... } section, enforced natively by check_pool, but resolve_field has no arm that reaches it; a rule module cannot require the pool to sum to 10000 bps or hold at least two members.	a pool.sum / pool.count arm in resolve_field
No “declared as a number” op	wakala.agency.fee beyond fee_disclosed’s name-presence check; 0 is a legitimate value (a gratuitous agency), so no literal comparison captures “a number was declared at all.”	an existence/type-check op

None of these block what shipped: every one of the 26 classes still carries at least one, usually two or three, genuinely enforceable field constraint per module. This table is the honest residue after that, and each row is a concrete, scoped engine-work candidate for a contributor who would rather touch sema.rs than fiqh citations.

Ratification: tamper-evidence for a module, not a fork

“Ratification becomes a module, not a fork” is only true if a fork of a ratified module is detectable. A module carries an optional ratification block:

a ratified module (illustrative)

{
  "authority": "AAOIFI", "version": "2017",
  "ratification": {
    "status": "ratified",
    "ratified_by": "the ratifying board or authority",
    "ratification_date": "2027-03-01",
    "sha256_of_module": "…the hash `deduce rules hash` printed at review time…",
    "source_refs": ["AAOIFI Shari'ah Standard No. 12", "al-Baqarah 2:275"]
  },
  "regimes": { "…": {} }
}

The hash is computed over the module’s jurisprudential content (regimes) only, never over the ratification block itself, so recording a ratification can’t change the very hash it pins. deduce rules hash rules/aaoifi.rules.json prints the current value; a ratifying authority reviews the content that hash represents and pastes it in alongside status: "ratified".

deduce rules verify rules/aaoifi.rules.json, and every check/build that loads a module via --rules, then reports:

• RULES-3 (warning, never blocks): no ratification block, or status isn’t "ratified". The module’s verdicts are draft, not compliance-grade. All six modules shipped with Deducible are currently marked "draft": none has actually been reviewed and signed off by a board. That is the honest state, not a placeholder to be quietly flipped later without a real review.
• RULES-2 (error, blocks): status: "ratified" but the content hash is missing, or present and no longer matching. The module was edited after a board signed off on it, or claimed ratification without anything to check it against.

This closes a narrow, mechanical gap: whether the content a board reviewed is the content actually loaded, byte for byte. It does not, and cannot, verify that the JSON is a faithful encoding of the cited fatwa or standard: that translation from text to {field, op, value} is itself a scholar’s judgment call, not a computable property. See the epistemic boundary.

Why this matters

• Pluralism, modelled honestly. Fiqh differs between schools and bodies. The rule module makes the difference explicit and auditable instead of baking one opinion into the tool, across the full catalogue now, not a curated sample of it.
• A clean ratification surface. A Shariʿah-advisory firm ratifies one JSON module, a bounded and reviewable artifact, rather than auditing a compiler. This is the open contribution surface; see Contributing.
• A neutral engine. It enforces whatever the active, human-authored module says, and reports which authority and citation each verdict rests on.

The common-law regime works the same way. commercial_escrow lives under a common_law block in the same module file, with PENALTY-1, CERTAINTY-1, and DISPUTE-1 constraints citing English cases. One engine, a different rule-base.