Skip to content

core: fail closed without current Program evidence #464

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
lemone112 wants to merge 2 commits into from
Closed

core: fail closed without current Program evidence #464

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
f57baa2
core: fail closed without current Program evidence
lemone112 Jul 26, 2026
3dc76d7
core: revoke outputs on unknown session handoff
lemone112 Jul 26, 2026
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
8 changes: 4 additions & 4 deletions crates/labcolors-core/src/generic_boundary_tests.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -411,17 +411,17 @@ fn public_session_keeps_evidence_but_owner_alone_grants_updates_and_operations()
"pub struct RemoveV1<'owner, 'session> {",
"impl RemoveV1<'_, '_>",
),
(
"pub struct HoldV1<'owner, 'session> {",
"impl<'session> HoldV1<'_, 'session>",
),
] {
assert!(
source_scope(PROGRAM_SOURCE, payload, end)
.contains("_scope: BorrowScopeV1<'owner, 'session>,"),
"{payload} must retain both owner and immutable Session borrows",
);
}
assert!(
!PROGRAM_SOURCE.contains("HoldV1") && !PROGRAM_SOURCE.contains("OperationV1::Hold"),
"past evidence must not become a current emission authority",
);
}

#[test]
Expand Down
113 changes: 33 additions & 80 deletions crates/labcolors-core/src/program.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,11 +16,17 @@
//!
//! | Состояние | Операции |
//! |---|---|
//! | `Waiting` | нет |
//! | `Waiting` + `Empty` | нет |
//! | `Waiting` + допущенный `Unknown` | `Remove` для каждого выхода |
//! | `Ready` | `Set` для каждого выхода |
//! | `Stale` | `Hold` последнего доказанного результата |
//! | `Failed` с прошлым результатом | `Hold` |
//! | `Failed` без прошлого результата | `Remove` |
//! | `Stale` | `Remove` для каждого выхода |
//! | `Failed` | `Remove` для каждого выхода |
//!
//! Прошлый Verified-сертификат остаётся в evidence для диагностики, но не
//! разрешает эмиссию: он относится к прошлому наблюдению, а не к текущему
//! неизвестному или нарушающему контексту. Непустая сырая голова без текущего
//! Verified-сертификата также отзывает выходы: это закрывает передачу sink от
//! одной Session другой Session того же Owner.
//!
//! [`CertificateV1::Verified`] хранит выбранное состояние, все клетки
//! доказательства и сертифицированные выходы. [`CertificateV1::Conflict`]
Expand Down Expand Up @@ -1505,11 +1511,11 @@ impl SchemaOrderedScenarioSourceV1 for ScenarioSourceV1<'_> {
/// Закрытая классификация lifecycle Session.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum StateKindV1 {
/// Допущенного вычислимого наблюдения ещё нет.
/// Допущенного вычислимого наблюдения ещё нет; сырая голова может быть `Unknown`.
Waiting,
/// Текущая ревизия сертифицирована.
Ready,
/// Новое наблюдение недоступно, сохранён прошлый сертификат.
/// Новое наблюдение недоступно; прошлый сертификат сохранён для диагностики.
Stale,
/// Текущая ревизия имеет исчерпывающий конфликт.
Failed,
Expand Down Expand Up @@ -1636,7 +1642,14 @@ impl<'owner, 'session> ProjectionV1<'owner, 'session> {
self,
) -> impl ExactSizeIterator<Item = OperationV1<'owner, 'session>> + FusedIterator {
let inner = match self.evidence.state() {
SessionState::Waiting => OperationSourceV1::Empty,
SessionState::Waiting
if matches!(
self.evidence.session.raw_head(),
ObservationHeadViewV1::Empty
) =>
{
OperationSourceV1::Empty
}
SessionState::Ready { current } => {
debug_assert_eq!(current.outputs().len(), self.owner.compiled.output_count());
debug_assert!(
Expand All @@ -1653,23 +1666,17 @@ impl<'owner, 'session> ProjectionV1<'owner, 'session> {
scope: self.scope,
}
}
SessionState::Stale { previous } => OperationSourceV1::Hold {
outputs: previous.outputs().iter(),
certificate: VerifiedCertificateV1 { inner: previous },
scope: self.scope,
},
SessionState::Failed {
previous: Some(previous),
..
} => OperationSourceV1::Hold {
outputs: previous.outputs().iter(),
certificate: VerifiedCertificateV1 { inner: previous },
scope: self.scope,
},
SessionState::Failed { previous: None, .. } => OperationSourceV1::Remove {
slots: OwnerOutputSlotsV1::new(&self.owner.compiled),
scope: self.scope,
},
// `Waiting + Empty` — единственное состояние без действия и без
// полномочий на sink. После admission сырой головы любое состояние
// без текущего Verified-доказательства подчиняется одному закону
// отзыва. Так же fail-closed обрабатывается внутренне недостижимое
// сегодня сочетание `Waiting + Observed`.
SessionState::Waiting | SessionState::Stale { .. } | SessionState::Failed { .. } => {
OperationSourceV1::Remove {
slots: OwnerOutputSlotsV1::new(&self.owner.compiled),
scope: self.scope,
}
}
};
OperationsV1 { inner }
}
Expand Down Expand Up @@ -2350,7 +2357,7 @@ impl<'session> SetV1<'_, 'session> {
}
}

/// Операция удаления результата без допустимого предыдущего значения.
/// Операция удаления результата без сертификата для текущего контекста.
#[derive(Clone, Copy)]
pub struct RemoveV1<'owner, 'session> {
output_slot: OutputSlotIdV1,
Expand All @@ -2364,26 +2371,6 @@ impl RemoveV1<'_, '_> {
}
}

/// Операция удержания прошлого результата с его Verified-сертификатом.
#[derive(Clone, Copy)]
pub struct HoldV1<'owner, 'session> {
output: &'session ProgramOutputV1,
certificate: VerifiedCertificateV1<'session>,
_scope: BorrowScopeV1<'owner, 'session>,
}

impl<'session> HoldV1<'_, 'session> {
/// Возвращает удерживаемый клиентский выходной слот.
pub const fn output_slot(self) -> OutputSlotIdV1 {
OutputSlotIdV1::from_core((*self.output).output())
}

/// Возвращает сертификат удерживаемого результата.
pub const fn certificate(self) -> VerifiedCertificateV1<'session> {
self.certificate
}
}

/// Полное закрытое множество операций над непрозрачными выходными слотами.
///
/// Каждый payload заимствует точные Owner и снимок Session. Скопированные
Expand Down Expand Up @@ -2440,23 +2427,6 @@ impl<'session> HoldV1<'_, 'session> {
/// }
/// ```
///
/// ```compile_fail,E0515
/// use labcolors_core::program::{
/// HoldV1, OperationV1, OwnerV1,
/// SessionV1,
/// };
///
/// fn escape_hold<'session>(
/// owner: OwnerV1,
/// session: &'session SessionV1,
/// ) -> HoldV1<'session, 'session> {
/// match owner.project(session).unwrap().operations().next().unwrap() {
/// OperationV1::Hold(hold) => hold,
/// _ => panic!("fixture supplies Hold"),
/// }
/// }
/// ```
///
/// ```compile_fail,E0502
/// use labcolors_core::program::{
/// OperationV1, OwnerV1, SessionV1,
Expand Down Expand Up @@ -2485,10 +2455,8 @@ impl<'session> HoldV1<'_, 'session> {
pub enum OperationV1<'owner, 'session> {
/// Установить сертифицированный результат.
Set(SetV1<'owner, 'session>),
/// Удалить результат, когда допустимого прошлого значения нет.
/// Удалить результат, когда текущий контекст не сертифицирован.
Remove(RemoveV1<'owner, 'session>),
/// Удержать последний сертифицированный результат.
Hold(HoldV1<'owner, 'session>),
}

struct CertificatesV1<'a> {
Expand Down Expand Up @@ -2575,11 +2543,6 @@ enum OperationSourceV1<'owner, 'session> {
certificate: VerifiedCertificateV1<'session>,
scope: BorrowScopeV1<'owner, 'session>,
},
Hold {
outputs: slice::Iter<'session, ProgramOutputV1>,
certificate: VerifiedCertificateV1<'session>,
scope: BorrowScopeV1<'owner, 'session>,
},
Remove {
slots: OwnerOutputSlotsV1<'owner>,
scope: BorrowScopeV1<'owner, 'session>,
Expand Down Expand Up @@ -2608,15 +2571,6 @@ impl<'owner, 'session> Iterator for OperationsV1<'owner, 'session> {
_scope: *scope,
}))
}
OperationSourceV1::Hold {
outputs,
certificate,
scope,
} => Some(OperationV1::Hold(HoldV1 {
output: outputs.next()?,
certificate: *certificate,
_scope: *scope,
})),
OperationSourceV1::Remove { slots, scope } => Some(OperationV1::Remove(RemoveV1 {
output_slot: slots.next()?,
_scope: *scope,
Expand All @@ -2628,7 +2582,6 @@ impl<'owner, 'session> Iterator for OperationsV1<'owner, 'session> {
let remaining = match &self.inner {
OperationSourceV1::Empty => 0,
OperationSourceV1::Set { outputs, .. } => outputs.len(),
OperationSourceV1::Hold { outputs, .. } => outputs.len(),
OperationSourceV1::Remove { slots, .. } => slots.len(),
};
(remaining, Some(remaining))
Expand Down
112 changes: 74 additions & 38 deletions crates/labcolors-core/src/program_mixed_evaluator_tests.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -675,12 +675,6 @@ fn consume_public_projection(projection: ProjectionV1<'_, '_>) -> ProjectionProb
probe.mix(2);
probe.mix(u64::from(remove.output_slot().value()));
}
OperationV1::Hold(hold) => {
probe.mix(3);
probe.mix(u64::from(hold.output_slot().value()));
probe.mix_bytes(hold.certificate().content_identity().as_bytes());
probe.mix(hold.certificate().observation().revision());
}
}
});
std::hint::black_box(probe)
Expand Down Expand Up @@ -1357,7 +1351,7 @@ fn observation_projection_is_invariant_under_every_scenario_permutation_and_keep
}

#[test]
fn concrete_program_projects_total_ready_and_stale_operations() {
fn concrete_program_projects_ready_and_fail_closed_stale_operations() {
let owner = OwnerV1::from_compiled(finite_program([[0x80; 3], [0; 3]]));
assert_eq!(owner.surface_input_port_count(), 1);
assert_eq!(
Expand Down Expand Up @@ -1464,28 +1458,76 @@ fn concrete_program_projects_total_ready_and_stale_operations() {
assert_eq!(certificates.len(), 1);
assert!(matches!(certificates[0], CertificateV1::Verified(_)));
assert_eq!(certificates[0].observation().revision(), 1);
let mut operations = stale.operations();
let Some(OperationV1::Hold(hold)) = operations.next() else {
panic!("Stale must emit one Hold operation");
};
assert_eq!(hold.output_slot(), OutputSlotIdV1::new(OUTPUT.value()));
assert_eq!(
hold.certificate().observation().revision(),
certificates[0].observation().revision()
);
assert_eq!(
hold.certificate().content_identity(),
certificates[0].content_identity()
);
assert_eq!(
CertificateV1::Verified(hold.certificate()).observation_backing_ptr_for_test(),
certificates[0].observation_backing_ptr_for_test(),
ready_backing
);
let mut operations = stale.operations();
let Some(OperationV1::Remove(remove)) = operations.next() else {
panic!("Stale must remove an output that lacks current evidence");
};
assert_eq!(remove.output_slot(), OutputSlotIdV1::new(OUTPUT.value()));
assert!(operations.next().is_none());
}

#[test]
fn unknown_replacement_session_revokes_an_existing_owner_output() {
let owner = OwnerV1::from_compiled(finite_program([[0x80; 3], [0; 3]]));
let white = [Srgb8::new([0xFF; 3])];
let scenarios = [ScenarioV1::new(1, &white)];

let mut first_session = owner.instantiate(11).unwrap();
let ready = owner
.update(
&mut first_session,
UpdateV1::Observed {
revision: 1,
scenarios: &scenarios,
},
)
.unwrap();
let mut sink = None;
for operation in ready.operations() {
match operation {
OperationV1::Set(set) => sink = Some((set.source(), set.opacity())),
OperationV1::Remove(_) => sink = None,
}
}
assert!(
sink.is_some(),
"the first Session must populate the shared sink"
);
drop(first_session);

let mut replacement_session = owner.instantiate(12).unwrap();
let unknown = owner
.update(
&mut replacement_session,
UpdateV1::Unknown {
revision: 1,
reason_id: 7,
},
)
.unwrap();
assert_eq!(unknown.evidence().kind(), StateKindV1::Waiting);
assert_unknown_head(unknown.evidence().observation_head(), 12, 1, 7);
assert_eq!(unknown.evidence().certificates().len(), 0);

let mut operations = unknown.operations();
let Some(OperationV1::Remove(remove)) = operations.next() else {
panic!("an explicit Unknown must revoke an existing owner output during handoff");
};
assert_eq!(remove.output_slot(), OutputSlotIdV1::new(OUTPUT.value()));
sink = None;
assert!(operations.next().is_none());
assert!(
sink.is_none(),
"the replacement Session must not leave stale paint"
);
}

#[test]
fn concrete_program_distinguishes_failed_remove_from_failed_hold() {
fn concrete_program_failed_always_removes_but_retains_previous_evidence() {
let white = [Srgb8::new([0xFF; 3])];
let black = [Srgb8::new([0; 3])];
let white_only = [ScenarioV1::new(1, &white)];
Expand Down Expand Up @@ -1560,20 +1602,15 @@ fn concrete_program_distinguishes_failed_remove_from_failed_hold() {
.collect::<Vec<_>>(),
[("conflict", 2), ("verified", 1)]
);
let mut operations = failed.operations();
let Some(OperationV1::Hold(hold)) = operations.next() else {
panic!("Failed with previous evidence must emit one Hold operation");
};
assert_eq!(hold.output_slot(), OutputSlotIdV1::new(OUTPUT.value()));
assert_eq!(hold.certificate().observation().revision(), 1);
assert_eq!(
hold.certificate().content_identity(),
certificates[1].content_identity()
);
assert_eq!(
CertificateV1::Verified(hold.certificate()).observation_backing_ptr_for_test(),
certificates[1].observation_backing_ptr_for_test(),
previous_backing
);
let mut operations = failed.operations();
let Some(OperationV1::Remove(remove)) = operations.next() else {
panic!("Failed must remove an output that violates the current context");
};
assert_eq!(remove.output_slot(), OutputSlotIdV1::new(OUTPUT.value()));
assert!(operations.next().is_none());
}

Expand Down Expand Up @@ -2016,7 +2053,7 @@ fn failed_without_previous_removes_every_output_in_canonical_exact_order() {
}

#[test]
fn ready_and_stale_project_every_output_in_the_same_canonical_order() {
fn ready_sets_and_stale_removes_every_output_in_the_same_canonical_order() {
let owner = OwnerV1::from_compiled(finite_program_with_outputs(
[[0x80; 3], [0; 3]],
vec![
Expand Down Expand Up @@ -2062,11 +2099,10 @@ fn ready_and_stale_project_every_output_in_the_same_canonical_order() {
let mut operations = stale.operations();
assert_eq!(operations.len(), 2);
for expected in [OUTPUT, SECOND_OUTPUT] {
let Some(OperationV1::Hold(hold)) = operations.next() else {
panic!("Stale must hold every previously verified output");
let Some(OperationV1::Remove(remove)) = operations.next() else {
panic!("Stale must remove every output that lacks current evidence");
};
assert_eq!(hold.output_slot().value(), expected.value());
assert_eq!(hold.certificate().observation().revision(), 1);
assert_eq!(remove.output_slot().value(), expected.value());
}
assert!(operations.next().is_none());
}
Loading
Loading