meta_language/
foundation_models.rs

1//! The foundations meta-language knows, as data.
2//!
3//! `src/data/foundation-models.json` is written from
4//! `parity/foundation-models.json` by `js/scripts/build-foundation-models.mjs`;
5//! the npm package ships the same file. It records integer, overflow,
6//! universe, effect, proof and logic models, the models each language uses,
7//! and the explicit correspondences between distinct models. No model is the
8//! universal logic every other model reduces to: a consumer brings its own
9//! foundation and proof authority and relates it to these models through
10//! correspondences.
11
12use std::collections::{BTreeMap, BTreeSet};
13use std::sync::OnceLock;
14
15use serde::Deserialize;
16use serde_json::{Map, Value};
17
18use crate::SourceAlias;
19
20const FOUNDATION_MODELS_JSON: &str = include_str!("data/foundation-models.json");
21
22/// The kinds of correspondence between two distinct models; none of them claims the models are the same.
23pub const CORRESPONDENCE_KINDS: [&str; 4] = ["embedding", "conditional", "encoding", "restatement"];
24
25/// The families whose models are logics or proof authorities.
26///
27/// A model of one of them that every other model of its family embeds into, or (beyond the
28/// booleans every language has) that every language is made to use, would be
29/// a hard-coded universal logic.
30pub const LOGIC_FAMILIES: [&str; 3] = ["logic-model", "proof-system", "universe-model"];
31
32/// A family of foundation models, such as `integer-model` or `proof-system`.
33#[derive(Debug, Clone, PartialEq, Eq, Deserialize)]
34#[serde(deny_unknown_fields)]
35pub struct FoundationFamily {
36    /// Stable identity of the family.
37    pub id: String,
38    /// What the family's models describe.
39    pub definition: String,
40}
41
42/// One foundation model: a meaning, not a spelling.
43#[derive(Debug, Clone, PartialEq, Eq, Deserialize)]
44#[serde(rename_all = "camelCase", deny_unknown_fields)]
45pub struct FoundationModel {
46    /// Stable identity, `<family>.<name>`, such as `overflow-model.wrapping`.
47    pub id: String,
48    /// The family the model belongs to.
49    pub family: String,
50    /// What the model means.
51    pub definition: String,
52    /// The properties that distinguish the model from the other models of its family.
53    pub properties: Map<String, Value>,
54    /// The names languages give the model.
55    pub source_aliases: Vec<SourceAlias>,
56}
57
58/// A recorded relation between two distinct models and the condition under which it holds.
59#[derive(Debug, Clone, PartialEq, Eq, Deserialize)]
60#[serde(rename_all = "camelCase", deny_unknown_fields)]
61pub struct FoundationCorrespondence {
62    /// The model the correspondence starts from.
63    pub from: String,
64    /// The model the correspondence leads to.
65    pub to: String,
66    /// One of [`CORRESPONDENCE_KINDS`].
67    pub kind: String,
68    /// When the two models agree.
69    pub condition: String,
70    /// The translation encodings and assumptions this correspondence justifies.
71    #[serde(default)]
72    pub translation_encodings: Vec<String>,
73}
74
75/// Two models that must never be merged, with the reason.
76#[derive(Debug, Clone, PartialEq, Eq, Deserialize)]
77#[serde(rename_all = "camelCase", deny_unknown_fields)]
78pub struct FoundationDistinction {
79    /// The two models.
80    pub models: Vec<String>,
81    /// What distinguishes them.
82    pub reason: String,
83    /// The translation encodings and assumptions this distinction justifies.
84    #[serde(default)]
85    pub translation_encodings: Vec<String>,
86}
87
88/// The models one language uses.
89#[derive(Debug, Clone, PartialEq, Eq, Deserialize)]
90#[serde(deny_unknown_fields)]
91pub struct LanguageFoundation {
92    /// The language, such as `Rust` or `Lean`.
93    pub language: String,
94    /// The identities of the models the language uses, one or more per family.
95    pub models: Vec<String>,
96}
97
98/// A foundation register: the shape of `parity/foundation-models.json`.
99#[derive(Debug, Clone, PartialEq, Eq, Deserialize)]
100#[serde(deny_unknown_fields)]
101pub struct FoundationRegister {
102    /// What the register records.
103    pub description: String,
104    /// The model families.
105    pub families: Vec<FoundationFamily>,
106    /// The models.
107    pub models: Vec<FoundationModel>,
108    /// The correspondences between distinct models.
109    pub correspondences: Vec<FoundationCorrespondence>,
110    /// The models that must stay distinct.
111    pub distinctions: Vec<FoundationDistinction>,
112    /// The models each language uses.
113    pub languages: Vec<LanguageFoundation>,
114}
115
116/// A way a register fails to keep foundations neutral.
117#[derive(Debug, Clone, PartialEq, Eq)]
118pub struct FoundationProblem {
119    /// The problem kind, the same string the JavaScript runtime reports, such as `universal-model`.
120    pub kind: &'static str,
121    /// The model, correspondence or language the problem is about.
122    pub subject: String,
123    /// A readable explanation.
124    pub message: String,
125}
126
127/// Returns the embedded foundation register.
128#[must_use]
129pub fn foundation_register() -> &'static FoundationRegister {
130    static REGISTER: OnceLock<FoundationRegister> = OnceLock::new();
131    REGISTER.get_or_init(|| {
132        serde_json::from_str(FOUNDATION_MODELS_JSON)
133            .expect("the embedded foundation models are valid")
134    })
135}
136
137/// Returns the model named `id`.
138#[must_use]
139pub fn foundation_model(id: &str) -> Option<&'static FoundationModel> {
140    foundation_register()
141        .models
142        .iter()
143        .find(|model| model.id == id)
144}
145
146/// Returns the models `language` uses, optionally only those of one family.
147#[must_use]
148pub fn language_foundation_models(
149    language: &str,
150    family: Option<&str>,
151) -> Vec<&'static FoundationModel> {
152    foundation_register()
153        .languages
154        .iter()
155        .filter(|entry| entry.language == language)
156        .flat_map(|entry| entry.models.iter().filter_map(|id| foundation_model(id)))
157        .filter(|model| family.is_none_or(|family| model.family == family))
158        .collect()
159}
160
161/// Returns the recorded correspondences between two models, in either direction.
162#[must_use]
163pub fn foundation_correspondences(a: &str, b: &str) -> Vec<&'static FoundationCorrespondence> {
164    foundation_register()
165        .correspondences
166        .iter()
167        .filter(|entry| (entry.from == a && entry.to == b) || (entry.from == b && entry.to == a))
168        .collect()
169}
170
171/// Checks that a register keeps foundations neutral.
172///
173/// Every model belongs to a declared family, distinct models are not merged or
174/// claimed equal, every correspondence states its condition, every language
175/// names its own models, and no model is a universal logic. Unknown fields such
176/// as `universal` are rejected when the register is parsed. An empty result
177/// means the register is neutral; the kinds match the JavaScript runtime's
178/// `checkFoundationModels`.
179#[must_use]
180pub fn check_foundation_models(register: &FoundationRegister) -> Vec<FoundationProblem> {
181    let mut problems = Vec::new();
182    let mut report = |kind, subject: &str, message: String| {
183        problems.push(FoundationProblem {
184            kind,
185            subject: subject.to_owned(),
186            message,
187        });
188    };
189    let mut families = BTreeSet::new();
190    for family in &register.families {
191        if !families.insert(family.id.as_str()) {
192            report(
193                "duplicate",
194                &family.id,
195                format!("family {} is declared twice", family.id),
196            );
197        }
198    }
199    let mut models = BTreeMap::new();
200    for model in &register.models {
201        if models.insert(model.id.as_str(), model).is_some() {
202            report(
203                "duplicate",
204                &model.id,
205                format!("model {} is declared twice", model.id),
206            );
207        }
208        if !families.contains(model.family.as_str()) {
209            report(
210                "unknown-family",
211                &model.id,
212                format!("{} belongs to undeclared family {}", model.id, model.family),
213            );
214        } else if !model.id.starts_with(&format!("{}.", model.family)) {
215            report(
216                "identity",
217                &model.id,
218                format!(
219                    "{} is not named under its family {}",
220                    model.id, model.family
221                ),
222            );
223        }
224        if model.definition.is_empty() {
225            report(
226                "definition",
227                &model.id,
228                format!("{} has no definition", model.id),
229            );
230        }
231        if model.properties.is_empty() {
232            report(
233                "properties",
234                &model.id,
235                format!(
236                    "{} records no properties, so its distinctness cannot be checked",
237                    model.id
238                ),
239            );
240        }
241    }
242    for (index, model) in register.models.iter().enumerate() {
243        for other in &register.models[index + 1..] {
244            // Map equality ignores key order, like the JavaScript runtime's canonical JSON comparison.
245            if model.family == other.family && model.properties == other.properties {
246                report(
247                    "indistinct-models",
248                    &model.id,
249                    format!(
250                        "{} and {} record the same properties: one meaning must be one model with source aliases",
251                        model.id, other.id
252                    ),
253                );
254            }
255        }
256    }
257    let mut pairs = BTreeSet::new();
258    for entry in &register.correspondences {
259        let subject = format!("{} -> {}", entry.from, entry.to);
260        for end in [&entry.from, &entry.to] {
261            if !models.contains_key(end.as_str()) {
262                report(
263                    "unknown-model",
264                    &subject,
265                    format!("{subject} names undeclared model {end}"),
266                );
267            }
268        }
269        if entry.from == entry.to {
270            report(
271                "self-correspondence",
272                &subject,
273                format!("{subject} relates a model to itself"),
274            );
275        }
276        if !CORRESPONDENCE_KINDS.contains(&entry.kind.as_str()) {
277            report(
278                "correspondence-kind",
279                &subject,
280                format!(
281                    "{subject} has kind {}; two distinct models never correspond exactly, and the same meaning must be one model",
282                    entry.kind
283                ),
284            );
285        }
286        if entry.condition.trim().chars().count() < 20 {
287            report(
288                "unconditioned-correspondence",
289                &subject,
290                format!("{subject} does not state the condition under which the models agree"),
291            );
292        }
293        let key = if entry.from <= entry.to {
294            (&entry.from, &entry.to)
295        } else {
296            (&entry.to, &entry.from)
297        };
298        if !pairs.insert(key) {
299            report(
300                "duplicate",
301                &subject,
302                format!("{subject} is recorded twice"),
303            );
304        }
305    }
306    for entry in &register.distinctions {
307        let subject = entry.models.join(" / ");
308        if entry.models.len() != 2 {
309            report(
310                "distinction",
311                &subject,
312                "a distinction names exactly two models".to_owned(),
313            );
314        }
315        for id in &entry.models {
316            if !models.contains_key(id.as_str()) {
317                report(
318                    "unknown-model",
319                    &subject,
320                    format!("distinction {subject} names undeclared model {id}"),
321                );
322            }
323        }
324        if entry.reason.trim().chars().count() < 20 {
325            report(
326                "distinction",
327                &subject,
328                format!("distinction {subject} gives no reason"),
329            );
330        }
331    }
332    for entry in &register.languages {
333        let mut used = BTreeSet::new();
334        for id in &entry.models {
335            match models.get(id.as_str()) {
336                Some(model) => {
337                    used.insert(model.family.as_str());
338                }
339                None => report(
340                    "unknown-model",
341                    &entry.language,
342                    format!("{} uses undeclared model {id}", entry.language),
343                ),
344            }
345        }
346        for family in &families {
347            if !used.contains(family) {
348                report(
349                    "language-family",
350                    &entry.language,
351                    format!("{} does not record its {family}", entry.language),
352                );
353            }
354        }
355    }
356    for family in LOGIC_FAMILIES
357        .into_iter()
358        .filter(|family| families.contains(family))
359    {
360        let members: Vec<_> = register
361            .models
362            .iter()
363            .filter(|model| model.family == family)
364            .collect();
365        if members.len() < 2 {
366            continue;
367        }
368        for model in &members {
369            let embedded = members
370                .iter()
371                .filter(|other| other.id != model.id)
372                .all(|other| {
373                    register.correspondences.iter().any(|entry| {
374                        entry.kind == "embedding" && entry.from == other.id && entry.to == model.id
375                    })
376                });
377            if embedded {
378                report(
379                    "universal-model",
380                    &model.id,
381                    format!(
382                        "every other {family} embeds into {}, which makes it a hard-coded universal logic",
383                        model.id
384                    ),
385                );
386            }
387            if family != "logic-model"
388                && register.languages.len() > 1
389                && register
390                    .languages
391                    .iter()
392                    .all(|entry| entry.models.contains(&model.id))
393            {
394                report(
395                    "universal-model",
396                    &model.id,
397                    format!(
398                        "every language is made to use {}, which makes it a hard-coded universal foundation",
399                        model.id
400                    ),
401                );
402            }
403        }
404    }
405    problems
406}
meta_language/foundation_models.rs

meta_language/
foundation_models.rs
