meta_language/
semantic_translation.rs

1//! Semantic translations produced by the portable-core translator.
2//!
3//! A program in the portable core is parsed, type-checked and emitted as a native target program
4//! that prints the same lines and restates the same theorems. [`SemanticTranslation`] records what
5//! that translation relied on: its encodings, assumptions, proof obligations, source mappings,
6//! runtime dependencies and provenance.
7//!
8//! Mirrors the semantic half of `js/src/program-translation.js`.
9
10use sha2::{Digest, Sha256};
11
12use crate::translation::check::check_program;
13use crate::translation::diagnostics::TranslationError;
14use crate::translation::emit_common::{Assumption, Emitted, Encoding, IN_BOUNDS_READS, Mapping};
15use crate::translation::{
16    Span, emit_javascript::emit_javascript, emit_lean::emit_lean, emit_rocq::emit_rocq,
17    emit_rust::emit_rust, javascript::parse_javascript, lean::parse_lean, rocq::parse_rocq,
18    rust::parse_rust,
19};
20
21const PROVENANCE_MARKER: &str = "meta-language:translation-provenance:v1";
22const TRANSLATOR: &str = "meta-language portable-core translator";
23
24/// What a semantic translation preserves: the printed lines and every stated proposition.
25pub const SEMANTIC_OBSERVATION: &str = "the lines main prints, in order, on executions that do not abort, and the proposition of every source theorem and assertion over the translated definitions";
26
27/// The contract encoding of a semantic translation.
28pub const SEMANTIC_ENCODING: &str =
29    "portable-core translation; the encodings it chose are listed in semantics.encodings";
30
31/// How a proof obligation of the source is met in the target.
32#[derive(Clone, Debug, PartialEq, Eq)]
33pub struct TranslationObligation {
34    /// Source theorem, or `main:assert@<offset>` for an assertion.
35    pub source: String,
36    /// Target declaration that states it.
37    pub target: String,
38    /// `theorem` or `assertion`.
39    pub kind: String,
40    /// Whether the statement has no free variables.
41    pub closed_goal: bool,
42    /// `target-kernel`, `source-kernel` or `runtime-assertion`.
43    pub discharge: String,
44    /// The target-side check of a source-kernel proof (`bounded`).
45    pub check: Option<String>,
46}
47
48/// Where a semantic translation came from.
49#[derive(Clone, Debug, PartialEq, Eq)]
50pub struct TranslationProvenance {
51    /// The translator that produced the artifact.
52    pub translator: &'static str,
53    /// Canonical source language.
54    pub source_language: &'static str,
55    /// Lowercase hexadecimal SHA-256 of the UTF-8 source.
56    pub source_sha256: String,
57    /// Source length in bytes.
58    pub source_bytes: usize,
59    /// The comment the artifact starts with.
60    pub header: String,
61}
62
63/// The record of one semantic translation.
64#[derive(Clone, Debug, PartialEq, Eq)]
65pub struct SemanticTranslation {
66    /// The target's entry point, when the source has a main program.
67    pub entry: Option<String>,
68    /// How the target's observations are made.
69    pub observation_procedure: &'static str,
70    /// Representation choices for constructs without a direct target equivalent.
71    pub encodings: Vec<Encoding>,
72    /// Assumptions, with the program-specific details.
73    pub assumptions: Vec<Assumption>,
74    /// Source theorems and assertions and how the target discharges them.
75    pub obligations: Vec<TranslationObligation>,
76    /// Where each source declaration went, with its source span in UTF-16 code units.
77    pub mappings: Vec<Mapping>,
78    /// Libraries and host features the emitted program needs.
79    pub runtime_dependencies: Vec<String>,
80    /// Where the translation came from.
81    pub provenance: TranslationProvenance,
82}
83
84/// Why a program stayed outside the portable core.
85#[derive(Clone, Debug, PartialEq, Eq)]
86pub struct TranslationDiagnostic {
87    /// `syntax`, `type` or `unsupported`.
88    pub kind: &'static str,
89    /// The message with its span suffix.
90    pub message: String,
91    /// The source range, in UTF-16 code units.
92    pub span: Option<Span>,
93}
94
95/// Provenance recovered from an artifact's first line.
96#[derive(Clone, Debug, PartialEq, Eq)]
97pub struct ReadTranslationProvenance {
98    /// Canonical source language.
99    pub source_language: &'static str,
100    /// Lowercase hexadecimal SHA-256 of the UTF-8 source.
101    pub source_sha256: String,
102    /// Source length in bytes.
103    pub source_bytes: usize,
104}
105
106/// Runs the portable-core pipeline for canonical language names.
107pub fn emit(
108    source: &str,
109    source_language: &str,
110    target_language: &str,
111) -> Result<Emitted, TranslationDiagnostic> {
112    let surface = match source_language {
113        "JavaScript" => parse_javascript(source),
114        "Rust" => parse_rust(source),
115        "Lean" => parse_lean(source),
116        _ => parse_rocq(source),
117    };
118    let emitted = surface
119        .and_then(|surface| check_program(&surface))
120        .and_then(|program| match target_language {
121            "JavaScript" => emit_javascript(&program),
122            "Rust" => emit_rust(&program),
123            "Lean" => emit_lean(&program),
124            _ => emit_rocq(&program),
125        });
126    emitted.map_err(|error: TranslationError| TranslationDiagnostic {
127        kind: error.kind.as_str(),
128        message: error.message(),
129        span: error.span,
130    })
131}
132
133const fn comment(target_language: &str) -> (&'static str, &'static str) {
134    match target_language.as_bytes() {
135        b"Lean" => ("-- ", ""),
136        b"Rocq" => ("(* ", " *)"),
137        _ => ("// ", ""),
138    }
139}
140
141/// The artifact text and its semantic record.
142pub fn record(
143    source: &str,
144    source_language: &'static str,
145    target_language: &str,
146    emitted: Emitted,
147) -> (String, SemanticTranslation) {
148    let source_sha256 = Sha256::digest(source.as_bytes()).iter().fold(
149        String::with_capacity(64),
150        |mut hex, byte| {
151            use std::fmt::Write as _;
152            let _ = write!(hex, "{byte:02x}");
153            hex
154        },
155    );
156    let (open, close) = comment(target_language);
157    let header = format!(
158        "{open}{PROVENANCE_MARKER} source={source_language} sha256={source_sha256} bytes={}{close}",
159        source.len()
160    );
161    let kernel_target = matches!(target_language, "Lean" | "Rocq");
162    let obligations = emitted
163        .theorems
164        .into_iter()
165        .map(|theorem| TranslationObligation {
166            source: theorem.source,
167            target: theorem.target,
168            kind: theorem.kind,
169            closed_goal: theorem.closed_goal,
170            discharge: theorem.discharge.unwrap_or_else(|| {
171                if kernel_target {
172                    "target-kernel"
173                } else {
174                    "runtime-assertion"
175                }
176                .to_owned()
177            }),
178            check: theorem.check,
179        })
180        .collect();
181    let semantics = SemanticTranslation {
182        entry: emitted.entry,
183        observation_procedure: observation_procedure(target_language),
184        encodings: emitted.encodings,
185        assumptions: emitted.assumptions,
186        obligations,
187        mappings: emitted.mappings,
188        runtime_dependencies: runtime_dependencies(target_language, &emitted.text),
189        provenance: TranslationProvenance {
190            translator: TRANSLATOR,
191            source_language,
192            source_sha256,
193            source_bytes: source.len(),
194            header: header.clone(),
195        },
196    };
197    (format!("{header}\n{}", emitted.text), semantics)
198}
199
200/// The fixed assumption statements a contract lists for these assumptions, in their order.
201pub fn assumption_statements(assumptions: &[Assumption]) -> &'static [&'static str] {
202    const NONE: &[&str] = &[];
203    const READS: &[&str] = &[IN_BOUNDS_READS.statement];
204    let ids: Vec<&str> = assumptions
205        .iter()
206        .map(|assumption| assumption.id.as_str())
207        .collect();
208    match ids.as_slice() {
209        [] => NONE,
210        [first] if *first == IN_BOUNDS_READS.id => READS,
211        _ => unreachable!("unknown assumptions {ids:?}"),
212    }
213}
214
215const fn observation_procedure(target_language: &str) -> &'static str {
216    match target_language.as_bytes() {
217        b"JavaScript" => {
218            "run the module with node; --ml-check-theorems evaluates the theorem properties instead of main"
219        }
220        b"Rust" => {
221            "compile with rustc and run the binary; --ml-check-theorems evaluates the theorem properties instead of main"
222        }
223        b"Lean" => {
224            "lean --run executes main after the Lean kernel has checked every definition and theorem"
225        }
226        _ => {
227            "rocq compile checks every definition and proof; Eval vm_compute in main prints the list of output lines"
228        }
229    }
230}
231
232/// The libraries and host features the emitted program needs, read from its text.
233fn runtime_dependencies(target_language: &str, code: &str) -> Vec<String> {
234    let mut dependencies = Vec::new();
235    match target_language {
236        "JavaScript" => {
237            dependencies.push("ECMAScript 2026 host with BigInt".to_owned());
238            if code.contains("process.argv") {
239                dependencies.push("Node.js process.argv (selects --ml-check-theorems)".to_owned());
240            }
241        }
242        "Rust" => {
243            dependencies.push("Rust 1.99.0 standard library".to_owned());
244            if code.contains("\npub mod ml {") {
245                dependencies.push(
246                    "ml::Big arbitrary-precision integers, defined inside the artifact".to_owned(),
247                );
248            }
249            if code.contains("\npub mod ml_number {") {
250                dependencies.push(
251                    "ml_number JavaScript Number formatting and SameValue, defined inside the artifact"
252                        .to_owned(),
253                );
254            }
255        }
256        "Lean" => {
257            dependencies.push("Lean 4.34.1 core library".to_owned());
258            dependencies.extend(
259                code.lines()
260                    .filter_map(|line| line.strip_prefix("import "))
261                    .map(|module| module.trim().to_owned()),
262            );
263        }
264        _ => {
265            dependencies.push("Rocq 9.3".to_owned());
266            for line in code.lines() {
267                let Some(rest) = line.strip_prefix("From ") else {
268                    continue;
269                };
270                let Some((library, modules)) = rest.split_once(" Require Import ") else {
271                    continue;
272                };
273                let Some(modules) = modules.strip_suffix('.') else {
274                    continue;
275                };
276                if library.is_empty() || !library.chars().all(|c| c.is_ascii_alphabetic()) {
277                    continue;
278                }
279                dependencies.extend(
280                    modules
281                        .split_whitespace()
282                        .map(|module| format!("{library}.{module}")),
283                );
284            }
285        }
286    }
287    dependencies
288}
289
290/// Reads the provenance comment a semantic translation starts with.
291pub fn read_provenance(
292    code: &str,
293    target_language: &str,
294) -> Result<ReadTranslationProvenance, String> {
295    let (open, close) = comment(target_language);
296    let first_line = code.split('\n').next().unwrap_or_default();
297    let fields = first_line
298        .strip_prefix(open)
299        .and_then(|line| line.strip_prefix(PROVENANCE_MARKER))
300        .and_then(|line| line.strip_prefix(' '))
301        .and_then(|line| line.strip_suffix(close))
302        .ok_or_else(|| format!("missing {target_language} provenance comment"))?;
303    let field = |name: &str| {
304        fields.split(' ').find_map(|field| {
305            field
306                .strip_prefix(name)
307                .and_then(|rest| rest.strip_prefix('='))
308        })
309    };
310    let invalid = || "expected source, sha256 and bytes fields".to_owned();
311    let source_language = field("source")
312        .and_then(crate::language_support)
313        .ok_or_else(invalid)?
314        .name;
315    let source_sha256 = field("sha256")
316        .filter(|hash| {
317            hash.len() == 64
318                && hash
319                    .bytes()
320                    .all(|b| b.is_ascii_digit() || (b'a'..=b'f').contains(&b))
321        })
322        .ok_or_else(invalid)?
323        .to_owned();
324    let source_bytes = field("bytes")
325        .and_then(|bytes| bytes.parse::<usize>().ok())
326        .ok_or_else(invalid)?;
327    Ok(ReadTranslationProvenance {
328        source_language,
329        source_sha256,
330        source_bytes,
331    })
332}
meta_language/semantic_translation.rs

meta_language/
semantic_translation.rs
