vyre-conform 0.1.0

Conformance suite for vyre backends — proves byte-identical output to CPU reference
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

use std::process;
use super::vyre_conform::proof::algebra::formal::smt;

fn run(args: Vec<String>) -> Result<String, String> {
    match args.as_slice() {
        [] => Err("Fix: missing subcommand. Use `dump --format=smt`.".to_string()),
        [command] if command == "--help" || command == "-h" => Ok(help()),
        [command, flag] if command == "dump" && flag == "--format=smt" => smt::dump_smt()
            .map_err(|error| format!("Fix: failed to load formal algebraic-law specs: {error}")),
        [command, flag, value] if command == "dump" && flag == "--format" && value == "smt" => {
            smt::dump_smt()
                .map_err(|error| format!("Fix: failed to load formal algebraic-law specs: {error}"))
        }
        [command, ..] if command == "dump" => {
            Err("Fix: unsupported dump format. Use `dump --format=smt`.".to_string())
        }
        [command, ..] => Err(format!(
            "Fix: unknown subcommand `{command}`. Use `dump --format=smt`."
        )),
    }
}