Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,10 @@ begin.

### Added

- Added a verified, non-cloneable target-instance lifecycle that binds adapter, target-build,
owner-attempt, and bounded instance identity; admits only typed prepare, execute, reset, cleanup,
and discard transitions; prevents execution reuse before a confident reset; and now surrounds
the real Linux CLI adapter with correlated prepared, executing, and cleaned/discarded events.
- Completed the §§71–80 control-plane slice: a verified bounded scheduler; portable storage
interfaces and conservative collection; schema-version-4 domain, replay, scenario, and
persistence records; the full initial CLI grammar; fact-separated portable reports; five-seed
Expand Down
4 changes: 3 additions & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -69,13 +69,15 @@ explicit Verus verification targets rather than delegated to an external YAML pa
| Evidence and provenance graph | Verified structural admission, append-only/idempotent transitions, borrowed retries, normative edge direction, and atomic multi-input derivations, with schema-version-4 SQLite persistence and bounded report projections. |
| Trusted-boundary enforcement | Verified scanner/reconciliation, approved baseline, and CI known-defect fixture |
| Crucible YAML and configuration | The verified profile-1 pipeline covers bounded decoding, lexical analysis, CST formation, semantic resolution, alias/tag handling, duplicate rejection, merge expansion, canonical DAG lowering, typed schema compilation, kind binding, and lossless recognized/unknown mapping partitioning. The Verus-written schema-version-1 bridge recursively validates the complete declared field tree, enforces execution-facing invariants, emits deterministic canonical YAML, authenticates source and canonical bytes with project-owned SHA-256, and powers `crucible config validate` and `config canonicalize`. Its current public proof authenticates versions, caller-lowered bounds, charged work, and both digests; the exact executable-to-pure proof of field preservation, canonical serialization, and all execution invariants required by §12.2 remains committed depth work after the runnable product spine, alongside broader YAML conformance, self-fuzzing, migrations, and compatibility-mode CLI exposure |
| Execution and evidence core | Portable raw execution outcomes now have independent completion/termination/events, every platform-specific variant, caller-lowered event/extension caps, exact stable tags, a bounded canonical version-1 byte codec, typed malformed-input diagnostics, preserved rejection bytes, and Verus semantic-validation contracts. Immutable raw observations retain typed identities, exact stream truncation accounting, portable resource evidence, versioned extensions, independent caps, and canonical full-field round trips. The first Linux CLI adapter executes direct argv through bubblewrap/prlimit without a target-visible host control mount, drains bounded streams, terminates the process group at timeout, and transactionally persists observations or disjoint harness failures. A pure proof binding accepted observation bytes to the exact decoded value and additional platform/input adapters remain required depth and breadth |
| Execution and evidence core | Portable raw execution outcomes now have independent completion/termination/events, every platform-specific variant, caller-lowered event/extension caps, exact stable tags, a bounded canonical version-1 byte codec, typed malformed-input diagnostics, preserved rejection bytes, and Verus semantic-validation contracts. Immutable raw observations retain typed identities, exact stream truncation accounting, portable resource evidence, versioned extensions, independent caps, and canonical full-field round trips. A verified non-cloneable target-instance lifecycle preserves adapter/build/owner identity, requires reset before reuse, and discards uncertain instances. The first Linux CLI adapter executes direct argv through bubblewrap/prlimit under that lifecycle without a target-visible host control mount, drains bounded streams, terminates the process group at timeout, and transactionally persists observations or disjoint harness failures. A pure proof binding accepted observation bytes to the exact decoded value and additional platform/input adapters remain required depth and breadth |
| Bug-finding engines and target adapters | The bounded seven-class scheduler, Linux local CLI adapter, process-exit oracle, finding persistence/deduplication, inspection, replay sampling, aggregate high-throughput fuzz retention, and known-defect rediscovery are operational. Native fuzzers, specialized engine execution, successful reducers, and the remaining target/platform adapters stay in their later owning phases. |

The complete specification is organized through the [normative specification index](crucible.md).
The delivery sequence and current milestone are summarized in [ROADMAP.md](ROADMAP.md). The accepted
§§71–80 units are listed in the
[scheduling/storage/CLI/reporting work-slice ledger](docs/work-slices/scheduling-storage-cli-reporting.md).
Phase 1 execution-core ownership and remaining acceptance units are listed in the
[Phase 1 work-slice ledger](docs/work-slices/phase-1-execution-core.md).
Release staging controls order, not the committed end-state scope.

## Design principles
Expand Down
7 changes: 7 additions & 0 deletions ROADMAP.md
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,13 @@ streaming corpus ingestion, native fuzzers, minimization reducers, additional pl
scenario execution remain governed by their owning specification sections. Delivery order changes
do not remove an acceptance criterion or later capability.

Phase 1 execution-core breadth and exit acceptance are divided into the all-or-nothing units in
[the Phase 1 work-slice ledger](docs/work-slices/phase-1-execution-core.md). The existing Linux
direct-argument boundary and common exclusive adapter lifecycle are accepted; all input-delivery
modes, cancellation and terminal-path cleanup, executor identity completion, macOS and Windows
backends, architecture conformance, and corpus-level phase acceptance remain planned until their
complete evidence gates pass.

Current work establishes and extends:

- public project governance and contribution processes;
Expand Down
44 changes: 42 additions & 2 deletions crates/crucible-cli/src/local_run.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,9 @@ use crate::{EffectiveExecutionConfiguration, MAX_LOCAL_ARTIFACT_BYTES};
use crucible_core::{
canonical_raw_observation_limits, validate_raw_observation, ArtifactRef, CapturedStreamRef,
CompletionDisposition, HarnessTerminationReason, RawExecutionEvent, RawExecutionOutcome,
RawObservation, RecordedDuration, ResourceSnapshot, RunAttemptId, RunId, TerminationRecord,
ValidatedRawObservation,
RawObservation, RecordedDuration, ResourceSnapshot, RunAttemptId, RunId, TargetAdapterIdentity,
TargetAdapterKind, TargetBuildId, TargetId, TargetInstanceLifecycle, TargetLifecycleAction,
TargetLifecycleError, TerminationRecord, ValidatedRawObservation,
};
#[expect(
unused_imports,
Expand Down Expand Up @@ -1863,4 +1864,43 @@ pub fn build_local_raw_observation(
}
}

pub fn prepare_local_cli_target_instance(
plan: &LocalExecutionPlan,
target_id: TargetId,
target_build_id: TargetBuildId,
owner_attempt_id: RunAttemptId,
instance_ordinal: u64,
) -> (result: Result<TargetInstanceLifecycle, TargetLifecycleError>)
requires
local_execution_plan_well_formed_spec(plan@),
ensures
match &result {
Ok(instance) => {
crucible_core::target_adapter::target_instance_lifecycle_well_formed_spec(instance@)
&& instance@.adapter.kind == TargetAdapterKind::Cli && instance@.adapter.version
== 1 && instance@.target_id == target_id@ && instance@.target_build_id
== target_build_id@ && instance@.owner_attempt_id == owner_attempt_id@
&& instance@.instance_ordinal == instance_ordinal && instance@.state
== crucible_core::TargetLifecycleState::Prepared
},
Err(_) => true,
},
{
let adapter_kind = match plan.backend() {
LocalExecutionBackend::LinuxBubblewrapPrlimitV1 => TargetAdapterKind::Cli,
};
let adapter = TargetAdapterIdentity::new(adapter_kind, 1)?;
let allocated = TargetInstanceLifecycle::new(
adapter,
target_id,
target_build_id,
owner_attempt_id,
instance_ordinal,
)?;
crucible_core::advance_target_instance_lifecycle(
allocated,
TargetLifecycleAction::PrepareSucceeded,
)
}

} // verus!
157 changes: 140 additions & 17 deletions crates/crucible-cli/src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -12,27 +12,28 @@ use crucible_cli::{
inspection_observation_codec_limits, local_capability_manifest, metadata_table_sql,
migration_checksum, migration_table_sql, object_address_for_artifact,
object_address_matches_id, parse_cli_args, prepare_artifact_publication,
prepare_local_execution, render_run_inspection_report, run_migration_checksum,
run_migration_name, run_migration_sql, stored_artifact_is_exact, target_build_manifest,
validate_configuration, validate_local_capability_probe, validate_run_inspection,
ArtifactStoreError, CapturedOutput, CliAction, CliParseError, ConfigurationError,
ConfigurationErrorKind, DatabaseSnapshot, InitializationDecision, InitializationError,
InspectionArtifactError, InspectionControls, InspectionHarnessFailure, InspectionObservation,
InspectionPreviews, InspectionReportError, InspectionStatus, InspectionTarget,
InspectionValidationError, LocalExecutionClassificationError, LocalExecutionPlan,
LocalNetworkPolicy, LocalOracleVerdict, LocalRunPlanError, LocalRuntimeIdentity,
LocalTermination, MigrationRecord, ObjectAddress, PathKind, PreparedArtifactPublication,
RawLocalExecution, ReportFormat, ReservedRun, RunAttemptStatus, RunInspectionSnapshot,
RunStoreTransition, StoredArtifactSnapshot, WorkspaceMetadata, WorkspaceSnapshot,
MAX_CLI_ARGUMENTS, MAX_CLI_ARGUMENT_BYTES, MAX_CONFIGURATION_SOURCE_BYTES,
prepare_local_cli_target_instance, prepare_local_execution, render_run_inspection_report,
run_migration_checksum, run_migration_name, run_migration_sql, stored_artifact_is_exact,
target_build_manifest, validate_configuration, validate_local_capability_probe,
validate_run_inspection, ArtifactStoreError, CapturedOutput, CliAction, CliParseError,
ConfigurationError, ConfigurationErrorKind, DatabaseSnapshot, InitializationDecision,
InitializationError, InspectionArtifactError, InspectionControls, InspectionHarnessFailure,
InspectionObservation, InspectionPreviews, InspectionReportError, InspectionStatus,
InspectionTarget, InspectionValidationError, LocalExecutionClassificationError,
LocalExecutionPlan, LocalNetworkPolicy, LocalOracleVerdict, LocalRunPlanError,
LocalRuntimeIdentity, LocalTermination, MigrationRecord, ObjectAddress, PathKind,
PreparedArtifactPublication, RawLocalExecution, ReportFormat, ReservedRun, RunAttemptStatus,
RunInspectionSnapshot, RunStoreTransition, StoredArtifactSnapshot, WorkspaceMetadata,
WorkspaceSnapshot, MAX_CLI_ARGUMENTS, MAX_CLI_ARGUMENT_BYTES, MAX_CONFIGURATION_SOURCE_BYTES,
MAX_INSPECTION_OBSERVATION_BYTES, MAX_LOCAL_ARGUMENT_WIRE_BYTES, MAX_LOCAL_ARTIFACT_BYTES,
MAX_LOCAL_CONTROL_STATUS_BYTES, MAX_LOCAL_RUNTIME_IDENTITY_TEXT_BYTES,
WORKSPACE_APPLICATION_ID, WORKSPACE_SCHEMA_VERSION,
};
use crucible_core::{
decode_raw_observation, derive_replay_seeds, encode_raw_observation, ArtifactId, ArtifactRef,
ContentDigest, PersistenceRetentionPolicy, MAX_GC_CANDIDATES, MAX_PERSISTENCE_BATCH_BYTES,
MAX_PERSISTENCE_BATCH_ITEMS,
advance_target_instance_lifecycle, decode_raw_observation, derive_replay_seeds,
encode_raw_observation, ArtifactId, ArtifactRef, ContentDigest, PersistenceRetentionPolicy,
TargetBuildId, TargetId, TargetLifecycleAction, TargetLifecycleState, MAX_GC_CANDIDATES,
MAX_PERSISTENCE_BATCH_BYTES, MAX_PERSISTENCE_BATCH_ITEMS,
};
use rusqlite::limits::Limit;
use rusqlite::{params, Connection, OpenFlags, OptionalExtension};
Expand Down Expand Up @@ -6959,14 +6960,136 @@ fn run_local_configuration(path: &str, retention_policy: PersistenceRetentionPol
);
return;
}
let raw_execution = match host_local_run_action(
let target_build_id = prefixed_identifier(
"target-build-",
target_manifest_publication.artifact.id.as_str(),
);
let target_id = prefixed_identifier("target-", target_build_id.as_str());
let lifecycle = match prepare_local_cli_target_instance(
&plan,
TargetId::new(target_id),
TargetBuildId::new(target_build_id),
reservation.attempt_id().clone(),
1,
) {
Ok(value) => value,
Err(_) => {
persist_failure_then_complete(
root.as_str(),
&reservation,
"TargetLifecycle",
RunCommandError::Execution,
);
return;
},
};
host_structured_log(
HostLogAction::Event,
"target-instance-prepared",
"",
"local-cli",
"",
reservation.run_id().as_str(),
reservation.attempt_id().as_str(),
lifecycle.target_id().as_str(),
lifecycle.target_build_id().as_str(),
"local-process",
"",
);
let lifecycle = match advance_target_instance_lifecycle(
lifecycle,
TargetLifecycleAction::BeginExecute,
) {
Ok(value) => value,
Err(_) => {
persist_failure_then_complete(
root.as_str(),
&reservation,
"TargetLifecycle",
RunCommandError::Execution,
);
return;
},
};
host_structured_log(
HostLogAction::Event,
"target-instance-executing",
"",
"local-cli",
"",
reservation.run_id().as_str(),
reservation.attempt_id().as_str(),
lifecycle.target_id().as_str(),
lifecycle.target_build_id().as_str(),
"local-process",
"",
);
let execution_result = host_local_run_action(
HostLocalRunAction::Execute,
path,
root.as_str(),
&plan,
target_contents.as_slice(),
target_argument_wire.as_slice(),
);
let lifecycle = match advance_target_instance_lifecycle(
lifecycle,
TargetLifecycleAction::FinishExecute,
) {
Ok(value) => value,
Err(_) => {
persist_failure_then_complete(
root.as_str(),
&reservation,
"TargetLifecycle",
RunCommandError::Execution,
);
return;
},
};
let cleanup_action = match &execution_result {
Err(HostLocalRunError::Cleanup) => TargetLifecycleAction::CleanupUncertain,
_ => TargetLifecycleAction::CleanupSucceeded,
};
let lifecycle = match advance_target_instance_lifecycle(lifecycle, cleanup_action) {
Ok(value) => value,
Err(_) => {
persist_failure_then_complete(
root.as_str(),
&reservation,
"TargetLifecycle",
RunCommandError::Execution,
);
return;
},
};
let lifecycle_event = match lifecycle.state() {
TargetLifecycleState::Cleaned => "target-instance-cleaned",
TargetLifecycleState::Discarded => "target-instance-discarded",
_ => {
persist_failure_then_complete(
root.as_str(),
&reservation,
"TargetLifecycle",
RunCommandError::Execution,
);
return;
},
};
host_structured_log(
HostLogAction::Event,
lifecycle_event,
"",
"local-cli",
"",
reservation.run_id().as_str(),
reservation.attempt_id().as_str(),
lifecycle.target_id().as_str(),
lifecycle.target_build_id().as_str(),
"local-process",
"",
);
let raw_execution = match execution_result {
Ok(HostLocalRunOutcome::Executed(raw)) => raw,
Ok(HostLocalRunOutcome::WorkspaceRoot(_))
| Ok(HostLocalRunOutcome::CapabilityProbe(_, _))
Expand Down
28 changes: 28 additions & 0 deletions crates/crucible-cli/tests/logging_cli.rs
Original file line number Diff line number Diff line change
Expand Up @@ -84,5 +84,33 @@ verification: {{verus: {{required: true, deny_unregistered_assumptions: true, de
assert_eq!(correlated["fields"]["severity"], "INFO");
assert!(correlated["fields"]["target_build_id"].is_string());

let lifecycle = records
.iter()
.filter_map(|record| {
let event = record["fields"]["event"].as_str()?;
event.starts_with("target-instance-").then_some((
event,
record["fields"]["target_id"].as_str(),
record["fields"]["target_build_id"].as_str(),
record["fields"]["worker_id"].as_str(),
))
})
.collect::<Vec<_>>();
assert_eq!(
lifecycle.iter().map(|entry| entry.0).collect::<Vec<_>>(),
[
"target-instance-prepared",
"target-instance-executing",
"target-instance-cleaned",
]
);
assert!(lifecycle.iter().all(|entry| {
entry.1.is_some()
&& entry.2.is_some()
&& entry.3 == Some("local-process")
&& entry.1 == lifecycle[0].1
&& entry.2 == lifecycle[0].2
}));

std::fs::remove_dir_all(root).expect("remove workspace");
}
Loading
Loading