Skip to content
DeducibleDeducible

Getting started

The toolchain

Section titled “The toolchain”

The compiler is written in Rust. The brand is Deducible; the CLI binary is deduce. 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 binary is `deduce`
cargo run --bin deduce -- --help

deduce exposes a small set of verbs:

Terminal window
deduce parse  <spec.fiqh>          # show the parsed AST
deduce check  <spec.fiqh>          # run the fiqh invariant engine only
deduce build  <spec.fiqh> --root . # check, then emit Solidity + tests + manifest
deduce nl     <prompt.txt>         # draft a .fiqh from natural language, then re-check it
deduce 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
$ deduce 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
$ deduce check home.fiqh
✗ RIBA-1  38:5  capital is guaranteed to 'bank'; a guaranteed return of capital turns a
                partnership into an interest-bearing loan (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

That is the whole idea. The forbidden contract is not flagged. It cannot be produced.

Build artifacts

Section titled “Build artifacts”

deduce build home.fiqh --root . --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 an authority’s rule-base with --rules aaoifi | dsn-mui | hanafi | maliki | shafii | hanbali. The --rules flag governs both check and build: a spec the chosen authority refuses will not generate a contract.

Next

Section titled “Next”