Skip to content
DeducibleDeducible

Getting started

The toolchain

Section titled “The toolchain”

The compiler, deducible, is written in Rust. Clone it and build:

Terminal window
git clone https://github.com/dihannahdi/deducible
cd deducible/fiqh-compiler


# build & run the test suite
cargo test


# the CLI lives in crates/fiqhc
cargo run --bin deducible -- --help

deducible exposes a small set of verbs:

Terminal window
deducible parse  <spec.fiqh>          # show the parsed AST
deducible check  <spec.fiqh>          # run the fiqh invariant engine only
deducible build  <spec.fiqh>          # check, then emit Solidity + tests + manifest
deducible nl     <prompt.txt>         # draft a .fiqh from natural language, then re-check it
deducible lsp                          # language server (diagnostics in your editor)

Your first spec

Section titled “Your first spec”

A diminishing-partnership home-finance contract, home.fiqh (paste it into the Playground to follow along):

home.fiqh
instrument HomeFinance : musharakah_mutanaqisah {
  meta { basis: "AAOIFI Shari'ah Standard No. 12"; currency: tinybar; }
  parties {
    bank   : financier;
    client : acquirer;
    valuer : oracle independent;
  }
  capital {
    bank   : 8000 bps;
    client : 2000 bps;
    require bank + client == 10000 bps;
  }
  returns {
    rent   { basis: bank.share; rate: 1 per_bps_period; }
    buyout { price: oracle.fairValue * bps; transfers: bank.share -> client.share; }
  }
  risk {
    loss: proportional_to_ownership;
    capital_guarantee: none;
  }
  invariant ownership_conserved  { bank.share + client.share == 10000 }
  invariant loss_follows_capital { loss == proportional_to_ownership }
  invariant role_separation      { valuer != bank }
  lifecycle { fund; payRent; buyShare(bps); settle; }
}

Check it:

Terminal window
$ deducible check home.fiqh
✓ consistent

Now slip in the quiet clause that turns it back into a loan — set capital_guarantee: bank and loss: none:

Terminal window
$ deducible check home.fiqh
✗ RIBA-1  38:5  capital_guarantee returns capital whole regardless of outcome — riba.
                al-Baqarah 2:275 · AAOIFI SS No. 12
✗ RISK-1  37:5  loss must follow ownership (al-ghunm bi-l-ghurm).
  2 errors · no contract emitted
$ echo $?
1

Build artifacts

Section titled “Build artifacts”

deducible build home.fiqh --target all emits, into out/:

Artifact What it is
<Name>Gen.sol a Solidity contract whose invariants mirror the checked rules
<Name>Gen.test.js a Hardhat test asserting those invariants on-chain
<Name>.deploy.json a deploy descriptor (oracle mode, parties, params)
<Name>.manifest.json a portable, ledger-agnostic invariant manifest

Choose a single target with --target solidity | manifest | zk | all, and a jurisdiction’s rule-base with --rules aaoifi | dsn-mui.

Next

Section titled “Next”