Execute the M2 admission refusal spine and four discriminating controls

dag/gunbc/census_closure_frontier.dag

@@ -44,6 +44,8 @@ import extdeps.ebay.marketplace_account_deletion { ebay_account_deletion_frontie
 import gunbc.cloudflare.r2_permission_group_observe { cloudflare_permission_group_observation_frontier_rows }
 import gunbc.where_refinement_predicate_vocabulary { http_status_where_clause_names_declaration_frontier_rows }
 
+import product.fabric.job_admission { job_admission_frontier_rows }
+
 fn census_closure_frontier_row_groups() -> List<List<FrontierRow>> {
   [
     hetzner_money_rate_frontier_rows,
@@ -80,6 +82,7 @@ fn census_closure_frontier_row_groups() -> List<List<FrontierRow>> {
     cloudflare_permission_group_observation_frontier_rows,
     http_status_where_clause_names_declaration_frontier_rows,
     colo_types_frontier_rows,
+    job_admission_frontier_rows,
   ]
 }
 

dag/gunbc/product/fabric/job_admission.dag

@@ -0,0 +1,107 @@
+module product.fabric.job_admission
+
+import std.types { List }
+import std.roster_frontier { FrontierRow, frontier_row_decl }
+import std.decl_ref { decl_ref }
+import std.dissolution { unbound_dissolution }
+import v2.std.optional { Present, Absent }
+import product.fabric.identity { FabricIdentity, WorkKey, fabric_identity_eq }
+
+// Customer declaration admission precedes provider-route selection. This is a
+// stated divergence from product.fabric.provider_admission: its ProviderUseScope
+// and data_handling_profile establish permission for a chosen route under a
+// posture revision, with agreement and program dispositions. This fold has no
+// route or posture and establishes only whether a declaration can advance to
+// that gate. Its receipt is not a ProviderUsePermit and cannot replace one.
+// Unresolved customer classification HOLDS before a route is selected; provider
+// disposition uncertainty retains provider_admission's own refusal semantics.
+// These are declarations at the customer boundary, not a compliance regime.
+// No producer currently supplies authority to handle declared ePHI. A declaration
+// of ordinary data is not evidence of a broader handling authority.
+type JobClassification
+  = DeclaredNonEphi
+  | DeclaredEphi
+  | ClassificationUnresolved
+
+type JobAdmissionRefusal
+  = EphiHandlingAuthorityHasNoProducer
+  | ClassificationReceiptMissing
+  | ClassificationReceiptSubjectMismatch
+
+type JobClassificationReceipt<P> sole_constructor {
+  subject: FabricIdentity<P, WorkKey>
+  issuer_frontier: FrontierRow
+}
+
+// Explicitly deferred by cool-crane-190 for the pre-regime admission spine.
+// Carried by each receipt so its missing authority cannot disappear in transport.
+data classification_receipt_issuer_frontier: FrontierRow = frontier_row_decl(
+  ref: decl_ref(module_path: "product.fabric.job_admission", decl_name: "JobClassificationReceipt"),
+  reason: "This self-issued receipt establishes that classification was performed, not that an authenticated principal authorized admission. An independently authorized issuer is owed.",
+  dissolution: unbound_dissolution(description: "An issuer authority binds admission evidence to an authenticated customer principal and refuses self-issued evidence on the deployed admission path. A declared issuer type alone does not discharge this frontier."),
+)
+
+data job_admission_billing_frontier: FrontierRow = frontier_row_decl(
+  ref: decl_ref(module_path: "test.claim.job_admission_witness", decl_name: "submit_invoice_fixture"),
+  reason: "The zero-net invoice join is exercised by a fixture; the real billing receipt is not yet its consumer.",
+  dissolution: unbound_dissolution(description: "billing-receipts joins metered usage times founding price, promotional credit, and net due to the admission result for the same work identity, and executes controls proving a zero-net invoice preserves admission, hold, and refusal. A fixture or declared invoice type alone is insufficient."),
+)
+
+data job_admission_runner_frontier: FrontierRow = frontier_row_decl(
+  ref: decl_ref(module_path: "product.fabric.job_admission", decl_name: "admit_job"),
+  reason: "Pure witnesses execute this fold; they do not establish enforcement on the deployed runner launch path.",
+  dissolution: unbound_dissolution(description: "The deployed runner calls admit_job before launch and only launches its admitted arm, with executed controls proving held and refused jobs cannot launch. The separate authenticated-issuer obligation must also be discharged before treating this result as authenticated admission authorization."),
+)
+
+// Known-red admission is temporary feature-gap quarantine, not permanent
+// mutation evidence (gunbc.explicit_witness_admission.known_red_class_note).
+// floor_expected_red likewise requires a row to be under repair. Neither is
+// authority to quarantine an intentionally broken admission fixture forever.
+data job_admission_mutation_harness_frontier: FrontierRow = frontier_row_decl(
+  ref: decl_ref(module_path: "test.claim.job_admission_witness", decl_name: "zero_dollar_net_invoice_cannot_admit_a_job_with_another_jobs_receipt"),
+  reason: "The invoice bypass is authorable as fixture source, but its mutation proof has no permanent expected-red consumer. Temporary known-red quarantine is for feature gaps that must become green; it cannot enroll this deliberately broken fixture as permanent evidence. The ordinary invoice witnesses do not establish that the mutation is executed.",
+  dissolution: unbound_dissolution(description: "A scheduled permanent source-mutation consumer runs the unchanged invoice controls against submit_invoice_fixture with the net_due == money_amount_micro(count: 0) arm calling classify_job directly and the paid arm retaining admit_job. It requires the zero-dollar other-job-receipt control to fail by assertion and paid_invoice_does_not_supply_an_admission_receipt to pass in the same mutated run, refuses unexpected green or a pre-verdict failure, and runs the original controls on restored source. The mutation and both expectations remain enrolled after this frontier dissolves; a one-off run, copied receipt, temporary known-red row, or declared harness alone does not close it."),
+)
+
+data job_admission_frontier_rows: List<FrontierRow> = [
+  classification_receipt_issuer_frontier,
+  job_admission_billing_frontier,
+  job_admission_runner_frontier,
+  job_admission_mutation_harness_frontier,
+]
+
+type JobAdmission<P>
+  = JobAdmitted { receipt: JobClassificationReceipt<P> }
+  | JobHeld { subject: FabricIdentity<P, WorkKey> }
+  | JobRefused { subject: FabricIdentity<P, WorkKey>, reason: JobAdmissionRefusal }
+
+// The producer and the execution boundary share the classification fold. Hold
+// remains distinguishable even if the caller has no receipt yet.
+fn classify_job<P>(subject: FabricIdentity<P, WorkKey>, classification: JobClassification) -> JobAdmission<P> {
+  match classification {
+    DeclaredNonEphi => JobAdmitted { receipt: JobClassificationReceipt { subject: subject, issuer_frontier: classification_receipt_issuer_frontier } }
+    DeclaredEphi => JobRefused { subject: subject, reason: EphiHandlingAuthorityHasNoProducer }
+    ClassificationUnresolved => JobHeld { subject: subject }
+  }
+}
+
+// An invoice is not an input to admission. This boundary rechecks the current
+// declaration: a previously admitted subject does not authorize changed handling.
+// sole_constructor confines receipt literals to this file. It does not establish
+// caller identity or truth of a customer's declaration: classify_job is a public
+// decision producer. This receipt records that decision, not authenticated consent.
+// The issuer capability owed is carried in classification_receipt_issuer_frontier.
+fn admit_job<P>(subject: FabricIdentity<P, WorkKey>, classification: JobClassification, receipt: JobClassificationReceipt<P>?) -> JobAdmission<P> {
+  match classify_job(subject: subject, classification: classification) {
+    JobHeld { subject: s } => JobHeld { subject: s }
+    JobRefused { subject: s, reason: r } => JobRefused { subject: s, reason: r }
+    JobAdmitted { receipt: _ } => match receipt {
+      Absent => JobRefused { subject: subject, reason: ClassificationReceiptMissing }
+      Present { value: r } => if fabric_identity_eq(left: subject, right: r.subject) {
+        JobAdmitted { receipt: r }
+      } else {
+        JobRefused { subject: subject, reason: ClassificationReceiptSubjectMismatch }
+      }
+    }
+  }
+}

dag/test/claim/job_admission_witness_test.dag

@@ -0,0 +1,179 @@
+module test.claim.job_admission_witness
+
+import std.types { Bool, NonEmptyStr }
+import std.roster_frontier { FrontierRow }
+import gunbc.census_closure_frontier { census_closure_frontier_rows }
+import std.measure { MoneyAmountMicro, money_amount_micro, money_amount_micro_count }
+import v2.std.optional { Present, Absent }
+import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }
+import product.fabric.identity { FabricIdentity, WorkKey, fabric_identity_eq }
+import product.fabric.job_admission {
+  classification_receipt_issuer_frontier, job_admission_billing_frontier, job_admission_runner_frontier,
+  job_admission_mutation_harness_frontier,
+  JobAdmission, JobClassification, JobClassificationReceipt, JobAdmitted, JobHeld, JobRefused,
+  DeclaredNonEphi, DeclaredEphi, ClassificationUnresolved,
+  EphiHandlingAuthorityHasNoProducer, ClassificationReceiptMissing,
+  ClassificationReceiptSubjectMismatch, classify_job, admit_job,
+}
+
+data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly
+
+data subject: FabricIdentity<NonEmptyStr, WorkKey> = FabricIdentity {
+  principal: "pilot-customer",
+  key: "job-a" as WorkKey,
+}
+
+fn receipt() -> JobClassificationReceipt<NonEmptyStr>? {
+  match classify_job(subject: subject, classification: DeclaredNonEphi) {
+    JobAdmitted { receipt: r } => Present { value: r }
+    _ => Absent
+  }
+}
+
+// A receipt is present in both classification controls, so neither can pass
+// collaterally through ClassificationReceiptMissing.
+test fn declared_ephi_refuses_for_absent_handling_authority() -> Bool {
+  match admit_job(subject: subject, classification: DeclaredEphi, receipt: receipt()) {
+    JobRefused { subject: s, reason: EphiHandlingAuthorityHasNoProducer } => fabric_identity_eq(left: s, right: subject)
+    _ => false
+  }
+}
+
+test fn unresolved_classification_holds_with_a_receipt() -> Bool {
+  match admit_job(subject: subject, classification: ClassificationUnresolved, receipt: receipt()) {
+    JobHeld { subject: s } => fabric_identity_eq(left: s, right: subject)
+    _ => false
+  }
+}
+
+test fn ordinary_job_without_receipt_refuses_for_missing_receipt() -> Bool {
+  match admit_job(subject: subject, classification: DeclaredNonEphi, receipt: Absent) {
+    JobRefused { subject: s, reason: ClassificationReceiptMissing } => fabric_identity_eq(left: s, right: subject)
+    _ => false
+  }
+}
+
+test fn ordinary_job_with_its_receipt_is_admitted() -> Bool {
+  match admit_job(subject: subject, classification: DeclaredNonEphi, receipt: receipt()) {
+    JobAdmitted { receipt: r } => fabric_identity_eq(left: r.subject, right: subject)
+    _ => false
+  }
+}
+
+test fn unresolved_without_receipt_still_holds() -> Bool {
+  match admit_job(subject: subject, classification: ClassificationUnresolved, receipt: Absent) {
+    JobHeld { subject: s } => fabric_identity_eq(left: s, right: subject)
+    _ => false
+  }
+}
+
+test fn receipt_cannot_cross_customer_boundary() -> Bool {
+  match admit_job(subject: FabricIdentity { principal: "other-customer", key: subject.key }, classification: DeclaredNonEphi, receipt: receipt()) {
+    JobRefused { subject: _, reason: ClassificationReceiptSubjectMismatch } => true
+    _ => false
+  }
+}
+
+// Controlled USD fixture, not the billing model. billing-receipts replaces
+// this integration boundary with its metered gross/credit/net invoice carrier.
+// The fixture exercises no credit and a credit exactly equal to gross. Excess
+// credit has no constructor here; the real invoice policy belongs to billing.
+type FixturePromotionalCredit
+  = NoFixtureCredit
+  | FullFixtureCredit
+
+type InvoiceFixture {
+  gross_charge: MoneyAmountMicro
+  promotional_credit: FixturePromotionalCredit
+}
+
+fn applied_credit(invoice: InvoiceFixture) -> MoneyAmountMicro {
+  match invoice.promotional_credit {
+    NoFixtureCredit => money_amount_micro(count: 0)
+    FullFixtureCredit => invoice.gross_charge
+  }
+}
+
+fn net_due(invoice: InvoiceFixture) -> MoneyAmountMicro {
+  match invoice.promotional_credit {
+    NoFixtureCredit => invoice.gross_charge
+    FullFixtureCredit => money_amount_micro(count: 0)
+  }
+}
+
+type InvoiceAdmissionFixture {
+  invoice: InvoiceFixture
+  admission: JobAdmission<NonEmptyStr>
+}
+
+fn submit_invoice_fixture(invoice: InvoiceFixture, classification: JobClassification, admission_receipt: JobClassificationReceipt<NonEmptyStr>?) -> InvoiceAdmissionFixture {
+  InvoiceAdmissionFixture {
+    invoice: invoice,
+    admission: admit_job(subject: subject, classification: classification, receipt: admission_receipt),
+  }
+}
+
+// This fourth red is independently discriminating: classification is decided,
+// handling is ordinary, and a receipt EXISTS. It belongs to another job. A pilot
+// bypass on net == 0 would turn this precise refusal into admission.
+test fn zero_dollar_net_invoice_cannot_admit_a_job_with_another_jobs_receipt() -> Bool {
+  let invoice = InvoiceFixture { gross_charge: money_amount_micro(count: 12000000), promotional_credit: FullFixtureCredit }
+  let other_job = FabricIdentity { principal: subject.principal, key: "job-b" as WorkKey }
+  match classify_job(subject: other_job, classification: DeclaredNonEphi) {
+    JobAdmitted { receipt: r } => match submit_invoice_fixture(invoice: invoice, classification: DeclaredNonEphi, admission_receipt: Present { value: r }).admission {
+      JobRefused { subject: s, reason: ClassificationReceiptSubjectMismatch } =>
+        money_amount_micro_count(m: invoice.gross_charge) > 0 && net_due(invoice: invoice) == money_amount_micro(count: 0) && fabric_identity_eq(left: s, right: subject)
+      _ => false
+    }
+    _ => false
+  }
+}
+
+test fn zero_dollar_invoice_keeps_an_admitted_customer_admitted() -> Bool {
+  let invoice = InvoiceFixture { gross_charge: money_amount_micro(count: 12000000), promotional_credit: FullFixtureCredit }
+  match submit_invoice_fixture(invoice: invoice, classification: DeclaredNonEphi, admission_receipt: receipt()).admission {
+    JobAdmitted { receipt: r } => net_due(invoice: invoice) == money_amount_micro(count: 0) && fabric_identity_eq(left: r.subject, right: subject)
+    _ => false
+  }
+}
+
+test fn zero_dollar_invoice_does_not_resolve_classification() -> Bool {
+  match submit_invoice_fixture(invoice: InvoiceFixture { gross_charge: money_amount_micro(count: 12000000), promotional_credit: FullFixtureCredit }, classification: ClassificationUnresolved, admission_receipt: receipt()).admission {
+    JobHeld { subject: s } => fabric_identity_eq(left: s, right: subject)
+    _ => false
+  }
+}
+
+test fn paid_invoice_does_not_supply_an_admission_receipt() -> Bool {
+  match submit_invoice_fixture(invoice: InvoiceFixture { gross_charge: money_amount_micro(count: 12000000), promotional_credit: NoFixtureCredit }, classification: DeclaredNonEphi, admission_receipt: Absent).admission {
+    JobRefused { subject: _, reason: ClassificationReceiptMissing } => true
+    _ => false
+  }
+}
+
+// Changing only the invoice preserves all three dispositions, including the
+// missing-receipt and ePHI refusals. This prevents a zero-only pilot exception.
+fn credit_preserves_admission(classification: JobClassification, admission_receipt: JobClassificationReceipt<NonEmptyStr>?) -> Bool {
+  let paid = submit_invoice_fixture(invoice: InvoiceFixture { gross_charge: money_amount_micro(count: 12000000), promotional_credit: NoFixtureCredit }, classification: classification, admission_receipt: admission_receipt)
+  let credited = submit_invoice_fixture(invoice: InvoiceFixture { gross_charge: money_amount_micro(count: 12000000), promotional_credit: FullFixtureCredit }, classification: classification, admission_receipt: admission_receipt)
+  applied_credit(invoice: paid.invoice) == money_amount_micro(count: 0) && applied_credit(invoice: credited.invoice) == credited.invoice.gross_charge &&
+  net_due(invoice: paid.invoice) == money_amount_micro(count: 12000000) && net_due(invoice: credited.invoice) == money_amount_micro(count: 0) && paid.admission == credited.admission
+}
+
+test fn promotional_credit_preserves_every_admission_disposition() -> Bool {
+  credit_preserves_admission(classification: DeclaredNonEphi, admission_receipt: receipt()) &&
+  credit_preserves_admission(classification: DeclaredEphi, admission_receipt: receipt()) &&
+  credit_preserves_admission(classification: ClassificationUnresolved, admission_receipt: receipt()) &&
+  credit_preserves_admission(classification: DeclaredNonEphi, admission_receipt: Absent)
+}
+
+fn frontier_enrolled_once(row: FrontierRow) -> Bool {
+  count(filter(census_closure_frontier_rows(), enrolled => enrolled == row)) == 1
+}
+
+test fn admission_frontiers_reach_the_dissolution_census() -> Bool {
+  frontier_enrolled_once(row: classification_receipt_issuer_frontier) &&
+  frontier_enrolled_once(row: job_admission_billing_frontier) &&
+  frontier_enrolled_once(row: job_admission_runner_frontier) &&
+  frontier_enrolled_once(row: job_admission_mutation_harness_frontier)
+}