Function check_inputs_closed

zisk/host/src/main.rs:639–684

Pre-flight closure check for `--require-closed`. Bails unless every typing dependency of every constant the batch will certify is itself either (a) certified somewhere in this batch (any input's work items), or (b) already in the on-disk `store` (a prior proof — re-verified and folded at aggregation). Axioms need no special case: they are themselves work items, so they land in (a) as certified dec

(
  inputs: &[Option<PathBuf>],
  store: &std::collections::HashSet<[u8; 32]>,
)

    for w in work {
      for t in w.proven_targets() {
        certified.insert(*t.as_bytes());
      }
    }
  }

  // Every non-blob ref of every certified constant must be in `certified`.
  let mut missing: Vec<(String, Address)> = Vec::new();
  let mut axioms = 0usize;
  let mut checked = 0usize;
  for (label, env, work) in parsed {
    for w in work {
      for t in w.proven_targets() {
        let Some(c) = env.get_const(&t) else { continue };
        if matches!(&c.info, ConstantInfo::Axio(_)) {
          axioms += 1;
        }
        checked += 1;
        for r in &c.refs {
          if env.get_blob(r).is_some() {
            continue;
          }
          if !certified.contains(r.as_bytes()) {
            missing.push((label.clone(), r.clone()));
          }
        }
      }
    }
  }
  (missing, checked, axioms)
}

/// Pre-flight closure check for `--require-closed`. Bails unless every typing
/// dependency of every constant the batch will certify is itself either
/// (a) certified somewhere in this batch (any input's work items), or (b)
/// already in the on-disk `store` (a prior proof — re-verified and folded at
/// aggregation). Axioms need no special case: they are themselves work items,
/// so they land in (a) as certified declarations, and their inhabitation is the
/// irreducible "modulo axioms" residual. Literal blob refs (Nat/Str data) are
/// well-typed by construction and never count.
///
/// Sound under the store-closure invariant: a constant enters the store only
/// via a run, so if every run uses `--require-closed` the store is itself
/// closed and (b) holds transitively. Store entries' own refs aren't re-checked
/// here (their definitions live in other envs), but aggregation re-verifies the
/// covering proofs that certified them.
fn check_inputs_closed(
  inputs: &[Option<PathBuf>],
  store: &std::collections::HashSet<[u8; 32]>,
) -> Result<()> {