version: "1.0.0"
target_crate: forjar
bindings:
- contract: blake3-state-v1.yaml
equation: hash_string
module_path: "forjar::tripwire::hasher::hash_string"
function: hash_string
signature: "fn hash_string(s: &str) -> String"
status: implemented
notes: "Returns 'blake3:' || hex(BLAKE3(s))"
- contract: blake3-state-v1.yaml
equation: hash_file
module_path: "forjar::tripwire::hasher::hash_file"
function: hash_file
signature: "fn hash_file(path: &Path) -> Result<String, String>"
status: implemented
notes: "Streaming 64KB buffer for large files"
- contract: blake3-state-v1.yaml
equation: composite_hash
module_path: "forjar::tripwire::hasher::composite_hash"
function: composite_hash
signature: "fn composite_hash(components: &[&str]) -> String"
status: implemented
notes: "NUL-separated component concatenation"
- contract: dag-ordering-v1.yaml
equation: topological_sort
module_path: "forjar::core::resolver::build_execution_order"
function: build_execution_order
signature: "fn build_execution_order(config: &ForjarConfig) -> Result<Vec<String>, String>"
status: implemented
notes: "Kahn's algorithm with alphabetical tie-breaking"
- contract: dag-ordering-v1.yaml
equation: kahn_sort
module_path: "forjar::core::resolver::kahn_sort"
function: kahn_sort
signature: "fn kahn_sort(resource_ids: &[String], in_degree: &mut HashMap<String, usize>, adjacency: &mut HashMap<String, Vec<String>>) -> Vec<String>"
status: implemented
notes: "Private helper; tested via build_execution_order"
- contract: execution-safety-v1.yaml
equation: atomic_write
module_path: "forjar::core::state::save_lock"
function: save_lock
signature: "fn save_lock(state_dir: &Path, lock: &StateLock) -> Result<(), String>"
status: implemented
notes: "temp + rename pattern; creates parent dirs"
- contract: execution-safety-v1.yaml
equation: jidoka_stop
module_path: "forjar::core::executor::record_failure"
function: record_failure
signature: "fn record_failure(ctx: &mut RecordCtx, resource_id: &str, resource_type: &ResourceType, duration: f64, error: &str) -> bool"
status: implemented
notes: "Private helper; returns should_stop based on FailurePolicy"
- contract: recipe-determinism-v1.yaml
equation: expand_recipe
module_path: "forjar::core::recipe::expand_recipe"
function: expand_recipe
signature: "fn expand_recipe(recipe_id: &str, recipe_file: &RecipeFile, machine: &MachineTarget, provided_inputs: &HashMap<String, Value>, external_depends_on: &[String]) -> Result<IndexMap<String, Resource>, String>"
status: implemented
notes: "Namespaces resource IDs, propagates machine target"
- contract: recipe-determinism-v1.yaml
equation: validate_inputs
module_path: "forjar::core::recipe::validate_inputs"
function: validate_inputs
signature: "fn validate_inputs(recipe: &RecipeMetadata, provided: &HashMap<String, Value>) -> Result<HashMap<String, String>, String>"
status: implemented
notes: "Type-checks all 6 input types (string, int, bool, path, enum, list)"
- contract: recipe-determinism-v1.yaml
equation: validate_input_type
module_path: "forjar::core::recipe::validate_input_type"
function: validate_input_type
signature: "fn validate_input_type(name: &str, type_name: &str, value: &Value, decl: &RecipeInput) -> Result<String, String>"
status: implemented
notes: "Private helper; dispatches to type-specific validation"
- contract: idempotent-apply-v1.yaml
equation: plan_fixed_point
module_path: "forjar::core::planner::plan"
function: plan
signature: "fn plan(config: &ForjarConfig, execution_order: &[String], locks: &HashMap<String, StateLock>, tag_filter: Option<&str>) -> ExecutionPlan"
status: implemented
notes: "Counter-conservation debug_assert; second plan over converged locks yields zero changes"
- contract: idempotent-apply-v1.yaml
equation: hash_determinism
module_path: "forjar::core::planner::hash_desired_state"
function: hash_desired_state
signature: "fn hash_desired_state(resource: &Resource) -> String"
status: implemented
notes: "FJ-2200 determinism debug_assert_eq; stable field order, BLAKE3 over NUL-joined components"
- contract: idempotent-apply-v1.yaml
equation: noop_fixed_point
module_path: "forjar::core::planner::determine_present_action"
function: determine_present_action
signature: "fn determine_present_action(resource_id: &str, resource: &Resource, machine_name: &str, locks: &HashMap<String, StateLock>) -> PlanAction"
status: implemented
notes: "Private helper; FJ-2200 debug_assert enforces converged + matching hash → NoOp"
- contract: plan-apply-equivalence-v1.yaml
equation: plan_determinism
module_path: "forjar::core::planner::plan"
function: plan
signature: "fn plan(config: &ForjarConfig, execution_order: &[String], locks: &HashMap<String, StateLock>, tag_filter: Option<&str>) -> ExecutionPlan"
status: implemented
notes: "Pure function; forjar plan (src/cli/plan.rs) and forjar apply (executor::apply) share it"
- contract: plan-apply-equivalence-v1.yaml
equation: apply_executes_plan
module_path: "forjar::core::executor::apply"
function: apply
signature: "fn apply(cfg: &ApplyConfig) -> Result<Vec<ApplyResult>, String>"
status: implemented
notes: "Executor iterates plan.changes only; outcome-conservation debug_assert in apply_machine"
- contract: plan-apply-equivalence-v1.yaml
equation: noop_no_execution
module_path: "forjar::core::executor::apply_single_resource"
function: apply_single_resource
signature: "fn apply_single_resource(cfg: &ApplyConfig, change: &PlannedChange, machine: &Machine, ctx: &mut RecordCtx, converged_resources: &HashSet<String>) -> Result<ResourceOutcome, String>"
status: implemented
notes: "Private helper; planned NoOp without force/trigger short-circuits to Unchanged"
- contract: destroy-undo-roundtrip-v1.yaml
equation: snapshot_generation
module_path: "forjar::cli::generation::create_generation"
function: create_generation
signature: "fn create_generation(state_dir: &Path, config_path: Option<&Path>) -> Result<u32, String>"
status: implemented
notes: "FJ-1386; monotonic numbering, atomic current-symlink switch, debug_assert on current"
- contract: destroy-undo-roundtrip-v1.yaml
equation: restore_generation
module_path: "forjar::cli::generation::rollback_to_generation"
function: rollback_to_generation
signature: "fn rollback_to_generation(state_dir: &Path, generation: u32, yes: bool) -> Result<(), String>"
status: implemented
notes: "Restores snapshot then atomically re-points current; debug_assert on current"
- contract: destroy-undo-roundtrip-v1.yaml
equation: undo_roundtrip
module_path: "forjar::cli::undo::cmd_undo"
function: cmd_undo
signature: "fn cmd_undo(file: &Path, state_dir: &Path, generations: u32, machine_filter: Option<&str>, dry_run: bool, yes: bool) -> Result<(), String>"
status: implemented
notes: "FJ-2003; targets current − n, rejects impossible targets, re-applies to converge"
- contract: codegen-dispatch-v1.yaml
equation: check_script
module_path: "forjar::core::codegen::check_script"
function: check_script
signature: "fn check_script(resource: &Resource) -> Result<String, String>"
status: implemented
notes: "Dispatches to resource-specific check handlers"
- contract: codegen-dispatch-v1.yaml
equation: apply_script
module_path: "forjar::core::codegen::apply_script"
function: apply_script
signature: "fn apply_script(resource: &Resource) -> Result<String, String>"
status: implemented
notes: "Dispatches to resource-specific apply handlers"
- contract: codegen-dispatch-v1.yaml
equation: state_query_script
module_path: "forjar::core::codegen::state_query_script"
function: state_query_script
signature: "fn state_query_script(resource: &Resource) -> Result<String, String>"
status: implemented
notes: "Dispatches to resource-specific state query handlers"
- contract: overlay-interface-v1.yaml
equation: emit_service_unit
module_path: "forjar::resources::overlay_interface::apply_script"
function: apply_script
signature: "fn apply_script(resource: &Resource) -> String"
status: implemented
notes: "Plain Type=oneshot; NEVER RemainAfterExit (timer restart re-runs ExecStart)"
- contract: overlay-interface-v1.yaml
equation: emit_timer_unit
module_path: "forjar::resources::overlay_interface::apply_script"
function: apply_script
signature: "fn apply_script(resource: &Resource) -> String"
status: implemented
notes: "OnCalendar=minutely + RandomizedDelaySec=30 + AccuracySec=1s; never OnUnitActiveSec (MUST-4)"
- contract: overlay-interface-v1.yaml
equation: dad_before_bind
module_path: "forjar::resources::overlay_interface::apply_script"
function: apply_script
signature: "fn apply_script(resource: &Resource) -> String"
status: implemented
notes: "RFC 5227 arping -D probe precedes ip addr add; loud refusal + nonzero exit on a reply (MUST-1)"
- contract: overlay-interface-v1.yaml
equation: status_heartbeat
module_path: "forjar::resources::overlay_interface::apply_script"
function: apply_script
signature: "fn apply_script(resource: &Resource) -> String"
status: implemented
notes: "Writes /run/fleet-overlay/status.json each run; monotonic repair_count; nonzero exit on persistent-absent (MUST-2)"
- contract: overlay-interface-v1.yaml
equation: overlay_ip_injective
module_path: "forjar::core::parser::resource_types::validate_overlay_ip_injective"
function: validate_overlay_ip_injective
signature: "fn validate_overlay_ip_injective(config: &ForjarConfig, errors: &mut Vec<ValidationError>)"
status: implemented
notes: "Plan/validate-time duplicate overlay_ip rejection; names both resource ids (MUST-1)"
- contract: overlay-interface-v1.yaml
equation: hash_overlay_hosts_sensitive
module_path: "forjar::core::planner::hash_desired_state"
function: hash_desired_state
signature: "fn hash_desired_state(resource: &Resource) -> String"
status: implemented
notes: "overlay_hosts folded into the desired-state hash (order-independent); MATERIAL FIX so plan never false-NoOps a changed /etc/hosts block"
- contract: overlay-interface-v1.yaml
equation: apply_idempotent
module_path: "forjar::resources::overlay_interface::state_query_script"
function: state_query_script
signature: "fn state_query_script(resource: &Resource) -> String"
status: implemented
notes: "Heartbeat class (fresh/stale/missing) on stdout (drift-visible); raw monotonic values to stderr to avoid false drift; re-run is a plan-level NoOp"
- contract: provable-iac-v1.yaml
equation: provability
module_path: "forjar::core::prove::prove"
function: prove
signature: "fn prove(cfg: &ForjarConfig, file: &str) -> ProofReport"
status: implemented
- contract: provable-iac-v1.yaml
equation: provability
module_path: "forjar::core::prove::checkers::acyclicity"
function: acyclicity
signature: "fn acyclicity(cfg: &ForjarConfig) -> InvariantResult"
status: implemented
- contract: provable-iac-v1.yaml
equation: provability
module_path: "forjar::core::prove::checkers::conflict_freedom"
function: conflict_freedom
signature: "fn conflict_freedom(cfg: &ForjarConfig) -> InvariantResult"
status: implemented
- contract: provable-iac-v1.yaml
equation: provability
module_path: "forjar::core::prove::has_conflict"
function: has_conflict
signature: "fn has_conflict(keys: &[u64]) -> bool"
status: implemented
- contract: provable-iac-v1.yaml
equation: provability
module_path: "forjar::core::prove::plan_hash"
function: plan_hash
signature: "fn plan_hash(cfg: &ForjarConfig) -> String"
status: implemented
- contract: apply-receipt-v1.yaml
equation: receipt_completeness
module_path: "forjar::core::executor::resource_ops::displaced_hash"
function: displaced_hash
signature: "fn displaced_hash(previous: Option<ResourceLock>) -> Option<String>"
status: implemented
notes: "The before-side of a converge. `BTreeMap::insert` returns the displaced
entry, so this costs no extra read. An empty stored hash collapses to None —
a recorded failure is not a previous state. Falsifiers RCP-006/007/008, all
three confirmed RED under mutation."
- contract: apply-receipt-v1.yaml
equation: receipt_completeness
module_path: "forjar::tripwire::eventlog::append_event"
function: append_event
signature: "fn append_event(state_dir: &Path, machine: &str, event: ProvenanceEvent) -> Result<(), String>"
status: implemented
notes: "Deletion is now representable via ProvenanceEvent::ResourceDeleted and
round-trips to the log. paiml/infra#208 is a deletion — every real file under
~/.cargo/bin removed, every symlink left — so the one event class that would
have named it did not exist. Falsifier RCP-001.
This entry named `receipt_deletion` until #298. apply-receipt-v1.yaml has
never defined that equation, and nothing noticed, because verify_bindings
reads `status:` and never opens the contract. Deletion representability is
part of receipt_completeness, whose invariants are `action IN {created,
changed, deleted, unchanged, failed}` and `action = deleted => after_digest
= null AND before_digest != null`."
- contract: plan-declares-its-quantifier-v1.yaml
equation: plan_ranges_over_config_and_lock_only
module_path: "forjar::core::planner::plan"
function: plan
signature: "fn plan(config: &ForjarConfig, order: &[String], locks: &HashMap<String, StateLock>, tag: Option<&str>) -> ExecutionPlan"
status: implemented
notes: "Takes no Machine and opens no transport, so the invariance in target
state is structural rather than asserted. Stated so that making plan
host-aware has to contradict a written equation instead of quietly
widening the domain."
- contract: plan-declares-its-quantifier-v1.yaml
equation: disclosure_is_a_function_of_unconsulted_observations
module_path: "forjar::cli::print_helpers::unconsulted_observations"
function: unconsulted_observations
signature: "fn unconsulted_observations(locks: &HashMap<String, StateLock>) -> usize"
status: implemented
notes: "Counts lock entries whose observed_state() is Some — what plan is
BLIND TO, never what has drifted. Establishing drift requires reaching the
machine, which is drift's job; a count presented as 'N drifted' would be
the same defect this contract exists to prevent."
- contract: plan-declares-its-quantifier-v1.yaml
equation: disclosure_is_a_function_of_unconsulted_observations
module_path: "forjar::cli::plan_json::print_plan_json"
function: print_plan_json
signature: "fn print_plan_json(plan: &ExecutionPlan, config: &ForjarConfig, unconsulted: usize) -> Result<(), String>"
status: implemented
notes: "forjar#342 residual. The MACHINE-READABLE surface, and the one the
issue's motivating incident actually ran through — a nightly lane parsing
forjar output. Emits `lock_relative` and `unconsulted_observations`
unconditionally so a parser has a total function, and `disclosure` only
when the count is non-zero, which is the biconditional itself."
- contract: plan-declares-its-quantifier-v1.yaml
equation: disclosure_is_a_function_of_unconsulted_observations
module_path: "forjar::mcp::handlers::PlanHandler"
function: handle
signature: "async fn handle(&self, input: PlanInput) -> Result<PlanOutput>"
status: implemented
notes: "forjar#342 residual. One PlanOutput serves the CLI `verb call`, MCP
stdio and HTTP transports (src/verb/registry.rs), so this row covers three
surfaces. The count ranges over the locks the handler planned over — the
same convention `load_machine_locks` uses on the CLI, so the two agree by
construction rather than by coincidence."
- contract: plan-declares-its-quantifier-v1.yaml
equation: disclosure_names_the_command_that_can_answer
module_path: "forjar::cli::print_helpers::print_scope_disclosure"
function: print_scope_disclosure
signature: "fn print_scope_disclosure(unconsulted: usize)"
status: implemented
notes: "Names `forjar drift` in the disclosure. Telling an operator an
answer is incomplete without telling them how to complete it converts a
silent gap into a loud one and stops there. The sentence itself now lives
in `scope_disclosure`, which RETURNS it, so the machine-readable surfaces
serialise the same text rather than reimplementing it."
- contract: apply-converges-observed-drift-v1.yaml
equation: live_oracle_is_read
module_path: "forjar::tripwire::drift::detect_drift_full"
function: detect_drift_full
signature: "fn detect_drift_full(lock: &StateLock, machine: &Machine, resources: &IndexMap<String, Resource>) -> Vec<DriftFinding>"
status: implemented
notes: "detect_nonfile_drift no longer excludes ResourceType::File, so the
live_hash written on every apply is finally read. That hash comes from
state_query_script run ON THE TARGET and covers content+owner+group+mode+
existence — strictly stronger than the controller-side, bytes-only,
content-only content_hash it was passed over for. 320 of 329 locked file
resources on the paiml fleet had no content_hash at all. Falsifier
CONV-001, probed: restoring the exclusion takes the matrix 9/9 → 4/9."
- contract: apply-converges-observed-drift-v1.yaml
equation: apply_reads_what_drift_reads
module_path: "forjar::cli::apply_drift::check_pre_apply_drift"
function: check_pre_apply_drift
signature: "fn check_pre_apply_drift(config: &ForjarConfig, state_dir: &Path, machine_filter: Option<&str>, force: bool, verbose: bool) -> Result<(), String>"
status: implemented
notes: "Private to cli::apply. Now calls detect_drift_full — the same entry
point cli/drift.rs uses — instead of the narrower detect_drift_with_machine.
Without this the fix lands only in the reporting command and apply keeps
printing `unchanged` while `drift` prints DRIFTED. Falsifier CONV-004."
- contract: apply-converges-observed-drift-v1.yaml
equation: observed_drift_plans_update
module_path: "forjar::core::planner::determine_present_action"
function: determine_present_action
signature: "fn determine_present_action(resource_id: &str, resource: &Resource, machine_name: &str, locks: &HashMap<String, StateLock>) -> PlanAction"
status: implemented
notes: "No planner change was needed: it already maps any non-Converged status
to Update (`Previously failed or drifted`). ResourceStatus::Drifted was
DEFINED AND NEVER WRITTEN — check_pre_apply_drift now writes it and persists
the lock. Shares determine_present_action with idempotent-apply-v1, and the
two constrain it in opposite directions on purpose. Falsifier CONV-002."
- contract: apply-converges-observed-drift-v1.yaml
equation: directory_identity_excludes_entry_count
module_path: "forjar::resources::file::state_query_script"
function: state_query_script
signature: "fn state_query_script(resource: &Resource) -> String"
status: implemented
notes: "Branches on `[ -d ]` and omits stat's size= for directories. THE
ANTI-BRICK BINDING: a directory's size tracks its entry count (measured
4096 → 12288 at 400 entries), so without this the live_hash comparison marks
every managed directory permanently drifted and, once the apply gate reads
drift, permanently un-appliable. Falsifier CONV-003."