Zero to a checked contract

By the end of this you will have written a .fiqh spec, watched the compiler refuse a disguised loan, compiled a compliant one to Solidity, and read the generated contract well enough to deploy it. No prior fiqh or Rust knowledge assumed — only that you can run a terminal.

Step 0 — Try it with zero install

Open the Playground. It runs the real engine (as WebAssembly) in your browser. Pick Musharakah — green ✓ consistent. Pick Disguised loan — red ✕ refused, with cited diagnostics. That refusal is the whole idea; the rest of this tutorial is you reproducing it locally and turning the green one into a real contract.

Step 1 — Get the toolchain

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

git clone https://github.com/dihannahdi/deducible
cd deducible/fiqh-compiler
cargo test                       # build + run the suite (should be all green)
cargo run --bin deducible -- --help     # the CLI

You now have deducible with the verbs parse, check, build, nl, lsp, fuzz.

Step 2 — Write a spec

Create 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; }
}

Each block has a job: parties assigns roles (note valuer : oracle independent — the valuer may not be the bank), capital sets the split, returns says rent prices the bank’s living share (not the principal) and the buyout tracks the oracle, risk ties loss to ownership and guarantees nothing, and the invariants make those promises machine-checkable.

Step 3 — Check it

$ deducible check home.fiqh
✓ consistent

The engine ran every invariant for the musharakah_mutanaqisah class and found no violation.

Step 4 — Break it (the lesson)

Turn the partnership back into a loan. Change two lines:

loss: proportional_to_ownership;
capital_guarantee: none;
loss: none;
capital_guarantee: bank;

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

You cannot produce this contract. Not “it warns you” — deducible build emits nothing and exits 1. Revert the two lines before continuing.

Step 5 — Build it

$ deducible build home.fiqh --target all
  → out/HomeFinanceGen.sol
  → out/HomeFinanceGen.test.js
  → out/HomeFinance.deploy.json
  → out/HomeFinance.manifest.json

Four artifacts: the Solidity contract, a Hardhat test asserting the invariants on-chain, a deploy descriptor, and the portable invariant manifest.

Step 6 — Read what it generated

The invariants are not comments in the output — they are mechanisms. In HomeFinanceGen.sol:

settle() pays each partner its share of the current oracle value from an escrowed pool — so a loss is borne by transfer, enforcing RISK-1. There is no code path that returns a fixed principal, which is how RIBA-1 is enforced (the guarantee is unrepresentable).
role modifiers (onlyBank, onlyValuer, …) make cross-role calls revert — the valuer can’t settle, the bank can’t attest.
every external function that moves value carries nonReentrant (a property the codegen-safety test enforces across all generated contracts).

Run the generated test on a local EVM to see the invariants hold:

npx hardhat test

Step 7 — Deploy (testnet)

The deploy descriptor drives a Hedera ContractCreateFlow:

node scripts/deploy_generated.js out/HomeFinance.deploy.json

Budget ~40 ℏ for a small contract; the cost is dominated by bytecode upload, and msg.value is in tinybar. The full cost and gas breakdown — and what’s already been proven live (a partnership that can’t exit whole; zakat paid to the cent) — is in Live on Hedera.

Where to go next

Change the rules, not the engine — Rule modules: see the same spec pass under AAOIFI but get refused under DSN-MUI.
Add another instrument — study mudarabah / ijarah_imbt in the Playground, then write your own class.
Embed the engine — the FFI / Wasm / LSP / gateway surfaces let it run inside a core-banking stack, a browser, or a CI gate.
Understand the surrounding fiqh — the five C’s and their algorithms.