macroonz_compiler/explanation/types.rs
1//! The explanation home's declarations: the universal roster and its typed answers, the seat a related kind is accounted at, one complete view, and how coverage refuses.
2//!
3//! Declarations only.
4//! Every road that reaches a private field lives in `type_guard.rs`, this file's own child, which is what makes a view's parentage taken rather than supplied.
5
6use crate::bounded::{Bounded, Capped};
7use crate::diagnostic::{REPAIR_LIMIT, Repair};
8use crate::identity::{
9 self, ClosureId, ExplanationId, Identity, OwnerFact, PlanId, Profile, Provenance,
10};
11use crate::kind::{Disposition, Kind, Question};
12use crate::plan::{DEPENDENCY_LIMIT, InvalidationSet, MEMBERSHIP_LIMIT, PlannedOutput};
13use core::marker::PhantomData;
14
15#[path = "type_guard.rs"]
16mod guard;
17
18/// How many questions every kind owes, whatever it is.
19///
20/// The width of a complete view's universal half, checked against the roster itself where the roster is written down.
21pub const UNIVERSAL_QUESTION_COUNT: usize = 9;
22
23/// Owner facts one answer may carry as the assumptions a projection rests on.
24pub const ASSUMPTION_LIMIT: usize = 16;
25
26/// Related kinds one answer may account for.
27pub const RELATED_KIND_LIMIT: usize = 16;
28
29/// Questions one kind may declare beyond the universal roster.
30///
31/// A kind whose roster outgrows this refuses: an answer sheet cut to fit is byte for byte the shape of a complete one.
32pub const DECLARED_QUESTION_LIMIT: usize = 32;
33
34/// Issues one coverage refusal carries before it begins counting the rest.
35///
36/// One per universal seat, one per declared seat at the widest roster, and room for the answers that stand outside a roster entirely.
37pub const EXPLANATION_ISSUE_LIMIT: usize = 48;
38
39/// One question every generated thing answers, whatever kind it is.
40///
41/// A kind narrows nothing here — its own questions are a second roster answered beside this one — so no kind can owe less by declaring less.
42/// A row's position is what a complete view's preimage carries for it, so a row is appended and never renumbered.
43#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
44pub enum UniversalQuestion {
45 /// What are you?
46 WhatAreYou,
47 /// Which owner required you?
48 WhichOwnerRequired,
49 /// Which declaration caused you?
50 WhichDeclarationCaused,
51 /// Which profile were you decided under?
52 WhichProfile,
53 /// Which output identity and digest are you?
54 WhichOutputAndDigest,
55 /// Which assumptions do you rest on?
56 WhichAssumptions,
57 /// What invalidates you?
58 WhatInvalidates,
59 /// Why was a related projection not generated?
60 WhyRelatedNotGenerated,
61 /// What repairs a refusal?
62 WhatRepairsARefusal,
63}
64
65/// One kind a projection is related to, and what happened to that kind.
66#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
67pub struct RelatedDisposition {
68 /// The related kind's declared name.
69 pub kind: &'static str,
70 /// What happened to it.
71 pub disposition: Disposition,
72}
73
74/// One seat's half of the output-and-digest answer: the member the plan declared there, and the digest the closure proved over its rendered bytes.
75#[derive(Debug, Clone, PartialEq, Eq, Hash)]
76pub struct AnsweredOutput {
77 /// The planned member, boxed so one row does not set the width of the roster.
78 pub output: Box<PlannedOutput>,
79 /// The digest proved over the rendered bytes.
80 pub digest: Identity<identity::OutputBytes>,
81}
82
83/// One typed answer to a universal question.
84///
85/// Every arm carries the exact values that answer its row — identities, typed rosters, typed dispositions — and never a sentence standing in for a fact.
86#[derive(Debug, Clone, PartialEq, Eq, Hash)]
87pub enum UniversalAnswer {
88 /// The kind this output is.
89 Kind {
90 /// The kind's declared name.
91 name: &'static str,
92 },
93 /// The owner fact that required it.
94 Owner {
95 /// The requiring fact.
96 owner: OwnerFact,
97 },
98 /// The declarations it was derived from.
99 CausingDeclarations {
100 /// The content commitment the request walked in with.
101 commitment: Identity<identity::CapturedDeclaration>,
102 /// The captures that content declares it stands on.
103 dependencies: Bounded<Identity<identity::CapturedDeclaration>, DEPENDENCY_LIMIT>,
104 },
105 /// The profile it was decided under.
106 Profile {
107 /// The profile, at the version it was decided at.
108 profile: Profile,
109 },
110 /// Every member it is, and the digest proved over each one's rendered bytes.
111 ///
112 /// The complete set in roster order, never a chosen row: a kind's roster may fill several seats, and an answer naming one of them would be coverage-complete syntax over a flattened denominator — the second output's identity and digest simply absent from a view that claims the whole expansion.
113 /// Each row is two values because they come from two places: the member is what the plan declared, and the digest is what the closure proved.
114 OutputAndDigest {
115 /// One row per rendered seat, in roster order; never empty in a lawful expansion, because a rendering is structurally non-empty — and completion refuses a set that does not restate the proof's own roster, so a shortened or reordered answer cannot ride a coverage-complete view.
116 outputs: Bounded<AnsweredOutput, MEMBERSHIP_LIMIT>,
117 },
118 /// The owner facts it rests on.
119 Assumptions {
120 /// The assumed facts.
121 assumptions: Bounded<OwnerFact, ASSUMPTION_LIMIT>,
122 },
123 /// The triggers whose change makes it stale.
124 Invalidators {
125 /// The watch set.
126 triggers: InvalidationSet,
127 },
128 /// What happened to every kind it is related to.
129 RelatedDispositions {
130 /// The accounted kinds.
131 related: Bounded<RelatedDisposition, RELATED_KIND_LIMIT>,
132 },
133 /// The owner-declared repairs that apply.
134 Repairs {
135 /// The declared repairs.
136 repairs: Bounded<Repair, REPAIR_LIMIT>,
137 },
138}
139
140/// One way a set of answers fails to cover the questions a kind owes.
141///
142/// No row is payload-free: an issue names the question it is about, because a bare row makes the reader guess which seat to repair.
143#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
144pub enum ExplanationIssue {
145 /// A universal question has no answer.
146 UniversalUnanswered {
147 /// The unanswered question.
148 question: UniversalQuestion,
149 },
150 /// A universal question was answered more than once.
151 UniversalAnsweredTwice {
152 /// The doubled question.
153 question: UniversalQuestion,
154 },
155 /// A question the kind declared has no answer.
156 DeclaredUnanswered {
157 /// The question's declared name.
158 question: &'static str,
159 /// Its position in the kind's roster.
160 slot: u16,
161 },
162 /// A question the kind declared was answered more than once.
163 DeclaredAnsweredTwice {
164 /// The question's declared name.
165 question: &'static str,
166 /// Its position in the kind's roster.
167 slot: u16,
168 },
169 /// An answer names a question its own roster does not carry.
170 QuestionOutsideRoster {
171 /// The question's declared name.
172 question: &'static str,
173 },
174 /// More seats were offered than a declared bound admits.
175 SeatBoundExceeded {
176 /// The declared bound.
177 bound: u64,
178 /// The observed count.
179 observed: u64,
180 },
181 /// The output answer does not restate the proof's own rendered roster.
182 ///
183 /// The lawful rows are derivable from the closure a view is completed over, so the pass rebuilds them and compares whole — a missing seat, an extra row, a reordered roster, and a digest that is not the proof's all land here rather than riding a coverage-complete view.
184 OutputsBesideTheProof {
185 /// Rows the proof's rendered roster carries.
186 expected: u16,
187 /// Rows the supplied answer carried.
188 observed: u16,
189 /// The first roster position where the supplied answer stops restating the proof — the shorter roster's own end where one merely ran out.
190 diverges: u16,
191 },
192}
193
194/// How the explanation protocol says no.
195///
196/// Coverage issues are independent and co-establishable — several questions may stand unanswered while another is doubled — so the body carries every issue the pass established rather than electing a primary one, and says so where it kept only what fits.
197#[must_use = "a coverage refusal carries every uncovered, doubled, and inadmissible question"]
198#[derive(Debug, Clone, PartialEq, Eq, Hash)]
199pub struct ExplanationError {
200 body: Capped<ExplanationIssue, EXPLANATION_ISSUE_LIMIT>,
201}
202
203/// One complete explanation: every question a kind owes, answered exactly once, over the plan and the proof the answers are ABOUT.
204///
205/// Holding one is the coverage proof, and there is no partial view — a set of answers that could not be completed is a refusal instead.
206///
207/// # Authority
208///
209/// **The parentage is taken and never supplied.**
210/// A view assembled from two identities beside the answers would name a plan and a closure it was never written over: every question answered correctly, about a different expansion of the same kind, and the type parameter cannot catch that because a kind is not an expansion.
211///
212/// # Ordering
213///
214/// The universal seats stand in the compiler's roster order and the declared seats in the kind's, never in the order a caller supplied them.
215/// That order is what the identity is derived over, so one set of answers is one explanation however it was assembled.
216#[must_use = "a complete view is the proof every question has exactly one answer, over the plan and closure it names"]
217#[derive(Debug, Clone, PartialEq, Eq)]
218pub struct View<K: Kind> {
219 plan: PlanId,
220 closure: ClosureId,
221 universal: Bounded<UniversalAnswer, UNIVERSAL_QUESTION_COUNT>,
222 declared: Bounded<<K::Question as Question>::Answer, DECLARED_QUESTION_LIMIT>,
223 identity: ExplanationId,
224 provenance: Provenance,
225 kind: PhantomData<K>,
226}