Codegen & manifest

Once sema proves a spec consistent, codegen lowers it. Codegen is multi-target and deterministic — the same spec always produces the same bytes.

deducible build <spec> --target solidity | manifest | zk | all   # default: all

Target	Output
`solidity`	`<Name>Gen.sol` + `<Name>Gen.test.js` (Hardhat) + `<Name>.deploy.json`
`manifest`	`<Name>.manifest.json` — portable, ledger-agnostic invariant set
`zk`	a Circom circuit + a Groth16 (snarkjs) manifest + a `settleWithProof()` gate
`all`	all of the above

Invariant → Solidity

Each checked invariant becomes an enforced mechanism in the generated contract, not a comment. The mapping is intentionally narrow and auditable:

Invariant (sema)	Solidity mechanism
`RISK-1` proportional loss	`settle()` pays each partner its share of the current oracle value from an escrowed pool — loss is borne by transfer, not emitted as an event
`RIBA-1` no capital guarantee	absence of any code path that returns a fixed principal; no guarantee state variable can be expressed
role separation (anti-self-dealing)	per-role modifiers (`onlyBank`, `onlyArbiter`, …); cross-role calls revert
oracle / `GHARAR-1`	constructor wires `IValuationOracle`; `fairValue()` reverts when value is majhul
`ZAKAT-1`	`payZakat()` routes exactly 250 bps of the base to the existing maslahah fund
`CONT-1` jawa’ih	`declareJaaihah()` drives `effectiveRentDue → 0` while `rentDue` is unchanged (abatement, not deferral)
`CONT-2` faraid	`dissolveByFaraid(heirs, bps)` validates `Σ bps == 10000` then distributes by transfer

Two structural guarantees hold for every generated contract, checked by tests/codegen_safety.rs:

every external/public function containing .call{value:} carries nonReentrant (internal helpers are exempt);
role modifiers, a pinned pragma, and @dev INVARIANT: annotations are present.

This is a property over the generator, so it holds for instruments not yet written.

Consensus valuation oracle (gharar as a computed quantity)

The single trusted valuer is itself a source of gharar. The oracle { mode: consensus; … } section generates a ConsensusValuationOracle implementing IValuationOracle (so it drops into any instrument). The relayer is trusted with nothing:

attest   each committee member signs  keccak256(round, value, oracle, chainId)
verify   oracle ecrecovers the signer and checks committee membership (sig-based; no funded accounts)
value    fairValue() = median of attestations lying within ±gharar_bound_bps of the median
revert   if fewer than `quorum` attestations agree within the band:
         the value is majhūl → fairValue() REVERTS

So gharar stops being a hidden assumption and becomes an on-chain quantity: dispersion beyond the band, or agreement below quorum, makes the value formally unknowable and the call fails closed. Compile-time guards: ORACLE-1 quorum ≤ committee; ORACLE-2…5 gharar_bound_bps ∈ (0, 10000) and committee/quorum well-formed. Off-chain, independent agents each reason a value over their own comparables and sign with an ephemeral key — convergent committees drive a lifecycle; divergent ones revert.

The invariant manifest

The manifest is the ledger-agnostic core: the same facts sema checked, serialised as machine-checkable constraints, independent of Solidity or any chain.

{
  "contract": "musharakah_mutanaqisah",
  "regime": "islamic",
  "authority": "AAOIFI",
  "constraints": [
    { "code": "RISK-1",  "field": "loss_share",        "op": "eq", "value": "by_ownership",
      "citation": "AAOIFI SS No. 12" },
    { "code": "RIBA-1",  "field": "capital_guarantee", "op": "eq", "value": false,
      "citation": "al-Baqarah 2:275" },
    { "code": "ZAKAT-1", "field": "zakat.rate_bps",     "op": "eq", "value": 250,
      "citation": "al-Tawbah 9:103" }
  ]
}

op is one of eq | ne | gt | lt | ge | le. The manifest is consumed by the invariant gateway: POST /enforce {target, terms} evaluates a flat dotted-key terms object against the constraints and returns allow/deny with the cited violations — enforcement without re-running the compiler, in any runtime.

Deploy descriptor

<Name>.deploy.json is what the Node deploy runner consumes: constructor params, oracle mode (single or consensus with committee/quorum/gharar_bound_bps), party roles, and the opted-in section config (zakat beneficiary, contingency flags). The runner (scripts/deploy_generated.js) reads it and drives a ContractCreateFlow.

ZK target

--target zk emits a Circom circuit whose private witnesses are the loss amounts and whose public constraints encode INV-1 + RISK-1 as R1CS, a Groth16 manifest describing the snarkjs pipeline, and a Solidity settleWithProof() that gates settlement on a verified proof. See Concealment for the protocol. The circuit is emitted but not yet compiled in-container (no circom toolchain); the sigma-protocol PoC in zk.rs proves the math.