logicaffeine_kernel/interface/lean/
pipeline.rs

1//! The Lean → LOGOS pipeline, one named stage at a time, and the benchmark protocol's dispatch.
2//!
3//! Parsing and validation ([`intake`](super::intake)), environment import and checking (the reader),
4//! audit construction ([`ImportReport`](super::ImportReport)), assumption policy, emission
5//! ([`emit`](super::emit)) and packaging ([`package`](super::package)) stay separate here, each
6//! recording its own [`receipt`](super::receipt) stage, so a result is never one unexplained
7//! Boolean (competition rule R1). The reader interleaves translation and checking per declaration;
8//! that is reported honestly — a declaration the kernel refused leaves `translated` `not_run`, since
9//! the closure's translation never finished.
10//!
11//! Everything here is pure: no file, process or clock. Reading the export, running Lean, publishing
12//! the package and replaying it in a fresh process are the command's (`largo lean`).
13
14use super::intake::{self, STAGE_A};
15use super::receipt::{Receipt, StageStatus, STAGES};
16use super::{
17    emit, native_decide, package, reference, DiagnosticCode, ImportReport, Outcome, Verdict,
18};
19use serde_json::{json, Value};
20use std::collections::BTreeMap;
21
22pub const RESULT_SCHEMA: &str = "logos-lean-result/1";
23
24/// One typed, located diagnostic of a result.
25#[derive(Clone, Debug, PartialEq, Eq)]
26pub struct Diagnostic {
27    pub code: DiagnosticCode,
28    /// The receipt stage it concerns.
29    pub stage: &'static str,
30    /// The Lean declaration (dotted name) it concerns.
31    pub declaration: Option<String>,
32    /// The 1-based line of the input it concerns.
33    pub line: Option<usize>,
34    pub message: String,
35    outcome: Outcome,
36}
37
38impl Diagnostic {
39    /// A diagnostic of a classified code. An unclassified or usage code is an unsupported feature.
40    pub fn new(stage: &'static str, code: DiagnosticCode, message: impl Into<String>) -> Self {
41        Diagnostic {
42            code,
43            stage,
44            declaration: None,
45            line: None,
46            message: message.into(),
47            outcome: Outcome::of_refusal(code, false),
48        }
49    }
50    /// The diagnostic a refusal carries, with its location.
51    pub fn of_refusal(stage: &'static str, verdict: &Verdict) -> Self {
52        let reason = verdict.reason();
53        Diagnostic {
54            code: reason.code(),
55            stage,
56            declaration: reason.declaration().map(str::to_string),
57            line: reason.line(),
58            message: reason.message().to_string(),
59            outcome: verdict.outcome(),
60        }
61    }
62    pub fn with_declaration(mut self, declaration: impl Into<String>) -> Self {
63        self.declaration = Some(declaration.into());
64        self
65    }
66    pub fn with_line(mut self, line: usize) -> Self {
67        self.line = Some(line);
68        self
69    }
70    /// The outcome this diagnostic decides when its stage is the first that did not pass.
71    pub fn outcome(&self) -> Outcome {
72        self.outcome
73    }
74    pub fn to_json(&self) -> Value {
75        json!({
76            "code": self.code.as_str(),
77            "stage": self.stage,
78            "declaration": self.declaration,
79            "line": self.line,
80            "message": self.message,
81        })
82    }
83}
84
85/// Information the result does not carry from the Lean input.
86#[derive(Clone, Debug, PartialEq, Eq)]
87pub struct Loss {
88    pub category: String,
89    pub detail: String,
90}
91
92/// A published package, as the result names it.
93#[derive(Clone, Debug, PartialEq, Eq)]
94pub struct PackageRef {
95    pub path: String,
96    pub manifest_sha256: String,
97}
98
99/// What the run observed of Lean itself.
100#[derive(Clone, Debug, PartialEq, Eq)]
101pub enum LeanEvidence {
102    /// A pre-exported artifact: Lean was not run, so its acceptance is not established.
103    NotObserved,
104    /// Lean compiled the project in isolation, and `#print axioms` reported `axioms` (Lean names)
105    /// for the target.
106    Accepted {
107        axioms: Vec<String>,
108        /// The original Lean sources, by project-relative path (published under `source/`).
109        sources: BTreeMap<String, Vec<u8>>,
110        /// The pinned toolchain and exporter identities.
111        toolchain: String,
112        exporter: String,
113    },
114}
115
116impl LeanEvidence {
117    /// What the package records of the producing run.
118    fn build_options(&self) -> package::BuildOptions {
119        match self {
120            LeanEvidence::NotObserved => package::BuildOptions::default(),
121            LeanEvidence::Accepted {
122                axioms,
123                sources,
124                toolchain,
125                exporter,
126            } => package::BuildOptions {
127                lean_sources: sources.clone(),
128                lean_run: Some(package::LeanRun {
129                    toolchain: toolchain.clone(),
130                    exporter: exporter.clone(),
131                    accepted: true,
132                    detail: format!("compiled in isolation; #print axioms: {axioms:?}"),
133                }),
134            },
135        }
136    }
137}
138
139/// Budgets declared before any work.
140#[derive(Clone, Copy, Debug, PartialEq, Eq)]
141pub struct Limits {
142    pub max_export_bytes: u64,
143}
144
145impl Default for Limits {
146    fn default() -> Self {
147        Limits {
148            max_export_bytes: 1 << 30,
149        }
150    }
151}
152
153/// A `logos-lean-result/1` document under construction.
154#[derive(Clone, Debug, PartialEq)]
155pub struct LeanResult {
156    pub receipt: Receipt,
157    pub target_lean: String,
158    pub target_logos: Option<String>,
159    pub assumptions: Vec<String>,
160    pub information_losses: Vec<Loss>,
161    pub diagnostics: Vec<Diagnostic>,
162    /// The importer's audit (`logos-lean-import-report/1`), when the import ran.
163    pub audit: Option<Value>,
164    pub package: Option<PackageRef>,
165}
166
167impl LeanResult {
168    /// A result for `target` in which nothing has run.
169    pub fn new(target_lean: impl Into<String>) -> Self {
170        LeanResult {
171            receipt: Receipt::unstarted(),
172            target_lean: target_lean.into(),
173            target_logos: None,
174            assumptions: Vec::new(),
175            information_losses: Vec::new(),
176            diagnostics: Vec::new(),
177            audit: None,
178            package: None,
179        }
180    }
181
182    pub fn status(&self, stage: &str) -> StageStatus {
183        self.receipt
184            .stage(stage)
185            .map(|s| s.status)
186            .unwrap_or(StageStatus::NotRun)
187    }
188
189    pub fn pass(&mut self, stage: &'static str, detail: impl Into<String>) {
190        self.receipt.set(stage, StageStatus::Passed, detail);
191    }
192
193    /// Record `stage` as `status` for the reason `diagnostic` gives.
194    pub fn mark(&mut self, stage: &'static str, status: StageStatus, diagnostic: Diagnostic) {
195        self.receipt.set(stage, status, diagnostic.message.clone());
196        self.diagnostics.push(Diagnostic {
197            stage,
198            ..diagnostic
199        });
200    }
201
202    /// `stage` failed for the reason `diagnostic` gives.
203    pub fn fail(&mut self, stage: &'static str, diagnostic: Diagnostic) {
204        self.mark(stage, StageStatus::Failed, diagnostic);
205    }
206
207    /// The outcome: the first stage that failed decides it; otherwise every stage passed
208    /// (`verified`), or the first stage that did not decides it.
209    pub fn outcome(&self) -> Outcome {
210        let decided_by = |stage: &str| {
211            self.diagnostics
212                .iter()
213                .find(|d| d.stage == stage)
214                .map(Diagnostic::outcome)
215                .unwrap_or(Outcome::UnsupportedFeature)
216        };
217        if let Some(stage) = STAGES
218            .iter()
219            .find(|s| self.status(s) == StageStatus::Failed)
220        {
221            return decided_by(stage);
222        }
223        match STAGES
224            .iter()
225            .find(|s| self.status(s) != StageStatus::Passed)
226        {
227            None => Outcome::Verified,
228            Some(stage) => decided_by(stage),
229        }
230    }
231
232    pub fn exit_code(&self) -> i32 {
233        self.outcome().exit_code()
234    }
235
236    /// Explain a stage that did not run where it decides the outcome: when nothing failed, a
237    /// `lean_accepted` stage that was never observed is the reason the result is not verified.
238    pub fn finish(&mut self) {
239        let failed = STAGES.iter().any(|s| self.status(s) == StageStatus::Failed);
240        let lean = "lean_accepted";
241        if !failed
242            && self.status(lean) == StageStatus::NotRun
243            && !self.diagnostics.iter().any(|d| d.stage == lean)
244        {
245            self.diagnostics.push(Diagnostic::new(
246                lean,
247                DiagnosticCode::LeanAcceptanceNotObserved,
248                "the input is a pre-exported artifact: this run did not observe Lean accept its source, so the \
249                 result cannot be verified (import the Lean project with --project to establish it)",
250            ));
251        }
252    }
253
254    pub fn to_json(&self) -> Value {
255        let stages: serde_json::Map<String, Value> = STAGES
256            .iter()
257            .map(|s| (s.to_string(), Value::from(self.status(s).as_str())))
258            .collect();
259        json!({
260            "schema": RESULT_SCHEMA,
261            "outcome": self.outcome().as_str(),
262            "stages": stages,
263            "target": { "lean": self.target_lean, "logos": self.target_logos },
264            "assumptions": self.assumptions,
265            "information_losses": self.information_losses.iter()
266                .map(|l| json!({"category": l.category, "detail": l.detail}))
267                .collect::<Vec<_>>(),
268            "diagnostics": self.diagnostics.iter().map(Diagnostic::to_json).collect::<Vec<_>>(),
269            "package": self.package.as_ref().map(|p| json!({"path": p.path, "manifest_sha256": p.manifest_sha256})),
270            "audit": self.audit,
271        })
272    }
273}
274
275/// A result and, when every stage up to packaging passed, the package to publish and replay.
276pub struct Checked {
277    pub result: LeanResult,
278    pub package: Option<package::PackageFiles>,
279}
280
281/// The stage a refusal from the import belongs to. The reader interleaves translation and checking,
282/// so a refusal that names its stage keeps it (every verdict of the independent kernel, a resource
283/// limit included, is the recheck's); otherwise a kernel refutation is the primary check's, a
284/// refused independent recheck or audit is the recheck's, and everything else — malformed,
285/// unsupported, over budget — stopped the translation.
286pub(super) fn import_stage(verdict: &Verdict) -> &'static str {
287    if let Some(stage) = verdict.reason().stage() {
288        return stage;
289    }
290    match verdict.reason().code() {
291        DiagnosticCode::InvalidProof => "primary_check",
292        DiagnosticCode::RecheckRefused | DiagnosticCode::AuditIncomplete => "independent_recheck",
293        _ => "translated",
294    }
295}
296
297/// Run every in-process stage over a Lean export for the dotted Lean name `target`: intake, import
298/// and check, independent recheck, assumption policy, emission and package assembly. `fresh_replay`
299/// is left to the caller, which must replay the published package in a new process.
300pub fn check_export(
301    export: &str,
302    target: &str,
303    evidence: &LeanEvidence,
304    limits: &Limits,
305) -> Checked {
306    let mut result = LeanResult::new(target);
307    let package = run_stages(&mut result, export, target, evidence, limits);
308    Checked { result, package }
309}
310
311fn run_stages(
312    result: &mut LeanResult,
313    export: &str,
314    target: &str,
315    evidence: &LeanEvidence,
316    limits: &Limits,
317) -> Option<package::PackageFiles> {
318    if let LeanEvidence::Accepted { .. } = evidence {
319        result.pass("lean_accepted", "Lean compiled the project in isolation");
320    }
321    let kernel_target = match intake::kernel_name(target) {
322        Ok(name) => name,
323        Err(verdict) => {
324            result.fail(
325                "translated",
326                Diagnostic::of_refusal("translated", &verdict).with_declaration(target),
327            );
328            return None;
329        }
330    };
331    if export.len() as u64 > limits.max_export_bytes {
332        result.fail(
333            "translated",
334            Diagnostic::new(
335                "translated",
336                DiagnosticCode::ResourceLimit,
337                format!(
338                    "the export is {} bytes; the declared budget is {} bytes",
339                    export.len(),
340                    limits.max_export_bytes
341                ),
342            ),
343        );
344        return None;
345    }
346    let read = match intake::read(export, &STAGE_A) {
347        Ok(read) => read,
348        Err(verdict) => {
349            result.fail("translated", Diagnostic::of_refusal("translated", &verdict));
350            return None;
351        }
352    };
353    let closure = match read.closure(&kernel_target) {
354        Ok(closure) => closure,
355        Err(verdict) => {
356            result.fail(
357                "translated",
358                Diagnostic::of_refusal("translated", &verdict).with_declaration(target),
359            );
360            return None;
361        }
362    };
363
364    match super::runtime_refusal::check(export, &kernel_target, &read) {
365        Ok(Some(audit)) => {
366            result.pass("translated", "the runtime bodies were lowered into a conditional judgment; the originals remain quarantined");
367            result.pass("primary_check", "the primary kernel checked the conditional judgment under local assumptions; the unsafe target was not proved or imported");
368            result.pass("independent_recheck", "the independent kernel checked the same conditional judgment; no unsafe declaration entered the environment");
369            result.audit = Some(audit.to_json());
370            result.assumptions = audit.assumptions.clone();
371            let disagreement = match evidence {
372                LeanEvidence::Accepted { axioms, .. } => {
373                    let stated: std::collections::BTreeSet<_> = axioms.iter().collect();
374                    let observed: std::collections::BTreeSet<_> =
375                        audit.assumptions.iter().collect();
376                    stated.len() != axioms.len() || stated != observed
377                }
378                LeanEvidence::NotObserved => false,
379            };
380            let code = if disagreement {
381                DiagnosticCode::AssumptionDisagreement
382            } else {
383                DiagnosticCode::DisallowedAssumption
384            };
385            let detail = if disagreement {
386                "Lean's reported assumptions differ from the original source dependency closure of the conditionally checked runtime judgment"
387            } else {
388                "the runtime body's conditional check requires a disallowed assumption; the original unsafe target is not proved, imported, or published"
389            };
390            result.fail(
391                "assumption_policy",
392                Diagnostic::new("assumption_policy", code, detail).with_declaration(target),
393            );
394            result.diagnostics.extend(
395                audit
396                    .taint
397                    .iter()
398                    .filter(|path| {
399                        !intake::STAGE_A
400                            .allowed_axioms
401                            .contains(&path.assumption.as_str())
402                    })
403                    .map(|path| {
404                        Diagnostic::new(
405                            "assumption_policy",
406                            DiagnosticCode::DisallowedAssumption,
407                            format!("taint path to {}: {}", path.assumption, path.render()),
408                        )
409                        .with_declaration(target)
410                    }),
411            );
412            return None;
413        }
414        Ok(None) => {}
415        Err(verdict) => {
416            let stage = import_stage(&verdict);
417            result.fail(
418                stage,
419                Diagnostic::of_refusal(stage, &verdict).with_declaration(target),
420            );
421            return None;
422        }
423    }
424
425    let (imported, report) = match super::import_retaining_closure(export, &kernel_target, &closure)
426    {
427        Ok(imported) => imported,
428        Err(verdict) => {
429            let stage = import_stage(&verdict);
430            result.fail(stage, Diagnostic::of_refusal(stage, &verdict));
431            return None;
432        }
433    };
434    result.pass(
435        "translated",
436        format!("{} declarations of the target's closure", closure.len()),
437    );
438    result.pass(
439        "primary_check",
440        "the LOGOS kernel accepted every declaration of the export",
441    );
442    result.pass(
443        "independent_recheck",
444        format!(
445            "{} definitions, theorems, opaques and axioms rechecked independently",
446            report.declarations.len()
447        ),
448    );
449    result.audit = Some(report.to_json());
450    result.information_losses = losses(&report);
451
452    // Assumption policy: the target's transitive assumptions of statement and proof, computed by the
453    // package from the checked environment with Lean's `#print axioms` semantics (an axiom reached
454    // counts; the axioms its own type mentions do not). In project mode Lean's own report must agree
455    // with them as the package's contract says; a run that did not observe Lean publishes no package,
456    // and its result is held to the audit of the checked proof alone.
457    let print_axioms = match evidence {
458        LeanEvidence::Accepted { axioms, .. } => Some(axioms.clone()),
459        LeanEvidence::NotObserved => None,
460    };
461    let build = match package::build_observed(
462        export,
463        target,
464        &evidence.build_options(),
465        print_axioms.as_deref(),
466    ) {
467        Ok(build) => build,
468        Err(verdict) => {
469            result.mark(
470                "assumption_policy",
471                status_of(&verdict),
472                self_verification_failure("assumption_policy", &verdict),
473            );
474            return None;
475        }
476    };
477    let manifest: Option<package::Manifest> = build
478        .files
479        .get(package::MANIFEST)
480        .and_then(|m| serde_json::from_slice(m).ok());
481    if let Some(manifest) = &manifest {
482        result.assumptions = manifest
483            .assumptions
484            .transitive
485            .iter()
486            .map(|a| intake::lean_name(a))
487            .collect();
488        // The checked proof the result reports is its package's: every re-derived step is disclosed
489        // exactly as the package discloses it.
490        result.information_losses.extend(
491            manifest
492                .information_losses
493                .iter()
494                .filter(|loss| loss.category == native_decide::INFORMATION_CATEGORY)
495                .map(|loss| Loss {
496                    category: loss.category.clone(),
497                    detail: loss.detail.clone(),
498                }),
499        );
500    }
501    let policy = match evidence {
502        LeanEvidence::Accepted { .. } => build
503            .receipt
504            .stage("assumption_policy")
505            .expect("every stage is on the receipt")
506            .clone(),
507        LeanEvidence::NotObserved => build.audit.clone(),
508    };
509    match policy.status {
510        StageStatus::Passed => result.pass("assumption_policy", policy.detail.clone()),
511        StageStatus::Failed => {
512            let code = if policy.code.as_deref() == Some("assumption_disagreement") {
513                DiagnosticCode::AssumptionDisagreement
514            } else {
515                DiagnosticCode::DisallowedAssumption
516            };
517            result.fail(
518                "assumption_policy",
519                Diagnostic::new("assumption_policy", code, policy.detail.clone())
520                    .with_declaration(target),
521            );
522            result.diagnostics.extend(super::taint::diagnostics(
523                &imported,
524                &kernel_target,
525                target,
526                &result.assumptions,
527            ));
528            return None;
529        }
530        StageStatus::NotRun | StageStatus::Unsupported => {
531            // The package's own rebuild of the imported environment did not reach the policy.
532            let blocker = build
533                .receipt
534                .first_failure()
535                .map(|s| format!("{}: {}", s.name, s.detail))
536                .unwrap_or(policy.detail.clone());
537            result.fail(
538                "assumption_policy",
539                Diagnostic::new(
540                    "assumption_policy",
541                    DiagnosticCode::InternalInconsistency,
542                    format!("LOGOS's own package of {target} did not reach its assumption policy: {blocker}"),
543                ),
544            );
545            return None;
546        }
547    }
548
549    // Emission, reparsed in a fresh context (by the emitter), and the reparsed target statement held
550    // against the independent reference translation of the Lean type (rule R8).
551    let document = match emit::emit_document(&imported, &kernel_target) {
552        Ok(document) => document,
553        Err(verdict) => {
554            result.mark(
555                "emission_reparsed",
556                status_of(&verdict),
557                self_verification_failure("emission_reparsed", &verdict),
558            );
559            return None;
560        }
561    };
562    drop(imported);
563    result
564        .information_losses
565        .extend(document.losses.iter().map(|(category, detail)| Loss {
566            category: category.clone(),
567            detail: detail.clone(),
568        }));
569    let reference = match reference::reference_declaration(export, &kernel_target) {
570        Ok(reference) => reference,
571        Err(verdict) => {
572            result.mark(
573                "emission_reparsed",
574                status_of(&verdict),
575                self_verification_failure("emission_reparsed", &verdict),
576            );
577            return None;
578        }
579    };
580    if let Err(fault) = emit::check_statement(&document, &reference) {
581        result.fail(
582            "emission_reparsed",
583            Diagnostic::new(
584                "emission_reparsed",
585                DiagnosticCode::InternalInconsistency,
586                format!("the emitted statement of {target} does not match the reference translation: {fault}"),
587            )
588            .with_declaration(target),
589        );
590        return None;
591    }
592    result.target_logos = Some(document.target.clone());
593    result.pass(
594        "emission_reparsed",
595        "the LOGOS document reparsed in a fresh context to the checked declarations, and its statement is the reference translation's",
596    );
597
598    // A package is built only for a result that can be verified: without Lean's acceptance observed
599    // it could never be published, and replaying it would decide nothing.
600    if result.status("lean_accepted") != StageStatus::Passed {
601        return None;
602    }
603    match package::publishable(build) {
604        Ok(files) => Some(files),
605        Err(verdict) => {
606            result.mark(
607                "fresh_replay",
608                status_of(&verdict),
609                self_verification_failure("fresh_replay", &verdict),
610            );
611            None
612        }
613    }
614}
615
616/// A refusal of LOGOS's own artifact — emission, packaging, replay — once every check of the user's
617/// input passed. Unsupported capabilities, budgets and environment failures keep their codes; any
618/// other refusal (a rejection, a malformed or ill-typed artifact of our own making) is an
619/// [`InternalInconsistency`](DiagnosticCode::InternalInconsistency): the fault is ours, and it is never
620/// reported as the user's mathematics being wrong.
621pub fn self_verification_failure(stage: &'static str, verdict: &Verdict) -> Diagnostic {
622    let diagnostic = Diagnostic::of_refusal(stage, verdict);
623    match verdict.outcome() {
624        Outcome::UnsupportedFeature | Outcome::ResourceLimit | Outcome::InfrastructureFailure => {
625            diagnostic
626        }
627        _ => Diagnostic {
628            message: format!(
629                "LOGOS's own {stage} artifact failed self-verification ({}): {}",
630                diagnostic.code, diagnostic.message
631            ),
632            ..Diagnostic::new(stage, DiagnosticCode::InternalInconsistency, "")
633        },
634    }
635}
636
637/// A capability that declined is `unsupported`; anything that refused is `failed`.
638fn status_of(verdict: &Verdict) -> StageStatus {
639    match verdict {
640        Verdict::Decline(_) if verdict.outcome() == Outcome::UnsupportedFeature => {
641            StageStatus::Unsupported
642        }
643        _ => StageStatus::Failed,
644    }
645}
646
647fn losses(report: &ImportReport) -> Vec<Loss> {
648    report
649        .metadata_losses
650        .iter()
651        .map(|loss| Loss {
652            category: "SOURCE_METADATA".into(),
653            detail: format!(
654                "expression {}: {} = {}",
655                loss.expression, loss.key, loss.value
656            ),
657        })
658        .collect()
659}
660
661/// The Lean Kernel Arena benchmark protocol: one input path, `ACCEPT` on stdout and exit 0 on
662/// acceptance, exit 1 on rejection, exit 2 on decline. Kept byte-for-byte for benchmark consumers.
663pub fn run_cli(
664    arguments: impl IntoIterator<Item = std::ffi::OsString>,
665    stdout: &mut dyn std::io::Write,
666    stderr: &mut (dyn std::io::Write + Send),
667) -> i32 {
668    use super::{check_import, check_import_with_trace, declined};
669    let mut path = None;
670    let mut trace = false;
671    let mut audit_declarations = false;
672    let options = (|| {
673        for argument in arguments {
674            if argument == "--trace-stages" {
675                trace = true;
676            } else if argument == "--audit-declarations" {
677                audit_declarations = true;
678            } else if path.is_none() {
679                path = Some(std::path::PathBuf::from(argument));
680            } else {
681                return Err(declined(DiagnosticCode::Usage, "expected one input path"));
682            }
683        }
684        path.ok_or_else(|| declined(DiagnosticCode::Usage, "expected input path"))
685    })();
686    let input = options.and_then(|p| {
687        std::fs::read_to_string(p)
688            .map_err(|e| declined(DiagnosticCode::Infrastructure, e.to_string()))
689    });
690    let result = if trace {
691        let writer = std::sync::Mutex::new(&mut *stderr);
692        let emit = |event: &Value| {
693            if let Ok(mut writer) = writer.lock() {
694                let _ = serde_json::to_writer(&mut **writer, event);
695                let _ = writer.write_all(b"\n");
696                let _ = writer.flush();
697            }
698        };
699        let result = input
700            .and_then(|s| check_import_with_trace(&s, audit_declarations, Some(&emit)).map(|_| ()));
701        let code = result.as_ref().err().map_or(0, Verdict::code);
702        emit(&json!({"schema":"logos-lean-stages/1","event":"verdict",
703            "code":code,"outcome":match code {0=>"accept",1=>"reject",_=>"decline"}}));
704        result
705    } else {
706        input.and_then(|s| check_import(&s, audit_declarations).map(|_| ()))
707    };
708    match result {
709        Ok(()) => {
710            let _ = writeln!(stdout, "ACCEPT");
711            0
712        }
713        Err(error) => {
714            if !trace {
715                let _ = writeln!(stderr, "{error:?}");
716            }
717            error.code()
718        }
719    }
720}
721
722#[cfg(test)]
723#[path = "../../../../logicaffeine_tests/unit/logicaffeine_kernel/interface/lean/pipeline/native_controls.rs"]
724mod native_controls;
logicaffeine_kernel/interface/lean/pipeline.rs

logicaffeine_kernel/interface/lean/
pipeline.rs
