From 35472cba2a2eb9901b59cdeb58c67db98e2bb829 Mon Sep 17 00:00:00 2001 From: Daniel from Labpics <63733699+lemone112@users.noreply.github.com> Date: Sat, 25 Jul 2026 00:54:48 +0300 Subject: [PATCH 1/2] core: single-own compiled observation schemas --- ...rt-reference-surplus-q55-bps-proof-v1.json | 2 +- .../src/generic_boundary_tests.rs | 154 +++++++++++++++--- crates/labcolors-core/src/observation.rs | 22 ++- .../labcolors-core/src/observation_tests.rs | 20 ++- crates/labcolors-core/src/point_support.rs | 5 +- .../labcolors-core/src/point_support_tests.rs | 56 ++++++- crates/labcolors-core/src/program_session.rs | 17 +- .../src/program_session_tests.rs | 53 +++++- crates/labcolors-core/src/session.rs | 17 +- crates/labcolors-core/src/session_tests.rs | 113 +++++++++++-- scripts/verify_point_support_surplus.py | 9 +- 11 files changed, 403 insertions(+), 65 deletions(-) diff --git a/crates/labcolors-core/contracts/point-support-reference-surplus-q55-bps-proof-v1.json b/crates/labcolors-core/contracts/point-support-reference-surplus-q55-bps-proof-v1.json index eea0972c..30b34af0 100644 --- a/crates/labcolors-core/contracts/point-support-reference-surplus-q55-bps-proof-v1.json +++ b/crates/labcolors-core/contracts/point-support-reference-surplus-q55-bps-proof-v1.json @@ -1 +1 @@ -{"artifact_id":"wcag22-srgb8-luminance-q55-v1","basis_point_proof":{"checks":30,"drop_all_semantics":"zero required surplus; current must still meet the anchor","drop_domain_inclusive":[0,10000],"nonpositive_baseline_semantics":"zero required surplus; current must meet the anchor"},"bound_id":"point-support-reference-surplus-q55-bps-v1","certified_claim":"for every successfully evaluated enabled stability cell, decision is Retained iff current_lower_surplus >= (10000-drop_bps)/10000 * max(baseline_lower_surplus,0); the declared anchor remains a separate hard floor","comparator_proof":{"algorithm":"euclidean-continued-fraction-ordering-v1","dense_denominator_inclusive":[1,31],"dense_numerator_inclusive":[0,31],"dense_small_cases":984064,"invariant":"equal integer parts; reciprocal proper fractions reverse order","largest_fibonacci_index":186,"oracle":"unbounded-integer-cross-product","random_cases":250000,"random_corpus_sha256":"97c4af7b452b31a4ab92645f70c17acb38bf57ca55484e32ad9d7d79d97a333d","random_seed":210583930,"termination":"each nonterminal denominator becomes a strictly smaller remainder","u128_adversarial_cases":190},"declared_operation_law":"q55-lower-reference-distance-explicit-anchor-bps-retention-v1","excluded_claim":"does not certify retention against the unknown exact baseline surplus, renderer equivalence outside encoded-sRGB8 source-over, or a successful result when evaluation fails","integer_replay_envelope":{"assumption":"every Q55 luminance upper <= scale + 3","i128_max":170141183460469231731687303715884105727,"offset_cleared_denominator_max":756604737398243388,"positive_baseline_numerator_max":1188950301625811064,"rational_denominator_max":1513209474796486776,"required_denominator_max":15132094747964867760000,"required_numerator_max":11889503016258110640000,"signed_anchor_abs_coarse_max":5296233161787703716,"u128_max":340282366920938463463374607431768211455,"u64_max":18446744073709551615},"profile_id":"srgb8-q55-retained-reference-surplus-bps-v1","proof_id":"point-support-reference-surplus-integer-v1","proof_payload_sha256":"108ce18deb22866e8637024b0984e529f329dfdc6c9940de0abc4217a6c6a774","q55_dependency":{"artifact_id":"wcag22-srgb8-luminance-q55-v1","artifact_sha256":"7ff239d9052b346f3c50da01ca65ca2330892ed1a3ff30e190797fcef6f03604","maximum_luminance_upper":36028797018963971,"outward_interval_width_bound":3,"proof_id":"wcag22-srgb8-full-domain-q55-v1","proof_payload_sha256":"3c639a7c875046c46b56b51ecdd67d5ecaf14a1134490c88a222e7037b63c0f2","proof_sha256":"ac59cf89503170c789223b91d775213a19d4e571ef930f2ea609fcd51b14defd","q55_scale":36028797018963968},"reference_and_anchor_proof":{"anchor_identity_checks":75,"orientation_law":"distance-magnitude-symmetric-orientation-reported-separately","overlap_lower_distance":"0/1","separated_endpoint_checks":504},"schema_version":2,"site_id":"point-support-retained-reference-surplus-v1","source_binding_exclusions":["whole-crate compilation or compiler/toolchain attestation","binary, package, FFI, renderer, or browser transport attestation","unrelated Lab Colors modules outside the declared point-support semantic cone"],"source_binding_law":"point-support-rust-whole-file-semantic-cone-v2","source_binding_schema_version":2,"source_binding_scope":"exact bytes of the private point-support Rust semantic cone and its two WCAG include_str inputs; comments and cfg(test) text are intentionally significant","source_closure_sha256":"ac2e23b4d89850df7bc6697a79dfc715192e998bbabcf47fe88c415e8c332df8","source_files":[{"kind":"compile-time-input","path":"crates/labcolors-core/contracts/wcag22-srgb8-q55-proof-v1.json","sha256":"ac59cf89503170c789223b91d775213a19d4e571ef930f2ea609fcd51b14defd"},{"kind":"compile-time-input","path":"crates/labcolors-core/contracts/wcag22-srgb8-v1.json","sha256":"b4bb7e5f17a99f2c911fdbe3da23a48b049277b796291094950f14680cc3cc7b"},{"kind":"rust-source","path":"crates/labcolors-core/src/appearance.rs","sha256":"09be54900efe29ffdac8705efd0d6d613055c90d634446ca4b228f51a63997d0"},{"kind":"rust-source","path":"crates/labcolors-core/src/composition.rs","sha256":"195a67327a3bd86d7816b634481389930bf68577bb1202fad14c2ea152df8625"},{"kind":"rust-source","path":"crates/labcolors-core/src/constraints/exact.rs","sha256":"892576a8621185352583e63dc0a1aacac32e32a8063b6fe24ae16d4ff9dce7cb"},{"kind":"rust-source","path":"crates/labcolors-core/src/constraints/mod.rs","sha256":"e73b9c0b8c3a4112cb53987753d5a6b5f639774b0b872afaea9836e6647a2f7d"},{"kind":"rust-source","path":"crates/labcolors-core/src/constraints/wcag22.rs","sha256":"856093c91159d8b3faab001f2d6524d33d7b16458a5a4e98ea65f8c62ab2694c"},{"kind":"rust-source","path":"crates/labcolors-core/src/hash.rs","sha256":"f97a0fd7d6ad3162f0f1dfb326fccfb7ed40da9a8fa67a5b8a239a1ae2ae49c3"},{"kind":"rust-source","path":"crates/labcolors-core/src/lcs_occurrence.rs","sha256":"6f202ad7425a235b9d18caba0c817fc33a2b8e042050a34f5ddff3fd09efc53d"},{"kind":"rust-source","path":"crates/labcolors-core/src/lib.rs","sha256":"b3edb3764119c0b4fd50f52b62cbc07fa81c4bfdf1246b91f20eb3d8d4eebd31"},{"kind":"rust-source","path":"crates/labcolors-core/src/numerics.rs","sha256":"e73a12136494f2ef9aca4e943ab38302c1439f054cecab36a552d35252c164f9"},{"kind":"rust-source","path":"crates/labcolors-core/src/observation.rs","sha256":"4b43f6f0363436d0cb80fe5e4517555198ba41aef28379e5507dae0a59138838"},{"kind":"rust-source","path":"crates/labcolors-core/src/point_support.rs","sha256":"0755210e3e591d7049f293a0f0b7647681631f32feee5ad7d3b3309cffca8f9d"},{"kind":"rust-source","path":"crates/labcolors-core/src/session.rs","sha256":"7aac1eac64c7e24add1eafc0b66be62f16258fadf2519669785724fc582fc37f"},{"kind":"rust-source","path":"crates/labcolors-core/src/srgb8.rs","sha256":"6c95324eb05476f35f75375a9af0b2b4a41b8b2978c46e67d2ce1aea5adde342"},{"kind":"rust-source","path":"crates/labcolors-core/src/wcag22.rs","sha256":"7ba7864eb7e73789bad6c63c64a4dc2dcc08c2da6921375fb9564fca230c2780"},{"kind":"rust-source","path":"crates/labcolors-core/src/wcag22/kernel.rs","sha256":"c97980c1ca2c7ea9cabff9c8d2fb7282773cca180ae15948391c29c9d6196040"},{"kind":"rust-source","path":"crates/labcolors-core/src/wcag22/q55_data.rs","sha256":"af4d23d6b70c45ce6efa839e7dda4bb0a61f6aae43cb805af6fa9b29e6c3bae2"},{"kind":"rust-source","path":"crates/labcolors-core/src/wcag22_evidence.rs","sha256":"3c5a75b07254c6071a64700af208a64987d0f0ea9698eadc54a9e74585ce1f72"}],"source_negative_controls":43,"universal_algebraic_certificate":{"basis_point_scale_instantiation":10000,"domain":"integers; Q55 scale Q>0; anchor L>=D>=0; lighter monotonicity L2>=L1>D>=0; darker monotonicity L>D2>=D1>=0; current/baseline denominators b,q>0; basis-point scale B>0 instantiated as 10000; p>0; a>=0; 0<=drop_bps<=B","identities":["three explicit anchor-surplus formulas after denominator clearing","reference distance is monotone increasing in lighter L","reference distance is monotone decreasing in darker D","positive-baseline retained threshold is p*(B-drop)/(q*B)","a/b >= p*(B-drop)/(q*B) iff a*q*B >= p*(B-drop)*b"],"method":"exact-sparse-integer-polynomial-identities-plus-positive-denominator-order-lemma-v1","nonpositive_baseline_case":"max(baseline,0)=0; retained threshold is exactly zero","symbolic_mutation_controls":{"anchor_coefficients_and_denominator":6,"retained_cross_product":5},"wolfram_language_cross_check":{"query":"FullSimplify[{20 g/d - 0 == 20 g/d, 20 g/d - 2 == (20 g - 2 d)/d, 20 g/d - 7/2 == (40 g - 7 d)/(2 d), Equivalent[a/b >= p (s-x)/(q s), a q s >= p (s-x) b], Max[p/q, 0] (s-x)/s == Piecewise[{{0, p <= 0}}, p (s-x)/(q s)]}, Assumptions -> Element[{a,b,p,q,s,x,g,d}, Integers] && a >= 0 && b > 0 && q > 0 && s > 0 && 0 <= x <= s && d > 0 && g >= 0]","query_sha256":"8cdbb9964583030c8b92498961896cb2a98613f1cb31eb7c54acdf8e16beff10","result":"{True, True, True, True, True}","result_sha256":"13a8f2ee8d0fde335a638e46d7cc8a8427b9a1437c77d22cfcf925bb87fa6303"}},"verifier_sha256":"defa5abb202fd2f3d9a08208a4888f79e1bceeba2b00b168efa00e4465875c66"} +{"artifact_id":"wcag22-srgb8-luminance-q55-v1","basis_point_proof":{"checks":30,"drop_all_semantics":"zero required surplus; current must still meet the anchor","drop_domain_inclusive":[0,10000],"nonpositive_baseline_semantics":"zero required surplus; current must meet the anchor"},"bound_id":"point-support-reference-surplus-q55-bps-v1","certified_claim":"for every successfully evaluated enabled stability cell, decision is Retained iff current_lower_surplus >= (10000-drop_bps)/10000 * max(baseline_lower_surplus,0); the declared anchor remains a separate hard floor","comparator_proof":{"algorithm":"euclidean-continued-fraction-ordering-v1","dense_denominator_inclusive":[1,31],"dense_numerator_inclusive":[0,31],"dense_small_cases":984064,"invariant":"equal integer parts; reciprocal proper fractions reverse order","largest_fibonacci_index":186,"oracle":"unbounded-integer-cross-product","random_cases":250000,"random_corpus_sha256":"97c4af7b452b31a4ab92645f70c17acb38bf57ca55484e32ad9d7d79d97a333d","random_seed":210583930,"termination":"each nonterminal denominator becomes a strictly smaller remainder","u128_adversarial_cases":190},"declared_operation_law":"q55-lower-reference-distance-explicit-anchor-bps-retention-v1","excluded_claim":"does not certify retention against the unknown exact baseline surplus, renderer equivalence outside encoded-sRGB8 source-over, or a successful result when evaluation fails","integer_replay_envelope":{"assumption":"every Q55 luminance upper <= scale + 3","i128_max":170141183460469231731687303715884105727,"offset_cleared_denominator_max":756604737398243388,"positive_baseline_numerator_max":1188950301625811064,"rational_denominator_max":1513209474796486776,"required_denominator_max":15132094747964867760000,"required_numerator_max":11889503016258110640000,"signed_anchor_abs_coarse_max":5296233161787703716,"u128_max":340282366920938463463374607431768211455,"u64_max":18446744073709551615},"profile_id":"srgb8-q55-retained-reference-surplus-bps-v1","proof_id":"point-support-reference-surplus-integer-v1","proof_payload_sha256":"20af49448f088da3b30a0e31b8e5b9bb2e23b36a470bcac351c2629e3f345a48","q55_dependency":{"artifact_id":"wcag22-srgb8-luminance-q55-v1","artifact_sha256":"7ff239d9052b346f3c50da01ca65ca2330892ed1a3ff30e190797fcef6f03604","maximum_luminance_upper":36028797018963971,"outward_interval_width_bound":3,"proof_id":"wcag22-srgb8-full-domain-q55-v1","proof_payload_sha256":"3c639a7c875046c46b56b51ecdd67d5ecaf14a1134490c88a222e7037b63c0f2","proof_sha256":"ac59cf89503170c789223b91d775213a19d4e571ef930f2ea609fcd51b14defd","q55_scale":36028797018963968},"reference_and_anchor_proof":{"anchor_identity_checks":75,"orientation_law":"distance-magnitude-symmetric-orientation-reported-separately","overlap_lower_distance":"0/1","separated_endpoint_checks":504},"schema_version":2,"site_id":"point-support-retained-reference-surplus-v1","source_binding_exclusions":["whole-crate compilation or compiler/toolchain attestation","binary, package, FFI, renderer, or browser transport attestation","unrelated Lab Colors modules outside the declared point-support semantic cone"],"source_binding_law":"point-support-rust-whole-file-semantic-cone-v2","source_binding_schema_version":2,"source_binding_scope":"exact bytes of the private point-support Rust semantic cone and its two WCAG include_str inputs; comments and cfg(test) text are intentionally significant","source_closure_sha256":"669326bce56a2901f7fbbd8b4c23f26f8b33daceb1471b81c98763940b41d3e4","source_files":[{"kind":"compile-time-input","path":"crates/labcolors-core/contracts/wcag22-srgb8-q55-proof-v1.json","sha256":"ac59cf89503170c789223b91d775213a19d4e571ef930f2ea609fcd51b14defd"},{"kind":"compile-time-input","path":"crates/labcolors-core/contracts/wcag22-srgb8-v1.json","sha256":"b4bb7e5f17a99f2c911fdbe3da23a48b049277b796291094950f14680cc3cc7b"},{"kind":"rust-source","path":"crates/labcolors-core/src/appearance.rs","sha256":"09be54900efe29ffdac8705efd0d6d613055c90d634446ca4b228f51a63997d0"},{"kind":"rust-source","path":"crates/labcolors-core/src/composition.rs","sha256":"195a67327a3bd86d7816b634481389930bf68577bb1202fad14c2ea152df8625"},{"kind":"rust-source","path":"crates/labcolors-core/src/constraints/exact.rs","sha256":"892576a8621185352583e63dc0a1aacac32e32a8063b6fe24ae16d4ff9dce7cb"},{"kind":"rust-source","path":"crates/labcolors-core/src/constraints/mod.rs","sha256":"e73b9c0b8c3a4112cb53987753d5a6b5f639774b0b872afaea9836e6647a2f7d"},{"kind":"rust-source","path":"crates/labcolors-core/src/constraints/wcag22.rs","sha256":"856093c91159d8b3faab001f2d6524d33d7b16458a5a4e98ea65f8c62ab2694c"},{"kind":"rust-source","path":"crates/labcolors-core/src/hash.rs","sha256":"f97a0fd7d6ad3162f0f1dfb326fccfb7ed40da9a8fa67a5b8a239a1ae2ae49c3"},{"kind":"rust-source","path":"crates/labcolors-core/src/lcs_occurrence.rs","sha256":"6f202ad7425a235b9d18caba0c817fc33a2b8e042050a34f5ddff3fd09efc53d"},{"kind":"rust-source","path":"crates/labcolors-core/src/lib.rs","sha256":"b3edb3764119c0b4fd50f52b62cbc07fa81c4bfdf1246b91f20eb3d8d4eebd31"},{"kind":"rust-source","path":"crates/labcolors-core/src/numerics.rs","sha256":"e73a12136494f2ef9aca4e943ab38302c1439f054cecab36a552d35252c164f9"},{"kind":"rust-source","path":"crates/labcolors-core/src/observation.rs","sha256":"887f139e6750cc99cd751b3c7e47276971293f74091130028a1746fa29ebb104"},{"kind":"rust-source","path":"crates/labcolors-core/src/point_support.rs","sha256":"6f6a376ff036d3d65960c004e6566e1bca580f19f5bd3cd333a80b0da5b5c242"},{"kind":"rust-source","path":"crates/labcolors-core/src/session.rs","sha256":"4f77643206077c080e5e9b182e896145bfb69bf3db8aa4c1ac7d4c5360ea8504"},{"kind":"rust-source","path":"crates/labcolors-core/src/srgb8.rs","sha256":"6c95324eb05476f35f75375a9af0b2b4a41b8b2978c46e67d2ce1aea5adde342"},{"kind":"rust-source","path":"crates/labcolors-core/src/wcag22.rs","sha256":"7ba7864eb7e73789bad6c63c64a4dc2dcc08c2da6921375fb9564fca230c2780"},{"kind":"rust-source","path":"crates/labcolors-core/src/wcag22/kernel.rs","sha256":"c97980c1ca2c7ea9cabff9c8d2fb7282773cca180ae15948391c29c9d6196040"},{"kind":"rust-source","path":"crates/labcolors-core/src/wcag22/q55_data.rs","sha256":"af4d23d6b70c45ce6efa839e7dda4bb0a61f6aae43cb805af6fa9b29e6c3bae2"},{"kind":"rust-source","path":"crates/labcolors-core/src/wcag22_evidence.rs","sha256":"3c5a75b07254c6071a64700af208a64987d0f0ea9698eadc54a9e74585ce1f72"}],"source_negative_controls":43,"universal_algebraic_certificate":{"basis_point_scale_instantiation":10000,"domain":"integers; Q55 scale Q>0; anchor L>=D>=0; lighter monotonicity L2>=L1>D>=0; darker monotonicity L>D2>=D1>=0; current/baseline denominators b,q>0; basis-point scale B>0 instantiated as 10000; p>0; a>=0; 0<=drop_bps<=B","identities":["three explicit anchor-surplus formulas after denominator clearing","reference distance is monotone increasing in lighter L","reference distance is monotone decreasing in darker D","positive-baseline retained threshold is p*(B-drop)/(q*B)","a/b >= p*(B-drop)/(q*B) iff a*q*B >= p*(B-drop)*b"],"method":"exact-sparse-integer-polynomial-identities-plus-positive-denominator-order-lemma-v1","nonpositive_baseline_case":"max(baseline,0)=0; retained threshold is exactly zero","symbolic_mutation_controls":{"anchor_coefficients_and_denominator":6,"retained_cross_product":5},"wolfram_language_cross_check":{"query":"FullSimplify[{20 g/d - 0 == 20 g/d, 20 g/d - 2 == (20 g - 2 d)/d, 20 g/d - 7/2 == (40 g - 7 d)/(2 d), Equivalent[a/b >= p (s-x)/(q s), a q s >= p (s-x) b], Max[p/q, 0] (s-x)/s == Piecewise[{{0, p <= 0}}, p (s-x)/(q s)]}, Assumptions -> Element[{a,b,p,q,s,x,g,d}, Integers] && a >= 0 && b > 0 && q > 0 && s > 0 && 0 <= x <= s && d > 0 && g >= 0]","query_sha256":"8cdbb9964583030c8b92498961896cb2a98613f1cb31eb7c54acdf8e16beff10","result":"{True, True, True, True, True}","result_sha256":"13a8f2ee8d0fde335a638e46d7cc8a8427b9a1437c77d22cfcf925bb87fa6303"}},"verifier_sha256":"1889fd73f85a80d1d9daacd6bb2261e87d3a02df49304d6016c37825252c6af8"} diff --git a/crates/labcolors-core/src/generic_boundary_tests.rs b/crates/labcolors-core/src/generic_boundary_tests.rs index f3b5f8f1..6c717b5a 100644 --- a/crates/labcolors-core/src/generic_boundary_tests.rs +++ b/crates/labcolors-core/src/generic_boundary_tests.rs @@ -1,3 +1,6 @@ +use std::ffi::OsStr; +use std::path::PathBuf; + const APPEARANCE_SOURCE: &str = include_str!("appearance.rs"); const CONSTRAINTS_SOURCE: &str = include_str!("constraints/mod.rs"); const EXACT_CONSTRAINT_SOURCE: &str = include_str!("constraints/exact.rs"); @@ -66,6 +69,40 @@ fn contains_rust_identifier(source: &str, identifier: &str) -> bool { }) } +fn production_rust_sources() -> Vec<(String, String)> { + let root = PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("src"); + let mut pending = vec![root.clone()]; + let mut sources = Vec::new(); + while let Some(directory) = pending.pop() { + for entry in std::fs::read_dir(&directory).expect("Core source directory must be readable") + { + let path = entry.expect("Core source entry must be readable").path(); + if path.is_dir() { + pending.push(path); + continue; + } + let is_production_rust = path.extension() == Some(OsStr::new("rs")) + && !path + .file_name() + .and_then(OsStr::to_str) + .is_some_and(|name| name.ends_with("_tests.rs")); + if !is_production_rust { + continue; + } + let relative = path + .strip_prefix(&root) + .expect("Core source must remain below its manifest root") + .to_string_lossy() + .into_owned(); + let source = + std::fs::read_to_string(&path).expect("Core Rust source must be valid UTF-8"); + sources.push((relative, source)); + } + } + sources.sort_unstable_by(|left, right| left.0.cmp(&right.0)); + sources +} + #[test] fn generic_physical_and_transport_modules_contain_no_client_or_legacy_vocabulary() { for (path, source) in GENERIC_SOURCES { @@ -324,6 +361,23 @@ fn shared_observation_ssot_has_one_backing_without_lifecycle_or_adapter_facades( .contains("pub(crate) struct CanonicalObservationSchemaV1(Rc<[SurfaceInputPortId]>);"), "compiled schema and observations must share the same Rc-backed schema", ); + assert!( + OBSERVATION_SOURCE.contains( + "#[derive(Debug, PartialEq, Eq)]\n#[cfg_attr(test, derive(Clone))]\npub(crate) struct CanonicalObservationSchemaV1", + ), + "production schema ownership must not expose a general Clone capability", + ); + assert_eq!( + OBSERVATION_SOURCE + .matches("schema.share_for_observation()") + .count(), + 2, + "only keyed and schema-ordered admission may share a schema handle", + ); + assert!( + !OBSERVATION_SOURCE.contains("schema: schema.clone()"), + "admission must use the private schema-sharing capability", + ); for forbidden in ["std::sync::Arc", "Arc<", "RefCell<", "Mutex<", "RwLock<"] { assert!( !OBSERVATION_SOURCE.contains(forbidden), @@ -368,7 +422,6 @@ fn shared_observation_ssot_has_one_backing_without_lifecycle_or_adapter_facades( "impl Session", ); for required in [ - "schema: CanonicalObservationSchemaV1,", "raw_head: SessionObservationHeadV1,", "state: SessionState,", ] { @@ -378,6 +431,10 @@ fn shared_observation_ssot_has_one_backing_without_lifecycle_or_adapter_facades( "Session must own exactly one `{required}` field", ); } + assert!( + !session_owner.contains("schema: CanonicalObservationSchemaV1,"), + "the concrete plan is the sole Session-local owner of its canonical schema", + ); for forbidden in [ "current_unknown", "observation: RevisionBoundObservationV1", @@ -398,6 +455,7 @@ fn shared_observation_ssot_has_one_backing_without_lifecycle_or_adapter_facades( "type Verified: SessionEvidenceV1;", "type Violation: SessionEvidenceV1;", "fn try_acquire_owner(&self) -> Option;", + "owner: &'a Self::OwnerLease,", "SessionUpdateError::OwnerExpired", ".is_same_binding_as(expected_observation)", "SessionUpdateError::EvidenceBindingInvariant", @@ -407,15 +465,20 @@ fn shared_observation_ssot_has_one_backing_without_lifecycle_or_adapter_facades( "Session must reject detached evaluator evidence; missing `{required}`", ); } + let session_plan_implementors = production_rust_sources() + .into_iter() + .filter_map(|(path, source)| { + let count = source.matches("SessionPlanV1 for").count(); + (count != 0).then_some((path, count)) + }) + .collect::>(); assert_eq!( - POINT_SUPPORT_SOURCE - .matches("impl SessionPlanV1 for CompiledPointSupportRecheckV1") - .count() - + PROGRAM_SESSION_SOURCE - .matches("SessionPlanV1 for ProgramSessionPlan") - .count(), - 2, - "only the point-support and Program compiled plans may inhabit Session", + session_plan_implementors, + vec![ + ("point_support.rs".to_owned(), 1), + ("program_session.rs".to_owned(), 1), + ], + "only the audited point-support and Program plans may inhabit Session", ); for (path, source) in [ ("session.rs", SESSION_SOURCE), @@ -446,21 +509,51 @@ fn shared_observation_ssot_has_one_backing_without_lifecycle_or_adapter_facades( ); } - let update = normalized_source_scope( - SESSION_SOURCE, - "pub(crate) fn update(", - "/// Move exactly one retained verified witness", - ); - let owner_preflight = update - .find(".try_acquire_owner()") - .expect("Session update must acquire the exact owner generation"); - let admission = update - .find("prepare_observation(") - .expect("Session update must perform canonical admission"); - assert!( - owner_preflight < admission, - "owner expiry must precede raw admission and physical execution", - ); + for (name, update, prepare) in [ + ( + "keyed", + source_scope( + SESSION_SOURCE, + "pub(crate) fn update(", + "/// Stream-affine `Unknown` admission", + ), + "prepare_observation(", + ), + ( + "schema-ordered", + source_scope( + SESSION_SOURCE, + "pub(crate) fn update_schema_ordered", + "fn apply_prepared_update", + ), + "prepare_schema_ordered_observation(", + ), + ] { + let owner_preflight = update + .find(".try_acquire_owner()") + .unwrap_or_else(|| panic!("{name} update must acquire the exact owner generation")); + let schema = update + .find("let schema = self.plan.observation_schema(&owner);") + .unwrap_or_else(|| panic!("{name} update must derive schema from that owner")); + let admission = update + .find(prepare) + .unwrap_or_else(|| panic!("{name} update must perform canonical admission")); + assert!( + owner_preflight < schema && schema < admission, + "{name} update must pin owner, derive its schema, then admit", + ); + assert_eq!( + update + .matches("let schema = self.plan.observation_schema(&owner);") + .count(), + 1, + "{name} update must borrow exactly one schema", + ); + assert!( + !update.contains("observation_schema(&owner).clone()"), + "{name} admission must not create a transient schema owner", + ); + } let consuming_entry = source_scope( POINT_SUPPORT_SOURCE, @@ -646,6 +739,19 @@ fn program_session_owns_context_bound_lcs_evidence_and_one_session_scratch_cache !plan.contains("epoch: Rc>,"), "a Program Session must not prolong its CompiledProgram owner", ); + assert!( + !plan.contains("schema: CanonicalObservationSchemaV1,"), + "a Program Session must derive schema from its pinned owner generation", + ); + let instantiate = source_scope( + PROGRAM_SESSION_SOURCE, + "pub(crate) fn instantiate(", + "/// Failure while preparing mutable storage", + ); + assert!( + !instantiate.contains("observation_group.schema.clone()"), + "empty Program Sessions must not add persistent schema handles", + ); let compiled = source_scope( PROGRAM_SESSION_SOURCE, "pub struct CompiledProgram", diff --git a/crates/labcolors-core/src/observation.rs b/crates/labcolors-core/src/observation.rs index 1cab558e..7dc0ae56 100644 --- a/crates/labcolors-core/src/observation.rs +++ b/crates/labcolors-core/src/observation.rs @@ -190,7 +190,8 @@ impl ObservedScenarioSet { /// Canonical immutable schema shared by the compiled recheck and every /// admitted observation backing created for it. -#[derive(Debug, Clone, PartialEq, Eq)] +#[derive(Debug, PartialEq, Eq)] +#[cfg_attr(test, derive(Clone))] pub(crate) struct CanonicalObservationSchemaV1(Rc<[SurfaceInputPortId]>); impl CanonicalObservationSchemaV1 { @@ -202,10 +203,22 @@ impl CanonicalObservationSchemaV1 { Rc::ptr_eq(&self.0, &other.0) } + /// Admission is the sole production boundary allowed to share the compiled + /// schema handle: the immutable observation backing must prove the exact + /// schema against which it was admitted. + fn share_for_observation(&self) -> Self { + Self(Rc::clone(&self.0)) + } + #[cfg(test)] pub(crate) fn backing_ptr_for_test(&self) -> *const SurfaceInputPortId { self.0.as_ptr() } + + #[cfg(test)] + pub(crate) fn strong_count_for_test(&self) -> usize { + Rc::strong_count(&self.0) + } } #[derive(Debug, PartialEq, Eq)] @@ -214,7 +227,8 @@ struct ObservationBackingV1 { set: ObservedScenarioSet, } -/// Sealed observation admitted against the Session-owned compiled schema. +/// Sealed observation admitted against the exact schema owned by its sealed +/// Session plan. #[derive(Debug, Clone, PartialEq, Eq)] pub(crate) struct RevisionBoundObservationV1 { stream: ObservationStreamId, @@ -575,7 +589,7 @@ pub(crate) fn prepare_observation<'owner, Owner: ObservationOwnerV1>( stream, revision: update.revision, backing: Rc::new(ObservationBackingV1 { - schema: schema.clone(), + schema: schema.share_for_observation(), set, }), }, @@ -688,7 +702,7 @@ pub(crate) fn prepare_schema_ordered_observation< stream, revision, backing: Rc::new(ObservationBackingV1 { - schema: schema.clone(), + schema: schema.share_for_observation(), set, }), }, diff --git a/crates/labcolors-core/src/observation_tests.rs b/crates/labcolors-core/src/observation_tests.rs index 1aea99f0..579af3a2 100644 --- a/crates/labcolors-core/src/observation_tests.rs +++ b/crates/labcolors-core/src/observation_tests.rs @@ -335,11 +335,21 @@ fn independent_equal_admissions_do_not_alias_observation_or_schema_backing() { left.apply(observed_update(STREAM, 1, first)).unwrap(); right.apply(observed_update(STREAM, 1, second)).unwrap(); - let left = revision_bound(&left); - let right = revision_bound(&right); - assert_eq!(left, right); - assert_ne!(left.backing_ptr_for_test(), right.backing_ptr_for_test()); - assert_ne!(left.schema_ptr_for_test(), right.schema_ptr_for_test()); + let left_observation = revision_bound(&left); + let right_observation = revision_bound(&right); + assert_eq!(left_observation, right_observation); + assert!( + !left_observation.shares_schema_backing_with(&right.schema), + "equal schema values from another owner must not inherit authority", + ); + assert_ne!( + left_observation.backing_ptr_for_test(), + right_observation.backing_ptr_for_test() + ); + assert_ne!( + left_observation.schema_ptr_for_test(), + right_observation.schema_ptr_for_test() + ); } #[test] diff --git a/crates/labcolors-core/src/point_support.rs b/crates/labcolors-core/src/point_support.rs index 94a01b54..a61baa55 100644 --- a/crates/labcolors-core/src/point_support.rs +++ b/crates/labcolors-core/src/point_support.rs @@ -331,7 +331,10 @@ impl SessionPlanV1 for CompiledPointSupportRecheckV1 { Some(()) } - fn observation_schema(&self) -> &CanonicalObservationSchemaV1 { + fn observation_schema<'a>( + &'a self, + _owner: &'a Self::OwnerLease, + ) -> &'a CanonicalObservationSchemaV1 { &self.surface_schema } diff --git a/crates/labcolors-core/src/point_support_tests.rs b/crates/labcolors-core/src/point_support_tests.rs index 83b39fda..25565796 100644 --- a/crates/labcolors-core/src/point_support_tests.rs +++ b/crates/labcolors-core/src/point_support_tests.rs @@ -16,7 +16,7 @@ use crate::point_support::{ PointSupportStabilityAnchorV1, PointSupportStabilityAssessmentV1, PointSupportStabilityDecisionV1, PointSupportStabilityPolicyV1, }; -use crate::session::{Session, SessionState}; +use crate::session::{Session, SessionPlanV1, SessionState}; use crate::wcag22::Wcag22CriterionV1; const STREAM: ObservationStreamId = ObservationStreamId::new(31); @@ -60,6 +60,60 @@ fn compiled( .unwrap() } +#[test] +fn point_support_session_owns_exactly_one_canonical_schema_handle() { + let requirements = compiled(vec![occurrence( + OCCURRENCE_A, + SURFACE_A, + paint(PAINT_A, [0; 3], 1.0), + Some([0; 3]), + PointSupportCriterionRequirementV1::NotRequested, + PointSupportStabilityPolicyV1::Disabled, + )]); + + assert_eq!( + requirements.observation_schema(&()).strong_count_for_test(), + 1, + ); + + let schema_ptr = requirements.observation_schema(&()).backing_ptr_for_test(); + let mut session = Session::new(STREAM, requirements); + assert_eq!( + session + .plan() + .observation_schema(&()) + .strong_count_for_test(), + 1, + ); + + let report_schema_ptr = match session + .update(observed_update(1, [(1, vec![(SURFACE_A, [0; 3])])])) + .unwrap() + { + SessionState::Ready { current } => current.report().observation().schema_ptr_for_test(), + _ => panic!("the exact point-support requirement must verify"), + }; + assert_eq!(report_schema_ptr, schema_ptr); + assert_eq!( + session + .plan() + .observation_schema(&()) + .strong_count_for_test(), + 2, + ); + + session + .update(observed_update(1, [(1, vec![(SURFACE_A, [0; 3])])])) + .unwrap(); + assert_eq!( + session + .plan() + .observation_schema(&()) + .strong_count_for_test(), + 2, + ); +} + fn observed_update( revision: u64, scenarios: impl IntoIterator)>, diff --git a/crates/labcolors-core/src/program_session.rs b/crates/labcolors-core/src/program_session.rs index f542b612..5c49e46b 100644 --- a/crates/labcolors-core/src/program_session.rs +++ b/crates/labcolors-core/src/program_session.rs @@ -1134,6 +1134,14 @@ where .map(|output| output.output) } + #[cfg(test)] + pub(crate) fn observation_schema_strong_count_for_test(&self) -> usize { + self.owner_generation + .observation_group + .schema + .strong_count_for_test() + } + /// Membership is the exact live owner allocation, never equivalent /// compiled content. The Session's `Weak` keeps the old control block /// address reserved until the Session itself is destroyed. @@ -1171,7 +1179,6 @@ where stream, ProgramSessionPlan { owner_generation: Rc::downgrade(&self.owner_generation), - schema: self.owner_generation.observation_group.schema.clone(), bindings, workspace, modeled_occurrences, @@ -1622,7 +1629,6 @@ where ProgramConstraintInvocationOf: Copy, { owner_generation: Weak>, - schema: CanonicalObservationSchemaV1, bindings: AdmittedAppearanceBindings, workspace: AppearanceWorkspace, modeled_occurrences: Vec>, @@ -1649,8 +1655,11 @@ where self.owner_generation.upgrade().map(ProgramOwnerLeaseV1) } - fn observation_schema(&self) -> &CanonicalObservationSchemaV1 { - &self.schema + fn observation_schema<'a>( + &'a self, + owner: &'a Self::OwnerLease, + ) -> &'a CanonicalObservationSchemaV1 { + &owner.0.observation_group.schema } fn evaluate( diff --git a/crates/labcolors-core/src/program_session_tests.rs b/crates/labcolors-core/src/program_session_tests.rs index 50059864..bc933725 100644 --- a/crates/labcolors-core/src/program_session_tests.rs +++ b/crates/labcolors-core/src/program_session_tests.rs @@ -16,7 +16,7 @@ use crate::program_session::{ Source, SourceId, Surface, Target, TargetId, canonical_surface_input_port_sequence_matches, check_render_node_count, }; -use crate::session::{SessionState, SessionUpdateError}; +use crate::session::{SessionPlanV1, SessionState, SessionUpdateError}; const SOURCE: SourceId = SourceId::new(1); const TARGET: TargetId = TargetId::new(1); @@ -548,6 +548,57 @@ fn independently_instantiated_streams_expire_with_their_compiled_owner_generatio assert_eq!(second.raw_head(), ObservationHeadViewV1::Empty); } +#[test] +fn program_sessions_reuse_the_owner_canonical_schema_handle() { + let compiled = exact_compiled(ConstraintSet::new( + vec![ConstraintInvocation::hard( + REQUIRED, + OCCURRENCE, + Srgb8::new([0x80; 3]), + )], + vec![], + )); + + assert_eq!(compiled.observation_schema_strong_count_for_test(), 1); + + let mut first = compiled.instantiate(STREAM_A).unwrap(); + assert_eq!(compiled.observation_schema_strong_count_for_test(), 1); + let second = compiled.instantiate(STREAM_B).unwrap(); + assert_eq!(compiled.observation_schema_strong_count_for_test(), 1); + + drop(second); + assert_eq!(compiled.observation_schema_strong_count_for_test(), 1); + + let schema_ptr = { + let owner = first.plan().try_acquire_owner().unwrap(); + first + .plan() + .observation_schema(&owner) + .backing_ptr_for_test() + }; + let report_schema_ptr = match first + .update(observed_update(STREAM_A, 1, &[(1, [0xFF; 3])])) + .unwrap() + { + SessionState::Ready { current } => current.report().observation().schema_ptr_for_test(), + _ => panic!("the exact Program must verify"), + }; + assert_eq!(report_schema_ptr, schema_ptr); + let ObservationHeadViewV1::Observed(raw) = first.raw_head() else { + panic!("the raw head must retain the admitted observation"); + }; + assert_eq!(raw.schema_ptr_for_test(), schema_ptr); + assert_eq!(compiled.observation_schema_strong_count_for_test(), 2); + + first + .update(observed_update(STREAM_A, 1, &[(1, [0xFF; 3])])) + .unwrap(); + assert_eq!(compiled.observation_schema_strong_count_for_test(), 2); + + drop(first); + assert_eq!(compiled.observation_schema_strong_count_for_test(), 1); +} + #[test] fn multi_case_hard_failure_retains_the_full_matrix_without_outputs() { let low = ConstraintId::new(1); diff --git a/crates/labcolors-core/src/session.rs b/crates/labcolors-core/src/session.rs index b873580b..9b8d9be6 100644 --- a/crates/labcolors-core/src/session.rs +++ b/crates/labcolors-core/src/session.rs @@ -78,7 +78,13 @@ pub(crate) trait SessionPlanV1: private::PlanSealed { fn try_acquire_owner(&self) -> Option; - fn observation_schema(&self) -> &CanonicalObservationSchemaV1; + /// Return the canonical schema reached through the same owner lease that + /// will authorize evaluation. Self-owned plans may return their own schema; + /// weakly bound plans must derive it from the pinned generation. + fn observation_schema<'a>( + &'a self, + owner: &'a Self::OwnerLease, + ) -> &'a CanonicalObservationSchemaV1; fn evaluate( &mut self, @@ -156,7 +162,6 @@ type SessionUpdateResult<'session, Plan> = Result< #[derive(Debug)] pub(crate) struct Session { stream: ObservationStreamId, - schema: CanonicalObservationSchemaV1, plan: Plan, raw_head: SessionObservationHeadV1, state: SessionState, @@ -164,10 +169,8 @@ pub(crate) struct Session { impl Session { pub(crate) fn new(stream: ObservationStreamId, plan: Plan) -> Self { - let schema = plan.observation_schema().clone(); Self { stream, - schema, plan, raw_head: SessionObservationHeadV1::Empty, state: SessionState::Waiting, @@ -199,7 +202,8 @@ impl Session { .plan .try_acquire_owner() .ok_or(SessionUpdateError::OwnerExpired)?; - let prepared = prepare_observation(&mut self.raw_head, self.stream, &self.schema, update) + let schema = self.plan.observation_schema(&owner); + let prepared = prepare_observation(&mut self.raw_head, self.stream, schema, update) .map_err(SessionUpdateError::Observation)?; apply_prepared_update(&mut self.plan, &mut self.state, &owner, prepared) @@ -232,10 +236,11 @@ impl Session { .plan .try_acquire_owner() .ok_or(SessionUpdateError::OwnerExpired)?; + let schema = self.plan.observation_schema(&owner); let prepared = prepare_schema_ordered_observation( &mut self.raw_head, self.stream, - &self.schema, + schema, revision, source, order_scratch, diff --git a/crates/labcolors-core/src/session_tests.rs b/crates/labcolors-core/src/session_tests.rs index 2da91b7f..76ad9d8d 100644 --- a/crates/labcolors-core/src/session_tests.rs +++ b/crates/labcolors-core/src/session_tests.rs @@ -7,8 +7,8 @@ use crate::lcs_occurrence::ColorSignal; use crate::observation::{ CanonicalObservationSchemaV1, ObservationError, ObservationHeadViewV1, ObservationPayloadInput, ObservationStreamId, ObservationUpdateInput, ObservedScenarioSetInput, Revision, - RevisionBoundObservationV1, ScenarioId, ScenarioInput, SurfaceInputBinding, UnknownReasonId, - canonicalize_observation_schema, + RevisionBoundObservationV1, ScenarioId, ScenarioInput, SchemaOrderedScenarioSourceV1, + SurfaceInputBinding, UnknownReasonId, canonicalize_observation_schema, }; use crate::session::{ Session, SessionDecision, SessionEvidenceV1, SessionObservationBindingPermitV1, SessionPlanV1, @@ -91,7 +91,10 @@ impl SessionPlanV1 for SentinelPlan { Some(()) } - fn observation_schema(&self) -> &CanonicalObservationSchemaV1 { + fn observation_schema<'a>( + &'a self, + _owner: &'a Self::OwnerLease, + ) -> &'a CanonicalObservationSchemaV1 { &self.schema } @@ -133,17 +136,21 @@ impl SessionPlanV1 for SentinelPlan { } #[derive(Debug)] -struct ReplacingOwnerPlan { +struct ReplacingOwnerGeneration { schema: CanonicalObservationSchemaV1, - generation: std::rc::Weak<()>, - owner_slot: Rc>>>, +} + +#[derive(Debug)] +struct ReplacingOwnerPlan { + generation: std::rc::Weak, + owner_slot: Rc>>>, evaluations: Rc>, } impl session_private::PlanSealed for ReplacingOwnerPlan {} impl SessionPlanV1 for ReplacingOwnerPlan { - type OwnerLease = Rc<()>; + type OwnerLease = Rc; type Verified = SentinelVerified; type Violation = SentinelViolation; type Error = SentinelError; @@ -152,8 +159,11 @@ impl SessionPlanV1 for ReplacingOwnerPlan { self.generation.upgrade() } - fn observation_schema(&self) -> &CanonicalObservationSchemaV1 { - &self.schema + fn observation_schema<'a>( + &'a self, + owner: &'a Self::OwnerLease, + ) -> &'a CanonicalObservationSchemaV1 { + &owner.schema } fn evaluate( @@ -163,10 +173,16 @@ impl SessionPlanV1 for ReplacingOwnerPlan { _permit: SessionObservationBindingPermitV1, ) -> Result, Self::Error> { self.evaluations.set(self.evaluations.get() + 1); + assert!( + observation.shares_schema_backing_with(&owner.schema), + "admission and evaluation must use the same pinned generation" + ); let old_generation = self .owner_slot .borrow_mut() - .replace(Rc::new(())) + .replace(Rc::new(ReplacingOwnerGeneration { + schema: canonicalize_observation_schema(vec![SURFACE]).unwrap(), + })) .expect("the first owner generation must still be installed"); assert!(Rc::ptr_eq(owner, &old_generation)); drop(old_generation); @@ -178,6 +194,32 @@ impl SessionPlanV1 for ReplacingOwnerPlan { } } +struct OneOrderedScenario { + id: ScenarioId, + value: Srgb8, +} + +impl SchemaOrderedScenarioSourceV1 for OneOrderedScenario { + fn scenario_count(&self) -> usize { + 1 + } + + fn scenario_id(&self, scenario_index: usize) -> ScenarioId { + assert_eq!(scenario_index, 0); + self.id + } + + fn value_count(&self, scenario_index: usize) -> usize { + assert_eq!(scenario_index, 0); + 1 + } + + fn value(&self, scenario_index: usize, binding_index: usize) -> Srgb8 { + assert_eq!((scenario_index, binding_index), (0, 0)); + self.value + } +} + fn session() -> ( Session, SentinelControl, @@ -346,6 +388,51 @@ fn exact_replay_is_idempotent_and_never_invokes_the_plan() { assert_eq!(session.raw_head().revision(), Some(Revision::new(2))); } +#[test] +fn schema_ordered_admission_shares_only_the_plan_schema_handle() { + let (mut session, control, schema_ptr) = session(); + assert_eq!( + session + .plan() + .observation_schema(&()) + .strong_count_for_test(), + 1, + ); + let source = OneOrderedScenario { + id: ScenarioId::new(1), + value: Srgb8::new([255; 3]), + }; + let mut order_scratch = Vec::new(); + + let SessionState::Ready { current } = session + .update_schema_ordered(Revision::new(1), &source, &mut order_scratch) + .unwrap() + else { + panic!("white sentinel input must verify"); + }; + assert_eq!(current.observation.schema_ptr_for_test(), schema_ptr); + assert_eq!( + session + .plan() + .observation_schema(&()) + .strong_count_for_test(), + 2, + ); + assert_eq!(control.evaluation_count(), 1); + + session + .update_schema_ordered(Revision::new(1), &source, &mut order_scratch) + .unwrap(); + assert_eq!( + session + .plan() + .observation_schema(&()) + .strong_count_for_test(), + 2, + ); + assert_eq!(control.evaluation_count(), 1); +} + #[test] fn equal_content_at_a_higher_revision_rebinds_fresh_evidence() { let (mut session, control, _) = session(); @@ -467,14 +554,14 @@ fn detached_plan_evidence_is_rejected_before_raw_or_lifecycle_commit() { #[test] fn reentrant_owner_replacement_finishes_on_its_pinned_generation_then_expires() { - let schema = canonicalize_observation_schema(vec![SURFACE]).unwrap(); - let first_generation = Rc::new(()); + let first_generation = Rc::new(ReplacingOwnerGeneration { + schema: canonicalize_observation_schema(vec![SURFACE]).unwrap(), + }); let owner_slot = Rc::new(RefCell::new(Some(Rc::clone(&first_generation)))); let evaluations = Rc::new(Cell::new(0)); let mut session = Session::new( STREAM, ReplacingOwnerPlan { - schema, generation: Rc::downgrade(&first_generation), owner_slot: Rc::clone(&owner_slot), evaluations: Rc::clone(&evaluations), diff --git a/scripts/verify_point_support_surplus.py b/scripts/verify_point_support_surplus.py index c7c8aa2f..2a0b3993 100755 --- a/scripts/verify_point_support_surplus.py +++ b/scripts/verify_point_support_surplus.py @@ -58,7 +58,7 @@ SOURCE_BINDING_LAW = "point-support-rust-whole-file-semantic-cone-v2" SOURCE_BINDING_DOMAIN = b"labcolors.point-support.rust-whole-file-semantic-cone.v2" EXPECTED_SOURCE_CAPSULE_SHA256 = ( - "ac2e23b4d89850df7bc6697a79dfc715192e998bbabcf47fe88c415e8c332df8" + "669326bce56a2901f7fbbd8b4c23f26f8b33daceb1471b81c98763940b41d3e4" ) EXPECTED_Q55_PROOF_SHA256 = ( "ac59cf89503170c789223b91d775213a19d4e571ef930f2ea609fcd51b14defd" @@ -201,7 +201,7 @@ def verify_source_binding() -> tuple[str, int]: (OBSERVATION_SOURCE, b" self.backing.set.values(case_index)\n", b" None\n"), (OBSERVATION_SOURCE, b" values.extend(bindings.iter().map(|binding| binding.value));\n", b" values.extend(bindings.iter().map(|_| Srgb8::new([0, 0, 0])));\n"), (OBSERVATION_SOURCE, b" Rc::ptr_eq(&self.0, &other.0)\n", b" self == other\n"), - (OBSERVATION_SOURCE, b" schema: schema.clone(),\n", b" schema: CanonicalObservationSchemaV1(Rc::from(schema.as_slice())),\n"), + (OBSERVATION_SOURCE, b" Self(Rc::clone(&self.0))\n", b" Self(Rc::from(self.as_slice()))\n"), (OBSERVATION_SOURCE, b"if expected_input != actual_input", b"if expected_input == actual_input"), (OBSERVATION_SOURCE, b"Some(observation.revision)", b"None"), (OBSERVATION_SOURCE, b"(self.owner, self.observation)", b"unreachable!()"), @@ -385,11 +385,10 @@ def multiply( result: dict[tuple[int, ...], int] = {} for left_monomial, left_coefficient in left.items(): for right_monomial, right_coefficient in right.items(): + assert len(left_monomial) == len(right_monomial) monomial = tuple( left_power + right_power - for left_power, right_power in zip( - left_monomial, right_monomial, strict=True - ) + for left_power, right_power in zip(left_monomial, right_monomial) ) result[monomial] = ( result.get(monomial, 0) + left_coefficient * right_coefficient From 43d94980b4c6e94b9ab49fc74de2d246ebac0d74 Mon Sep 17 00:00:00 2001 From: Daniel from Labpics <63733699+lemone112@users.noreply.github.com> Date: Sun, 26 Jul 2026 09:21:45 +0300 Subject: [PATCH 2/2] chore(proof): document Python 3.9 zip invariant --- .../point-support-reference-surplus-q55-bps-proof-v1.json | 2 +- scripts/verify_point_support_surplus.py | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/crates/labcolors-core/contracts/point-support-reference-surplus-q55-bps-proof-v1.json b/crates/labcolors-core/contracts/point-support-reference-surplus-q55-bps-proof-v1.json index 30b34af0..13d9b054 100644 --- a/crates/labcolors-core/contracts/point-support-reference-surplus-q55-bps-proof-v1.json +++ b/crates/labcolors-core/contracts/point-support-reference-surplus-q55-bps-proof-v1.json @@ -1 +1 @@ -{"artifact_id":"wcag22-srgb8-luminance-q55-v1","basis_point_proof":{"checks":30,"drop_all_semantics":"zero required surplus; current must still meet the anchor","drop_domain_inclusive":[0,10000],"nonpositive_baseline_semantics":"zero required surplus; current must meet the anchor"},"bound_id":"point-support-reference-surplus-q55-bps-v1","certified_claim":"for every successfully evaluated enabled stability cell, decision is Retained iff current_lower_surplus >= (10000-drop_bps)/10000 * max(baseline_lower_surplus,0); the declared anchor remains a separate hard floor","comparator_proof":{"algorithm":"euclidean-continued-fraction-ordering-v1","dense_denominator_inclusive":[1,31],"dense_numerator_inclusive":[0,31],"dense_small_cases":984064,"invariant":"equal integer parts; reciprocal proper fractions reverse order","largest_fibonacci_index":186,"oracle":"unbounded-integer-cross-product","random_cases":250000,"random_corpus_sha256":"97c4af7b452b31a4ab92645f70c17acb38bf57ca55484e32ad9d7d79d97a333d","random_seed":210583930,"termination":"each nonterminal denominator becomes a strictly smaller remainder","u128_adversarial_cases":190},"declared_operation_law":"q55-lower-reference-distance-explicit-anchor-bps-retention-v1","excluded_claim":"does not certify retention against the unknown exact baseline surplus, renderer equivalence outside encoded-sRGB8 source-over, or a successful result when evaluation fails","integer_replay_envelope":{"assumption":"every Q55 luminance upper <= scale + 3","i128_max":170141183460469231731687303715884105727,"offset_cleared_denominator_max":756604737398243388,"positive_baseline_numerator_max":1188950301625811064,"rational_denominator_max":1513209474796486776,"required_denominator_max":15132094747964867760000,"required_numerator_max":11889503016258110640000,"signed_anchor_abs_coarse_max":5296233161787703716,"u128_max":340282366920938463463374607431768211455,"u64_max":18446744073709551615},"profile_id":"srgb8-q55-retained-reference-surplus-bps-v1","proof_id":"point-support-reference-surplus-integer-v1","proof_payload_sha256":"20af49448f088da3b30a0e31b8e5b9bb2e23b36a470bcac351c2629e3f345a48","q55_dependency":{"artifact_id":"wcag22-srgb8-luminance-q55-v1","artifact_sha256":"7ff239d9052b346f3c50da01ca65ca2330892ed1a3ff30e190797fcef6f03604","maximum_luminance_upper":36028797018963971,"outward_interval_width_bound":3,"proof_id":"wcag22-srgb8-full-domain-q55-v1","proof_payload_sha256":"3c639a7c875046c46b56b51ecdd67d5ecaf14a1134490c88a222e7037b63c0f2","proof_sha256":"ac59cf89503170c789223b91d775213a19d4e571ef930f2ea609fcd51b14defd","q55_scale":36028797018963968},"reference_and_anchor_proof":{"anchor_identity_checks":75,"orientation_law":"distance-magnitude-symmetric-orientation-reported-separately","overlap_lower_distance":"0/1","separated_endpoint_checks":504},"schema_version":2,"site_id":"point-support-retained-reference-surplus-v1","source_binding_exclusions":["whole-crate compilation or compiler/toolchain attestation","binary, package, FFI, renderer, or browser transport attestation","unrelated Lab Colors modules outside the declared point-support semantic cone"],"source_binding_law":"point-support-rust-whole-file-semantic-cone-v2","source_binding_schema_version":2,"source_binding_scope":"exact bytes of the private point-support Rust semantic cone and its two WCAG include_str inputs; comments and cfg(test) text are intentionally significant","source_closure_sha256":"669326bce56a2901f7fbbd8b4c23f26f8b33daceb1471b81c98763940b41d3e4","source_files":[{"kind":"compile-time-input","path":"crates/labcolors-core/contracts/wcag22-srgb8-q55-proof-v1.json","sha256":"ac59cf89503170c789223b91d775213a19d4e571ef930f2ea609fcd51b14defd"},{"kind":"compile-time-input","path":"crates/labcolors-core/contracts/wcag22-srgb8-v1.json","sha256":"b4bb7e5f17a99f2c911fdbe3da23a48b049277b796291094950f14680cc3cc7b"},{"kind":"rust-source","path":"crates/labcolors-core/src/appearance.rs","sha256":"09be54900efe29ffdac8705efd0d6d613055c90d634446ca4b228f51a63997d0"},{"kind":"rust-source","path":"crates/labcolors-core/src/composition.rs","sha256":"195a67327a3bd86d7816b634481389930bf68577bb1202fad14c2ea152df8625"},{"kind":"rust-source","path":"crates/labcolors-core/src/constraints/exact.rs","sha256":"892576a8621185352583e63dc0a1aacac32e32a8063b6fe24ae16d4ff9dce7cb"},{"kind":"rust-source","path":"crates/labcolors-core/src/constraints/mod.rs","sha256":"e73b9c0b8c3a4112cb53987753d5a6b5f639774b0b872afaea9836e6647a2f7d"},{"kind":"rust-source","path":"crates/labcolors-core/src/constraints/wcag22.rs","sha256":"856093c91159d8b3faab001f2d6524d33d7b16458a5a4e98ea65f8c62ab2694c"},{"kind":"rust-source","path":"crates/labcolors-core/src/hash.rs","sha256":"f97a0fd7d6ad3162f0f1dfb326fccfb7ed40da9a8fa67a5b8a239a1ae2ae49c3"},{"kind":"rust-source","path":"crates/labcolors-core/src/lcs_occurrence.rs","sha256":"6f202ad7425a235b9d18caba0c817fc33a2b8e042050a34f5ddff3fd09efc53d"},{"kind":"rust-source","path":"crates/labcolors-core/src/lib.rs","sha256":"b3edb3764119c0b4fd50f52b62cbc07fa81c4bfdf1246b91f20eb3d8d4eebd31"},{"kind":"rust-source","path":"crates/labcolors-core/src/numerics.rs","sha256":"e73a12136494f2ef9aca4e943ab38302c1439f054cecab36a552d35252c164f9"},{"kind":"rust-source","path":"crates/labcolors-core/src/observation.rs","sha256":"887f139e6750cc99cd751b3c7e47276971293f74091130028a1746fa29ebb104"},{"kind":"rust-source","path":"crates/labcolors-core/src/point_support.rs","sha256":"6f6a376ff036d3d65960c004e6566e1bca580f19f5bd3cd333a80b0da5b5c242"},{"kind":"rust-source","path":"crates/labcolors-core/src/session.rs","sha256":"4f77643206077c080e5e9b182e896145bfb69bf3db8aa4c1ac7d4c5360ea8504"},{"kind":"rust-source","path":"crates/labcolors-core/src/srgb8.rs","sha256":"6c95324eb05476f35f75375a9af0b2b4a41b8b2978c46e67d2ce1aea5adde342"},{"kind":"rust-source","path":"crates/labcolors-core/src/wcag22.rs","sha256":"7ba7864eb7e73789bad6c63c64a4dc2dcc08c2da6921375fb9564fca230c2780"},{"kind":"rust-source","path":"crates/labcolors-core/src/wcag22/kernel.rs","sha256":"c97980c1ca2c7ea9cabff9c8d2fb7282773cca180ae15948391c29c9d6196040"},{"kind":"rust-source","path":"crates/labcolors-core/src/wcag22/q55_data.rs","sha256":"af4d23d6b70c45ce6efa839e7dda4bb0a61f6aae43cb805af6fa9b29e6c3bae2"},{"kind":"rust-source","path":"crates/labcolors-core/src/wcag22_evidence.rs","sha256":"3c5a75b07254c6071a64700af208a64987d0f0ea9698eadc54a9e74585ce1f72"}],"source_negative_controls":43,"universal_algebraic_certificate":{"basis_point_scale_instantiation":10000,"domain":"integers; Q55 scale Q>0; anchor L>=D>=0; lighter monotonicity L2>=L1>D>=0; darker monotonicity L>D2>=D1>=0; current/baseline denominators b,q>0; basis-point scale B>0 instantiated as 10000; p>0; a>=0; 0<=drop_bps<=B","identities":["three explicit anchor-surplus formulas after denominator clearing","reference distance is monotone increasing in lighter L","reference distance is monotone decreasing in darker D","positive-baseline retained threshold is p*(B-drop)/(q*B)","a/b >= p*(B-drop)/(q*B) iff a*q*B >= p*(B-drop)*b"],"method":"exact-sparse-integer-polynomial-identities-plus-positive-denominator-order-lemma-v1","nonpositive_baseline_case":"max(baseline,0)=0; retained threshold is exactly zero","symbolic_mutation_controls":{"anchor_coefficients_and_denominator":6,"retained_cross_product":5},"wolfram_language_cross_check":{"query":"FullSimplify[{20 g/d - 0 == 20 g/d, 20 g/d - 2 == (20 g - 2 d)/d, 20 g/d - 7/2 == (40 g - 7 d)/(2 d), Equivalent[a/b >= p (s-x)/(q s), a q s >= p (s-x) b], Max[p/q, 0] (s-x)/s == Piecewise[{{0, p <= 0}}, p (s-x)/(q s)]}, Assumptions -> Element[{a,b,p,q,s,x,g,d}, Integers] && a >= 0 && b > 0 && q > 0 && s > 0 && 0 <= x <= s && d > 0 && g >= 0]","query_sha256":"8cdbb9964583030c8b92498961896cb2a98613f1cb31eb7c54acdf8e16beff10","result":"{True, True, True, True, True}","result_sha256":"13a8f2ee8d0fde335a638e46d7cc8a8427b9a1437c77d22cfcf925bb87fa6303"}},"verifier_sha256":"1889fd73f85a80d1d9daacd6bb2261e87d3a02df49304d6016c37825252c6af8"} +{"artifact_id":"wcag22-srgb8-luminance-q55-v1","basis_point_proof":{"checks":30,"drop_all_semantics":"zero required surplus; current must still meet the anchor","drop_domain_inclusive":[0,10000],"nonpositive_baseline_semantics":"zero required surplus; current must meet the anchor"},"bound_id":"point-support-reference-surplus-q55-bps-v1","certified_claim":"for every successfully evaluated enabled stability cell, decision is Retained iff current_lower_surplus >= (10000-drop_bps)/10000 * max(baseline_lower_surplus,0); the declared anchor remains a separate hard floor","comparator_proof":{"algorithm":"euclidean-continued-fraction-ordering-v1","dense_denominator_inclusive":[1,31],"dense_numerator_inclusive":[0,31],"dense_small_cases":984064,"invariant":"equal integer parts; reciprocal proper fractions reverse order","largest_fibonacci_index":186,"oracle":"unbounded-integer-cross-product","random_cases":250000,"random_corpus_sha256":"97c4af7b452b31a4ab92645f70c17acb38bf57ca55484e32ad9d7d79d97a333d","random_seed":210583930,"termination":"each nonterminal denominator becomes a strictly smaller remainder","u128_adversarial_cases":190},"declared_operation_law":"q55-lower-reference-distance-explicit-anchor-bps-retention-v1","excluded_claim":"does not certify retention against the unknown exact baseline surplus, renderer equivalence outside encoded-sRGB8 source-over, or a successful result when evaluation fails","integer_replay_envelope":{"assumption":"every Q55 luminance upper <= scale + 3","i128_max":170141183460469231731687303715884105727,"offset_cleared_denominator_max":756604737398243388,"positive_baseline_numerator_max":1188950301625811064,"rational_denominator_max":1513209474796486776,"required_denominator_max":15132094747964867760000,"required_numerator_max":11889503016258110640000,"signed_anchor_abs_coarse_max":5296233161787703716,"u128_max":340282366920938463463374607431768211455,"u64_max":18446744073709551615},"profile_id":"srgb8-q55-retained-reference-surplus-bps-v1","proof_id":"point-support-reference-surplus-integer-v1","proof_payload_sha256":"2e7c31a9b66fa310e0a7e33291bc167283157034703c47d86d7e22b5323acee6","q55_dependency":{"artifact_id":"wcag22-srgb8-luminance-q55-v1","artifact_sha256":"7ff239d9052b346f3c50da01ca65ca2330892ed1a3ff30e190797fcef6f03604","maximum_luminance_upper":36028797018963971,"outward_interval_width_bound":3,"proof_id":"wcag22-srgb8-full-domain-q55-v1","proof_payload_sha256":"3c639a7c875046c46b56b51ecdd67d5ecaf14a1134490c88a222e7037b63c0f2","proof_sha256":"ac59cf89503170c789223b91d775213a19d4e571ef930f2ea609fcd51b14defd","q55_scale":36028797018963968},"reference_and_anchor_proof":{"anchor_identity_checks":75,"orientation_law":"distance-magnitude-symmetric-orientation-reported-separately","overlap_lower_distance":"0/1","separated_endpoint_checks":504},"schema_version":2,"site_id":"point-support-retained-reference-surplus-v1","source_binding_exclusions":["whole-crate compilation or compiler/toolchain attestation","binary, package, FFI, renderer, or browser transport attestation","unrelated Lab Colors modules outside the declared point-support semantic cone"],"source_binding_law":"point-support-rust-whole-file-semantic-cone-v2","source_binding_schema_version":2,"source_binding_scope":"exact bytes of the private point-support Rust semantic cone and its two WCAG include_str inputs; comments and cfg(test) text are intentionally significant","source_closure_sha256":"669326bce56a2901f7fbbd8b4c23f26f8b33daceb1471b81c98763940b41d3e4","source_files":[{"kind":"compile-time-input","path":"crates/labcolors-core/contracts/wcag22-srgb8-q55-proof-v1.json","sha256":"ac59cf89503170c789223b91d775213a19d4e571ef930f2ea609fcd51b14defd"},{"kind":"compile-time-input","path":"crates/labcolors-core/contracts/wcag22-srgb8-v1.json","sha256":"b4bb7e5f17a99f2c911fdbe3da23a48b049277b796291094950f14680cc3cc7b"},{"kind":"rust-source","path":"crates/labcolors-core/src/appearance.rs","sha256":"09be54900efe29ffdac8705efd0d6d613055c90d634446ca4b228f51a63997d0"},{"kind":"rust-source","path":"crates/labcolors-core/src/composition.rs","sha256":"195a67327a3bd86d7816b634481389930bf68577bb1202fad14c2ea152df8625"},{"kind":"rust-source","path":"crates/labcolors-core/src/constraints/exact.rs","sha256":"892576a8621185352583e63dc0a1aacac32e32a8063b6fe24ae16d4ff9dce7cb"},{"kind":"rust-source","path":"crates/labcolors-core/src/constraints/mod.rs","sha256":"e73b9c0b8c3a4112cb53987753d5a6b5f639774b0b872afaea9836e6647a2f7d"},{"kind":"rust-source","path":"crates/labcolors-core/src/constraints/wcag22.rs","sha256":"856093c91159d8b3faab001f2d6524d33d7b16458a5a4e98ea65f8c62ab2694c"},{"kind":"rust-source","path":"crates/labcolors-core/src/hash.rs","sha256":"f97a0fd7d6ad3162f0f1dfb326fccfb7ed40da9a8fa67a5b8a239a1ae2ae49c3"},{"kind":"rust-source","path":"crates/labcolors-core/src/lcs_occurrence.rs","sha256":"6f202ad7425a235b9d18caba0c817fc33a2b8e042050a34f5ddff3fd09efc53d"},{"kind":"rust-source","path":"crates/labcolors-core/src/lib.rs","sha256":"b3edb3764119c0b4fd50f52b62cbc07fa81c4bfdf1246b91f20eb3d8d4eebd31"},{"kind":"rust-source","path":"crates/labcolors-core/src/numerics.rs","sha256":"e73a12136494f2ef9aca4e943ab38302c1439f054cecab36a552d35252c164f9"},{"kind":"rust-source","path":"crates/labcolors-core/src/observation.rs","sha256":"887f139e6750cc99cd751b3c7e47276971293f74091130028a1746fa29ebb104"},{"kind":"rust-source","path":"crates/labcolors-core/src/point_support.rs","sha256":"6f6a376ff036d3d65960c004e6566e1bca580f19f5bd3cd333a80b0da5b5c242"},{"kind":"rust-source","path":"crates/labcolors-core/src/session.rs","sha256":"4f77643206077c080e5e9b182e896145bfb69bf3db8aa4c1ac7d4c5360ea8504"},{"kind":"rust-source","path":"crates/labcolors-core/src/srgb8.rs","sha256":"6c95324eb05476f35f75375a9af0b2b4a41b8b2978c46e67d2ce1aea5adde342"},{"kind":"rust-source","path":"crates/labcolors-core/src/wcag22.rs","sha256":"7ba7864eb7e73789bad6c63c64a4dc2dcc08c2da6921375fb9564fca230c2780"},{"kind":"rust-source","path":"crates/labcolors-core/src/wcag22/kernel.rs","sha256":"c97980c1ca2c7ea9cabff9c8d2fb7282773cca180ae15948391c29c9d6196040"},{"kind":"rust-source","path":"crates/labcolors-core/src/wcag22/q55_data.rs","sha256":"af4d23d6b70c45ce6efa839e7dda4bb0a61f6aae43cb805af6fa9b29e6c3bae2"},{"kind":"rust-source","path":"crates/labcolors-core/src/wcag22_evidence.rs","sha256":"3c5a75b07254c6071a64700af208a64987d0f0ea9698eadc54a9e74585ce1f72"}],"source_negative_controls":43,"universal_algebraic_certificate":{"basis_point_scale_instantiation":10000,"domain":"integers; Q55 scale Q>0; anchor L>=D>=0; lighter monotonicity L2>=L1>D>=0; darker monotonicity L>D2>=D1>=0; current/baseline denominators b,q>0; basis-point scale B>0 instantiated as 10000; p>0; a>=0; 0<=drop_bps<=B","identities":["three explicit anchor-surplus formulas after denominator clearing","reference distance is monotone increasing in lighter L","reference distance is monotone decreasing in darker D","positive-baseline retained threshold is p*(B-drop)/(q*B)","a/b >= p*(B-drop)/(q*B) iff a*q*B >= p*(B-drop)*b"],"method":"exact-sparse-integer-polynomial-identities-plus-positive-denominator-order-lemma-v1","nonpositive_baseline_case":"max(baseline,0)=0; retained threshold is exactly zero","symbolic_mutation_controls":{"anchor_coefficients_and_denominator":6,"retained_cross_product":5},"wolfram_language_cross_check":{"query":"FullSimplify[{20 g/d - 0 == 20 g/d, 20 g/d - 2 == (20 g - 2 d)/d, 20 g/d - 7/2 == (40 g - 7 d)/(2 d), Equivalent[a/b >= p (s-x)/(q s), a q s >= p (s-x) b], Max[p/q, 0] (s-x)/s == Piecewise[{{0, p <= 0}}, p (s-x)/(q s)]}, Assumptions -> Element[{a,b,p,q,s,x,g,d}, Integers] && a >= 0 && b > 0 && q > 0 && s > 0 && 0 <= x <= s && d > 0 && g >= 0]","query_sha256":"8cdbb9964583030c8b92498961896cb2a98613f1cb31eb7c54acdf8e16beff10","result":"{True, True, True, True, True}","result_sha256":"13a8f2ee8d0fde335a638e46d7cc8a8427b9a1437c77d22cfcf925bb87fa6303"}},"verifier_sha256":"e93845aacc62968c9a21a1c7b8ef7222434b64c2100e3a177b3288051d03507d"} diff --git a/scripts/verify_point_support_surplus.py b/scripts/verify_point_support_surplus.py index 2a0b3993..858b86ce 100755 --- a/scripts/verify_point_support_surplus.py +++ b/scripts/verify_point_support_surplus.py @@ -386,6 +386,8 @@ def multiply( for left_monomial, left_coefficient in left.items(): for right_monomial, right_coefficient in right.items(): assert len(left_monomial) == len(right_monomial) + # Python 3.9 lacks zip(..., strict=True); this assertion gives + # the same no-truncation guarantee without raising the floor. monomial = tuple( left_power + right_power for left_power, right_power in zip(left_monomial, right_monomial)