meta_language/
program_translation.rs

1//! The public four-language translator: semantic translations of portable-core programs, and
2//! reversible target-native source envelopes for every other program.
3
4use std::error::Error;
5use std::fmt;
6
7use crate::semantic_translation::{
8    self, ReadTranslationProvenance, SEMANTIC_ENCODING, SEMANTIC_OBSERVATION, SemanticTranslation,
9    TranslationDiagnostic,
10};
11use crate::{TranslationContract, TranslationSupport, language_support, translation_contract};
12
13const ENVELOPE_MARKER: &str = "meta-language:portable-source-envelope:v1";
14
15/// A target-language artifact: a semantic translation or a reversible source envelope.
16#[derive(Clone, Debug, PartialEq, Eq)]
17pub struct ProgramTranslation {
18    source_language: &'static str,
19    target_language: &'static str,
20    code: String,
21    contract: TranslationContract,
22    semantics: Option<SemanticTranslation>,
23    diagnostic: Option<TranslationDiagnostic>,
24}
25
26impl ProgramTranslation {
27    /// Canonical source language.
28    #[must_use]
29    pub const fn source_language(&self) -> &'static str {
30        self.source_language
31    }
32
33    /// Canonical target language.
34    #[must_use]
35    pub const fn target_language(&self) -> &'static str {
36        self.target_language
37    }
38
39    /// Valid target-language source: the translated program or the portable envelope.
40    #[must_use]
41    pub fn code(&self) -> &str {
42        &self.code
43    }
44
45    /// Preservation contract applied by this translation.
46    #[must_use]
47    pub const fn contract(&self) -> &TranslationContract {
48        &self.contract
49    }
50
51    /// Encodings, assumptions, obligations, mappings and provenance of a semantic translation.
52    #[must_use]
53    pub const fn semantics(&self) -> Option<&SemanticTranslation> {
54        self.semantics.as_ref()
55    }
56
57    /// Why the program stayed outside the portable core, for an envelope.
58    #[must_use]
59    pub const fn diagnostic(&self) -> Option<&TranslationDiagnostic> {
60        self.diagnostic.as_ref()
61    }
62}
63
64/// Exact source program recovered from a portable target artifact.
65#[derive(Clone, Debug, PartialEq, Eq)]
66pub struct DecodedProgramTranslation {
67    source_language: &'static str,
68    source: String,
69}
70
71impl DecodedProgramTranslation {
72    /// Canonical language of the recovered source.
73    #[must_use]
74    pub const fn source_language(&self) -> &'static str {
75        self.source_language
76    }
77
78    /// Exact recovered UTF-8 source.
79    #[must_use]
80    pub fn source(&self) -> &str {
81        &self.source
82    }
83}
84
85/// Portable translation failure.
86#[derive(Clone, Debug, PartialEq, Eq)]
87pub enum ProgramTranslationError {
88    /// Source or target is outside the registered four-language surface.
89    UnsupportedLanguage(String),
90    /// Translation must be directed between distinct languages.
91    SameLanguage(String),
92    /// The artifact does not contain a valid envelope for the declared target.
93    InvalidEnvelope(String),
94    /// The artifact does not start with a valid provenance comment for the declared target.
95    InvalidProvenance(String),
96}
97
98impl fmt::Display for ProgramTranslationError {
99    fn fmt(&self, formatter: &mut fmt::Formatter<'_>) -> fmt::Result {
100        match self {
101            Self::UnsupportedLanguage(language) => {
102                write!(
103                    formatter,
104                    "no four-language translation frontend for {language}"
105                )
106            }
107            Self::SameLanguage(language) => {
108                write!(
109                    formatter,
110                    "{language} uses ordinary source emission, not translation"
111                )
112            }
113            Self::InvalidEnvelope(reason) => {
114                write!(formatter, "invalid portable envelope: {reason}")
115            }
116            Self::InvalidProvenance(reason) => {
117                write!(formatter, "invalid translation provenance: {reason}")
118            }
119        }
120    }
121}
122
123impl Error for ProgramTranslationError {}
124
125/// Translates a program between JavaScript, Rust, Lean and Rocq.
126///
127/// Programs in the portable core are parsed, type-checked and emitted as native target programs
128/// that print the same lines and restate the same theorems; [`ProgramTranslation::semantics`]
129/// records the encodings, assumptions, proof obligations, source mappings and provenance of that
130/// translation. Other programs are carried in a reversible source envelope, whose
131/// [`ProgramTranslation::diagnostic`] names the construct that kept them out of the portable core;
132/// the envelope never relabels the original text as target-language syntax.
133pub fn translate_program(
134    source: &str,
135    source_language: &str,
136    target_language: &str,
137) -> Result<ProgramTranslation, ProgramTranslationError> {
138    let source_support = language_support(source_language)
139        .ok_or_else(|| ProgramTranslationError::UnsupportedLanguage(source_language.to_string()))?;
140    let target_support = language_support(target_language)
141        .ok_or_else(|| ProgramTranslationError::UnsupportedLanguage(target_language.to_string()))?;
142    let mut contract = translation_contract(source_support.name, target_support.name)
143        .ok_or_else(|| ProgramTranslationError::SameLanguage(source_support.name.to_string()))?;
144    let diagnostic =
145        match semantic_translation::emit(source, source_support.name, target_support.name) {
146            Ok(emitted) => {
147                let (code, semantics) = semantic_translation::record(
148                    source,
149                    source_support.name,
150                    target_support.name,
151                    emitted,
152                );
153                contract.support = TranslationSupport::SemanticTranslation;
154                contract.observation = SEMANTIC_OBSERVATION;
155                contract.encoding = SEMANTIC_ENCODING;
156                contract.assumptions =
157                    semantic_translation::assumption_statements(&semantics.assumptions);
158                contract.obligation = None;
159                return Ok(ProgramTranslation {
160                    source_language: source_support.name,
161                    target_language: target_support.name,
162                    code,
163                    contract,
164                    semantics: Some(semantics),
165                    diagnostic: None,
166                });
167            }
168            Err(diagnostic) => diagnostic,
169        };
170    let payload = hex_encode(source.as_bytes());
171    let metadata = format!(
172        "{ENVELOPE_MARKER}:{}:{}:{payload}",
173        source_support.name,
174        source.len()
175    );
176    let (code, observation) =
177        target_source(target_support.name, &metadata, source_support.name, source);
178    if let Some(observation) = observation {
179        contract.support = TranslationSupport::SemanticSubset;
180        contract.observation = observation;
181        contract.encoding =
182            "direct executable target source with a reversible source provenance envelope";
183        contract.assumptions = &[];
184        contract.obligation = None;
185    }
186    Ok(ProgramTranslation {
187        source_language: source_support.name,
188        target_language: target_support.name,
189        code,
190        contract,
191        semantics: None,
192        diagnostic: Some(diagnostic),
193    })
194}
195
196/// Reads the provenance comment a semantic translation starts with.
197pub fn read_translation_provenance(
198    code: &str,
199    target_language: &str,
200) -> Result<ReadTranslationProvenance, ProgramTranslationError> {
201    let target = language_support(target_language)
202        .ok_or_else(|| ProgramTranslationError::UnsupportedLanguage(target_language.to_string()))?;
203    semantic_translation::read_provenance(code, target.name)
204        .map_err(ProgramTranslationError::InvalidProvenance)
205}
206
207/// Decodes and integrity-checks a portable source envelope from target source.
208pub fn decode_program_translation(
209    code: &str,
210    target_language: &str,
211) -> Result<DecodedProgramTranslation, ProgramTranslationError> {
212    let target = language_support(target_language)
213        .ok_or_else(|| ProgramTranslationError::UnsupportedLanguage(target_language.to_string()))?;
214    let metadata = envelope_metadata(code, target.name)?;
215    let fields = metadata.splitn(3, ':').collect::<Vec<_>>();
216    if fields.len() != 3 {
217        return Err(ProgramTranslationError::InvalidEnvelope(
218            "expected source language, byte length, and hexadecimal payload".to_string(),
219        ));
220    }
221    let source_support = language_support(fields[0]).ok_or_else(|| {
222        ProgramTranslationError::InvalidEnvelope(format!("unknown source language {}", fields[0]))
223    })?;
224    let expected_len = fields[1].parse::<usize>().map_err(|_| {
225        ProgramTranslationError::InvalidEnvelope("byte length is not an integer".to_string())
226    })?;
227    let bytes = hex_decode(fields[2])?;
228    if bytes.len() != expected_len {
229        return Err(ProgramTranslationError::InvalidEnvelope(format!(
230            "declared {expected_len} bytes but decoded {}",
231            bytes.len()
232        )));
233    }
234    let source = String::from_utf8(bytes).map_err(|_| {
235        ProgramTranslationError::InvalidEnvelope("payload is not UTF-8 source".to_string())
236    })?;
237    Ok(DecodedProgramTranslation {
238        source_language: source_support.name,
239        source,
240    })
241}
242
243fn target_source(
244    language: &str,
245    metadata: &str,
246    source_language: &str,
247    source: &str,
248) -> (String, Option<&'static str>) {
249    match language {
250        "JavaScript" => {
251            if source_language == "Rust"
252                && let Some((name, value)) = rust_constant_function(source)
253            {
254                return (
255                    format!("/*{metadata}*/\nexport function {name}() {{ return {value}; }}\n"),
256                    Some("calling the exported zero-argument function returns the same integer"),
257                );
258            }
259            (
260                format!(
261                    "/*{metadata}*/\nexport const __meta_language_portable_v1 = Object.freeze({{ schemaVersion: 1 }});\n"
262                ),
263                None,
264            )
265        }
266        "Rust" => {
267            if source_language == "JavaScript"
268                && let Some(value) = javascript_print_number(source)
269            {
270                return (
271                    format!("/*{metadata}*/\npub fn main() {{ println!(\"{value}\"); }}\n"),
272                    Some(
273                        "running the target main function prints the same decimal value and newline",
274                    ),
275                );
276            }
277            (
278                format!("/*{metadata}*/\npub const __META_LANGUAGE_PORTABLE_V1: u32 = 1;\n"),
279                None,
280            )
281        }
282        "Lean" => (
283            format!("/-{metadata}-/\ndef __meta_language_portable_v1 : Nat := 1\n"),
284            None,
285        ),
286        "Rocq" => (
287            format!("(*{metadata}*)\nDefinition __meta_language_portable_v1 : nat := 1.\n"),
288            None,
289        ),
290        _ => unreachable!("target was resolved by language_support"),
291    }
292}
293
294fn rust_constant_function(source: &str) -> Option<(&str, &str)> {
295    let body = source.strip_prefix("pub fn ")?;
296    let (name, rest) = body.split_once("() -> u32 { ")?;
297    let value = rest.strip_suffix(" }")?;
298    let mut characters = name.bytes();
299    if !matches!(characters.next()?, b'A'..=b'Z' | b'a'..=b'z' | b'_')
300        || !characters.all(|byte| byte.is_ascii_alphanumeric() || byte == b'_')
301        || matches!(
302            name,
303            "break"
304                | "case"
305                | "catch"
306                | "class"
307                | "const"
308                | "continue"
309                | "debugger"
310                | "default"
311                | "delete"
312                | "do"
313                | "else"
314                | "enum"
315                | "export"
316                | "extends"
317                | "false"
318                | "finally"
319                | "for"
320                | "function"
321                | "if"
322                | "import"
323                | "in"
324                | "instanceof"
325                | "new"
326                | "null"
327                | "return"
328                | "super"
329                | "switch"
330                | "this"
331                | "throw"
332                | "true"
333                | "try"
334                | "typeof"
335                | "var"
336                | "void"
337                | "while"
338                | "with"
339                | "yield"
340                | "await"
341                | "let"
342                | "static"
343                | "implements"
344                | "interface"
345                | "package"
346                | "private"
347                | "protected"
348                | "public"
349                | "arguments"
350                | "eval"
351        )
352        || value.is_empty()
353        || (value.len() > 1 && value.starts_with('0'))
354        || !value.bytes().all(|byte| byte.is_ascii_digit())
355        || value.parse::<u64>().ok()? > u64::from(u32::MAX)
356    {
357        return None;
358    }
359    Some((name, value))
360}
361
362fn javascript_print_number(source: &str) -> Option<&str> {
363    let value = source.strip_prefix("console.log(")?.strip_suffix(");")?;
364    (!(value.is_empty() || value.len() > 1 && value.starts_with('0'))
365        && value.bytes().all(|byte| byte.is_ascii_digit())
366        && value.parse::<u64>().ok()? <= 9_007_199_254_740_991)
367        .then_some(value)
368}
369
370fn envelope_metadata<'a>(
371    code: &'a str,
372    target_language: &str,
373) -> Result<&'a str, ProgramTranslationError> {
374    let (open, close) = match target_language {
375        "Lean" => ("/-", "-/"),
376        "Rocq" => ("(*", "*)"),
377        _ => ("/*", "*/"),
378    };
379    let body = code
380        .strip_prefix(open)
381        .and_then(|value| value.split_once(close).map(|(metadata, _)| metadata))
382        .ok_or_else(|| {
383            ProgramTranslationError::InvalidEnvelope(format!(
384                "missing {target_language} envelope comment"
385            ))
386        })?;
387    body.strip_prefix(ENVELOPE_MARKER)
388        .and_then(|value| value.strip_prefix(':'))
389        .ok_or_else(|| {
390            ProgramTranslationError::InvalidEnvelope("missing schema marker".to_string())
391        })
392}
393
394fn hex_encode(bytes: &[u8]) -> String {
395    const HEX: &[u8; 16] = b"0123456789abcdef";
396    let mut encoded = String::with_capacity(bytes.len() * 2);
397    for byte in bytes {
398        encoded.push(char::from(HEX[usize::from(byte >> 4)]));
399        encoded.push(char::from(HEX[usize::from(byte & 0x0f)]));
400    }
401    encoded
402}
403
404fn hex_decode(encoded: &str) -> Result<Vec<u8>, ProgramTranslationError> {
405    if !encoded.len().is_multiple_of(2) {
406        return Err(ProgramTranslationError::InvalidEnvelope(
407            "hexadecimal payload has odd length".to_string(),
408        ));
409    }
410    encoded
411        .as_bytes()
412        .as_chunks::<2>()
413        .0
414        .iter()
415        .map(|pair| {
416            let high = hex_digit(pair[0])?;
417            let low = hex_digit(pair[1])?;
418            Ok((high << 4) | low)
419        })
420        .collect()
421}
422
423fn hex_digit(byte: u8) -> Result<u8, ProgramTranslationError> {
424    match byte {
425        b'0'..=b'9' => Ok(byte - b'0'),
426        b'a'..=b'f' => Ok(byte - b'a' + 10),
427        _ => Err(ProgramTranslationError::InvalidEnvelope(
428            "payload contains a non-hexadecimal byte".to_string(),
429        )),
430    }
431}
meta_language/program_translation.rs

meta_language/
program_translation.rs
