diff --git a/.github/workflows/arb.yml b/.github/workflows/arb.yml index e7487423..7a3daf2f 100644 --- a/.github/workflows/arb.yml +++ b/.github/workflows/arb.yml @@ -43,6 +43,13 @@ jobs: python3 proof/region/v1/arb/tests/gate.py PYTHONOPTIMIZE=2 python3 proof/region/v1/arb/tests/gate.py + - name: complete fast MPFI source contract with exact inventory + shell: bash + run: | + set -euo pipefail + python3 proof/region/v1/mpfi/tests/gate.py + PYTHONOPTIMIZE=2 python3 proof/region/v1/mpfi/tests/gate.py + - name: bind run-local native paths after the fast gate shell: bash run: | diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 25ccc292..3cc9b571 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -237,6 +237,9 @@ jobs: python -c '\''import unittest; suite = unittest.defaultTestLoader.discover("proof/region/v1/tests", pattern="test_*.py"); count = suite.countTestCases(); minimum = 25; assert count >= minimum, f"region-proof anti-vacuum floor failed: {count} < {minimum}"; print(f"region-proof discovered tests: {count}")'\'' python -m unittest discover -s proof/region/v1/tests -p "test_*.py" -v PYTHONOPTIMIZE=2 python -m unittest discover -s proof/region/v1/tests -p "test_*.py" -v + test -f proof/region/v1/mpfi/tests/gate.py + python proof/region/v1/mpfi/tests/gate.py + PYTHONOPTIMIZE=2 python proof/region/v1/mpfi/tests/gate.py python proof/region/v1/controller.py verify-fixtures --repo-root /workspace ' - name: toolchain env (runner.temp) diff --git a/proof/region/v1/PROTOCOL.md b/proof/region/v1/PROTOCOL.md index 58136184..f8b8c83b 100644 --- a/proof/region/v1/PROTOCOL.md +++ b/proof/region/v1/PROTOCOL.md @@ -13,8 +13,9 @@ Arb-enclosures и выпускает связанные transcript bytes; `SourceBoundArbControllerV1` заново собирает evaluator, запускает его и создаёт только provenance receipt. Ни один из этих путей не выполняет независимый semantic replay и не создаёт mathematical proof type. MPFI source lock, -archive admission и sealed source input (не evaluator replay) уже представлены, но MPFI -evaluator/source-bound receipt и semantic verifier в текущем release +archive admission и sealed source input (не evaluator replay) уже представлены. +`mpfi/evaluator` теперь содержит отдельный source-owned M1.5 build/run path; +MPFI source-bound receipt и semantic verifier в текущем release всё ещё отсутствуют. Structural protocol/admission сам не является математическим proof. @@ -29,9 +30,9 @@ evidence. В тесте протокола такое значение явно Протокол не входит в Cargo workspace, Core, WASM, FFI, bindings или packages. Текущий `SourceBoundEvaluatorReceiptV1` подтверждает причинную цепь только Arb. -MPFI source closure ещё не является provenance исполнения: MPFI source-bound +MPFI evaluator output ещё не является provenance исполнения: MPFI source-bound receipt, cross-path dependency overlap и diversity не представлены admitted -типом; structural coordinates не восполняют это отсутствие. +типом; structural coordinates и локальная сборка этого не восполняют. ## Бинарный формат и идентичность @@ -156,6 +157,19 @@ Arb controller связывает его с наблюдёнными BUILD/RUN границы доверия; receipt не заявляет отсутствие ambient inputs за пределами этой границы. Альтернативный JSON/TOML definition запрещён протоколом. +### MPFI runtime profile V1 + +Wire grammar сама не превращается в неограниченный allocator. Прямой M1.5 +executable принимает только профиль `LC-MPFI-RUNTIME-V1`: stdin job не более +16 MiB, не более 4096 bits на precision rung, не более 32 rung-ов, не более +1024 contextual knots и не более 16 MiB transcript output. Это operational +admission profile, а не математический предел definition/domain: лимиты job, +precision, rung-ов и knots возвращают typed `resource_limit` до MPFI +allocation, а переполнение transcript — typed `output_limit`. M2a обязан +связать тот же профиль с immutable executor limits и включить его в +source-bound BUILD/RUN evidence; прямой бинарь до этого не является +самостоятельным public evaluator API. + ## Фиксация источников и наблюдения целостности `SourceReleaseLockV1` фиксирует bytes и структурный состав архива. Поле @@ -310,9 +324,10 @@ session или сбой `TemporaryDirectory`), может вернуть `BuildR `session` и `completed_processes`. Transport не знает formula, ELF, comparator или source provenance: engine lane отдельно перепроверяет свой engine-owned input binding перед -каждым process и передаёт output admission. MPFI sealed source input ещё не -является MPFI build policy; будущая policy должна быть объявлена отдельно и не -может заимствовать Arb semantics. +каждым process и передаёт output admission. MPFI sealed source input сам по себе +не является MPFI build policy; `mpfi/build.sh` теперь объявляет source-owned +recipe, но его BUILD/RUN observation и receipt ещё не admitted. Recipe не +заимствует Arb semantics. ## Воспроизведение Arb, связанное с источником diff --git a/proof/region/v1/mpfi/build-inner.sh b/proof/region/v1/mpfi/build-inner.sh new file mode 100644 index 00000000..97c64b24 --- /dev/null +++ b/proof/region/v1/mpfi/build-inner.sh @@ -0,0 +1,221 @@ +#!/bin/sh +# Internal MPFI recipe. The source-bound transport dispatches this file only +# after establishing its clean child environment; it is not a standalone API. +set -eu + +if [ "$#" -ne 0 ]; then + printf '%s\n' 'mpfi build takes no arguments' >&2 + exit 64 +fi + +umask 022 + +readonly inputs=/build/snapshot/inputs +readonly workspace=/build/snapshot/workspace +readonly build=/build/work +readonly compiler=/usr/bin/clang-19 +readonly common_cflags='-O2 -g0 -fno-ident -fno-fast-math -ffp-contract=off -fno-lto -std=gnu17 -march=x86-64 -mtune=generic -ffile-prefix-map=/build=. -fdebug-prefix-map=/build=.' +readonly evaluator_cflags='-O2 -g0 -fno-fast-math -ffp-contract=off -fno-lto -march=x86-64 -mtune=generic -ffile-prefix-map=/build=. -fdebug-prefix-map=/build=. -std=c17 -Wall -Wextra -Werror -pedantic' +readonly prefix="$build/prefix" +readonly evaluator_sources='main.c wire.c hash.c interval.c region.c' +readonly mpfi_test_exclusions='^(tdiv_ext|texp10|trec_sqrt)$' + +require_regular() { + if [ ! -f "$1" ] || [ -L "$1" ]; then + printf 'missing regular build input: %s\n' "$1" >&2 + exit 66 + fi +} + +require_executable() { + if [ ! -f "$1" ] || [ ! -x "$1" ]; then + printf 'missing executable build tool: %s\n' "$1" >&2 + exit 66 + fi +} + +require_clang_19() { + version=$("$1" --version) || { + printf '%s\n' 'cannot inspect the admitted Clang compiler' >&2 + exit 67 + } + if ! printf '%s\n' "$version" | /usr/bin/grep -q 'clang version 19\.'; then + printf '%s\n' 'MPFI build requires the admitted Clang 19 compiler family' >&2 + exit 67 + fi +} + +require_directory() { + if [ ! -d "$1" ] || [ -L "$1" ]; then + printf 'missing normalized source directory: %s\n' "$1" >&2 + exit 66 + fi +} + +require_empty_directory() { + if [ ! -d "$1" ] || [ -L "$1" ]; then + printf 'missing build directory: %s\n' "$1" >&2 + exit 66 + fi + if [ -n "$(find "$1" -mindepth 1 -maxdepth 1 -print -quit)" ]; then + printf 'build directory is not empty: %s\n' "$1" >&2 + exit 65 + fi +} + +require_absent_pattern() { + pattern=$1 + path=$2 + message=$3 + inspection_error=$4 + if /usr/bin/grep -q "$pattern" "$path"; then + printf '%s\n' "$message" >&2 + exit 70 + else + grep_status=$? + if [ "$grep_status" -ne 1 ]; then + printf '%s\n' "$inspection_error" >&2 + exit 70 + fi + fi +} + +require_regular "$inputs/formula.generated.c" +require_directory "$inputs/sources/gmp" +require_directory "$inputs/sources/mpfr" +require_directory "$inputs/sources/mpfi" +require_regular "$workspace/proof/region/v1/mpfi/operations.py" +for source in main.c wire.c hash.c interval.c region.c; do + require_regular "$workspace/proof/region/v1/mpfi/evaluator/$source" +done +for header in wire.h hash.h interval.h region.h formula.h; do + require_regular "$workspace/proof/region/v1/mpfi/evaluator/$header" +done +printf '%s %s\n' \ + 'a8df7529261ba68e8fbf591cff283ec88a35cb98958b293bc7885d9fb4dd0fb6' \ + "$inputs/formula.generated.c" \ + | /usr/bin/sha256sum --check --strict - +/usr/bin/python3 "$workspace/proof/region/v1/mpfi/operations.py" \ + "$workspace/proof/region/v1/mpfi/evaluator" +require_executable "$compiler" +require_clang_19 "$compiler" +require_empty_directory "$build" + +/usr/bin/mkdir "$build/prefix" "$build/gmp" "$build/mpfr" "$build/mpfi" "$build/tmp" + +cd "$build/gmp" +ABI=64 CC="$compiler" CFLAGS="$common_cflags" \ + "$inputs/sources/gmp/configure" \ + --build=x86_64-pc-linux-gnu \ + --host=x86_64-pc-linux-gnu \ + --prefix="$prefix" \ + --disable-shared \ + --enable-static \ + --disable-assembly \ + --disable-cxx +/usr/bin/make -j1 +/usr/bin/make check -j1 +/usr/bin/make install + +cd "$build/mpfr" +CC="$compiler" CFLAGS="$common_cflags" \ + "$inputs/sources/mpfr/configure" \ + --build=x86_64-pc-linux-gnu \ + --host=x86_64-pc-linux-gnu \ + --prefix="$prefix" \ + --with-gmp="$prefix" \ + --disable-shared \ + --enable-static \ + --enable-formally-proven-code +/usr/bin/make -j1 +/usr/bin/make check -j1 +/usr/bin/make install + +cd "$build/mpfi" +CC="$compiler" CFLAGS="$common_cflags" \ + "$inputs/sources/mpfi/configure" \ + --build=x86_64-pc-linux-gnu \ + --host=x86_64-pc-linux-gnu \ + --prefix="$prefix" \ + --with-gmp="$prefix" \ + --with-mpfr="$prefix" \ + --disable-shared \ + --enable-static +/usr/bin/make -j1 +# MPFI 1.5.4 ships three non-runnable tests: two pass incompatible function +# pointers to the generic harness, while texp10 names a fixture absent from +# the sealed source archive. Exclude only those upstream defects; every other +# shipped test remains part of this source-bound library check. +make_database="$build/mpfi-check-database" +if ! /usr/bin/make -pn > "$make_database"; then + printf '%s\n' 'cannot inspect MPFI upstream test inventory' >&2 + exit 70 +fi +mpfi_tests=$( + /usr/bin/awk -v exclusions="$mpfi_test_exclusions" ' + /^check_PROGRAMS =/ && !found { + found = 1 + for (i = 3; i <= NF; i++) { + gsub(/\$\(EXEEXT\)/, "", $i) + if ($i !~ exclusions) + printf "%s ", $i + } + } + ' "$make_database" +) +if [ -z "$mpfi_tests" ]; then + printf '%s\n' 'MPFI upstream test inventory is empty after exclusions' >&2 + exit 70 +fi +/usr/bin/make check -j1 TESTS="$mpfi_tests" CFLAGS="$common_cflags" +/usr/bin/make install + +cd "$workspace/proof/region/v1/mpfi/evaluator" +for source in $evaluator_sources; do + object="$build/${source%.c}.o" + # shellcheck disable=SC2086 + "$compiler" $evaluator_cflags \ + -I. -I"$prefix/include" \ + -c "$source" \ + -o "$object" +done +# shellcheck disable=SC2086 +"$compiler" $evaluator_cflags \ + -I. -I"$prefix/include" \ + -c "$inputs/formula.generated.c" \ + -o "$build/formula.generated.o" +if ! /usr/bin/nm --undefined-only "$build"/*.o > "$build/evaluator-undefined-symbols"; then + printf '%s\n' 'cannot inspect evaluator undefined symbols' >&2 + exit 70 +fi +/usr/bin/python3 "$workspace/proof/region/v1/mpfi/operations.py" \ + --undefined-symbols "$build/evaluator-undefined-symbols" +# shellcheck disable=SC2086 +"$compiler" $evaluator_cflags \ + "$build/main.o" "$build/wire.o" "$build/hash.o" "$build/interval.o" \ + "$build/region.o" "$build/formula.generated.o" \ + -static -Wl,--build-id=none -fno-lto \ + "$prefix/lib/libmpfi.a" "$prefix/lib/libmpfr.a" "$prefix/lib/libgmp.a" \ + -lm -lpthread \ + -o "$build/mpfi-evaluator-v1" + +if ! /usr/bin/readelf -l "$build/mpfi-evaluator-v1" > "$build/program-headers"; then + printf '%s\n' 'cannot inspect evaluator program headers' >&2 + exit 70 +fi +require_absent_pattern \ + INTERP \ + "$build/program-headers" \ + 'evaluator unexpectedly contains PT_INTERP' \ + 'cannot inspect evaluator program headers' +if ! /usr/bin/readelf -d "$build/mpfi-evaluator-v1" > "$build/dynamic-section"; then + printf '%s\n' 'cannot inspect evaluator dynamic section' >&2 + exit 70 +fi +require_absent_pattern \ + NEEDED \ + "$build/dynamic-section" \ + 'evaluator unexpectedly contains DT_NEEDED' \ + 'cannot inspect evaluator dynamic section' + +/usr/bin/sha256sum "$build/mpfi-evaluator-v1" diff --git a/proof/region/v1/mpfi/build.sh b/proof/region/v1/mpfi/build.sh new file mode 100755 index 00000000..3c8e59ce --- /dev/null +++ b/proof/region/v1/mpfi/build.sh @@ -0,0 +1,33 @@ +#!/bin/sh +# Source-owned MPFI dispatcher. The trusted Docker/CI transport invokes this +# file from the fixed bundle path with a clean environment. Keep the outer +# shell limited to builtins: path resolution must happen only in the clean child. +# shellcheck disable=SC2016 +set -eu + +if [ "$#" -ne 0 ]; then + printf '%s\n' 'mpfi build takes no arguments' >&2 + exit 64 +fi + +exec /usr/bin/env -i \ + PATH=/usr/bin:/bin \ + LC_ALL=C \ + LANG=C \ + TZ=UTC \ + HOME=/nonexistent \ + TMPDIR=/build/work/tmp \ + SOURCE_DATE_EPOCH=0 \ + ZERO_AR_DATE=1 \ + ARFLAGS=crD \ + /bin/sh -c ' + set -eu + script_path=$(/usr/bin/readlink -f -- "$1") + script_dir=$(/usr/bin/dirname -- "$script_path") + inner="$script_dir/build-inner.sh" + if [ ! -f "$inner" ] || [ -L "$inner" ]; then + printf "%s\\n" "missing regular MPFI inner build recipe" >&2 + exit 66 + fi + exec /bin/sh "$inner" + ' /bin/sh "$0" diff --git a/proof/region/v1/mpfi/evaluator/formula.h b/proof/region/v1/mpfi/evaluator/formula.h new file mode 100644 index 00000000..87926a78 --- /dev/null +++ b/proof/region/v1/mpfi/evaluator/formula.h @@ -0,0 +1,19 @@ +#ifndef LABCOLOR_MPFI_FORMULA_H +#define LABCOLOR_MPFI_FORMULA_H + +#include + +#include + +#include "interval.h" + +lc_mpfi_status lc_mpfi_formula_point( + mpfi_ptr output, + const uint8_t rgb[3], + mpfi_srcptr context, + uint8_t surround +); +lc_mpfi_status lc_mpfi_formula_segment(mpfi_ptr output, mpfi_srcptr input); +lc_mpfi_status lc_mpfi_formula_singleton(mpfi_ptr output, mpfi_srcptr input); + +#endif diff --git a/proof/region/v1/mpfi/evaluator/formula.py b/proof/region/v1/mpfi/evaluator/formula.py new file mode 100755 index 00000000..7344cf4f --- /dev/null +++ b/proof/region/v1/mpfi/evaluator/formula.py @@ -0,0 +1,348 @@ +#!/usr/bin/env python3 +"""Generate the MPFI evaluator from the registered exact-real SSA. + +This is a separate parser and emitter from the Arb implementation. The two +engines intentionally consume the same immutable mathematical contract while +owning different C types, adapters and source identities. +""" + +from __future__ import annotations + +import hashlib +import sys +from dataclasses import dataclass +from pathlib import Path + + +SOURCE_SHA256 = "a6f77ac462f226453b1c27bbd8637b62780b9a640c317a6f50028dacd1de8540" +RELEASE_DOMAIN = b"labcolors.nominal-exact-real-lift.ascii-ssa.v1\0" +RELEASE_SHA256 = "2c626d8ee60eeb62ae4db53660d61bbc25e0efd4e557f0dc1e77565c130b6e52" + +_UNARY = frozenset(("root3", "sqrt", "exp", "log", "sin", "cos", "abs", "sign")) +_BINARY = frozenset(("add", "sub", "mul", "div", "min", "max", "pow_pos", "pow_nn", "ratio0")) +_EXPECTED = { + "point": ( + (("r8", "u8"), ("g8", "u8"), ("b8", "u8"), + ("adapting_luminance", "real"), ("background_ratio", "real"), + ("surround", "surround_profile")), + 226, + ("jp", "ap", "bp"), + 39, + ), + "segment": (tuple((name, "real") for name in ( + "segment_t", "segment_a", "segment_b", "segment_t0", "segment_t1", + "segment_c0a", "segment_c0b", "segment_c1a", "segment_c1b", + "segment_rho0", "segment_rho1", "segment_g00", "segment_g01", "segment_g11", + )), 27, ("segment_f",), 0), + "singleton": (tuple((name, "real") for name in ( + "singleton_a", "singleton_b", "singleton_ca", "singleton_cb", + "singleton_rho", "singleton_g00", "singleton_g01", "singleton_g11", + )), 12, ("singleton_f",), 0), +} + + +class FormulaError(ValueError): + pass + + +@dataclass(frozen=True) +class Node: + name: str + result: str + operator: str + arguments: tuple[str, ...] + + +@dataclass(frozen=True) +class Program: + name: str + inputs: tuple[tuple[str, str], ...] + nodes: tuple[Node, ...] + outputs: tuple[str, ...] + + +@dataclass(frozen=True) +class Formula: + decode: tuple[int, ...] + literals: tuple[tuple[str, int], ...] + programs: tuple[Program, ...] + + +class Cursor: + def __init__(self, lines: tuple[str, ...]): + self.lines = lines + self.index = 0 + + def take(self) -> str: + if self.index >= len(self.lines): + raise FormulaError(f"unexpected end at line {self.index + 1}") + value = self.lines[self.index] + self.index += 1 + return value + + def expect(self, value: str) -> None: + actual = self.take() + if actual != value: + raise FormulaError(f"expected {value!r}, got {actual!r}") + + +def _record(line: str, count: int) -> tuple[str, ...]: + values = tuple(line.split(" ")) + if len(values) != count: + raise FormulaError(f"record arity {len(values)} != {count}") + return values + + +def _bits(value: str) -> int: + if len(value) != 16 or any(ch not in "0123456789abcdef" for ch in value): + raise FormulaError("noncanonical binary64 payload") + bits = int(value, 16) + if bits & 0x7FF0000000000000 == 0x7FF0000000000000: + raise FormulaError("nonfinite binary64 payload") + if bits == 0x8000000000000000: + raise FormulaError("negative zero") + return bits + + +def _node_type_check(node: Node, symbols: dict[str, str]) -> None: + try: + argument_types = tuple(symbols[name] for name in node.arguments) + except KeyError as error: + raise FormulaError(f"unknown or forward reference {error.args[0]}") from None + if node.operator == "lookup": + valid = node.result == "real" and argument_types == ("decode_table", "u8") + elif node.operator == "eq": + valid = node.result == "bool" and len(argument_types) == 2 and argument_types[0] == argument_types[1] == "surround_profile" + elif node.operator == "select": + valid = len(argument_types) == 3 and argument_types[0] == "bool" and argument_types[1] == argument_types[2] == node.result == "real" + elif node.operator in _UNARY: + valid = node.result == "real" and argument_types == ("real",) + elif node.operator in _BINARY: + valid = node.result == "real" and argument_types == ("real", "real") + else: + valid = False + if not valid: + raise FormulaError(f"operator/type mismatch for {node.name}") + + +def _program(cursor: Cursor, name: str, globals_: dict[str, str]) -> Program: + expected_inputs, expected_nodes, expected_outputs, checkpoints = _EXPECTED[name] + cursor.expect(f"{name}_inputs {len(expected_inputs)}") + symbols = dict(globals_) + inputs: list[tuple[str, str]] = [] + for expected in expected_inputs: + record = _record(cursor.take(), 3) + if record != ("input", *expected) or record[1] in symbols: + raise FormulaError(f"foreign {name} input") + symbols[record[1]] = record[2] + inputs.append((record[1], record[2])) + cursor.expect(f"{name}_nodes {expected_nodes}") + nodes: list[Node] = [] + for _ in range(expected_nodes): + record = tuple(cursor.take().split(" ")) + if len(record) < 5 or record[0] != "node" or not record[1].islower(): + raise FormulaError("invalid node") + node = Node(record[1], record[2], record[3], record[4:]) + _node_type_check(node, symbols) + if node.name in symbols: + raise FormulaError("shadowed node") + symbols[node.name] = node.result + nodes.append(node) + if checkpoints: + cursor.expect(f"{name}_checkpoints {checkpoints}") + for _ in range(checkpoints): + checkpoint = _record(cursor.take(), 3) + if checkpoint[0] != "checkpoint" or checkpoint[2] not in {node.name for node in nodes}: + raise FormulaError("invalid checkpoint") + cursor.expect(f"{name}_outputs {len(expected_outputs)}") + outputs: list[str] = [] + for expected in expected_outputs: + record = _record(cursor.take(), 3) + if record != ("output", expected, "real") or symbols.get(expected) != "real": + raise FormulaError(f"foreign {name} output") + outputs.append(expected) + return Program(name, tuple(inputs), tuple(nodes), tuple(outputs)) + + +def parse(source: bytes) -> Formula: + if hashlib.sha256(source).hexdigest() != SOURCE_SHA256: + raise FormulaError("formula source is not the registered V1 content") + release = hashlib.sha256(RELEASE_DOMAIN + len(source).to_bytes(8, "big") + source).hexdigest() + if release != RELEASE_SHA256: + raise FormulaError("formula release mismatch") + if not source.isascii() or not source.endswith(b"\n") or source.endswith(b"\n\n"): + raise FormulaError("formula is not canonical ASCII with one final LF") + lines = tuple(source.decode("ascii")[:-1].split("\n")) + if any(not line or line.startswith(" ") or line.endswith(" ") or " " in line or "\t" in line or "\r" in line or "#" in line for line in lines): + raise FormulaError("formula contains a noncanonical line") + cursor = Cursor(lines) + cursor.expect("labcolors_exact_real_ssa 1") + cursor.expect("arithmetic exact_real_v1") + cursor.expect("types 4") + for declaration in ("type u8 unsigned_integer_0_255", "type real mathematical_real", "type bool exact_boolean", "type surround_profile closed_enum"): + cursor.expect(declaration) + cursor.expect("operators 20") + operators = tuple(cursor.take() for _ in range(20)) + if operators != ( + "operator lookup 2 real table_u8_exact_dyadic_at_ordinal", + "operator eq 2 bool exact_same_type_equality", + "operator select 3 same bool_true_second_else_third", + "operator add 2 real exact_x_plus_y", + "operator sub 2 real exact_x_minus_y", + "operator mul 2 real exact_x_times_y", + "operator div 2 real domain_y_ne_zero_x_div_y_else_domain_unproven", + "operator min 2 real exact_lesser_real", + "operator max 2 real exact_greater_real", + "operator root3 1 real domain_x_ge_zero_unique_y_ge_zero_y_cubed_eq_x_else_domain_unproven", + "operator sqrt 1 real domain_x_ge_zero_unique_y_ge_zero_y_squared_eq_x_else_domain_unproven", + "operator exp 1 real analytic_natural_exponential", + "operator log 1 real domain_x_gt_zero_analytic_natural_logarithm_else_domain_unproven", + "operator sin 1 real analytic_sine_radians", + "operator cos 1 real analytic_cosine_radians", + "operator abs 1 real exact_absolute_value", + "operator sign 1 real negative_minus_one_zero_zero_positive_one", + "operator pow_pos 2 real domain_x_gt_zero_exp_y_mul_log_x_else_domain_unproven", + "operator pow_nn 2 real if_x_eq_zero_and_y_gt_zero_zero_else_pow_pos", + "operator ratio0 2 real if_x_eq_zero_and_y_eq_zero_zero_else_domain_y_gt_zero_x_div_y", + ): + raise FormulaError("operator contract drift") + cursor.expect("decode_table decode_srgb8 256") + decode: list[int] = [] + for ordinal in range(256): + record = _record(cursor.take(), 3) + if record[:2] != ("decode", f"{ordinal:02x}"): + raise FormulaError("decode order drift") + decode.append(_bits(record[2])) + cursor.expect("literals 56") + literals: list[tuple[str, int]] = [] + names: set[str] = set() + values: set[int] = set() + for _ in range(56): + record = _record(cursor.take(), 3) + bits = _bits(record[2]) + if record[0] != "literal" or not record[1].islower() or record[1] in names or bits in values: + raise FormulaError("invalid literal") + names.add(record[1]) + values.add(bits) + literals.append((record[1], bits)) + cursor.expect("enum_type surround_profile 3") + enums = (("surround_average", 1), ("surround_dim", 2), ("surround_dark", 3)) + for name, tag in enums: + if _record(cursor.take(), 4) != ("enum", "surround_profile", name, f"{tag:02x}"): + raise FormulaError("surround enum drift") + globals_ = {"decode_srgb8": "decode_table"} + globals_.update({name: "real" for name, _ in literals}) + globals_.update({name: "surround_profile" for name, _ in enums}) + programs = tuple(_program(cursor, name, globals_) for name in ("point", "segment", "singleton")) + cursor.expect("driver 6") + for rule in ("rule tone_domain closed_first_last", "rule out_of_tone_domain outside", "rule one_knot_tone exact_equality_required", "rule one_knot_predicate singleton_f_le_zero", "rule multi_knot_predicate piecewise_linear_segment_f_le_zero", "rule boundary inclusive"): + cursor.expect(rule) + cursor.expect("end") + if cursor.index != len(lines): + raise FormulaError("trailing records") + return Formula(tuple(decode), tuple(literals), programs) + + +def _real_expr(name: str, slots: dict[str, int]) -> str: + return f"real + {slots[name]}" + + +def _emit_program(formula: Formula, program: Program) -> list[str]: + slots: dict[str, int] = {name: index for index, (name, _bits_value) in enumerate(formula.literals)} + surround = {"surround_average": "1", "surround_dim": "2", "surround_dark": "3"} + booleans: dict[str, str] = {} + for name, kind in program.inputs: + if kind == "real": + slots[name] = len(slots) + elif kind == "surround_profile": + surround[name] = "surround" + for node in program.nodes: + if node.result == "real": + slots[node.name] = len(slots) + else: + booleans[node.name] = f"condition_{len(booleans)}" + signatures = { + "point": "lc_mpfi_status lc_mpfi_formula_point(mpfi_ptr output, const uint8_t rgb[3], mpfi_srcptr context, uint8_t surround)", + "segment": "lc_mpfi_status lc_mpfi_formula_segment(mpfi_ptr output, mpfi_srcptr input)", + "singleton": "lc_mpfi_status lc_mpfi_formula_singleton(mpfi_ptr output, mpfi_srcptr input)", + } + lines = [signatures[program.name], "{", " lc_mpfi_status status = LC_MPFI_OK;", f" __mpfi_struct real[{len(slots)}];"] + lines.extend(f" mpfi_init2(real + {index}, mpfi_get_prec(output));" for index in range(len(slots))) + for name, bits in formula.literals: + lines.append(f" status = lc_mpfi_set_dyadic_bits(real + {slots[name]}, UINT64_C(0x{bits:016x}));") + lines.append(" if (status != LC_MPFI_OK) goto cleanup;") + real_cursor = 0 + u8_cursor = 0 + u8_values: dict[str, str] = {} + for name, kind in program.inputs: + if kind == "real": + source = "context" if program.name == "point" else "input" + lines.append(f" mpfi_set(real + {slots[name]}, {source} + {real_cursor});") + real_cursor += 1 + elif kind == "u8": + u8_values[name] = f"rgb[{u8_cursor}]" + u8_cursor += 1 + adapters = { + "add": "lc_mpfi_add", "sub": "lc_mpfi_sub", "mul": "lc_mpfi_mul", "div": "lc_mpfi_div", + "min": "lc_mpfi_min", "max": "lc_mpfi_max", "root3": "lc_mpfi_root3", "sqrt": "lc_mpfi_sqrt", + "exp": "lc_mpfi_exp", "log": "lc_mpfi_log", "sin": "lc_mpfi_sin", "cos": "lc_mpfi_cos", + "abs": "lc_mpfi_abs", "sign": "lc_mpfi_sign", "pow_pos": "lc_mpfi_pow_pos", + "pow_nn": "lc_mpfi_pow_nn", "ratio0": "lc_mpfi_ratio0", + } + for node in program.nodes: + target = _real_expr(node.name, slots) if node.result == "real" else "" + if node.operator == "lookup": + lines.append(f" status = lc_mpfi_set_dyadic_bits({target}, LC_MPFI_DECODE_BITS[(size_t){u8_values[node.arguments[1]]}]);") + lines.append(" if (status != LC_MPFI_OK) goto cleanup;") + elif node.operator == "eq": + lines.append(f" int {booleans[node.name]} = ({surround[node.arguments[0]]} == {surround[node.arguments[1]]});") + elif node.operator == "select": + condition = booleans[node.arguments[0]] + lines.append(f" mpfi_set({target}, {condition} ? {_real_expr(node.arguments[1], slots)} : {_real_expr(node.arguments[2], slots)});") + else: + arguments = ", ".join(_real_expr(argument, slots) for argument in node.arguments) + lines.append(f" status = {adapters[node.operator]}({target}, {arguments});") + lines.append(" if (status != LC_MPFI_OK) goto cleanup;") + for index, name in enumerate(program.outputs): + destination = f"output + {index}" if len(program.outputs) > 1 else "output" + lines.append(f" mpfi_set({destination}, {_real_expr(name, slots)});") + lines.append("cleanup:") + lines.extend(f" mpfi_clear(real + {index});" for index in range(len(slots) - 1, -1, -1)) + lines.extend((" return status;", "}", "")) + return lines + + +def emit(formula: Formula) -> bytes: + lines = [ + "/* Generated from the registered exact-real SSA; do not edit. */", + "#include ", + "#include ", + "#include \"formula.h\"", + "", + "static const uint64_t LC_MPFI_DECODE_BITS[256] = {", + ] + for index in range(0, 256, 4): + values = ", ".join(f"UINT64_C(0x{value:016x})" for value in formula.decode[index : index + 4]) + lines.append(f" {values},") + lines.append("};") + lines.append("") + for program in formula.programs: + lines.extend(_emit_program(formula, program)) + return ("\n".join(lines) + "\n").encode("ascii") + + +def main(argv: list[str]) -> int: + if len(argv) != 2: + print("usage: formula.py FORMULA", file=sys.stderr) + return 2 + try: + output = emit(parse(Path(argv[1]).read_bytes())) + except (OSError, FormulaError) as error: + print(f"formula rejected: {error}", file=sys.stderr) + return 1 + sys.stdout.buffer.write(output) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main(sys.argv)) diff --git a/proof/region/v1/mpfi/evaluator/hash.c b/proof/region/v1/mpfi/evaluator/hash.c new file mode 100644 index 00000000..b902bd9a --- /dev/null +++ b/proof/region/v1/mpfi/evaluator/hash.c @@ -0,0 +1,169 @@ +#include "hash.h" + +#include + +static const uint32_t constants[64] = { + UINT32_C(0x428a2f98), UINT32_C(0x71374491), UINT32_C(0xb5c0fbcf), UINT32_C(0xe9b5dba5), + UINT32_C(0x3956c25b), UINT32_C(0x59f111f1), UINT32_C(0x923f82a4), UINT32_C(0xab1c5ed5), + UINT32_C(0xd807aa98), UINT32_C(0x12835b01), UINT32_C(0x243185be), UINT32_C(0x550c7dc3), + UINT32_C(0x72be5d74), UINT32_C(0x80deb1fe), UINT32_C(0x9bdc06a7), UINT32_C(0xc19bf174), + UINT32_C(0xe49b69c1), UINT32_C(0xefbe4786), UINT32_C(0x0fc19dc6), UINT32_C(0x240ca1cc), + UINT32_C(0x2de92c6f), UINT32_C(0x4a7484aa), UINT32_C(0x5cb0a9dc), UINT32_C(0x76f988da), + UINT32_C(0x983e5152), UINT32_C(0xa831c66d), UINT32_C(0xb00327c8), UINT32_C(0xbf597fc7), + UINT32_C(0xc6e00bf3), UINT32_C(0xd5a79147), UINT32_C(0x06ca6351), UINT32_C(0x14292967), + UINT32_C(0x27b70a85), UINT32_C(0x2e1b2138), UINT32_C(0x4d2c6dfc), UINT32_C(0x53380d13), + UINT32_C(0x650a7354), UINT32_C(0x766a0abb), UINT32_C(0x81c2c92e), UINT32_C(0x92722c85), + UINT32_C(0xa2bfe8a1), UINT32_C(0xa81a664b), UINT32_C(0xc24b8b70), UINT32_C(0xc76c51a3), + UINT32_C(0xd192e819), UINT32_C(0xd6990624), UINT32_C(0xf40e3585), UINT32_C(0x106aa070), + UINT32_C(0x19a4c116), UINT32_C(0x1e376c08), UINT32_C(0x2748774c), UINT32_C(0x34b0bcb5), + UINT32_C(0x391c0cb3), UINT32_C(0x4ed8aa4a), UINT32_C(0x5b9cca4f), UINT32_C(0x682e6ff3), + UINT32_C(0x748f82ee), UINT32_C(0x78a5636f), UINT32_C(0x84c87814), UINT32_C(0x8cc70208), + UINT32_C(0x90befffa), UINT32_C(0xa4506ceb), UINT32_C(0xbef9a3f7), UINT32_C(0xc67178f2), +}; + +static uint32_t +load_word(const uint8_t *source) +{ + return ((uint32_t) source[0] << 24) + | ((uint32_t) source[1] << 16) + | ((uint32_t) source[2] << 8) + | (uint32_t) source[3]; +} + +static void +store_word(uint8_t *destination, uint32_t value) +{ + destination[0] = (uint8_t) (value >> 24); + destination[1] = (uint8_t) (value >> 16); + destination[2] = (uint8_t) (value >> 8); + destination[3] = (uint8_t) value; +} + +static uint32_t +rotate(uint32_t value, unsigned distance) +{ + return (value >> distance) | (value << (32U - distance)); +} + +static void +compress(lc_mpfi_sha256 *state, const uint8_t block[64]) +{ + uint32_t schedule[64]; + uint32_t a = state->words[0]; + uint32_t b = state->words[1]; + uint32_t c = state->words[2]; + uint32_t d = state->words[3]; + uint32_t e = state->words[4]; + uint32_t f = state->words[5]; + uint32_t g = state->words[6]; + uint32_t h = state->words[7]; + + for (size_t index = 0; index < 16; ++index) { + schedule[index] = load_word(block + index * 4); + } + for (size_t index = 16; index < 64; ++index) { + uint32_t older = schedule[index - 15]; + uint32_t newer = schedule[index - 2]; + uint32_t sigma0 = rotate(older, 7) ^ rotate(older, 18) ^ (older >> 3); + uint32_t sigma1 = rotate(newer, 17) ^ rotate(newer, 19) ^ (newer >> 10); + + schedule[index] = schedule[index - 16] + sigma0 + schedule[index - 7] + sigma1; + } + for (size_t index = 0; index < 64; ++index) { + uint32_t upper = rotate(e, 6) ^ rotate(e, 11) ^ rotate(e, 25); + uint32_t choose = (e & f) ^ ((~e) & g); + uint32_t first = h + upper + choose + constants[index] + schedule[index]; + uint32_t lower = rotate(a, 2) ^ rotate(a, 13) ^ rotate(a, 22); + uint32_t majority = (a & b) ^ (a & c) ^ (b & c); + uint32_t second = lower + majority; + + h = g; + g = f; + f = e; + e = d + first; + d = c; + c = b; + b = a; + a = first + second; + } + state->words[0] += a; + state->words[1] += b; + state->words[2] += c; + state->words[3] += d; + state->words[4] += e; + state->words[5] += f; + state->words[6] += g; + state->words[7] += h; +} + +void +lc_mpfi_sha256_init(lc_mpfi_sha256 *state) +{ + static const uint32_t initial[8] = { + UINT32_C(0x6a09e667), UINT32_C(0xbb67ae85), UINT32_C(0x3c6ef372), UINT32_C(0xa54ff53a), + UINT32_C(0x510e527f), UINT32_C(0x9b05688c), UINT32_C(0x1f83d9ab), UINT32_C(0x5be0cd19), + }; + + memcpy(state->words, initial, sizeof(initial)); + state->bits = 0; + state->used = 0; +} + +void +lc_mpfi_sha256_update( + lc_mpfi_sha256 *state, + const uint8_t *bytes, + size_t length +) +{ + while (length != 0) { + size_t available = sizeof(state->block) - state->used; + size_t take = length < available ? length : available; + + memcpy(state->block + state->used, bytes, take); + state->used += take; + bytes += take; + length -= take; + if (state->used == sizeof(state->block)) { + compress(state, state->block); + state->bits += UINT64_C(512); + state->used = 0; + } + } +} + +void +lc_mpfi_sha256_finish(lc_mpfi_sha256 *state, uint8_t digest[32]) +{ + uint64_t length = state->bits + (uint64_t) state->used * 8; + + state->block[state->used++] = UINT8_C(0x80); + if (state->used > 56) { + memset(state->block + state->used, 0, sizeof(state->block) - state->used); + compress(state, state->block); + state->used = 0; + } + memset(state->block + state->used, 0, 56 - state->used); + for (size_t index = 0; index < 8; ++index) { + state->block[63 - index] = (uint8_t) (length >> (index * 8)); + } + compress(state, state->block); + for (size_t index = 0; index < 8; ++index) { + store_word(digest + index * 4, state->words[index]); + } + memset(state, 0, sizeof(*state)); +} + +void +lc_mpfi_sha256_bytes( + const uint8_t *bytes, + size_t length, + uint8_t digest[32] +) +{ + lc_mpfi_sha256 state; + + lc_mpfi_sha256_init(&state); + lc_mpfi_sha256_update(&state, bytes, length); + lc_mpfi_sha256_finish(&state, digest); +} diff --git a/proof/region/v1/mpfi/evaluator/hash.h b/proof/region/v1/mpfi/evaluator/hash.h new file mode 100644 index 00000000..a833f61c --- /dev/null +++ b/proof/region/v1/mpfi/evaluator/hash.h @@ -0,0 +1,27 @@ +#ifndef LABCOLOR_MPFI_HASH_H +#define LABCOLOR_MPFI_HASH_H + +#include +#include + +typedef struct { + uint32_t words[8]; + uint64_t bits; + uint8_t block[64]; + size_t used; +} lc_mpfi_sha256; + +void lc_mpfi_sha256_init(lc_mpfi_sha256 *state); +void lc_mpfi_sha256_update( + lc_mpfi_sha256 *state, + const uint8_t *bytes, + size_t length +); +void lc_mpfi_sha256_finish(lc_mpfi_sha256 *state, uint8_t digest[32]); +void lc_mpfi_sha256_bytes( + const uint8_t *bytes, + size_t length, + uint8_t digest[32] +); + +#endif diff --git a/proof/region/v1/mpfi/evaluator/interval.c b/proof/region/v1/mpfi/evaluator/interval.c new file mode 100644 index 00000000..9affb726 --- /dev/null +++ b/proof/region/v1/mpfi/evaluator/interval.c @@ -0,0 +1,242 @@ +#include "interval.h" + +#include + +static lc_mpfi_status +lc_mpfi_set_rational_bits(mpfi_ptr output, uint64_t bits) +{ + uint64_t exponent_bits = (bits >> 52) & UINT64_C(0x7ff); + uint64_t significand = bits & UINT64_C(0x000fffffffffffff); + mpz_t numerator; + mpz_t denominator; + mpq_t rational; + long exponent; + + if (exponent_bits == UINT64_C(0x7ff) + || bits == UINT64_C(0x8000000000000000)) { + return LC_MPFI_INVALID_DYADIC; + } + if (exponent_bits == 0) { + exponent = -1074; + } else { + significand |= UINT64_C(0x0010000000000000); + exponent = (long) exponent_bits - 1075; + } + + mpz_init_set_ui(numerator, significand); + mpz_init_set_ui(denominator, 1); + if ((bits >> 63) != 0 && significand != 0) { + mpz_neg(numerator, numerator); + } + if (exponent >= 0) { + mpz_mul_2exp(numerator, numerator, (unsigned long) exponent); + } else { + mpz_mul_2exp(denominator, denominator, (unsigned long) -exponent); + } + mpq_init(rational); + mpq_set_num(rational, numerator); + mpq_set_den(rational, denominator); + mpq_canonicalize(rational); + mpfi_set_q(output, rational); + mpq_clear(rational); + mpz_clear(denominator); + mpz_clear(numerator); + return LC_MPFI_OK; +} + +lc_mpfi_status +lc_mpfi_set_dyadic_bits(mpfi_ptr output, uint64_t bits) +{ + return lc_mpfi_set_rational_bits(output, bits); +} + +lc_mpfi_status +lc_mpfi_add(mpfi_ptr output, mpfi_srcptr left, mpfi_srcptr right) +{ + mpfi_add(output, left, right); + return LC_MPFI_OK; +} + +lc_mpfi_status +lc_mpfi_sub(mpfi_ptr output, mpfi_srcptr left, mpfi_srcptr right) +{ + mpfi_sub(output, left, right); + return LC_MPFI_OK; +} + +lc_mpfi_status +lc_mpfi_mul(mpfi_ptr output, mpfi_srcptr left, mpfi_srcptr right) +{ + mpfi_mul(output, left, right); + return LC_MPFI_OK; +} + +lc_mpfi_status +lc_mpfi_div(mpfi_ptr output, mpfi_srcptr left, mpfi_srcptr right) +{ + if (mpfi_has_zero(right)) { + return LC_MPFI_DOMAIN_UNPROVEN; + } + mpfi_div(output, left, right); + return LC_MPFI_OK; +} + +static lc_mpfi_status +lc_mpfi_endpoint_select( + mpfi_ptr output, + mpfi_srcptr left, + mpfi_srcptr right, + int choose_lower +) +{ + mpfr_prec_t precision = mpfi_get_prec(output); + mpfr_t left_endpoint; + mpfr_t right_endpoint; + mpfr_t left_other; + mpfr_t right_other; + + mpfr_inits2(precision, left_endpoint, right_endpoint, left_other, right_other, (mpfr_ptr) 0); + mpfi_get_left(left_endpoint, left); + mpfi_get_right(right_endpoint, left); + mpfi_get_left(left_other, right); + mpfi_get_right(right_other, right); + if (choose_lower) { + mpfr_min(left_endpoint, left_endpoint, left_other, MPFR_RNDD); + mpfr_min(right_endpoint, right_endpoint, right_other, MPFR_RNDU); + } else { + mpfr_max(left_endpoint, left_endpoint, left_other, MPFR_RNDD); + mpfr_max(right_endpoint, right_endpoint, right_other, MPFR_RNDU); + } + mpfi_interv_fr(output, left_endpoint, right_endpoint); + mpfr_clears(left_endpoint, right_endpoint, left_other, right_other, (mpfr_ptr) 0); + return LC_MPFI_OK; +} + +lc_mpfi_status +lc_mpfi_min(mpfi_ptr output, mpfi_srcptr left, mpfi_srcptr right) +{ + return lc_mpfi_endpoint_select(output, left, right, 1); +} + +lc_mpfi_status +lc_mpfi_max(mpfi_ptr output, mpfi_srcptr left, mpfi_srcptr right) +{ + return lc_mpfi_endpoint_select(output, left, right, 0); +} + +lc_mpfi_status +lc_mpfi_root3(mpfi_ptr output, mpfi_srcptr input) +{ + if (!mpfi_is_nonneg(input)) { + return LC_MPFI_DOMAIN_UNPROVEN; + } + mpfi_cbrt(output, input); + return LC_MPFI_OK; +} + +lc_mpfi_status +lc_mpfi_sqrt(mpfi_ptr output, mpfi_srcptr input) +{ + if (!mpfi_is_nonneg(input)) { + return LC_MPFI_DOMAIN_UNPROVEN; + } + mpfi_sqrt(output, input); + return LC_MPFI_OK; +} + +lc_mpfi_status +lc_mpfi_exp(mpfi_ptr output, mpfi_srcptr input) +{ + mpfi_exp(output, input); + return LC_MPFI_OK; +} + +lc_mpfi_status +lc_mpfi_log(mpfi_ptr output, mpfi_srcptr input) +{ + if (!mpfi_is_pos(input)) { + return LC_MPFI_DOMAIN_UNPROVEN; + } + mpfi_log(output, input); + return LC_MPFI_OK; +} + +lc_mpfi_status +lc_mpfi_sin(mpfi_ptr output, mpfi_srcptr input) +{ + mpfi_sin(output, input); + return LC_MPFI_OK; +} + +lc_mpfi_status +lc_mpfi_cos(mpfi_ptr output, mpfi_srcptr input) +{ + mpfi_cos(output, input); + return LC_MPFI_OK; +} + +lc_mpfi_status +lc_mpfi_abs(mpfi_ptr output, mpfi_srcptr input) +{ + mpfi_abs(output, input); + return LC_MPFI_OK; +} + +lc_mpfi_status +lc_mpfi_sign(mpfi_ptr output, mpfi_srcptr input) +{ + if (mpfi_is_strictly_neg(input)) { + mpfi_set_si(output, -1); + } else if (mpfi_is_strictly_pos(input)) { + mpfi_set_si(output, 1); + } else if (mpfi_is_zero(input)) { + mpfi_set_si(output, 0); + } else { + mpfi_interv_si(output, -1, 1); + } + return LC_MPFI_OK; +} + +lc_mpfi_status +lc_mpfi_pow_pos(mpfi_ptr output, mpfi_srcptr base, mpfi_srcptr exponent) +{ + mpfi_t logarithm; + + if (!mpfi_is_pos(base)) { + return LC_MPFI_DOMAIN_UNPROVEN; + } + mpfi_init2(logarithm, mpfi_get_prec(output)); + mpfi_log(logarithm, base); + mpfi_mul(logarithm, logarithm, exponent); + mpfi_exp(output, logarithm); + mpfi_clear(logarithm); + return LC_MPFI_OK; +} + +lc_mpfi_status +lc_mpfi_pow_nn(mpfi_ptr output, mpfi_srcptr base, mpfi_srcptr exponent) +{ + if (mpfi_is_zero(base) && mpfi_is_pos(exponent)) { + mpfi_set_ui(output, 0); + return LC_MPFI_OK; + } + return lc_mpfi_pow_pos(output, base, exponent); +} + +lc_mpfi_status +lc_mpfi_ratio0( + mpfi_ptr output, + mpfi_srcptr numerator, + mpfi_srcptr denominator +) +{ + if (mpfi_is_zero(numerator) && mpfi_is_zero(denominator)) { + mpfi_set_ui(output, 0); + return LC_MPFI_OK; + } + if (!mpfi_is_pos(denominator)) { + return LC_MPFI_DOMAIN_UNPROVEN; + } + mpfi_div(output, numerator, denominator); + return LC_MPFI_OK; +} diff --git a/proof/region/v1/mpfi/evaluator/interval.h b/proof/region/v1/mpfi/evaluator/interval.h new file mode 100644 index 00000000..9bf9f01c --- /dev/null +++ b/proof/region/v1/mpfi/evaluator/interval.h @@ -0,0 +1,70 @@ +#ifndef LABCOLOR_MPFI_INTERVAL_H +#define LABCOLOR_MPFI_INTERVAL_H + +#include + +#include + +typedef enum { + LC_MPFI_OK = 0, + LC_MPFI_DOMAIN_UNPROVEN = 1, + LC_MPFI_INVALID_DYADIC = 2 +} lc_mpfi_status; + +lc_mpfi_status lc_mpfi_set_dyadic_bits(mpfi_ptr output, uint64_t bits); + +lc_mpfi_status lc_mpfi_add( + mpfi_ptr output, + mpfi_srcptr left, + mpfi_srcptr right +); +lc_mpfi_status lc_mpfi_sub( + mpfi_ptr output, + mpfi_srcptr left, + mpfi_srcptr right +); +lc_mpfi_status lc_mpfi_mul( + mpfi_ptr output, + mpfi_srcptr left, + mpfi_srcptr right +); +lc_mpfi_status lc_mpfi_div( + mpfi_ptr output, + mpfi_srcptr left, + mpfi_srcptr right +); +lc_mpfi_status lc_mpfi_min( + mpfi_ptr output, + mpfi_srcptr left, + mpfi_srcptr right +); +lc_mpfi_status lc_mpfi_max( + mpfi_ptr output, + mpfi_srcptr left, + mpfi_srcptr right +); +lc_mpfi_status lc_mpfi_root3(mpfi_ptr output, mpfi_srcptr input); +lc_mpfi_status lc_mpfi_sqrt(mpfi_ptr output, mpfi_srcptr input); +lc_mpfi_status lc_mpfi_exp(mpfi_ptr output, mpfi_srcptr input); +lc_mpfi_status lc_mpfi_log(mpfi_ptr output, mpfi_srcptr input); +lc_mpfi_status lc_mpfi_sin(mpfi_ptr output, mpfi_srcptr input); +lc_mpfi_status lc_mpfi_cos(mpfi_ptr output, mpfi_srcptr input); +lc_mpfi_status lc_mpfi_abs(mpfi_ptr output, mpfi_srcptr input); +lc_mpfi_status lc_mpfi_sign(mpfi_ptr output, mpfi_srcptr input); +lc_mpfi_status lc_mpfi_pow_pos( + mpfi_ptr output, + mpfi_srcptr base, + mpfi_srcptr exponent +); +lc_mpfi_status lc_mpfi_pow_nn( + mpfi_ptr output, + mpfi_srcptr base, + mpfi_srcptr exponent +); +lc_mpfi_status lc_mpfi_ratio0( + mpfi_ptr output, + mpfi_srcptr numerator, + mpfi_srcptr denominator +); + +#endif diff --git a/proof/region/v1/mpfi/evaluator/main.c b/proof/region/v1/mpfi/evaluator/main.c new file mode 100644 index 00000000..9d9906ce --- /dev/null +++ b/proof/region/v1/mpfi/evaluator/main.c @@ -0,0 +1,570 @@ +#include +#include +#include +#include +#include +#include +#include + +#include +#include "hash.h" +#include "wire.h" + +typedef struct { + uint8_t *bytes; + size_t length; + size_t capacity; + size_t maximum; + bool limit_exceeded; +} mpfi_buffer; + +typedef enum { + LC_MPFI_READ_OK = 0, + LC_MPFI_READ_EMPTY = 1, + LC_MPFI_READ_TOO_LARGE = 2, + LC_MPFI_READ_FAILED = 3 +} lc_mpfi_read_status; + +typedef enum { + LC_MPFI_EVALUATION_OK = 0, + LC_MPFI_EVALUATION_RESOURCE_LIMIT = 1, + LC_MPFI_EVALUATION_FAILED = 2 +} lc_mpfi_evaluation_status; + +static const uint8_t transcript_magic[8] = {'L', 'C', 'T', 'R', 'N', '1', 0, 0}; +static const uint8_t accounting_domain[] = + "labcolors.mpfi-evaluation-accounting.v1\0"; +static const uint8_t exact_trace_domain[] = + "labcolors.proof-region.exact-zero-signal-trace.v1\0"; +static const uint8_t boundary_domain[] = + "labcolors.mpfi-boundary-enclosure.v1\0"; + +static void +buffer_clear(mpfi_buffer *buffer) +{ + free(buffer->bytes); + memset(buffer, 0, sizeof(*buffer)); +} + +static bool +buffer_reserve(mpfi_buffer *buffer, size_t additional) +{ + size_t required; + size_t capacity; + uint8_t *replacement; + + if (additional > SIZE_MAX - buffer->length) { + return false; + } + required = buffer->length + additional; + if (buffer->maximum != 0 && required > buffer->maximum) { + buffer->limit_exceeded = true; + return false; + } + if (required <= buffer->capacity) { + return required == 0 || buffer->bytes != NULL; + } + capacity = buffer->capacity == 0 ? 4096 : buffer->capacity; + while (capacity < required) { + if (capacity > SIZE_MAX / 2) { + capacity = required; + break; + } + capacity *= 2; + } + replacement = realloc(buffer->bytes, capacity); + if (replacement == NULL) { + return false; + } + buffer->bytes = replacement; + buffer->capacity = capacity; + return true; +} + +static bool +buffer_append(mpfi_buffer *buffer, const uint8_t *bytes, size_t length) +{ + if (length == 0) { + return true; + } + if (!buffer_reserve(buffer, length)) { + return false; + } + memcpy(buffer->bytes + buffer->length, bytes, length); + buffer->length += length; + return true; +} + +static bool +buffer_u8(mpfi_buffer *buffer, uint8_t value) +{ + return buffer_append(buffer, &value, 1); +} + +static bool +buffer_u32(mpfi_buffer *buffer, uint32_t value) +{ + uint8_t encoded[4]; + + lc_mpfi_write_u32_be(encoded, value); + return buffer_append(buffer, encoded, sizeof(encoded)); +} + +static bool +buffer_u64(mpfi_buffer *buffer, uint64_t value) +{ + uint8_t encoded[8]; + + lc_mpfi_write_u64_be(encoded, value); + return buffer_append(buffer, encoded, sizeof(encoded)); +} + +static lc_mpfi_read_status +read_stdin(mpfi_buffer *input) +{ + uint8_t chunk[16384]; + + for (;;) { + ssize_t count = read(STDIN_FILENO, chunk, sizeof(chunk)); + + if (count < 0) { + if (errno == EINTR) { + continue; + } + return LC_MPFI_READ_FAILED; + } + if (count == 0) { + return input->length == 0 ? LC_MPFI_READ_EMPTY : LC_MPFI_READ_OK; + } + if (input->maximum != 0 + && (size_t) count > input->maximum - input->length) { + return LC_MPFI_READ_TOO_LARGE; + } + if (!buffer_append(input, chunk, (size_t) count)) { + return LC_MPFI_READ_FAILED; + } + } +} + +static bool +nonzero_digest(const uint8_t digest[32]) +{ + uint8_t value = 0; + + for (size_t index = 0; index < 32; ++index) { + value |= digest[index]; + } + return value != 0; +} + +static bool +parse_identity(const char *text, uint8_t identity[32]) +{ + uint8_t aggregate = 0; + + if (strlen(text) != 64) { + return false; + } + for (size_t index = 0; index < 32; ++index) { + uint8_t value = 0; + + for (size_t nibble = 0; nibble < 2; ++nibble) { + unsigned char character = (unsigned char) text[index * 2 + nibble]; + + value <<= 4; + if (character >= '0' && character <= '9') { + value |= (uint8_t) (character - '0'); + } else if (character >= 'a' && character <= 'f') { + value |= (uint8_t) (character - 'a' + 10); + } else { + return false; + } + } + identity[index] = value; + aggregate |= value; + } + return aggregate != 0; +} + +static void +hash_common_prefix( + lc_mpfi_sha256 *state, + const uint8_t *domain, + size_t domain_length, + const lc_mpfi_job *job, + uint32_t ordinal +) +{ + uint8_t ordinal_bytes[4]; + + lc_mpfi_write_u32_be(ordinal_bytes, ordinal); + lc_mpfi_sha256_init(state); + lc_mpfi_sha256_update(state, domain, domain_length); + lc_mpfi_sha256_update(state, job->job_identity, sizeof(job->job_identity)); + lc_mpfi_sha256_update(state, ordinal_bytes, sizeof(ordinal_bytes)); +} + +static bool +exact_trace_digest( + const lc_mpfi_job *job, + uint32_t ordinal, + uint64_t exact_branch, + uint8_t digest[32] +) +{ + lc_mpfi_sha256 state; + uint8_t branch_bytes[8]; + + hash_common_prefix( + &state, + exact_trace_domain, + sizeof(exact_trace_domain) - 1, + job, + ordinal + ); + lc_mpfi_write_u64_be(branch_bytes, exact_branch); + lc_mpfi_sha256_update(&state, branch_bytes, sizeof(branch_bytes)); + lc_mpfi_sha256_finish(&state, digest); + return nonzero_digest(digest); +} + +static bool +hash_mpfr_string(lc_mpfi_sha256 *state, mpfr_srcptr value) +{ + mpfr_exp_t exponent; + char *digits = mpfr_get_str(NULL, &exponent, 16, 0, value, MPFR_RNDN); + uint8_t exponent_bytes[8]; + uint8_t length_bytes[8]; + size_t length; + + if (digits == NULL) { + return false; + } + length = strlen(digits); + lc_mpfi_write_u64_be(length_bytes, (uint64_t) length); + lc_mpfi_write_u64_be(exponent_bytes, (uint64_t) exponent); + lc_mpfi_sha256_update(state, exponent_bytes, sizeof(exponent_bytes)); + lc_mpfi_sha256_update(state, length_bytes, sizeof(length_bytes)); + lc_mpfi_sha256_update(state, (const uint8_t *) digits, length); + mpfr_free_str(digits); + return true; +} + +static bool +boundary_digest( + const lc_mpfi_job *job, + uint32_t ordinal, + uint32_t precision, + const lc_mpfi_region_result *result, + uint8_t digest[32] +) +{ + lc_mpfi_sha256 state; + uint8_t precision_bytes[4]; + uint8_t status = (uint8_t) result->formula_status; + uint8_t present = result->has_enclosure ? 1 : 0; + __mpfr_struct lower; + __mpfr_struct upper; + bool success = false; + + hash_common_prefix(&state, boundary_domain, sizeof(boundary_domain) - 1, job, ordinal); + lc_mpfi_write_u32_be(precision_bytes, precision); + lc_mpfi_sha256_update(&state, precision_bytes, sizeof(precision_bytes)); + lc_mpfi_sha256_update(&state, &status, sizeof(status)); + lc_mpfi_sha256_update(&state, &present, sizeof(present)); + if (result->has_enclosure) { + mpfr_init2(&lower, result->precision); + mpfr_init2(&upper, result->precision); + mpfi_get_left(&lower, &result->enclosure); + mpfi_get_right(&upper, &result->enclosure); + success = hash_mpfr_string(&state, &lower) + && hash_mpfr_string(&state, &upper); + mpfr_clear(&upper); + mpfr_clear(&lower); + } else { + success = true; + } + if (!success) { + return false; + } + lc_mpfi_sha256_finish(&state, digest); + return nonzero_digest(digest); +} + +static void +account_point( + lc_mpfi_sha256 *state, + uint32_t ordinal, + uint32_t precision, + uint64_t consumed, + lc_mpfi_region_outcome outcome +) +{ + uint8_t record[17]; + + lc_mpfi_write_u32_be(record, ordinal); + lc_mpfi_write_u32_be(record + 4, precision); + lc_mpfi_write_u64_be(record + 8, consumed); + record[16] = (uint8_t) outcome; + lc_mpfi_sha256_update(state, record, sizeof(record)); +} + +static bool +append_digest_witness( + mpfi_buffer *witnesses, + uint8_t kind, + uint32_t ordinal, + const uint8_t digest[32] +) +{ + return buffer_u8(witnesses, kind) + && buffer_u32(witnesses, ordinal) + && buffer_append(witnesses, digest, 32); +} + +static bool +append_resource_witness( + mpfi_buffer *witnesses, + uint32_t ordinal, + uint8_t scope, + uint64_t grant +) +{ + return buffer_u8(witnesses, 3) + && buffer_u32(witnesses, ordinal) + && buffer_u8(witnesses, scope) + && buffer_u64(witnesses, grant) + && buffer_u64(witnesses, grant); +} + +static uint64_t +smaller(uint64_t left, uint64_t right) +{ + return left < right ? left : right; +} + +static lc_mpfi_evaluation_status +evaluate_job( + const lc_mpfi_job *job, + const uint8_t comparator_identity[32], + mpfi_buffer *output +) +{ + mpfi_buffer decisions = {0}; + mpfi_buffer witnesses = {0}; + lc_mpfi_domain_iterator iterator; + lc_mpfi_region_result result; + lc_mpfi_sha256 accounting; + uint64_t counters[4] = {0, 0, 0, 0}; + uint64_t equality_count = 0; + uint64_t witness_count = 0; + uint64_t remaining_global = job->policy.global_pregrant; + uint8_t accounting_digest[32]; + lc_mpfi_evaluation_status status = LC_MPFI_EVALUATION_FAILED; + + decisions.maximum = (size_t) LC_MPFI_MAX_OUTPUT_BYTES_V1; + witnesses.maximum = (size_t) LC_MPFI_MAX_OUTPUT_BYTES_V1; + + if (job->domain.point_count == 0 + || job->policy.precision_count == 0 + || job->domain.point_count > SIZE_MAX - 3 + || !lc_mpfi_region_result_init(&result, job->maximum_precision)) { + return LC_MPFI_EVALUATION_FAILED; + } + size_t decision_length = ((size_t) job->domain.point_count + 3) / 4; + if (decision_length == 0 + || !buffer_reserve(&decisions, decision_length) + || decisions.bytes == NULL) { + goto cleanup_buffers; + } + memset(decisions.bytes, 0, decision_length); + decisions.length = decision_length; + lc_mpfi_sha256_init(&accounting); + lc_mpfi_sha256_update( + &accounting, + accounting_domain, + sizeof(accounting_domain) - 1 + ); + lc_mpfi_sha256_update(&accounting, job->job_identity, 32); + lc_mpfi_sha256_update(&accounting, job->domain.identity, 32); + lc_mpfi_sha256_update(&accounting, job->policy.identity, 32); + lc_mpfi_sha256_update(&accounting, comparator_identity, 32); + lc_mpfi_domain_iterator_init(&iterator, &job->domain); + for (uint64_t point_index = 0; point_index < job->domain.point_count; ++point_index) { + uint64_t point_grant = smaller( + job->policy.per_point_work, + remaining_global + ); + uint64_t point_remaining = point_grant; + uint64_t point_consumed = 0; + uint8_t scope = job->policy.per_point_work <= remaining_global ? 1 : 2; + uint32_t ordinal; + uint32_t final_precision = job->policy.precision_ladder[0]; + uint8_t rgb[3]; + + remaining_global -= point_grant; + if (!lc_mpfi_domain_iterator_next(&iterator, &ordinal)) { + goto cleanup_buffers; + } + lc_mpfi_ordinal_to_rgb(ordinal, rgb); + for (size_t rung = 0; rung < job->policy.precision_count; ++rung) { + uint64_t grant = point_remaining; + + final_precision = job->policy.precision_ladder[rung]; + lc_mpfi_region_evaluate_rgb( + &result, + rgb, + job->context, + job->surround, + &job->region, + final_precision, + grant + ); + if (result.consumed_branches > grant + || result.consumed_branches > point_remaining) { + goto cleanup_buffers; + } + point_remaining -= result.consumed_branches; + point_consumed += result.consumed_branches; + if (result.outcome != LC_MPFI_REGION_BOUNDARY_UNPROVEN) { + break; + } + } + if ((unsigned) result.outcome > LC_MPFI_REGION_RESOURCE_LIMIT_REACHED) { + goto cleanup_buffers; + } + decisions.bytes[point_index / 4] |= + (uint8_t) result.outcome << (6U - 2U * (unsigned) (point_index % 4)); + ++counters[result.outcome]; + account_point( + &accounting, + ordinal, + final_precision, + point_consumed, + result.outcome + ); + if (result.outcome == LC_MPFI_REGION_INSIDE && result.exact_boundary) { + uint8_t digest[32]; + + if (!exact_trace_digest(job, ordinal, result.exact_branch, digest) + || !append_digest_witness(&witnesses, 1, ordinal, digest)) { + goto cleanup_buffers; + } + ++equality_count; + ++witness_count; + } else if (result.outcome == LC_MPFI_REGION_BOUNDARY_UNPROVEN) { + uint8_t digest[32]; + + if (!boundary_digest(job, ordinal, final_precision, &result, digest) + || !append_digest_witness(&witnesses, 2, ordinal, digest)) { + goto cleanup_buffers; + } + ++witness_count; + } else if (result.outcome == LC_MPFI_REGION_RESOURCE_LIMIT_REACHED) { + if (point_consumed != point_grant + || !append_resource_witness(&witnesses, ordinal, scope, point_grant)) { + goto cleanup_buffers; + } + ++witness_count; + } + } + lc_mpfi_sha256_finish(&accounting, accounting_digest); + if (!nonzero_digest(accounting_digest) + || !buffer_append(output, transcript_magic, sizeof(transcript_magic)) + || !buffer_append(output, job->job_identity, 32) + || !buffer_append(output, job->domain.identity, 32) + || !buffer_append(output, comparator_identity, 32) + || !buffer_u64(output, job->domain.point_count) + || !buffer_u64(output, decisions.length) + || !buffer_append(output, decisions.bytes, decisions.length)) { + goto cleanup_buffers; + } + for (size_t index = 0; index < 4; ++index) { + if (!buffer_u64(output, counters[index])) { + goto cleanup_buffers; + } + } + if (!buffer_u64(output, equality_count) + || !buffer_append(output, accounting_digest, sizeof(accounting_digest)) + || !buffer_u64(output, witness_count) + || !buffer_append(output, witnesses.bytes, witnesses.length)) { + goto cleanup_buffers; + } + status = LC_MPFI_EVALUATION_OK; + +cleanup_buffers: + if (status != LC_MPFI_EVALUATION_OK + && (decisions.limit_exceeded + || witnesses.limit_exceeded + || output->limit_exceeded)) { + status = LC_MPFI_EVALUATION_RESOURCE_LIMIT; + } + buffer_clear(&witnesses); + buffer_clear(&decisions); + lc_mpfi_region_result_clear(&result); + return status; +} + +int +main(int argc, char **argv) +{ + mpfi_buffer input = {0}; + mpfi_buffer output = {0}; + lc_mpfi_job job; + lc_mpfi_wire_error error; + uint8_t comparator_identity[32]; + int status = 1; + lc_mpfi_read_status read_status; + + input.maximum = (size_t) LC_MPFI_MAX_JOB_BYTES_V1; + output.maximum = (size_t) LC_MPFI_MAX_OUTPUT_BYTES_V1; + + if (argc != 5 + || strcmp(argv[1], "--manifest-identity") != 0 + || !parse_identity(argv[2], comparator_identity) + || strcmp(argv[3], "--job") != 0 + || strcmp(argv[4], "/dev/stdin") != 0) { + fputs( + "usage: mpfi-evaluator --manifest-identity HEX64 --job /dev/stdin\n", + stderr + ); + return 64; + } + read_status = read_stdin(&input); + if (read_status != LC_MPFI_READ_OK) { + const char *reason = read_status == LC_MPFI_READ_TOO_LARGE + ? "input_limit" + : read_status == LC_MPFI_READ_EMPTY ? "empty_input" : "io"; + + fprintf(stderr, "job read failed: %s\n", reason); + goto cleanup_input; + } + if (!lc_mpfi_parse_job(&job, input.bytes, input.length, &error)) { + fprintf(stderr, "job rejected: %s\n", lc_mpfi_wire_error_name(error)); + goto cleanup_input; + } + lc_mpfi_evaluation_status evaluation = + evaluate_job(&job, comparator_identity, &output); + if (evaluation != LC_MPFI_EVALUATION_OK) { + fprintf( + stderr, + "evaluation failed: %s\n", + evaluation == LC_MPFI_EVALUATION_RESOURCE_LIMIT + ? "output_limit" + : "internal" + ); + goto cleanup_job; + } + if (!lc_mpfi_write_all(STDOUT_FILENO, output.bytes, output.length)) { + fputs("result write failed\n", stderr); + goto cleanup_job; + } + status = 0; + +cleanup_job: + buffer_clear(&output); + lc_mpfi_job_clear(&job); +cleanup_input: + buffer_clear(&input); + return status; +} diff --git a/proof/region/v1/mpfi/evaluator/region.c b/proof/region/v1/mpfi/evaluator/region.c new file mode 100644 index 00000000..d6bbd1fd --- /dev/null +++ b/proof/region/v1/mpfi/evaluator/region.c @@ -0,0 +1,382 @@ +#include "region.h" + +#include + +#include "formula.h" + +static void +clear_knot(lc_mpfi_region_knot *knot) +{ + mpfi_clear(&knot->radius_squared); + mpfi_clear(&knot->center_b); + mpfi_clear(&knot->center_a); + mpfi_clear(&knot->tone); +} + +static void +init_knot(lc_mpfi_region_knot *knot, mpfr_prec_t precision) +{ + mpfi_init2(&knot->tone, precision); + mpfi_init2(&knot->center_a, precision); + mpfi_init2(&knot->center_b, precision); + mpfi_init2(&knot->radius_squared, precision); +} + +static void +reset_result(lc_mpfi_region_result *result) +{ + result->outcome = LC_MPFI_REGION_BOUNDARY_UNPROVEN; + result->formula_status = LC_MPFI_OK; + result->exact_boundary = false; + result->has_enclosure = false; + result->exact_branch = 0; + result->consumed_branches = 0; + mpfi_set_ui(&result->enclosure, 0); +} + +static bool +interval_strictly_below(mpfi_srcptr left, mpfi_srcptr right) +{ + mpfr_prec_t precision = mpfi_get_prec(left); + mpfr_t left_high; + mpfr_t right_low; + int result; + + mpfr_inits2(precision, left_high, right_low, (mpfr_ptr) 0); + mpfi_get_right(left_high, left); + mpfi_get_left(right_low, right); + result = mpfr_cmp(left_high, right_low) < 0; + mpfr_clears(left_high, right_low, (mpfr_ptr) 0); + return result != 0; +} + +static bool +interval_strictly_above(mpfi_srcptr left, mpfi_srcptr right) +{ + return interval_strictly_below(right, left); +} + +static bool +interval_at_least(mpfi_srcptr left, mpfi_srcptr right) +{ + mpfr_prec_t precision = mpfi_get_prec(left); + mpfr_t left_low; + mpfr_t right_high; + int result; + + mpfr_inits2(precision, left_low, right_high, (mpfr_ptr) 0); + mpfi_get_left(left_low, left); + mpfi_get_right(right_high, right); + result = mpfr_cmp(left_low, right_high) >= 0; + mpfr_clears(left_low, right_high, (mpfr_ptr) 0); + return result != 0; +} + +static bool +interval_at_most(mpfi_srcptr left, mpfi_srcptr right) +{ + mpfr_prec_t precision = mpfi_get_prec(left); + mpfr_t left_high; + mpfr_t right_low; + int result; + + mpfr_inits2(precision, left_high, right_low, (mpfr_ptr) 0); + mpfi_get_right(left_high, left); + mpfi_get_left(right_low, right); + result = mpfr_cmp(left_high, right_low) <= 0; + mpfr_clears(left_high, right_low, (mpfr_ptr) 0); + return result != 0; +} + +static bool +interval_equal(mpfi_srcptr left, mpfi_srcptr right) +{ + __mpfi_struct difference; + bool equal; + + mpfi_init2(&difference, mpfi_get_prec(left)); + mpfi_sub(&difference, left, right); + equal = mpfi_is_zero(&difference) != 0; + mpfi_clear(&difference); + return equal; +} + +static void +record_enclosure(lc_mpfi_region_result *result, mpfi_srcptr value) +{ + if (result->has_enclosure) { + mpfi_union(&result->enclosure, &result->enclosure, value); + } else { + mpfi_set(&result->enclosure, value); + result->has_enclosure = true; + } +} + +bool +lc_mpfi_region_init( + lc_mpfi_region *region, + size_t knot_count, + mpfr_prec_t precision +) +{ + region->knots = NULL; + region->knot_count = 0; + region->precision = precision; + mpfi_init2(®ion->metric_aa, precision); + mpfi_init2(®ion->metric_ab, precision); + mpfi_init2(®ion->metric_bb, precision); + if (knot_count == 0 || knot_count > SIZE_MAX / sizeof(*region->knots)) { + lc_mpfi_region_clear(region); + return false; + } + region->knots = calloc(knot_count, sizeof(*region->knots)); + if (region->knots == NULL) { + lc_mpfi_region_clear(region); + return false; + } + region->knot_count = knot_count; + for (size_t index = 0; index < knot_count; ++index) { + init_knot(region->knots + index, precision); + } + return true; +} + +void +lc_mpfi_region_clear(lc_mpfi_region *region) +{ + if (region->knots != NULL) { + for (size_t index = 0; index < region->knot_count; ++index) { + clear_knot(region->knots + index); + } + free(region->knots); + } + mpfi_clear(®ion->metric_bb); + mpfi_clear(®ion->metric_ab); + mpfi_clear(®ion->metric_aa); + region->knots = NULL; + region->knot_count = 0; + region->precision = 0; +} + +bool +lc_mpfi_region_result_init(lc_mpfi_region_result *result, mpfr_prec_t precision) +{ + if (precision == 0) { + return false; + } + result->precision = precision; + mpfi_init2(&result->enclosure, precision); + reset_result(result); + return true; +} + +void +lc_mpfi_region_result_clear(lc_mpfi_region_result *result) +{ + mpfi_clear(&result->enclosure); + result->precision = 0; +} + +static void +evaluate_singleton( + lc_mpfi_region_result *result, + mpfi_srcptr point, + const lc_mpfi_region *region, + mpfr_prec_t precision, + uint64_t branch_grant +) +{ + __mpfi_struct input[8]; + __mpfi_struct predicate; + + if (!interval_equal(point, ®ion->knots[0].tone)) { + __mpfi_struct overlap; + + mpfi_init2(&overlap, precision); + mpfi_intersect(&overlap, point, ®ion->knots[0].tone); + result->outcome = mpfi_is_empty(&overlap) + ? LC_MPFI_REGION_OUTSIDE + : LC_MPFI_REGION_BOUNDARY_UNPROVEN; + mpfi_clear(&overlap); + return; + } + if (branch_grant == 0) { + result->outcome = LC_MPFI_REGION_RESOURCE_LIMIT_REACHED; + return; + } + for (size_t index = 0; index < 8; ++index) { + mpfi_init2(input + index, precision); + } + mpfi_set(input + 0, point + 1); + mpfi_set(input + 1, point + 2); + mpfi_set(input + 2, ®ion->knots[0].center_a); + mpfi_set(input + 3, ®ion->knots[0].center_b); + mpfi_set(input + 4, ®ion->knots[0].radius_squared); + mpfi_set(input + 5, ®ion->metric_aa); + mpfi_set(input + 6, ®ion->metric_ab); + mpfi_set(input + 7, ®ion->metric_bb); + mpfi_init2(&predicate, precision); + result->formula_status = lc_mpfi_formula_singleton(&predicate, input); + result->consumed_branches = 1; + if (result->formula_status == LC_MPFI_OK) { + record_enclosure(result, &predicate); + if (mpfi_is_nonpos(&predicate)) { + result->outcome = LC_MPFI_REGION_INSIDE; + result->exact_boundary = mpfi_is_zero(&predicate) != 0; + result->exact_branch = 0; + } else if (mpfi_is_pos(&predicate)) { + result->outcome = LC_MPFI_REGION_OUTSIDE; + } + } + mpfi_clear(&predicate); + for (size_t index = 8; index-- != 0;) { + mpfi_clear(input + index); + } +} + +void +lc_mpfi_region_decide( + lc_mpfi_region_result *result, + mpfi_srcptr point, + const lc_mpfi_region *region, + mpfr_prec_t precision, + uint64_t branch_grant +) +{ + bool any_segment = false; + bool all_inside = true; + bool all_outside = true; + bool exact_zero = false; + bool outside_possible; + uint64_t exact_branch = 0; + __mpfi_struct segment_domain; + __mpfi_struct intersection; + + reset_result(result); + if (precision < 2) { + result->formula_status = LC_MPFI_DOMAIN_UNPROVEN; + return; + } + if (region->knot_count == 1) { + evaluate_singleton(result, point, region, precision, branch_grant); + return; + } + if (region->knot_count < 2) { + result->formula_status = LC_MPFI_DOMAIN_UNPROVEN; + return; + } + if (interval_strictly_below(point, ®ion->knots[0].tone) + || interval_strictly_above(point, ®ion->knots[region->knot_count - 1].tone)) { + result->outcome = LC_MPFI_REGION_OUTSIDE; + return; + } + outside_possible = !interval_at_least(point, ®ion->knots[0].tone) + || !interval_at_most(point, ®ion->knots[region->knot_count - 1].tone); + mpfi_init2(&segment_domain, precision); + mpfi_init2(&intersection, precision); + for (size_t index = 0; index + 1 < region->knot_count; ++index) { + const lc_mpfi_region_knot *left = region->knots + index; + const lc_mpfi_region_knot *right = region->knots + index + 1; + __mpfi_struct input[14]; + __mpfi_struct predicate; + + mpfi_union(&segment_domain, &left->tone, &right->tone); + mpfi_intersect(&intersection, point, &segment_domain); + if (mpfi_is_empty(&intersection)) { + continue; + } + any_segment = true; + if (result->consumed_branches == branch_grant) { + result->outcome = LC_MPFI_REGION_RESOURCE_LIMIT_REACHED; + break; + } + for (size_t input_index = 0; input_index < 14; ++input_index) { + mpfi_init2(input + input_index, precision); + } + mpfi_set(input + 0, &intersection); + mpfi_set(input + 1, point + 1); + mpfi_set(input + 2, point + 2); + mpfi_set(input + 3, &left->tone); + mpfi_set(input + 4, &right->tone); + mpfi_set(input + 5, &left->center_a); + mpfi_set(input + 6, &left->center_b); + mpfi_set(input + 7, &right->center_a); + mpfi_set(input + 8, &right->center_b); + mpfi_set(input + 9, &left->radius_squared); + mpfi_set(input + 10, &right->radius_squared); + mpfi_set(input + 11, ®ion->metric_aa); + mpfi_set(input + 12, ®ion->metric_ab); + mpfi_set(input + 13, ®ion->metric_bb); + mpfi_init2(&predicate, precision); + result->formula_status = lc_mpfi_formula_segment(&predicate, input); + ++result->consumed_branches; + if (result->formula_status == LC_MPFI_OK) { + bool inside = mpfi_is_nonpos(&predicate) != 0; + bool outside = mpfi_is_pos(&predicate) != 0; + bool branch_exact = mpfi_is_zero(&predicate) != 0; + + record_enclosure(result, &predicate); + all_inside = all_inside && inside; + all_outside = all_outside && outside; + if (branch_exact && !exact_zero) { + exact_branch = (uint64_t) index; + } + exact_zero = exact_zero || branch_exact; + } else { + all_inside = false; + all_outside = false; + } + mpfi_clear(&predicate); + for (size_t input_index = 14; input_index-- != 0;) { + mpfi_clear(input + input_index); + } + } + if (result->outcome == LC_MPFI_REGION_RESOURCE_LIMIT_REACHED) { + mpfi_clear(&intersection); + mpfi_clear(&segment_domain); + return; + } + if (!any_segment) { + result->outcome = LC_MPFI_REGION_BOUNDARY_UNPROVEN; + } else if (all_outside) { + result->outcome = LC_MPFI_REGION_OUTSIDE; + } else if (all_inside && !outside_possible) { + result->outcome = LC_MPFI_REGION_INSIDE; + result->exact_boundary = exact_zero; + result->exact_branch = exact_branch; + } else { + result->outcome = LC_MPFI_REGION_BOUNDARY_UNPROVEN; + } + mpfi_clear(&intersection); + mpfi_clear(&segment_domain); +} + +void +lc_mpfi_region_evaluate_rgb( + lc_mpfi_region_result *result, + const uint8_t rgb[3], + mpfi_srcptr context, + uint8_t surround, + const lc_mpfi_region *region, + mpfr_prec_t precision, + uint64_t branch_grant +) +{ + __mpfi_struct point[3]; + + reset_result(result); + if (precision < 2) { + result->formula_status = LC_MPFI_DOMAIN_UNPROVEN; + return; + } + for (size_t index = 0; index < 3; ++index) { + mpfi_init2(point + index, precision); + } + result->formula_status = lc_mpfi_formula_point(point, rgb, context, surround); + if (result->formula_status == LC_MPFI_OK) { + lc_mpfi_region_decide(result, point, region, precision, branch_grant); + } + for (size_t index = 3; index-- != 0;) { + mpfi_clear(point + index); + } +} diff --git a/proof/region/v1/mpfi/evaluator/region.h b/proof/region/v1/mpfi/evaluator/region.h new file mode 100644 index 00000000..d2d6e3a4 --- /dev/null +++ b/proof/region/v1/mpfi/evaluator/region.h @@ -0,0 +1,72 @@ +#ifndef LABCOLOR_MPFI_REGION_H +#define LABCOLOR_MPFI_REGION_H + +#include +#include +#include + +#include "interval.h" + +typedef enum { + LC_MPFI_REGION_INSIDE = 0, + LC_MPFI_REGION_OUTSIDE = 1, + LC_MPFI_REGION_BOUNDARY_UNPROVEN = 2, + LC_MPFI_REGION_RESOURCE_LIMIT_REACHED = 3 +} lc_mpfi_region_outcome; + +typedef struct { + __mpfi_struct tone; + __mpfi_struct center_a; + __mpfi_struct center_b; + __mpfi_struct radius_squared; +} lc_mpfi_region_knot; + +typedef struct { + __mpfi_struct metric_aa; + __mpfi_struct metric_ab; + __mpfi_struct metric_bb; + lc_mpfi_region_knot *knots; + size_t knot_count; + mpfr_prec_t precision; +} lc_mpfi_region; + +typedef struct { + lc_mpfi_region_outcome outcome; + lc_mpfi_status formula_status; + bool exact_boundary; + bool has_enclosure; + uint64_t exact_branch; + uint64_t consumed_branches; + __mpfi_struct enclosure; + mpfr_prec_t precision; +} lc_mpfi_region_result; + +bool lc_mpfi_region_init( + lc_mpfi_region *region, + size_t knot_count, + mpfr_prec_t precision +); +void lc_mpfi_region_clear(lc_mpfi_region *region); +bool lc_mpfi_region_result_init( + lc_mpfi_region_result *result, + mpfr_prec_t precision +); +void lc_mpfi_region_result_clear(lc_mpfi_region_result *result); +void lc_mpfi_region_decide( + lc_mpfi_region_result *result, + mpfi_srcptr point, + const lc_mpfi_region *region, + mpfr_prec_t precision, + uint64_t branch_grant +); +void lc_mpfi_region_evaluate_rgb( + lc_mpfi_region_result *result, + const uint8_t rgb[3], + mpfi_srcptr context, + uint8_t surround, + const lc_mpfi_region *region, + mpfr_prec_t precision, + uint64_t branch_grant +); + +#endif diff --git a/proof/region/v1/mpfi/evaluator/wire.c b/proof/region/v1/mpfi/evaluator/wire.c new file mode 100644 index 00000000..a3f1ba04 --- /dev/null +++ b/proof/region/v1/mpfi/evaluator/wire.c @@ -0,0 +1,822 @@ +#include "wire.h" + +#include +#include +#include +#include + +#include "hash.h" + +typedef struct { + const uint8_t *bytes; + size_t length; + size_t offset; + lc_mpfi_wire_error *error; +} mpfi_reader; + +static const uint8_t job_magic[8] = {'L', 'C', 'J', 'O', 'B', '1', 0, 0}; +static const uint8_t domain_magic[8] = {'L', 'C', 'D', 'O', 'M', '1', 0, 0}; +static const uint8_t policy_magic[8] = {'L', 'C', 'P', 'O', 'L', '1', 0, 0}; +static const uint8_t definition_domain[] = + "labcolors.contextual-region-family-provider.v1\0"; +static const uint8_t formula_domain[] = + "labcolors.nominal-exact-real-lift.ascii-ssa.v1\0"; +static const uint8_t domain_identity_label[] = + "labcolors.proof-region.domain.v1\0"; +static const uint8_t policy_identity_label[] = + "labcolors.proof-region.policy.v1\0"; +static const uint8_t job_identity_label[] = + "labcolors.proof-region.job.v1\0"; +static const size_t formula_spec_length = 24434; +static const uint8_t formula_release_v1[32] = { + 0x2c, 0x62, 0x6d, 0x8e, 0xe6, 0x0e, 0xeb, 0x62, + 0xae, 0x4d, 0xb5, 0x36, 0x60, 0xd6, 0x1b, 0xbc, + 0x25, 0xe0, 0xef, 0xd4, 0xe5, 0x57, 0xf0, 0xdc, + 0x1e, 0x77, 0x56, 0x5c, 0x13, 0x0b, 0x6e, 0x52, +}; + +static bool +reject(mpfi_reader *input, lc_mpfi_wire_error error) +{ + if (*input->error == LC_MPFI_WIRE_OK) { + *input->error = error; + } + return false; +} + +static size_t +available(const mpfi_reader *input) +{ + return input->length - input->offset; +} + +static bool +take(mpfi_reader *input, size_t length, lc_mpfi_slice *slice) +{ + if (length > available(input)) { + return reject(input, LC_MPFI_WIRE_TRUNCATED); + } + slice->bytes = input->bytes + input->offset; + slice->length = length; + input->offset += length; + return true; +} + +static bool +expect( + mpfi_reader *input, + const uint8_t *expected, + size_t length, + lc_mpfi_wire_error error +) +{ + lc_mpfi_slice actual; + + return take(input, length, &actual) + && (memcmp(actual.bytes, expected, length) == 0 || reject(input, error)); +} + +static bool +read_u8(mpfi_reader *input, uint8_t *value) +{ + lc_mpfi_slice byte; + + if (!take(input, 1, &byte)) { + return false; + } + *value = byte.bytes[0]; + return true; +} + +static bool +read_u32(mpfi_reader *input, uint32_t *value) +{ + lc_mpfi_slice bytes; + + if (!take(input, 4, &bytes)) { + return false; + } + *value = ((uint32_t) bytes.bytes[0] << 24) + | ((uint32_t) bytes.bytes[1] << 16) + | ((uint32_t) bytes.bytes[2] << 8) + | (uint32_t) bytes.bytes[3]; + return true; +} + +static bool +read_u64(mpfi_reader *input, uint64_t *value) +{ + lc_mpfi_slice bytes; + uint64_t result = 0; + + if (!take(input, 8, &bytes)) { + return false; + } + for (size_t index = 0; index < 8; ++index) { + result = (result << 8) | bytes.bytes[index]; + } + *value = result; + return true; +} + +static bool +read_blob(mpfi_reader *input, size_t exact_length, lc_mpfi_slice *value) +{ + uint64_t declared; + + if (!read_u64(input, &declared)) { + return false; + } + if (declared > SIZE_MAX + || (exact_length != SIZE_MAX && declared != exact_length)) { + return reject(input, LC_MPFI_WIRE_LENGTH_OUT_OF_BOUNDS); + } + if ((size_t) declared > available(input)) { + return reject(input, LC_MPFI_WIRE_LENGTH_OUT_OF_BOUNDS); + } + return take(input, (size_t) declared, value); +} + +static bool +finish(mpfi_reader *input) +{ + return available(input) == 0 + || reject(input, LC_MPFI_WIRE_TRAILING_BYTES); +} + +void +lc_mpfi_write_u32_be(uint8_t output[4], uint32_t value) +{ + output[0] = (uint8_t) (value >> 24); + output[1] = (uint8_t) (value >> 16); + output[2] = (uint8_t) (value >> 8); + output[3] = (uint8_t) value; +} + +void +lc_mpfi_write_u64_be(uint8_t output[8], uint64_t value) +{ + for (size_t index = 0; index < 8; ++index) { + output[7 - index] = (uint8_t) (value >> (index * 8)); + } +} + +static void +content_identity( + const uint8_t *label, + size_t label_length, + const uint8_t *bytes, + size_t length, + uint8_t digest[32] +) +{ + lc_mpfi_sha256 state; + uint8_t encoded_length[8]; + + lc_mpfi_write_u64_be(encoded_length, (uint64_t) length); + lc_mpfi_sha256_init(&state); + lc_mpfi_sha256_update(&state, label, label_length); + lc_mpfi_sha256_update(&state, encoded_length, sizeof(encoded_length)); + lc_mpfi_sha256_update(&state, bytes, length); + lc_mpfi_sha256_finish(&state, digest); +} + +static bool +decode_bits(lc_mpfi_slice field, uint64_t *bits) +{ + uint64_t value = 0; + + if (field.length != 8) { + return false; + } + for (size_t index = 0; index < 8; ++index) { + value = (value << 8) | field.bytes[index]; + } + if ((value >> 52 & UINT64_C(0x7ff)) == UINT64_C(0x7ff) + || value == UINT64_C(0x8000000000000000)) { + return false; + } + *bits = value; + return true; +} + +static bool +bits_to_rational(uint64_t bits, mpq_t result) +{ + uint64_t exponent_bits = (bits >> 52) & UINT64_C(0x7ff); + uint64_t significand = bits & UINT64_C(0x000fffffffffffff); + long exponent; + mpz_t numerator; + mpz_t denominator; + + if (exponent_bits == UINT64_C(0x7ff) + || bits == UINT64_C(0x8000000000000000)) { + return false; + } + if (exponent_bits == 0) { + exponent = -1074; + } else { + significand |= UINT64_C(0x0010000000000000); + exponent = (long) exponent_bits - 1075; + } + mpz_init_set_ui(numerator, significand); + mpz_init_set_ui(denominator, 1); + if ((bits >> 63) != 0 && significand != 0) { + mpz_neg(numerator, numerator); + } + if (exponent >= 0) { + mpz_mul_2exp(numerator, numerator, (unsigned long) exponent); + } else { + mpz_mul_2exp(denominator, denominator, (unsigned long) -exponent); + } + mpq_init(result); + mpq_set_num(result, numerator); + mpq_set_den(result, denominator); + mpq_canonicalize(result); + mpz_clear(denominator); + mpz_clear(numerator); + return true; +} + +static bool +field_rational(lc_mpfi_slice field, mpq_t result) +{ + uint64_t bits; + + return decode_bits(field, &bits) && bits_to_rational(bits, result); +} + +static bool +field_to_interval(lc_mpfi_slice field, mpfi_ptr output) +{ + uint64_t bits; + + if (!decode_bits(field, &bits)) { + return false; + } + return lc_mpfi_set_dyadic_bits(output, bits) == LC_MPFI_OK; +} + +static bool +fixed_one(lc_mpfi_slice field) +{ + return field.length == 1 && field.bytes[0] == 1; +} + +static bool +parse_definition( + lc_mpfi_job *job, + lc_mpfi_slice encoded, + mpfr_prec_t precision, + lc_mpfi_wire_error *error +) +{ + static const size_t prefix_lengths[22] = { + sizeof(definition_domain) - 1, 1, 1, 1, 1, 1, 1, 4, 1, 1, 4, + 8, 8, 1, 1, 1, 32, 1, 8, 8, 8, 8, + }; + mpfi_reader input = {encoded.bytes, encoded.length, 0, error}; + lc_mpfi_slice fields[22]; + uint64_t knot_count; + mpq_t adapting; + mpq_t background; + mpq_t metric_aa; + mpq_t metric_ab; + mpq_t metric_bb; + mpq_t determinant; + mpq_t product; + + for (size_t index = 0; index < 22; ++index) { + if (!read_blob(&input, prefix_lengths[index], fields + index)) { + return false; + } + } + knot_count = 0; + for (size_t index = 0; index < 8; ++index) { + knot_count = (knot_count << 8) | fields[21].bytes[index]; + } + if (knot_count == 0) { + return reject(&input, LC_MPFI_WIRE_NONCANONICAL); + } + if (knot_count > LC_MPFI_MAX_KNOTS_V1) { + return reject(&input, LC_MPFI_WIRE_RESOURCE_LIMIT); + } + if (knot_count > SIZE_MAX / 64 + || available(&input) != (size_t) knot_count * 64) { + return reject(&input, LC_MPFI_WIRE_NONCANONICAL); + } + if (memcmp(fields[0].bytes, definition_domain, sizeof(definition_domain) - 1) != 0) { + return reject(&input, LC_MPFI_WIRE_UNKNOWN_RELEASE); + } + for (size_t index = 1; index <= 17; ++index) { + bool required = index == 1 || index == 2 || index == 3 || index == 4 + || index == 5 || index == 6 || index == 8 || index == 9 + || index == 14 || index == 15 || index == 17; + + if (required && !fixed_one(fields[index])) { + return reject(&input, LC_MPFI_WIRE_UNKNOWN_RELEASE); + } + } + if (memcmp(fields[7].bytes, "\x01\x01\x01\x01", 4) != 0 + || memcmp(fields[10].bytes, "\x01\x01\x01\x01", 4) != 0 + || fields[13].bytes[0] < 1 || fields[13].bytes[0] > 3 + || memcmp(fields[16].bytes, formula_release_v1, 32) != 0) { + return reject(&input, LC_MPFI_WIRE_UNKNOWN_RELEASE); + } + bool adapting_ok = field_rational(fields[11], adapting); + bool background_ok = field_rational(fields[12], background); + + if (!adapting_ok || !background_ok + || mpq_sgn(adapting) <= 0 + || mpq_sgn(background) <= 0 + || mpq_cmp_ui(background, 1, 1) > 0) { + if (adapting_ok) { + mpq_clear(adapting); + } + if (background_ok) { + mpq_clear(background); + } + return reject(&input, LC_MPFI_WIRE_NONCANONICAL); + } + mpq_clear(adapting); + mpq_clear(background); + + bool metric_aa_ok = field_rational(fields[18], metric_aa); + bool metric_ab_ok = field_rational(fields[19], metric_ab); + bool metric_bb_ok = field_rational(fields[20], metric_bb); + + if (!metric_aa_ok || !metric_ab_ok || !metric_bb_ok) { + if (metric_aa_ok) { + mpq_clear(metric_aa); + } + if (metric_ab_ok) { + mpq_clear(metric_ab); + } + if (metric_bb_ok) { + mpq_clear(metric_bb); + } + return reject(&input, LC_MPFI_WIRE_NONCANONICAL); + } + mpq_init(determinant); + mpq_init(product); + mpq_mul(determinant, metric_aa, metric_bb); + mpq_mul(product, metric_ab, metric_ab); + mpq_sub(determinant, determinant, product); + if (mpq_sgn(metric_aa) <= 0 || mpq_sgn(determinant) <= 0) { + mpq_clear(product); + mpq_clear(determinant); + mpq_clear(metric_bb); + mpq_clear(metric_ab); + mpq_clear(metric_aa); + return reject(&input, LC_MPFI_WIRE_NONCANONICAL); + } + mpq_clear(product); + mpq_clear(determinant); + + mpfi_init2(&job->context[0], precision); + mpfi_init2(&job->context[1], precision); + job->context_ready = true; + if (!field_to_interval(fields[11], &job->context[0]) + || !field_to_interval(fields[12], &job->context[1])) { + return reject(&input, LC_MPFI_WIRE_NONCANONICAL); + } + job->surround = fields[13].bytes[0]; + memcpy(job->formula_release, fields[16].bytes, 32); + if (!lc_mpfi_region_init(&job->region, (size_t) knot_count, precision)) { + return reject(&input, LC_MPFI_WIRE_ALLOCATION_FAILED); + } + job->region_ready = true; + if (!field_to_interval(fields[18], &job->region.metric_aa) + || !field_to_interval(fields[19], &job->region.metric_ab) + || !field_to_interval(fields[20], &job->region.metric_bb)) { + return reject(&input, LC_MPFI_WIRE_NONCANONICAL); + } + bool have_previous_tone = false; + mpq_t previous_tone; + + for (size_t index = 0; index < (size_t) knot_count; ++index) { + lc_mpfi_slice knot_fields[4]; + lc_mpfi_region_knot *target = job->region.knots + index; + mpq_t tone; + mpq_t radius; + mpq_t center_a; + mpq_t center_b; + bool tone_ok; + bool radius_ok; + bool center_a_ok; + bool center_b_ok; + + for (size_t coordinate = 0; coordinate < 4; ++coordinate) { + if (!read_blob(&input, 8, knot_fields + coordinate)) { + if (have_previous_tone) { + mpq_clear(previous_tone); + } + return false; + } + } + tone_ok = field_rational(knot_fields[0], tone); + radius_ok = field_rational(knot_fields[3], radius); + center_a_ok = field_rational(knot_fields[1], center_a); + center_b_ok = field_rational(knot_fields[2], center_b); + if (!tone_ok || !radius_ok || !center_a_ok || !center_b_ok + || mpq_sgn(radius) < 0 + || (have_previous_tone && mpq_cmp(tone, previous_tone) <= 0)) { + if (tone_ok) { + mpq_clear(tone); + } + if (radius_ok) { + mpq_clear(radius); + } + if (center_a_ok) { + mpq_clear(center_a); + } + if (center_b_ok) { + mpq_clear(center_b); + } + if (have_previous_tone) { + mpq_clear(previous_tone); + } + return reject(&input, LC_MPFI_WIRE_NONCANONICAL); + } + if (have_previous_tone) { + mpq_clear(previous_tone); + } + mpq_init(previous_tone); + mpq_set(previous_tone, tone); + have_previous_tone = true; + mpq_clear(radius); + mpq_clear(tone); + mpq_clear(center_a); + mpq_clear(center_b); + if (!field_to_interval(knot_fields[0], &target->tone) + || !field_to_interval(knot_fields[1], &target->center_a) + || !field_to_interval(knot_fields[2], &target->center_b) + || !field_to_interval(knot_fields[3], &target->radius_squared)) { + if (have_previous_tone) { + mpq_clear(previous_tone); + } + return reject(&input, LC_MPFI_WIRE_NONCANONICAL); + } + } + if (have_previous_tone) { + mpq_clear(previous_tone); + } + return finish(&input); +} + +static bool +parse_domain( + lc_mpfi_domain *domain, + lc_mpfi_slice encoded, + const uint8_t expected[32], + lc_mpfi_wire_error *error +) +{ + mpfi_reader input = {encoded.bytes, encoded.length, 0, error}; + uint8_t release; + uint64_t range_count; + uint64_t maximum; + uint64_t total = 0; + + if (!expect(&input, domain_magic, sizeof(domain_magic), LC_MPFI_WIRE_BAD_MAGIC) + || !read_u8(&input, &release) + || release != 1 + || !read_u64(&input, &domain->point_count) + || domain->point_count == 0 + || domain->point_count > UINT64_C(0x1000000) + || !read_u64(&input, &range_count)) { + return *input.error != LC_MPFI_WIRE_OK + ? false + : reject(&input, LC_MPFI_WIRE_NONCANONICAL); + } + maximum = domain->point_count; + if (UINT64_C(0x1000001) - domain->point_count < maximum) { + maximum = UINT64_C(0x1000001) - domain->point_count; + } + if (range_count == 0 || range_count > maximum + || range_count > SIZE_MAX / sizeof(*domain->ranges) + || range_count > available(&input) / 8 + || (size_t) range_count * 8 != available(&input)) { + return reject(&input, LC_MPFI_WIRE_LENGTH_OUT_OF_BOUNDS); + } + domain->ranges = calloc((size_t) range_count, sizeof(*domain->ranges)); + if (domain->ranges == NULL) { + return reject(&input, LC_MPFI_WIRE_ALLOCATION_FAILED); + } + domain->range_count = (size_t) range_count; + for (size_t index = 0; index < domain->range_count; ++index) { + lc_mpfi_ordinal_range *range = domain->ranges + index; + + if (!read_u32(&input, &range->start) || !read_u32(&input, &range->end)) { + return false; + } + if (range->start >= range->end || range->end > UINT32_C(0x1000000) + || (index != 0 && range->start <= domain->ranges[index - 1].end)) { + return reject(&input, LC_MPFI_WIRE_NONCANONICAL); + } + total += (uint64_t) range->end - range->start; + } + if (total != domain->point_count || !finish(&input)) { + return *input.error != LC_MPFI_WIRE_OK + ? false + : reject(&input, LC_MPFI_WIRE_NONCANONICAL); + } + content_identity( + domain_identity_label, + sizeof(domain_identity_label) - 1, + encoded.bytes, + encoded.length, + domain->identity + ); + return memcmp(domain->identity, expected, 32) == 0 + || reject(&input, LC_MPFI_WIRE_DIGEST_MISMATCH); +} + +static bool +parse_policy( + lc_mpfi_policy *policy, + lc_mpfi_slice encoded, + const uint8_t expected[32], + lc_mpfi_wire_error *error +) +{ + mpfi_reader input = {encoded.bytes, encoded.length, 0, error}; + uint8_t equality_release; + uint8_t comparator_count; + + if (!expect(&input, policy_magic, sizeof(policy_magic), LC_MPFI_WIRE_BAD_MAGIC) + || !read_u8(&input, &equality_release) + || !read_u8(&input, &comparator_count)) { + return false; + } + if (equality_release != 1 || comparator_count != 2) { + return reject(&input, LC_MPFI_WIRE_UNKNOWN_RELEASE); + } + for (uint8_t expected_kind = 1; expected_kind <= 2; ++expected_kind) { + uint8_t kind; + uint32_t rung_count; + uint32_t previous = 0; + size_t minimum_tail = expected_kind == 1 ? 41 : 16; + uint32_t *ladder = NULL; + + if (!read_u8(&input, &kind) || !read_u32(&input, &rung_count)) { + return false; + } + if (kind != expected_kind || rung_count == 0 + || available(&input) < minimum_tail + || rung_count > (available(&input) - minimum_tail) / 4) { + return reject(&input, LC_MPFI_WIRE_NONCANONICAL); + } + if (rung_count > LC_MPFI_MAX_POLICY_RUNGS_V1) { + return reject(&input, LC_MPFI_WIRE_RESOURCE_LIMIT); + } + if (expected_kind == 2) { + if ((size_t) rung_count > SIZE_MAX / sizeof(*policy->precision_ladder)) { + return reject(&input, LC_MPFI_WIRE_LENGTH_OUT_OF_BOUNDS); + } + ladder = calloc(rung_count, sizeof(*ladder)); + if (ladder == NULL) { + return reject(&input, LC_MPFI_WIRE_ALLOCATION_FAILED); + } + } + for (size_t index = 0; index < rung_count; ++index) { + uint32_t precision; + + if (!read_u32(&input, &precision)) { + free(ladder); + return false; + } + if (precision == 0 || (index != 0 && precision <= previous) + || (uint64_t) precision > (uint64_t) MPFR_PREC_MAX) { + free(ladder); + return reject(&input, LC_MPFI_WIRE_NONCANONICAL); + } + if (precision > LC_MPFI_MAX_PRECISION_BITS_V1) { + free(ladder); + return reject(&input, LC_MPFI_WIRE_RESOURCE_LIMIT); + } + if (ladder != NULL) { + ladder[index] = precision; + } + previous = precision; + } + if (expected_kind == 1) { + uint64_t ignored; + + if (!read_u64(&input, &ignored) || !read_u64(&input, &ignored)) { + free(ladder); + return false; + } + } else { + if (!read_u64(&input, &policy->per_point_work) + || !read_u64(&input, &policy->global_pregrant)) { + free(ladder); + return false; + } + policy->precision_ladder = ladder; + policy->precision_count = rung_count; + } + } + if (!finish(&input)) { + return false; + } + content_identity( + policy_identity_label, + sizeof(policy_identity_label) - 1, + encoded.bytes, + encoded.length, + policy->identity + ); + return memcmp(policy->identity, expected, 32) == 0 + || reject(&input, LC_MPFI_WIRE_DIGEST_MISMATCH); +} + +static bool +formula_matches(lc_mpfi_slice formula) +{ + lc_mpfi_sha256 state; + uint8_t encoded_length[8]; + uint8_t digest[32]; + + if (formula.length != formula_spec_length) { + return false; + } + lc_mpfi_write_u64_be(encoded_length, (uint64_t) formula.length); + lc_mpfi_sha256_init(&state); + lc_mpfi_sha256_update(&state, formula_domain, sizeof(formula_domain) - 1); + lc_mpfi_sha256_update(&state, encoded_length, sizeof(encoded_length)); + lc_mpfi_sha256_update(&state, formula.bytes, formula.length); + lc_mpfi_sha256_finish(&state, digest); + return memcmp(digest, formula_release_v1, sizeof(formula_release_v1)) == 0; +} + +bool +lc_mpfi_parse_job( + lc_mpfi_job *job, + const uint8_t *bytes, + size_t length, + lc_mpfi_wire_error *error +) +{ + mpfi_reader input; + lc_mpfi_slice definition; + lc_mpfi_slice formula; + lc_mpfi_slice domain; + lc_mpfi_slice policy; + lc_mpfi_slice definition_digest; + lc_mpfi_slice declared_formula; + lc_mpfi_slice domain_identity; + lc_mpfi_slice policy_identity; + uint8_t actual[32]; + + memset(job, 0, sizeof(*job)); + *error = LC_MPFI_WIRE_OK; + if (length > (size_t) LC_MPFI_MAX_JOB_BYTES_V1) { + *error = LC_MPFI_WIRE_RESOURCE_LIMIT; + return false; + } + input = (mpfi_reader) {bytes, length, 0, error}; + if (!expect(&input, job_magic, sizeof(job_magic), LC_MPFI_WIRE_BAD_MAGIC) + || !take(&input, 32, &definition_digest) + || !read_blob(&input, SIZE_MAX, &definition) + || !take(&input, 32, &declared_formula) + || !read_blob(&input, formula_spec_length, &formula) + || !take(&input, 32, &domain_identity) + || !read_blob(&input, SIZE_MAX, &domain) + || !take(&input, 32, &policy_identity) + || !read_blob(&input, SIZE_MAX, &policy) + || !finish(&input)) { + lc_mpfi_job_clear(job); + return false; + } + lc_mpfi_sha256_bytes(definition.bytes, definition.length, actual); + if (memcmp(actual, definition_digest.bytes, 32) != 0) { + *error = LC_MPFI_WIRE_DIGEST_MISMATCH; + lc_mpfi_job_clear(job); + return false; + } + if (!parse_policy(&job->policy, policy, policy_identity.bytes, error) + || job->policy.precision_count == 0 + || !parse_domain(&job->domain, domain, domain_identity.bytes, error)) { + lc_mpfi_job_clear(job); + return false; + } + job->maximum_precision = job->policy.precision_ladder[ + job->policy.precision_count - 1 + ]; + if (!parse_definition(job, definition, job->maximum_precision, error) + || memcmp(declared_formula.bytes, job->formula_release, 32) != 0 + || !formula_matches(formula) + || memcmp(declared_formula.bytes, formula_release_v1, 32) != 0) { + if (*error == LC_MPFI_WIRE_OK) { + *error = LC_MPFI_WIRE_DIGEST_MISMATCH; + } + lc_mpfi_job_clear(job); + return false; + } + content_identity( + job_identity_label, + sizeof(job_identity_label) - 1, + bytes, + length, + job->job_identity + ); + return true; +} + +void +lc_mpfi_job_clear(lc_mpfi_job *job) +{ + free(job->policy.precision_ladder); + free(job->domain.ranges); + if (job->region_ready) { + lc_mpfi_region_clear(&job->region); + } + if (job->context_ready) { + mpfi_clear(&job->context[1]); + mpfi_clear(&job->context[0]); + } + memset(job, 0, sizeof(*job)); +} + +void +lc_mpfi_domain_iterator_init( + lc_mpfi_domain_iterator *iterator, + const lc_mpfi_domain *domain +) +{ + iterator->domain = domain; + iterator->range_index = 0; + iterator->ordinal = domain->ranges[0].start; + iterator->emitted = 0; +} + +bool +lc_mpfi_domain_iterator_next( + lc_mpfi_domain_iterator *iterator, + uint32_t *ordinal +) +{ + if (iterator->emitted == iterator->domain->point_count) { + return false; + } + *ordinal = iterator->ordinal; + ++iterator->emitted; + ++iterator->ordinal; + if (iterator->ordinal == iterator->domain->ranges[iterator->range_index].end + && iterator->emitted != iterator->domain->point_count) { + ++iterator->range_index; + iterator->ordinal = iterator->domain->ranges[iterator->range_index].start; + } + return true; +} + +void +lc_mpfi_ordinal_to_rgb(uint32_t ordinal, uint8_t rgb[3]) +{ + rgb[0] = (uint8_t) (ordinal >> 16); + rgb[1] = (uint8_t) (ordinal >> 8); + rgb[2] = (uint8_t) ordinal; +} + +const char * +lc_mpfi_wire_error_name(lc_mpfi_wire_error error) +{ + static const char *const names[] = { + "ok", + "truncated", + "trailing_bytes", + "length_out_of_bounds", + "bad_magic", + "unknown_release", + "noncanonical", + "digest_mismatch", + "allocation_failed", + "resource_limit", + }; + + return (unsigned) error < sizeof(names) / sizeof(names[0]) + ? names[error] + : "unknown_wire_error"; +} + +bool +lc_mpfi_write_all(int descriptor, const uint8_t *bytes, size_t length) +{ + while (length != 0) { + ssize_t written = write(descriptor, bytes, length); + + if (written < 0) { + if (errno == EINTR) { + continue; + } + return false; + } + if (written == 0) { + return false; + } + bytes += (size_t) written; + length -= (size_t) written; + } + return true; +} diff --git a/proof/region/v1/mpfi/evaluator/wire.h b/proof/region/v1/mpfi/evaluator/wire.h new file mode 100644 index 00000000..18c35a74 --- /dev/null +++ b/proof/region/v1/mpfi/evaluator/wire.h @@ -0,0 +1,104 @@ +#ifndef LABCOLOR_MPFI_WIRE_H +#define LABCOLOR_MPFI_WIRE_H + +#include +#include +#include + +#include "region.h" + +/* + * M1.5's direct executable has an explicit resource profile. These are + * operational admission bounds, not mathematical restrictions on the + * contextual-region wire grammar; M2a must bind the same profile to its + * controller/executor limits before minting any observation. + */ +#define LC_MPFI_MAX_JOB_BYTES_V1 \ + (UINT64_C(16) * UINT64_C(1024) * UINT64_C(1024)) +#define LC_MPFI_MAX_OUTPUT_BYTES_V1 \ + (UINT64_C(16) * UINT64_C(1024) * UINT64_C(1024)) +#define LC_MPFI_MAX_PRECISION_BITS_V1 UINT32_C(4096) +#define LC_MPFI_MAX_POLICY_RUNGS_V1 UINT32_C(32) +#define LC_MPFI_MAX_KNOTS_V1 UINT64_C(1024) + +typedef enum { + LC_MPFI_WIRE_OK = 0, + LC_MPFI_WIRE_TRUNCATED = 1, + LC_MPFI_WIRE_TRAILING_BYTES = 2, + LC_MPFI_WIRE_LENGTH_OUT_OF_BOUNDS = 3, + LC_MPFI_WIRE_BAD_MAGIC = 4, + LC_MPFI_WIRE_UNKNOWN_RELEASE = 5, + LC_MPFI_WIRE_NONCANONICAL = 6, + LC_MPFI_WIRE_DIGEST_MISMATCH = 7, + LC_MPFI_WIRE_ALLOCATION_FAILED = 8, + LC_MPFI_WIRE_RESOURCE_LIMIT = 9 +} lc_mpfi_wire_error; + +typedef struct { + const uint8_t *bytes; + size_t length; +} lc_mpfi_slice; + +typedef struct { + uint32_t start; + uint32_t end; +} lc_mpfi_ordinal_range; + +typedef struct { + lc_mpfi_ordinal_range *ranges; + size_t range_count; + uint64_t point_count; + uint8_t identity[32]; +} lc_mpfi_domain; + +typedef struct { + uint32_t *precision_ladder; + size_t precision_count; + uint64_t per_point_work; + uint64_t global_pregrant; + uint8_t identity[32]; +} lc_mpfi_policy; + +typedef struct { + const lc_mpfi_domain *domain; + size_t range_index; + uint32_t ordinal; + uint64_t emitted; +} lc_mpfi_domain_iterator; + +typedef struct { + lc_mpfi_region region; + __mpfi_struct context[2]; + uint8_t surround; + lc_mpfi_domain domain; + lc_mpfi_policy policy; + uint8_t formula_release[32]; + uint8_t job_identity[32]; + mpfr_prec_t maximum_precision; + bool context_ready; + bool region_ready; +} lc_mpfi_job; + +bool lc_mpfi_parse_job( + lc_mpfi_job *job, + const uint8_t *bytes, + size_t length, + lc_mpfi_wire_error *error +); +void lc_mpfi_job_clear(lc_mpfi_job *job); +void lc_mpfi_domain_iterator_init( + lc_mpfi_domain_iterator *iterator, + const lc_mpfi_domain *domain +); +bool lc_mpfi_domain_iterator_next( + lc_mpfi_domain_iterator *iterator, + uint32_t *ordinal +); +void lc_mpfi_ordinal_to_rgb(uint32_t ordinal, uint8_t rgb[3]); +const char *lc_mpfi_wire_error_name(lc_mpfi_wire_error error); + +bool lc_mpfi_write_all(int descriptor, const uint8_t *bytes, size_t length); +void lc_mpfi_write_u32_be(uint8_t output[4], uint32_t value); +void lc_mpfi_write_u64_be(uint8_t output[8], uint64_t value); + +#endif diff --git a/proof/region/v1/mpfi/operations.py b/proof/region/v1/mpfi/operations.py new file mode 100755 index 00000000..c99ca237 --- /dev/null +++ b/proof/region/v1/mpfi/operations.py @@ -0,0 +1,219 @@ +#!/usr/bin/env python3 +"""Machine-readable operation boundary for the MPFI comparator. + +This file is intentionally small: it is the source-level gate for the +evaluator, not a claim about every symbol shipped by the MPFI distribution. +The dependency's broader API remains outside the comparator's authority. + +The gate is deliberately conservative. A forbidden dependency name is +rejected wherever it appears, not only when it is followed by ``(``: a macro, +function pointer, or assembler alias can otherwise hide the call from a +call-shaped regular expression. +""" + +from __future__ import annotations + +import re +import sys +from pathlib import Path + + +ENGINE = "mpfi" +COMPILER_FAMILY = "clang" +TARGET = "x86_64-pc-linux-gnu" +COMPILE_FLAGS = ( + "-std=c17", + "-O2", + "-fno-fast-math", + "-ffp-contract=off", + "-fno-lto", + "-march=x86-64", + "-mtune=generic", +) + +# These are the only MPFI calls the evaluator is allowed to make. GMP/MPFR +# calls used to construct exact inputs and to serialize witness bounds are a +# separate dependency boundary and are listed below rather than silently +# widened by a future source edit. +ALLOWED_MPFI_CALLS = frozenset( + { + "mpfi_abs", + "mpfi_add", + "mpfi_cbrt", + "mpfi_clear", + "mpfi_cos", + "mpfi_div", + "mpfi_exp", + "mpfi_get_left", + "mpfi_get_prec", + "mpfi_get_right", + "mpfi_has_zero", + "mpfi_init2", + "mpfi_intersect", + "mpfi_interv_fr", + "mpfi_interv_si", + "mpfi_is_empty", + "mpfi_is_nonneg", + "mpfi_is_nonpos", + "mpfi_is_pos", + "mpfi_is_strictly_neg", + "mpfi_is_strictly_pos", + "mpfi_is_zero", + "mpfi_log", + "mpfi_mul", + "mpfi_set", + "mpfi_set_q", + "mpfi_set_si", + "mpfi_set_ui", + "mpfi_sin", + "mpfi_sqrt", + "mpfi_sub", + "mpfi_union", + } +) + +FORBIDDEN_MPFI_CALLS = frozenset( + { + "mpfi_atan2", + "mpfi_div_ext", + "mpfi_exp10", + "mpfi_rec_sqrt", + "mpfi_set_ld", + } +) + +ALLOWED_MPFR_CALLS = frozenset( + { + "mpfr_clear", + "mpfr_clears", + "mpfr_cmp", + # MPFI's interval intersection implementation reaches this MPFR + # helper through its public operation; keep the linked ABI closed + # without mistaking the helper for a new evaluator operation. + "mpfr_cmp3", + "mpfr_free_str", + "mpfr_get_str", + "mpfr_init2", + "mpfr_inits2", + "mpfr_max", + "mpfr_min", + } +) + +ALLOWED_GMP_CALLS = frozenset( + { + "mpq_canonicalize", + "mpq_clear", + "mpq_cmp", + "mpq_cmp_ui", + "mpq_init", + "mpq_mul", + "mpq_set", + "mpq_set_den", + "mpq_set_num", + "mpq_sgn", + "mpq_sub", + "mpz_clear", + # GMP's rational comparison/canonicalization path may emit this + # transitive limb comparison even when source calls stay mpq-only. + "mpz_cmp", + "mpz_init_set_ui", + "mpz_mul_2exp", + "mpz_neg", + } +) + +_CALL = re.compile(r"\b((?:mpfi|mpfr|mpq|mpz)_[A-Za-z0-9_]+)\s*\(") +def called_symbols(source: str) -> frozenset[str]: + return frozenset(_CALL.findall(source)) + + +def undefined_symbols(nm_output: str) -> frozenset[str]: + """Extract dependency symbols from ``nm -u`` without trusting formatting.""" + + symbols: set[str] = set() + for line in nm_output.splitlines(): + fields = line.split() + if not fields: + continue + symbol = fields[-1].lstrip("_") + # ELF GMP exports commonly spell mpq/mpz calls as __gmpq/__gmpz; + # normalize that ABI spelling before comparing the closed call set. + if symbol.startswith("gmp") and len(symbol) > 4 and symbol[3] != "_": + symbol = "mp" + symbol[3:] + if symbol.startswith(("mpfi_", "mpfr_", "mpq_", "mpz_")): + symbols.add(symbol) + return frozenset(symbols) + + +def validate_undefined_symbols(nm_output: str) -> tuple[str, ...]: + """Check the symbols the compiler left unresolved in evaluator objects.""" + + seen = undefined_symbols(nm_output) + allowed = ALLOWED_MPFI_CALLS | ALLOWED_MPFR_CALLS | ALLOWED_GMP_CALLS + errors: list[str] = [] + errors.extend( + f"forbidden undefined external symbol {symbol}" + for symbol in sorted(seen & FORBIDDEN_MPFI_CALLS) + ) + errors.extend( + f"unexpected undefined external symbol {symbol}" + for symbol in sorted(seen - allowed - FORBIDDEN_MPFI_CALLS) + ) + return tuple(errors) + + +def validate_sources(directory: Path) -> tuple[str, ...]: + paths = sorted(directory.glob("*.c")) + sorted(directory.glob("*.h")) + if not paths: + return ("evaluator source directory is empty",) + errors: list[str] = [] + seen: set[str] = set() + for path in paths: + text = path.read_text(encoding="utf-8") + seen.update(called_symbols(text)) + # Token-pasting can construct an operation name that this source gate + # cannot enumerate. The linked undefined-symbol gate is a second + # defence, but admitting such source would make the static contract + # depend on the compiler rather than remain auditable from the tree. + if "##" in text: + errors.append(f"{path.name}: token-pasting is forbidden") + for forbidden in FORBIDDEN_MPFI_CALLS: + if re.search(rf"\b{re.escape(forbidden)}\b", text): + errors.append(f"{path.name}: forbidden operation {forbidden}") + for marker in ("arb", "flint", "long double", "strtod", "fallback"): + if marker in text.lower(): + errors.append(f"{path.name}: forbidden dependency marker {marker}") + allowed = ALLOWED_MPFI_CALLS | ALLOWED_MPFR_CALLS | ALLOWED_GMP_CALLS + errors.extend( + f"unexpected external call {symbol}" + for symbol in sorted(seen - allowed) + ) + errors.extend( + f"required MPFI call is absent {symbol}" + for symbol in sorted(ALLOWED_MPFI_CALLS - seen) + ) + return tuple(errors) + + +def main(argv: list[str]) -> int: + if len(argv) == 2: + errors = validate_sources(Path(argv[1])) + elif len(argv) == 3 and argv[1] == "--undefined-symbols": + errors = validate_undefined_symbols(Path(argv[2]).read_text(encoding="utf-8")) + else: + print( + "usage: operations.py EVALUATOR_DIRECTORY | " + "--undefined-symbols NM_OUTPUT", + file=sys.stderr, + ) + return 2 + if errors: + for error in errors: + print(error, file=sys.stderr) + return 1 + return 0 + + +if __name__ == "__main__": + raise SystemExit(main(sys.argv)) diff --git a/proof/region/v1/mpfi/tests/gate.py b/proof/region/v1/mpfi/tests/gate.py new file mode 100644 index 00000000..763755a2 --- /dev/null +++ b/proof/region/v1/mpfi/tests/gate.py @@ -0,0 +1,82 @@ +#!/usr/bin/env python3 +"""Запускает обязательный MPFI source-contract gate с anti-vacuum inventory.""" + +from __future__ import annotations + +import hashlib +import sys +import unittest +from collections.abc import Iterator +from pathlib import Path + + +TEST_DIRECTORY = Path(__file__).resolve().parent +EXPECTED_TEST_COUNT = 20 +EXPECTED_TEST_INVENTORY_SHA256 = "f8151cf70a0e26b6e3df9b6c0e3f73f0ae369013529a7545b109c622ec8533bc" +_RUNTIME_REASON = "set LABCOLORS_MPFI_EVALUATOR to the controlled C17 binary" +EXPECTED_SKIPS = frozenset( + { + ( + "test_evaluator_source.RuntimeTests.test_frozen_fixture_produces_a_canonical_transcript", + _RUNTIME_REASON, + ), + ( + "test_evaluator_source.RuntimeTests.test_black_exact_zero_emits_the_canonical_trace_witness", + _RUNTIME_REASON, + ), + ( + "test_evaluator_source.RuntimeTests.test_input_limit_is_enforced_before_wire_parse", + _RUNTIME_REASON, + ), + } +) + + +def _iter_tests(suite: unittest.TestSuite) -> Iterator[unittest.TestCase]: + for item in suite: + if isinstance(item, unittest.TestSuite): + yield from _iter_tests(item) + elif isinstance(item, unittest.TestCase): + yield item + else: + raise TypeError("suite contains a non-test object") + + +def _inventory_digest(test_ids: tuple[str, ...]) -> str: + preimage = b"".join(test_id.encode("utf-8") + b"\n" for test_id in sorted(test_ids)) + return hashlib.sha256(preimage).hexdigest() + + +def run_gate() -> int: + suite = unittest.defaultTestLoader.discover( + str(TEST_DIRECTORY), + pattern="test_*.py", + ) + tests = tuple(_iter_tests(suite)) + test_ids = tuple(test.id() for test in tests) + actual_digest = _inventory_digest(test_ids) + if ( + not tests + or len(test_ids) != EXPECTED_TEST_COUNT + or len(set(test_ids)) != len(test_ids) + or actual_digest != EXPECTED_TEST_INVENTORY_SHA256 + ): + print( + "MPFI source gate inventory drift: " + f"count={len(test_ids)} sha256={actual_digest} " + f"expected_count={EXPECTED_TEST_COUNT} " + f"expected_sha256={EXPECTED_TEST_INVENTORY_SHA256}", + file=sys.stderr, + ) + return 1 + result = unittest.TextTestRunner(verbosity=2).run(suite) + actual_skips = frozenset((test.id(), reason) for test, reason in result.skipped) + if actual_skips != EXPECTED_SKIPS: + print(f"unexpected skips: {sorted(actual_skips - EXPECTED_SKIPS)!r}", file=sys.stderr) + print(f"missing skips: {sorted(EXPECTED_SKIPS - actual_skips)!r}", file=sys.stderr) + return 1 + return int(bool(result.failures or result.errors)) + + +if __name__ == "__main__": + raise SystemExit(run_gate()) diff --git a/proof/region/v1/mpfi/tests/test_evaluator_source.py b/proof/region/v1/mpfi/tests/test_evaluator_source.py new file mode 100644 index 00000000..142827d2 --- /dev/null +++ b/proof/region/v1/mpfi/tests/test_evaluator_source.py @@ -0,0 +1,553 @@ +#!/usr/bin/env python3 +"""Hostile source and runtime contract for the independent MPFI evaluator.""" + +from __future__ import annotations + +import hashlib +import os +import subprocess +import sys +import tempfile +import unittest +from pathlib import Path + +MPFI = Path(__file__).resolve().parents[1] +EVALUATOR = MPFI / "evaluator" +ENTRYPOINT = MPFI / "build.sh" +RECIPE = MPFI / "build-inner.sh" +REPO = MPFI.parents[3] +FORMULA = REPO / "crates/labcolors-core/contracts/contextual-region-formula-v1.lcir" +GENERATOR = EVALUATOR / "formula.py" +sys.path.insert(0, str(MPFI.parent)) + +from mpfi import operations # noqa: E402 + + +def generate(source: bytes) -> subprocess.CompletedProcess[bytes]: + with tempfile.TemporaryDirectory() as temporary: + path = Path(temporary) / "formula.lcir" + path.write_bytes(source) + return subprocess.run( + [sys.executable, str(GENERATOR), str(path)], + check=False, + capture_output=True, + stdin=subprocess.DEVNULL, + timeout=60, + env={ + "PATH": os.environ.get("PATH", ""), + "PYTHONDONTWRITEBYTECODE": "1", + "PYTHONHASHSEED": "0", + }, + ) + + +class FormulaSourceTests(unittest.TestCase): + def test_registered_formula_is_deterministic_and_has_no_binary64_path(self) -> None: + source = FORMULA.read_bytes() + first = generate(source) + second = generate(source) + + self.assertEqual(first.returncode, 0, first.stderr.decode()) + self.assertEqual(second.returncode, 0, second.stderr.decode()) + self.assertEqual(first.stdout, second.stdout) + self.assertEqual( + hashlib.sha256(first.stdout).hexdigest(), + "a8df7529261ba68e8fbf591cff283ec88a35cb98958b293bc7885d9fb4dd0fb6", + ) + self.assertIn(b"lc_mpfi_formula_point", first.stdout) + self.assertIn(b"lc_mpfi_formula_segment", first.stdout) + self.assertIn(b"lc_mpfi_formula_singleton", first.stdout) + self.assertNotIn(b"double", first.stdout) + + def test_formula_mutations_are_rejected_before_c_output(self) -> None: + source = FORMULA.read_bytes() + mutations = ( + (b"labcolors_exact_real_ssa 1", b"labcolors_exact_real_ssa 2"), + (b"operator add 2 real exact_x_plus_y", b"operator add 2 real exact_x_minus_y"), + (b"literal p1_7 3ffb333333333333", b"literal p1_7 3ffb333333333334"), + (b"rule boundary inclusive", b"rule boundary exclusive"), + (b"point_nodes 226", b"point_nodes 225"), + ) + for needle, replacement in mutations: + with self.subTest(replacement=replacement): + self.assertIn(needle, source) + result = generate(source.replace(needle, replacement, 1)) + self.assertNotEqual(result.returncode, 0) + self.assertEqual(result.stdout, b"") + for mutant in (source + b"\n", source.replace(b"\n", b"\r\n", 1)): + result = generate(mutant) + self.assertNotEqual(result.returncode, 0) + self.assertEqual(result.stdout, b"") + + def test_generator_does_not_import_the_protocol_or_the_other_engine(self) -> None: + source = GENERATOR.read_text(encoding="utf-8") + for forbidden in ( + "region_proof_protocol", + "controller", + "import arb", + "import flint", + "import numpy", + "import scipy", + ): + self.assertNotIn(forbidden, source) + + +class EvaluatorSourceTests(unittest.TestCase): + def test_public_build_entrypoint_cannot_be_bypassed_by_an_environment_sentinel(self) -> None: + entrypoint = ENTRYPOINT.read_text(encoding="utf-8") + recipe = RECIPE.read_text(encoding="utf-8") + + self.assertIn("/usr/bin/env -i", entrypoint) + self.assertIn("/usr/bin/readlink -f", entrypoint) + self.assertIn('inner="$script_dir/build-inner.sh"', entrypoint) + self.assertIn('/bin/sh "$inner"', entrypoint) + self.assertLess( + entrypoint.index("exec /usr/bin/env -i"), + entrypoint.index("script_path="), + ) + self.assertNotIn("LC_MPFI_BUILD_ENV_V1", entrypoint) + self.assertNotIn("LC_MPFI_BUILD_ENV_V1", recipe) + self.assertNotIn("/usr/bin/env -i", recipe) + + def test_source_owned_dispatch_cleans_child_environment(self) -> None: + with tempfile.TemporaryDirectory() as temporary: + root = Path(temporary) + entrypoint = root / "build.sh" + inner = root / "build-inner.sh" + observed = root / "environment" + entrypoint.write_text(ENTRYPOINT.read_text(encoding="utf-8"), encoding="utf-8") + entrypoint.chmod(0o755) + inner.write_text( + "#!/bin/sh\n" + f"/usr/bin/env | /usr/bin/sort > '{observed}'\n", + encoding="utf-8", + ) + result = subprocess.run( + [str(entrypoint)], + check=False, + capture_output=True, + text=True, + env={ + "LC_MPFI_BUILD_ENV_V1": "1", + "MAKEFLAGS": "--jobserver-auth=spoof", + "PYTHONPATH": "/host-controlled", + "CONFIG_SITE": "/host-controlled/site", + "PATH": "/host-controlled/bin", + }, + ) + self.assertEqual(result.returncode, 0, result.stderr) + environment = observed.read_text(encoding="utf-8") + self.assertIn("PATH=/usr/bin:/bin\n", environment) + for forbidden in ( + "LC_MPFI_BUILD_ENV_V1=1", + "MAKEFLAGS=--jobserver-auth=spoof", + "PYTHONPATH=/host-controlled", + "CONFIG_SITE=/host-controlled/site", + "PATH=/host-controlled/bin", + ): + self.assertNotIn(forbidden, environment) + + def test_source_tree_is_complete_and_operation_closed(self) -> None: + required = ( + "main.c", + "wire.c", + "wire.h", + "hash.c", + "hash.h", + "interval.c", + "interval.h", + "region.c", + "region.h", + "formula.h", + "formula.py", + ) + for name in required: + with self.subTest(name=name): + self.assertTrue((EVALUATOR / name).is_file(), name) + self.assertEqual(operations.validate_sources(EVALUATOR), ()) + + def test_mutating_an_allowed_call_to_a_forbidden_operation_is_red(self) -> None: + with tempfile.TemporaryDirectory() as temporary: + copy = Path(temporary) + for path in EVALUATOR.glob("*.c"): + (copy / path.name).write_text(path.read_text(encoding="utf-8"), encoding="utf-8") + for path in EVALUATOR.glob("*.h"): + (copy / path.name).write_text(path.read_text(encoding="utf-8"), encoding="utf-8") + interval = copy / "interval.c" + interval.write_text( + interval.read_text(encoding="utf-8").replace( + "mpfi_div(output, left, right)", + "mpfi_div_ext(output, left, right)", + 1, + ), + encoding="utf-8", + ) + errors = operations.validate_sources(copy) + self.assertTrue(any("forbidden operation mpfi_div_ext" in error for error in errors)) + + def test_forbidden_operation_aliases_and_asm_names_are_red(self) -> None: + with tempfile.TemporaryDirectory() as temporary: + copy = Path(temporary) + for path in EVALUATOR.glob("*.c"): + (copy / path.name).write_text(path.read_text(encoding="utf-8"), encoding="utf-8") + for path in EVALUATOR.glob("*.h"): + (copy / path.name).write_text(path.read_text(encoding="utf-8"), encoding="utf-8") + interval = copy / "interval.c" + interval.write_text( + interval.read_text(encoding="utf-8") + + "\n#define hidden_division mpfi_div_ext\n" + + "static void hidden_call(void) { hidden_division; }\n" + + 'static const char *hidden_asm_name = "mpfi_div_ext";\n', + encoding="utf-8", + ) + errors = operations.validate_sources(copy) + self.assertTrue(any("forbidden operation mpfi_div_ext" in error for error in errors)) + + interval.write_text( + interval.read_text(encoding="utf-8") + + "\n#define LABCOLOR_MPFI_NAME(part) mpfi_ ## part\n" + + "static void hidden_token(mpfi_ptr output, mpfi_srcptr left, mpfi_srcptr right) {\n" + + " LABCOLOR_MPFI_NAME(div_ext)(output, left, right);\n" + + "}\n", + encoding="utf-8", + ) + errors = operations.validate_sources(copy) + self.assertTrue(any("token-pasting" in error for error in errors)) + + def test_linked_undefined_operation_symbols_are_closed(self) -> None: + errors = operations.validate_undefined_symbols( + " U _mpfi_div_ext\n" + " U mpfi_div\n" + " U __gmpz_init_set_ui\n" + ) + self.assertEqual(errors, ("forbidden undefined external symbol mpfi_div_ext",)) + self.assertEqual( + operations.validate_undefined_symbols(" U mpfi_formula_point\n"), + ("unexpected undefined external symbol mpfi_formula_point",), + ) + self.assertEqual( + operations.validate_undefined_symbols(" U __gmpz_not_allowed\n"), + ("unexpected undefined external symbol mpz_not_allowed",), + ) + self.assertEqual( + operations.validate_undefined_symbols( + " U mpfr_cmp3\n" + " U __gmpz_cmp\n" + ), + (), + ) + + def test_elf_absence_checks_are_fail_closed_on_inspection_error(self) -> None: + recipe = RECIPE.read_text(encoding="utf-8") + start = recipe.index("require_absent_pattern()") + end = recipe.index("\nrequire_regular", start) + checker = recipe[start:end] + with tempfile.TemporaryDirectory() as temporary: + directory = Path(temporary) / "not-a-file" + directory.mkdir() + failed = subprocess.run( + ["/bin/sh", "-c", checker + "\nrequire_absent_pattern X \"$1\" message inspection\n", "sh", str(directory)], + check=False, + capture_output=True, + text=True, + ) + self.assertEqual(failed.returncode, 70) + + absent = Path(temporary) / "absent" + absent.write_text("nothing\n", encoding="utf-8") + passed = subprocess.run( + ["/bin/sh", "-c", checker + "\nrequire_absent_pattern X \"$1\" message inspection\n", "sh", str(absent)], + check=False, + capture_output=True, + text=True, + ) + self.assertEqual(passed.returncode, 0, passed.stderr) + + def test_build_recipe_is_closed_and_requires_clang_19(self) -> None: + recipe = RECIPE.read_text(encoding="utf-8") + self.assertIn("/usr/bin/clang-19", recipe) + self.assertIn("clang version 19\\.", recipe) + self.assertIn("-fno-fast-math", recipe) + self.assertIn("-ffp-contract=off", recipe) + self.assertIn("-fno-lto", recipe) + self.assertIn( + "readonly mpfi_test_exclusions='^(tdiv_ext|texp10|trec_sqrt)$'", + recipe, + ) + self.assertIn('/usr/bin/make check -j1 TESTS="$mpfi_tests"', recipe) + self.assertIn("mpfi-evaluator-v1", recipe) + self.assertIn("readelf", recipe) + self.assertIn("--undefined-only", recipe) + self.assertIn("--undefined-symbols", recipe) + self.assertNotIn("gcc", recipe.lower()) + + def test_upstream_test_inventory_observation_is_fail_closed(self) -> None: + recipe = RECIPE.read_text(encoding="utf-8") + self.assertIn( + 'if ! /usr/bin/make -pn > "$make_database"; then', + recipe, + ) + self.assertIn( + "' \"$make_database\"\n)", + recipe, + ) + self.assertNotIn( + "/usr/bin/make -pn \\\n | /usr/bin/awk", + recipe, + ) + + def test_compiler_admission_allows_a_stable_symlink_to_an_executable(self) -> None: + recipe = RECIPE.read_text(encoding="utf-8") + start = recipe.index("require_executable()") + end = recipe.index("\nrequire_empty_directory", start) + checker = recipe[start:end] + with tempfile.TemporaryDirectory() as temporary: + root = Path(temporary) + target = root / "clang-19" + target.write_text("#!/bin/sh\nexit 0\n", encoding="utf-8") + target.chmod(0o755) + link = root / "compiler" + link.symlink_to(target) + result = subprocess.run( + [ + "/bin/sh", + "-c", + checker + '\nrequire_executable "$1"\n', + "sh", + str(link), + ], + check=False, + capture_output=True, + text=True, + ) + self.assertEqual(result.returncode, 0, result.stderr) + + def test_clang_admission_accepts_distribution_version_banner(self) -> None: + recipe = RECIPE.read_text(encoding="utf-8") + start = recipe.index("require_clang_19()") + end = recipe.index("\nrequire_directory", start) + checker = recipe[start:end] + for banner in ("clang version 19.1.1", "Ubuntu clang version 19.1.1"): + with self.subTest(banner=banner), tempfile.TemporaryDirectory() as temporary: + compiler = Path(temporary) / "clang-19" + compiler.write_text( + f'#!/bin/sh\nprintf "%s\\n" "{banner}"\n', + encoding="utf-8", + ) + compiler.chmod(0o755) + result = subprocess.run( + [ + "/bin/sh", + "-c", + checker + '\nrequire_clang_19 "$1"\n', + "sh", + str(compiler), + ], + check=False, + capture_output=True, + text=True, + ) + self.assertEqual(result.returncode, 0, result.stderr) + + def test_clang_admission_rejects_a_failed_version_probe(self) -> None: + recipe = RECIPE.read_text(encoding="utf-8") + start = recipe.index("require_clang_19()") + end = recipe.index("\nrequire_directory", start) + checker = recipe[start:end] + with tempfile.TemporaryDirectory() as temporary: + compiler = Path(temporary) / "clang-19" + compiler.write_text( + '#!/bin/sh\nprintf "%s\\n" "clang version 19.1.1"\nexit 1\n', + encoding="utf-8", + ) + compiler.chmod(0o755) + result = subprocess.run( + [ + "/bin/sh", + "-c", + checker + '\nrequire_clang_19 "$1"\n', + "sh", + str(compiler), + ], + check=False, + capture_output=True, + text=True, + ) + self.assertEqual(result.returncode, 67, result.stderr) + + with tempfile.TemporaryDirectory() as temporary: + compiler = Path(temporary) / "clang-18" + compiler.write_text( + '#!/bin/sh\nprintf "%s\\n" "clang version 18.1.8"\n', + encoding="utf-8", + ) + compiler.chmod(0o755) + result = subprocess.run( + [ + "/bin/sh", + "-c", + checker + '\nrequire_clang_19 "$1"\n', + "sh", + str(compiler), + ], + check=False, + capture_output=True, + text=True, + ) + self.assertEqual(result.returncode, 67) + + def test_runtime_profile_is_explicit_and_checked_before_allocation(self) -> None: + wire = (EVALUATOR / "wire.h").read_text(encoding="utf-8") + wire_source = (EVALUATOR / "wire.c").read_text(encoding="utf-8") + main = (EVALUATOR / "main.c").read_text(encoding="utf-8") + for name in ( + "LC_MPFI_MAX_JOB_BYTES_V1", + "LC_MPFI_MAX_OUTPUT_BYTES_V1", + "LC_MPFI_MAX_PRECISION_BITS_V1", + "LC_MPFI_MAX_POLICY_RUNGS_V1", + "LC_MPFI_MAX_KNOTS_V1", + ): + with self.subTest(name=name): + self.assertIn(name, wire) + self.assertIn("LC_MPFI_MAX_JOB_BYTES_V1", wire_source) + self.assertIn("LC_MPFI_MAX_PRECISION_BITS_V1", wire_source) + self.assertIn("LC_MPFI_MAX_KNOTS_V1", wire_source) + self.assertIn("LC_MPFI_MAX_JOB_BYTES_V1", main) + self.assertIn("LC_MPFI_MAX_OUTPUT_BYTES_V1", main) + self.assertIn("output_limit", main) + + def test_no_pre_run_receipt_or_arb_compatibility_layer_exists(self) -> None: + self.assertFalse((MPFI / "receipt.py").exists()) + joined = "\n".join( + path.read_text(encoding="utf-8") + for path in EVALUATOR.glob("*.c") + ).lower() + for forbidden in ("arb", "flint", "fallback", "long double", "strtod"): + self.assertNotIn(forbidden, joined) + + +class RuntimeTests(unittest.TestCase): + @unittest.skipUnless( + os.environ.get("LABCOLORS_MPFI_EVALUATOR"), + "set LABCOLORS_MPFI_EVALUATOR to the controlled C17 binary", + ) + def test_frozen_fixture_produces_a_canonical_transcript(self) -> None: + executable = os.environ["LABCOLORS_MPFI_EVALUATOR"] + fixture = (REPO / "proof/region/v1/fixtures/proof-job-v1.bin").read_bytes() + manifest = bytes.fromhex("01" + "23" * 31) + result = subprocess.run( + [ + executable, + "--manifest-identity", + manifest.hex(), + "--job", + "/dev/stdin", + ], + input=fixture, + check=False, + capture_output=True, + timeout=300, + ) + self.assertEqual(result.returncode, 0, result.stderr.decode()) + self.assertEqual(result.stderr, b"") + sys.path.insert(0, str(REPO / "proof/region/v1")) + from region_proof_protocol import DecisionTranscriptV1 # noqa: PLC0415 + + transcript = DecisionTranscriptV1.parse(result.stdout) + self.assertEqual(transcript.encode(), result.stdout) + self.assertEqual(transcript.comparator_identity, manifest) + + @unittest.skipUnless( + os.environ.get("LABCOLORS_MPFI_EVALUATOR"), + "set LABCOLORS_MPFI_EVALUATOR to the controlled C17 binary", + ) + def test_black_exact_zero_emits_the_canonical_trace_witness(self) -> None: + sys.path.insert(0, str(REPO / "proof/region/v1")) + from region_proof_protocol import ( # noqa: PLC0415 + ComparatorBudgetV1, + ComparatorKindV1, + ContextualRegionDefinitionV1, + DecisionTranscriptV1, + ExactZeroSignalTraceV1, + ProofJobV1, + ProofPolicyV1, + ReducedDomainManifestV1, + ) + + registered = ContextualRegionDefinitionV1.parse( + (REPO / "proof/region/v1/fixtures/v5b2b-definition-0a8d1c3d.bin").read_bytes() + ) + zero = bytes(8) + definition = ContextualRegionDefinitionV1( + registered.fields[:21] + ((1).to_bytes(8, "big"),) + (zero,) * 4, + 1, + ) + policy = ProofPolicyV1( + 1, + ( + ComparatorBudgetV1(ComparatorKindV1.ARB, (128,), 1, 1), + ComparatorBudgetV1(ComparatorKindV1.MPFI, (192,), 1, 1), + ), + ) + job = ProofJobV1( + definition, + FORMULA.read_bytes(), + ReducedDomainManifestV1.from_ordinals((0,)), + policy, + ) + manifest = bytes.fromhex("ab" + "00" * 31) + result = subprocess.run( + [ + os.environ["LABCOLORS_MPFI_EVALUATOR"], + "--manifest-identity", + manifest.hex(), + "--job", + "/dev/stdin", + ], + input=job.encode(), + check=False, + capture_output=True, + timeout=300, + ) + self.assertEqual(result.returncode, 0, result.stderr.decode()) + transcript = DecisionTranscriptV1.parse(result.stdout) + self.assertEqual(tuple(transcript.iter_decisions()), (0,)) + self.assertEqual(transcript.counters, (1, 0, 0, 0)) + self.assertEqual(transcript.exact_equality_count, 1) + witness = tuple(transcript.iter_witnesses())[0] + self.assertIs(type(witness), ExactZeroSignalTraceV1) + self.assertEqual( + witness.trace_digest, + hashlib.sha256( + b"labcolors.proof-region.exact-zero-signal-trace.v1\0" + + job.identity + + (0).to_bytes(4, "big") + + (0).to_bytes(8, "big") + ).digest(), + ) + + @unittest.skipUnless( + os.environ.get("LABCOLORS_MPFI_EVALUATOR"), + "set LABCOLORS_MPFI_EVALUATOR to the controlled C17 binary", + ) + def test_input_limit_is_enforced_before_wire_parse(self) -> None: + result = subprocess.run( + [ + os.environ["LABCOLORS_MPFI_EVALUATOR"], + "--manifest-identity", + ("01" + "23" * 31), + "--job", + "/dev/stdin", + ], + input=bytes(16 * 1024 * 1024 + 1), + check=False, + capture_output=True, + timeout=60, + ) + self.assertNotEqual(result.returncode, 0) + self.assertEqual(result.stdout, b"") + self.assertEqual(result.stderr, b"job read failed: input_limit\n") + + +if __name__ == "__main__": + unittest.main() diff --git a/proof/region/v1/tests/test_mpfi_input.py b/proof/region/v1/tests/test_mpfi_input.py index 36c1c02e..64b2450d 100644 --- a/proof/region/v1/tests/test_mpfi_input.py +++ b/proof/region/v1/tests/test_mpfi_input.py @@ -757,7 +757,7 @@ def test_protocol_keeps_the_source_input_boundary_below_build_authority(self) -> reference, ) self.assertIn( - "MPFI sealed source input ещё не является MPFI build policy", + "MPFI sealed source input сам по себе не является MPFI build policy", transport_reference, ) self.assertIn("engine-owned input binding", transport_reference)