Function check_contracts 

pub fn check_contracts(
    requires: &[Contract],
    ensures: &[Contract],
    param_scope: &HashMap<String, TyId>,
    result_ty: TyId,
    has_result_param: bool,
    fn_label: &str,
    input: &ResolvedCommons,
    expr_types: &mut HashMap<ExprId, TypedExpr>,
    errors: &mut Vec<CompileError>,
    refs: &mut RefSink,
    hints: &mut HintSink,
    locals: &mut LocalsSink,
    requirements: &mut RequirementSink,
    callees: &mut HashMap<ExprId, Callee>,
    type_vars: &HashSet<String>,
    tys: &Types,
)

Check a function’s contract clauses (v0.115 §, testing track slice 3). A contract is the invariant predicate attached to a function (ADR 0144 — one predicate surface): each requires/ensures is a pure Bool-typed expression, requires over the parameters and ensures over the parameters plus result (the return value; the awaited element for an Effect). The pass enforces, mirroring check_invariants:

• bynk.contract.duplicate_name — two clauses (across requires/ensures) share a name; the name rides the failure report and dedup.
• bynk.contract.result_in_requires — a precondition references result (the return value is not yet bound on entry).
• bynk.contract.impure_predicate — a clause uses an effectful or test-only construct (Effect, ? propagation, expect, Val).
• bynk.contract.not_bool — a clause does not type to Bool.

Distinct from ADR 0127’s capability @requires annotation.