Module legal_compose 

Composition wires (§17, §19, §26 — legal_logic.md) — wiring existing real primitives into the legal-logic path:

• §17 ZK-gated eligibility — an obligation/permission gated on a zero-knowledge proof (the proof itself is zk_proofs::ZkProofSystem, real Groth16); this is the deontic gate over its verification result + selective disclosure of credential claims.
• §26 proportionality — composes the CAS (specialized_libs::symbolic_algebra): differentiate a harm expression, evaluate the marginal harm, and require it strictly below the advantage (the legal proportionality test).
• §19 sense-translation gate — enforces the Curation Directive on cross-cultural mapping: the machine may propose skos:closeMatch; only a human attests skos:exactMatch; an untranslatable concept routes to human review (never force-flattened).

Enums

Eligibility

Whether a ZK-gated obligation/permission is eligible to apply.

MatchStatus

The status of a cross-cultural / cross-lexical mapping.

Translation

The result of translating a natural-language term to a machine-logic construct.

Functions

anchored_to_instrument

Is a legal composition anchored to a cited instrument at all? (A composition citing 0 is ungrounded and must be routed to human review rather than asserted.)

composition_valid

A composition (and its proportionality test) is valid only when it is anchored to an established human-rights instrument (a non-zero instrument hash) AND is proportionate. This is the structural bind: legal reasoning may not float free of a cited instrument, and a restriction must pass proportionality. (proportionate is the proportionality_met verdict.)

marginal_harm

The marginal harm d/d(wrt) harm_expr evaluated at at — parses + differentiates + evaluates via symbolic_algebra. None if the expression won’t parse/evaluate.

proportionality_met

Proportionality test: an act is proportionate iff its marginal harm is strictly less than the advantage it secures (∂Harm/∂x < Advantage). None if the harm model is unparseable. The legal proportionality / necessity calculus.

selective_disclosure

Selective disclosure: reveal only the chosen reveal claim ids out of all_claims, into out (the rest of the credential graph stays undisclosed). Returns the count. Zero-heap.

translate_via_matrix

Translate a natural-language term to its machine-logic construct via a matrix of (nl_term_hash, machine_construct_hash) rows, gated by the Curation Directive: a mapping is only used if human_attested (the machine may propose, but only a human ratifies a definitive NL→logic equivalence). An unmapped or unattested term routes to human review.

translation_status

Enforce the Curation Directive on a sense mapping: a human attestation yields ExactMatch; absent that, a machine proposal yields CloseMatch; an untranslatable concept (or nothing proposed) yields RequiresHumanReview.

zk_eligibility

Gate an obligation on a ZK proof’s verification result (O(p | ZK(...))). The proof is produced/verified by zk_proofs::ZkProofSystem (real Groth16); this maps that boolean to the deontic eligibility, keeping the attribute value itself private.