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 is assumed. You need only be able to 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 for a green ✓ consistent. Pick Disguised loan for a 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 is Rust, and its binary is deduce. 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 deduce -- --help      # the CLI

You now have deduce 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, since the valuer may not be the bank). capital sets the split. returns says rent prices the bank’s living share rather than 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

$ deduce 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;

$ deduce check home.fiqh
✗ RIBA-1  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  loss must follow ownership (al-ghunm bi-l-ghurm).
  2 errors · no contract emitted

You cannot produce this contract. It does not warn you. deduce build emits nothing and exits 1. Revert the two lines before continuing.

Step 5: build it

$ deduce build home.fiqh --root . --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, and the rest) make cross-role calls revert. The valuer cannot settle, the bank cannot 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 around 40 ℏ for a small contract; the cost is dominated by bytecode upload, and msg.value is in tinybar. The full cost and gas breakdown, with what has already been proven live (a murābaḥah running its full lifecycle, a partnership that cannot exit whole, zakat paid to the cent), is in Live on Hedera.

Where to go next

The whole catalogue. Every contract class, family by family, lives in the instrument catalogue.
Change the rules, not the engine. Rule modules show the same spec consistent under one school and refused under another.
Embed the engine. The FFI, Wasm, LSP, and 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.