1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
//! Cross-reference table + the fixpoint verdict, a small port of
//! `crossRef.ml`. Owned by the compile driver (`lib.rs::compile_document_cst`),
//! **not** reset per trial — it *is* the fixpoint state that persists while
//! everything else (hooks, images, mutable store) resets each trial.
use std::collections::{BTreeMap, HashMap, HashSet};
/// A cross-reference table as it is carried BETWEEN runs — the payload of the
/// auxiliary file (`<doc>.satysfi-aux`). `BTreeMap` so serializing it is
/// deterministic: the same table must always produce the same file bytes.
pub type AuxTable = BTreeMap<String, String>;
/// `crossRef.ml:23`'s `count_max`.
const COUNT_MAX: u32 = 4;
/// What the driver should do after one trial finished and hooks fired.
#[derive(Debug, PartialEq, Eq)]
pub enum Verdict {
/// The table changed this trial; run another trial.
NeedsAnotherTrial,
/// The table stabilized. Carries the keys `get` missed during the
/// *final* trial (unresolved forward references; `crossRef.ml:78`).
CanTerminate(Vec<String>),
/// The table kept changing through `COUNT_MAX` trials; give up rather
/// than loop forever.
CountMax,
}
/// Port of `crossRef.ml`'s mutable cross-reference table.
#[derive(Debug, Default)]
pub struct CrossRefs {
table: HashMap<String, String>,
count: u32,
/// Keys `get` missed this trial (`crossRef.ml:116`).
unresolved: Vec<String>,
/// What each key's value looked like when it was READ (`get`) this trial —
/// `Some(v)` for a hit, `None` for a miss — recorded at the FIRST read.
/// A trial's LAYOUT depends only on the cross-reference values it actually
/// reads; this lets `verdict` retry only when a read value was invalidated,
/// not merely because some key was (re)registered.
read_this_trial: HashMap<String, Option<String>>,
/// Set when a `register` this trial gives a key a value differing from what
/// a `get` earlier this trial had already observed for it — i.e. the layout
/// used a now-stale cross-reference and must be recomputed.
stale: bool,
/// Keys this table was SEEDED with from a previous run's auxiliary file
/// (empty for a cold run). Tracked only to police them — see
/// [`CrossRefs::seed_unvalidated`].
seeded: HashSet<String>,
/// Keys `register`ed during the trial now in progress. Reset by
/// [`CrossRefs::verdict`] alongside the rest of the per-trial bookkeeping.
registered_this_trial: HashSet<String>,
/// Did the trial that just ended read a seeded value it never re-derived?
/// See [`CrossRefs::seed_unvalidated`].
seed_unvalidated: bool,
}
impl CrossRefs {
pub fn new() -> CrossRefs {
CrossRefs::default()
}
/// A table pre-populated from a previous run's auxiliary file.
///
/// Seeding only changes how fast the fixpoint converges, never where it
/// converges to: a seeded value a `get` observes and a later `register`
/// contradicts still marks the layout stale and forces another trial. It
/// mainly helps a forward reference (`\ref` to a later section) resolve
/// on trial 1 instead of trial 2.
pub fn seeded(table: AuxTable) -> CrossRefs {
CrossRefs {
seeded: table.keys().cloned().collect(),
table: table.into_iter().collect(),
..CrossRefs::default()
}
}
/// The table as it should be written back out.
///
/// Keys this run neither read nor registered are carried through
/// verbatim, so an auxiliary file round-trips with upstream SATySFi.
pub fn export(&self) -> AuxTable {
self.table
.iter()
.map(|(k, v)| (k.clone(), v.clone()))
.collect()
}
/// Did the trial that just ended READ a seeded value that it never
/// re-registered?
///
/// If so the layout depended on a value from a previous run that was
/// never re-derived this run (e.g. a `\label` the document dropped but
/// some `\ref` still targets) — unverifiable, not necessarily wrong. The
/// driver's answer is to discard the seed and redo the fixpoint cold, so
/// a warm build is always byte-identical to a cold one.
pub fn seed_unvalidated(&self) -> bool {
self.seed_unvalidated
}
/// `crossRef.ml:99`, plus the fixpoint-shortcut bookkeeping: if this key was
/// already READ this trial and the value the reader saw differs from `v`,
/// the layout is now stale and another trial is required. A key that is
/// (re)registered but never read this trial does NOT force a retrial — its
/// value cannot have affected the output — which is what lets a document
/// that only *writes* cross-references (e.g. page labels nothing `\ref`s)
/// converge in ONE trial.
pub fn register(&mut self, k: String, v: String) {
self.registered_this_trial.insert(k.clone());
if let Some(observed) = self.read_this_trial.get(&k) {
let unchanged = matches!(observed, Some(o) if *o == v);
if !unchanged {
self.stale = true;
}
}
self.table.insert(k, v);
}
/// `crossRef.ml:116` — records a miss (an unresolved forward reference)
/// alongside the ordinary lookup, and remembers what the reader observed so
/// a later `register` can tell whether that observation went stale.
pub fn get(&mut self, k: &str) -> Option<String> {
match self.table.get(k) {
Some(v) => {
let v = v.clone();
self.read_this_trial
.entry(k.to_string())
.or_insert_with(|| Some(v.clone()));
Some(v)
}
None => {
self.unresolved.push(k.to_string());
self.read_this_trial.entry(k.to_string()).or_insert(None);
None
}
}
}
/// `crossRef.ml:112` — like [`Self::get`] but records no miss
/// (`probe-cross-reference`): probing an absent key must NOT force
/// another fixpoint trial.
pub fn probe(&self, k: &str) -> Option<String> {
self.table.get(k).cloned()
}
/// `crossRef.ml:78` `needs_another_trial`, tightened: retry only if a value
/// the layout READ this trial was invalidated (`stale`), not on every
/// (re)registration. Consumes this trial's bookkeeping and resets it.
pub fn verdict(&mut self) -> Verdict {
// A seeded key the layout READ but this trial never re-registered is
// an unverified dependency (see `seed_unvalidated`); compute it before
// the per-trial bookkeeping below is cleared.
self.seed_unvalidated = self
.read_this_trial
.keys()
.any(|k| self.seeded.contains(k) && !self.registered_this_trial.contains(k));
self.read_this_trial.clear();
self.registered_this_trial.clear();
if self.stale {
if self.count >= COUNT_MAX {
Verdict::CountMax
} else {
self.unresolved.clear();
self.stale = false;
self.count += 1;
Verdict::NeedsAnotherTrial
}
} else {
Verdict::CanTerminate(std::mem::take(&mut self.unresolved))
}
}
}
#[cfg(test)]
mod tests {
use super::*;
#[test]
fn a_write_only_key_converges_on_the_first_trial() {
let mut cr = CrossRefs::new();
// A key that is registered but never READ this trial cannot have
// affected the layout, so the fixpoint terminates immediately.
cr.register("p".to_string(), "1".to_string());
assert_eq!(cr.verdict(), Verdict::CanTerminate(Vec::new()));
}
#[test]
fn a_forward_reference_needs_a_second_trial_then_converges() {
let mut cr = CrossRefs::new();
// Trial 1: read "p" before it exists (a forward ref) — the layout saw
// `None` — then register it. The observed value went stale, so retry.
assert_eq!(cr.get("p"), None);
cr.register("p".to_string(), "1".to_string());
assert_eq!(cr.verdict(), Verdict::NeedsAnotherTrial);
// Trial 2: the read now hits "1", and the re-registration matches it —
// nothing the layout read changed, so terminate.
assert_eq!(cr.get("p"), Some("1".to_string()));
cr.register("p".to_string(), "1".to_string());
assert_eq!(cr.verdict(), Verdict::CanTerminate(Vec::new()));
}
#[test]
fn a_read_reference_that_never_resolves_hits_count_max() {
let mut cr = CrossRefs::new();
for i in 0..(COUNT_MAX + 2) {
// A pathological document that READS a key and then registers a
// *new* value every trial never stabilizes; the cap must still
// terminate it (a write-only churn would converge on trial 1).
let _ = cr.get("k");
cr.register("k".to_string(), i.to_string());
let v = cr.verdict();
if v == Verdict::CountMax {
return;
}
}
panic!("expected CountMax within COUNT_MAX trials");
}
#[test]
fn an_unresolved_get_forces_another_trial_via_the_caller_not_verdict_alone() {
// `get` missing a key does not, by itself, set `changed` — only
// `register` does; the unresolved list is informational/diagnostic
// only. A document that never registers the key it `get`s converges
// immediately, with the miss surfaced in `CanTerminate`'s payload.
let mut cr = CrossRefs::new();
assert_eq!(cr.get("missing"), None);
assert_eq!(
cr.verdict(),
Verdict::CanTerminate(vec!["missing".to_string()])
);
}
#[test]
fn seeding_resolves_a_forward_reference_on_the_first_trial() {
// Cold, this is the two-trial case above: the layout reads "p"
// before anything registers it, so trial 1 goes stale. Seeded from
// the previous run's table, the same read hits the right value
// immediately and the re-registration confirms it in one trial.
let mut aux = AuxTable::new();
aux.insert("p".to_string(), "1".to_string());
let mut cr = CrossRefs::seeded(aux);
assert_eq!(cr.get("p"), Some("1".to_string()));
cr.register("p".to_string(), "1".to_string());
assert_eq!(cr.verdict(), Verdict::CanTerminate(Vec::new()));
assert!(!cr.seed_unvalidated(), "the seed was re-derived this run");
}
#[test]
fn a_seed_the_run_contradicts_still_forces_another_trial() {
// Seeding must not be able to freeze a wrong answer: a seeded value the
// layout reads and a later `register` contradicts is exactly the stale
// case, and retries just as an in-run value would.
let mut aux = AuxTable::new();
aux.insert("p".to_string(), "STALE".to_string());
let mut cr = CrossRefs::seeded(aux);
assert_eq!(cr.get("p"), Some("STALE".to_string()));
cr.register("p".to_string(), "1".to_string());
assert_eq!(cr.verdict(), Verdict::NeedsAnotherTrial);
}
#[test]
fn a_seed_that_is_read_but_never_re_registered_is_flagged() {
// The dangerous shape: the document still `\ref`s a key but no
// longer defines it, so nothing this run can confirm the seeded
// value. The fixpoint converges happily anyway, so `verdict` flags
// it and the driver redoes the run cold.
let mut aux = AuxTable::new();
aux.insert("p".to_string(), "1".to_string());
let mut cr = CrossRefs::seeded(aux);
assert_eq!(cr.get("p"), Some("1".to_string()));
assert_eq!(cr.verdict(), Verdict::CanTerminate(Vec::new()));
assert!(
cr.seed_unvalidated(),
"read a seeded value nothing re-derived"
);
}
#[test]
fn an_unread_seed_is_not_flagged_and_is_carried_through() {
// A seeded key the document never reads cannot have affected the
// layout, so it is no reason to redo anything, but it is still
// written back out (see `export`'s doc comment for why).
let mut aux = AuxTable::new();
aux.insert("changed".to_string(), "F".to_string());
aux.insert("stale-label".to_string(), "9".to_string());
let mut cr = CrossRefs::seeded(aux);
cr.register("other".to_string(), "1".to_string());
assert_eq!(cr.verdict(), Verdict::CanTerminate(Vec::new()));
assert!(!cr.seed_unvalidated());
let out = cr.export();
assert_eq!(out.get("changed").map(String::as_str), Some("F"));
assert_eq!(out.get("stale-label").map(String::as_str), Some("9"));
assert_eq!(out.get("other").map(String::as_str), Some("1"));
}
}