diff --git a/Project.toml b/Project.toml new file mode 100644 index 0000000..6a71c41 --- /dev/null +++ b/Project.toml @@ -0,0 +1,17 @@ +name = "Apodeixis" +uuid = "7d8c4f3a-6a31-4f21-9c72-1d496dd2ad67" +authors = ["Apodeixis.jl contributors"] +version = "0.1.0" + +[deps] +JuliaSyntax = "70703baa-626e-46a2-a12c-08ffd08c73b4" + +[compat] +julia = "1.9" +JuliaSyntax = "0.4, 1" + +[extras] +Test = "8dfed614-e22c-5e08-85e1-65c5234f0b40" + +[targets] +test = ["Test"] diff --git a/README.adoc b/README.adoc index bb804a4..86fab35 100644 --- a/README.adoc +++ b/README.adoc @@ -1,172 +1,88 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell // SPDX-FileCopyrightText: 2024-2026 Jonathan D.A. Jewell (hyperpolymath) -= {{PROJECT_NAME}} += Apodeixis.jl :toc: -:toc-placement: preamble +:toclevels: 2 -// ── Licensing ─────────────────────────────────────────────────────────────── -image:https://img.shields.io/badge/Code-MPL--2.0-blue.svg?logo=mozilla[Code licence: MPL-2.0,link="https://opensource.org/licenses/MPL-2.0"] -image:https://img.shields.io/badge/Docs-CC--BY--SA--4.0-blue.svg?logo=creativecommons[Docs licence: CC-BY-SA-4.0,link="https://creativecommons.org/licenses/by-sa/4.0/"] -image:https://img.shields.io/badge/Provenance-Quantum--Safe-blueviolet[Quantum-Safe Provenance,link="docs/legal/EXHIBIT-B-QUANTUM-SAFE.txt"] - -// ── Standard & quality gates ──────────────────────────────────────────────── -image:https://img.shields.io/badge/RSR-Rhodium_Standard-9C27B0[Rhodium Standard Repository,link="https://github.com/hyperpolymath/rhodium-standard-repositories"] -image:https://img.shields.io/endpoint?url=https://raw.githubusercontent.com/{{OWNER}}/{{REPO}}/governance-badges/badges/k9.json[K9 conformance,link="https://github.com/{{OWNER}}/{{REPO}}/actions/workflows/dogfood-gate.yml"] -image:https://www.bestpractices.dev/projects/{{OPENSSF_BP_ID}}/badge[OpenSSF Best Practices,link="https://www.bestpractices.dev/projects/{{OPENSSF_BP_ID}}"] -image:https://api.scorecard.dev/projects/github.com/{{OWNER}}/{{REPO}}/badge[OpenSSF Scorecard,link="https://scorecard.dev/viewer/?uri=github.com/{{OWNER}}/{{REPO}}"] -image:https://sonarcloud.io/api/project_badges/measure?project={{OWNER}}_{{REPO}}&metric=alert_status[SonarQube Quality Gate,link="https://sonarcloud.io/summary/new_code?id={{OWNER}}_{{REPO}}"] -image:https://archive.softwareheritage.org/badge/origin/https://{{FORGE}}/{{OWNER}}/{{REPO}}/[Archived in Software Heritage,link="https://archive.softwareheritage.org/browse/origin/?origin_url=https://{{FORGE}}/{{OWNER}}/{{REPO}}"] - -// ── Provenance & ecosystem ────────────────────────────────────────────────── -image:https://img.shields.io/badge/Idris-Inside-5E5086?logo=idris&logoColor=white[Idris Inside,link="https://github.com/hyperpolymath/proven"] -image:https://img.shields.io/badge/Zig-Zero--overhead-F7A41D?logo=zig&logoColor=black[Zig Zero-overhead FFI,link="https://github.com/hyperpolymath/typed-wasm"] -image:https://api.thegreenwebfoundation.org/greencheckimage/{{FORGE}}[Green Web,link="https://www.thegreenwebfoundation.org/green-web-check/?url={{FORGE}}"] - -{{PROJECT_DESCRIPTION}} +Apodeixis.jl is an early-stage Julia verification toolchain project. Its goal is +to connect Julia source contracts and compiler-specialized code with explicit +numeric semantics, memory/FFI proofs, and independently checked proof +certificates. The long-term design targets JuliaSyntax.jl, typed SSA from +`code_typed` / `Core.Compiler`, and an Idris2 + Zig boundary integrated with +Why3/SMT, Dedukti, Coq, and Lean. [IMPORTANT] ==== -*This file is a template.* You are reading `README.adoc` from the *RSR template repo* -(or a freshly-cloned copy of it). Run `just repo-init` to replace every `{{PLACEHOLDER}}` -token with your project's details, then delete this admonition. Until you do, the -`{{...}}` markers below are intentional placeholders, not content. +*Verification status:* the current executable is a source-policy audit, not a +formal verifier. A `POLICY CLEAN` result does not prove a contract, bounds +safety, type stability, allocation behavior, ABI correctness, or functional +safety. The typed-SSA analysis, VC generation, solver integration, and +Warrant-to-Receipt pipeline are planned work, not implemented features. ==== -== What this is - -A new repository scaffolded from the *Rhodium Standard Repository (RSR)* template: -a batteries-included starting point that ships with CI/CD, machine-readable project -metadata, an AI-agent gatekeeper protocol, a formally-typed ABI/FFI seam -(Idris2 + Zig), container and reproducible-build scaffolding, and governance -infrastructure — all wired and passing the RSR validators on day one. +== What exists today -Replace this section with a description of *your* project once initialised. +* A Julia package using JuliaSyntax.jl to parse source without expanding or + executing user macros. +* A fail-closed policy audit for selected unsafe constructs, unmodeled foreign + calls, unknown macros in `@verified` functions, and `@inbounds` placement. +* A CLI at `scripts/apodeixis.jl` and focused package tests. +* Architecture and implementation-plan documents describing the intended + frontend, numeric tiers, array/FFI seam, proof evidence, and staged roadmap. +* Idris2 ABI and Zig build scaffolding under `src/interface/`; these are + starting points, not yet a complete, target-validated Julia FFI proof seam. == Quick start +Julia 1.9 or newer is declared in the package compatibility bounds. Runtime +validation of the package is pending; see the implementation plan. + [source,bash] ---- -# 1. Create a repo from this template (or clone it), then from the repo root: -just repo-init # interactive bootstrap: fills every {{PLACEHOLDER}} - -# 2. See the available tasks: -just # lists all phases (build, test, validate, audit, ...) - -# 3. Check the repo still satisfies the RSR shape: -just validate # structure + metadata checks +julia --project=. -e 'using Pkg; Pkg.instantiate()' +julia --project=. -e 'using Pkg; Pkg.test()' +julia --project=. scripts/apodeixis.jl --help +julia --project=. scripts/apodeixis.jl audit path/to/source.jl ---- -`just repo-init` prompts for the project name, owner, author, licence contact, and the -other values listed in `.machine_readable/ai/PLACEHOLDERS.adoc`, substitutes them -across the tree, validates the result, and (if available) runs the `k9-svc` checks. - -[[ai-install]] -== AI-Assisted Installation (Recommended) +For a source file containing `@inbounds`, the initial policy checker also +requires a mutation-score percentage: -=== Just say it - -Say this to any AI assistant that can read a URL and run commands (or give you -commands to paste): - -[source,text] +[source,bash] ---- -Create a new repository from https://github.com/hyperpolymath/rsr-template-repo +julia --project=. scripts/apodeixis.jl audit --mutation-score 97.5 path/to/source.jl ---- -The URL is the key: it leads the assistant to -link:docs/AI_INSTALLATION_GUIDE.adoc[`docs/AI_INSTALLATION_GUIDE.adoc`], the -complete step-by-step recipe. The assistant checks your system, installs the -prerequisites, instantiates the template with `just repo-init`, and verifies the -result with `just doctor`. +This caller-supplied percentage currently satisfies only a policy gate. It is +not authenticated test evidence and does not discharge a bounds verification +condition. `@inbounds` remains unverified until the planned typed-SSA and VC +passes exist. -* "Set up rsr-template-repo so I can work on the template itself — https://github.com/hyperpolymath/rsr-template-repo" -* `./launcher.sh --ai-setup` (or `just ai-setup`) prints the line and the guide path. +== Design and implementation -=== What you will be asked +* link:docs/architecture/APODEIXIS-VERIFICATION-DESIGN.adoc[Verification architecture] — hybrid frontend, four numeric tiers, memory discipline, FFI seam, worked example, and proof lifecycle. +* link:docs/architecture/APODEIXIS-MVP-IMPLEMENTATION-PLAN.adoc[MVP implementation plan] — existing package slice, ordered implementation work, and acceptance gates. +* link:docs/architecture/APODEIXIS-ULTRAPLAN.adoc[Ultra-plan] — dependency-ordered work packages, acceptance gates, risks, and contributor handoff protocol. +* link:src/interface/Abi/README.adoc[ABI interface scaffolding] — current Idris2 ABI files and their limitations. -. Your operating system (Linux, macOS, or Windows via WSL2). -. The new project's name, owner, author and licence contact (the values listed in - `.machine_readable/ai/PLACEHOLDERS.adoc`). -. To confirm the privacy notice below. +The numeric design keeps mathematical integers/rationals, fixed-width +bitvectors, strict IEEE-754 values, and probabilistic evidence separate. +Statistical warrants are never treated as deterministic functional-safety +proofs. Full details and unsupported boundaries are recorded in the design +document. -=== Privacy and security +== Development status -[IMPORTANT] -==== -Setting up rsr-template-repo clones this repository and installs its developer -tools per-user with mise (no administrator rights, nothing sent anywhere). -`just repo-init` rewrites files only inside the new checkout; it creates no -remote repository and pushes nothing until you do. -==== +This is research-stage software with an intentionally narrow first slice. Julia +package tests have been added but must be run in a Julia-enabled environment +before the package is treated as runtime-validated. Each implementation phase +must add adversarial negative tests and preserve explicit `UNKNOWN` / +`UNSUPPORTED` outcomes; tests, JET reports, mutation scores, and benchmarks are +evidence and gates, not formal proofs. + +== License -=== Minting without a terminal - -Agents and CI can mint non-interactively: set `RSR_NON_INTERACTIVE=1` and pass -the answers as environment variables named like the prompts' variables in -`build/just/repo-init.just` (`PROJECT_NAME`, `REPO`, `OWNER`, `AUTHOR` and -`AUTHOR_EMAIL` are required; any other answer left unset is blank or takes its -default). Piping the answers to stdin in prompt order also works. - -=== Troubleshooting - -Run `just doctor`; each FAIL carries a code explained in -link:docs/SETUP.adoc#troubleshooting[`docs/SETUP.adoc` §Troubleshooting], and -`just heal` applies the automatic fixes. Prefer to do it yourself? The full -manual route is link:docs/SETUP.adoc[`docs/SETUP.adoc`]; developers and -maintainers can brief an AI with `just ai-warmup dev` / `just ai-warmup maintainer`. - -== What you get - -* *Machine-readable metadata* (`.machine_readable/descriptiles/`) — `STATE`, `META`, - `ECOSYSTEM`, `PLAYBOOK`, `AGENTIC`, `NEUROSYM`, `CLADE`, and `anchors/ANCHOR`, - in deed, so tools and agents can read the project's state and boundaries. -* *AI gatekeeper protocol* — `rsr-template-repo_chora.deed` (the repo deed) is the - universal entry point that tells an AI agent how to work in this repo before it - touches anything; it carries the AI allocation policy and the ply directory tree. -* *Typed ABI/FFI seam* — `src/interface/Abi/` (Idris2 type + layout proofs) over - `src/interface/ffi/` (Zig implementation), with generated C headers. -* *CI/CD* — GitHub Actions for quality, security (CodeQL, Scorecard, secret - scanning), multi-forge mirroring, and RSR anti-pattern enforcement. -* *Supply-chain & reproducibility* — container layering (stapeln), Guix shells, - SBOM, and signing hooks. -* *Governance* — `GOVERNANCE.adoc`, `MAINTAINERS.adoc`, `.github/` community health - files, and a release `AUDIT.adoc` gate. - -== Repository map - -The authoritative map is generated, so it cannot drift from the tree: -link:docs/architecture/REPOSITORY-MAP.adoc[docs/architecture/REPOSITORY-MAP.adoc] -(regenerate with `just repo-map`; CI fails if it is stale). - -The short version: - -[cols="1,3"] -|=== -| Path | What lives there - -| `README.adoc`, `CLAUDE.md` | Start here - humans and AI agents respectively. -| `src/`, `tests/` | The code and its tests. -| `docs/` | Human documentation, including the full map above. -| `.machine_readable/` | Manifests, contractiles and policies that tools read. -| `build/`, `Justfile` | Every task runs through `just`; phases live in `build/just/`. -| `ci/`, `.github/` | CI configuration; GitHub reads `.github/` and no other path. -|=== - -== Where to go next - -* link:docs/architecture/REPOSITORY-MAP.adoc[The repository map] — generated; what every directory is for. -* link:docs/EXPLAINME.adoc[EXPLAINME] — the engineering deep-dive: how the pieces actually work. -* link:docs/AFFIRMATION.adoc[AFFIRMATION] — the dated, signed honesty snapshot of the repo's true state. -* link:docs/AUDIT.adoc[AUDIT] — the release audit gate. -* link:docs/AI_INSTALLATION_GUIDE.adoc[AI installation guide] — for agents instantiating this template. -* link:.machine_readable/ai/PLACEHOLDERS.adoc[PLACEHOLDERS] — the full placeholder reference. - -== Licence - -Code, configuration and scripts are link:LICENSE[Mozilla Public License 2.0] -(`MPL-2.0`); prose documentation is `CC-BY-SA-4.0`. Both texts live in -`LICENSES/`, and per-file `SPDX-License-Identifier` headers are authoritative. -The GitHub-detected licence is MPL-2.0 (the root `LICENSE`). Long-term -attribution uses Quantum-Safe Provenance — see -link:docs/legal/EXHIBIT-B-QUANTUM-SAFE.txt[the Quantum-Safe Provenance exhibit]. +Code and configuration are licensed under MPL-2.0. Documentation is licensed +under CC-BY-SA-4.0. See link:LICENSE[LICENSE] and the texts under +link:LICENSES/[LICENSES/]. diff --git a/docs/README.adoc b/docs/README.adoc index dc7274f..c92f082 100644 --- a/docs/README.adoc +++ b/docs/README.adoc @@ -13,6 +13,9 @@ and CI fails if it goes stale, so prefer it over any hand-written listing. * link:onboarding/QUICKSTART-MAINTAINER.adoc[QUICKSTART-MAINTAINER] — maintaining one. * link:AI_INSTALLATION_GUIDE.adoc[AI_INSTALLATION_GUIDE] — for an AI agent instantiating the template. * link:EXPLAINME.adoc[EXPLAINME] — how the pieces actually work. +* link:architecture/APODEIXIS-VERIFICATION-DESIGN.adoc[Apodeixis verification design] — compiler, proof, numeric, and FFI architecture. +* link:architecture/APODEIXIS-MVP-IMPLEMENTATION-PLAN.adoc[Apodeixis MVP implementation plan] — current implementation slice and acceptance gates. +* link:architecture/APODEIXIS-ULTRAPLAN.adoc[Apodeixis ultra-plan] — staged work packages, dependencies, risks, release gates, and handoff process. == The tracks diff --git a/docs/architecture/APODEIXIS-MVP-IMPLEMENTATION-PLAN.adoc b/docs/architecture/APODEIXIS-MVP-IMPLEMENTATION-PLAN.adoc new file mode 100644 index 0000000..da42ab4 --- /dev/null +++ b/docs/architecture/APODEIXIS-MVP-IMPLEMENTATION-PLAN.adoc @@ -0,0 +1,215 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) Jonathan D.A. Jewell += Apodeixis.jl Implementation Plan +:toc: +:toclevels: 3 +:sectnums: + +== Purpose and current state + +This plan turns the architecture in +link:APODEIXIS-VERIFICATION-DESIGN.adoc[APODEIXIS-VERIFICATION-DESIGN] into +incremental, reviewable software. It prefers a tiny sound subset and explicit +`UNSUPPORTED` results over broad but ungrounded claims. For the detailed +work-package dependency graph and contributor handoff protocol, see the +link:APODEIXIS-ULTRAPLAN.adoc[Apodeixis Ultra-Plan]. + +The first source-policy slice now exists: + +[cols="1,3",options="header"] +|=== +|Path |Current responsibility + +|`Project.toml` +|Julia package metadata; JuliaSyntax.jl is the only runtime dependency. + +|`src/Apodeixis.jl` +|Parse source without macro expansion; emit typed policy findings for + dynamic escapes, forbidden constructs, unelaborated macros, and `@inbounds` + gates. `:policy_clean` means only that this policy pass found no issue. + +|`scripts/apodeixis.jl` +|`audit` command-line wrapper; reports `POLICY CLEAN (NOT VERIFIED)` or + rejection, with line and finding code. + +|`test/runtests.jl` +|Parser, policy, mutation-score, unsafe construct, nested boundary, and input + validation cases, runnable with `julia --project=. -e 'using Pkg; Pkg.test()'`. +|=== + +Runtime validation is still pending because Julia is not installed in the +current implementation environment. The code must pass `Pkg.test()` in CI +before this initial slice is considered validated. The repository's existing +shell `check-no-placeholders` currently reports many pre-existing template +tokens; it is not evidence about the new implementation. + +== 0.1 CLI behavior + +[source,bash] +---- +julia --project=. scripts/apodeixis.jl --help +julia --project=. scripts/apodeixis.jl audit src/example.jl +julia --project=. scripts/apodeixis.jl audit --mutation-score 97.5 src/example.jl +julia --project=. -e 'using Pkg; Pkg.test()' +---- + +The audit never calls `include`, `eval`, or macro expansion. It operates on +JuliaSyntax's parsed `Expr` tree. Passing `--mutation-score 95` only satisfies +the configured *policy* threshold for an `@inbounds` occurrence; it does not +establish that the score came from a trusted run, prove bounds, or issue a +Warrant. A later CLI must replace this manually supplied value with a signed or +CI-originated test artifact before that gate is used as release evidence. + +The initial rule set rejects `@eval`, `@generated`, and `@fastmath` macros; +`eval` and `invokelatest` calls; unmodeled `ccall`/lowered foreign calls; global +declarations at file scope or inside functions; unknown macros inside +`@verified`; and `@inbounds` outside an annotated function or without the +mutation threshold. +Any parse failure is rejected. The names +`@verified`, `@pre`, `@post`, `@invariant`, `@cap`, `@tier`, `@noalloc`, and +`@echo` are recognized as syntax markers only. No annotation is expanded or +semantically trusted yet. + +== Sequenced implementation work + +Use one reviewable PR per slice. Do not merge a downstream proof feature until +its fail-closed tests and independent evidence boundary are in place. + +[cols="1,1,3,3",options="header"] +|=== +|Slice |State |Implementation tasks |Acceptance gate + +|A. Package bootstrap and source policy +|Code present; Julia tests not yet run +|Run Julia 1.9+ CI; fix all package and parser API errors; test CLI exit codes; + publish findings as stable API; add parser version and source hash to output. +|`Pkg.test()` green on lowest and newest supported Julia; malicious macro + fixture is never evaluated; `POLICY CLEAN` text explicitly remains + non-verification. + +|B. Contract syntax model +|Not started +|Introduce `ContractSpec`, `CapabilitySpec`, and `TierSpec`; recognize only + literal, bounded syntax for the seven contract/effect annotations + (`@pre`, `@post`, `@invariant`, `@cap`, `@tier`, `@noalloc`, and `@echo`); + treat `@verified` as a separate function marker; preserve + JuliaSyntax source ranges; reject duplicate, malformed, dynamic, or unknown + attributes. Add canonical serialization and golden parser fixtures. +|Every accepted annotation round-trips deterministically; tests show macro + bodies are data and never execute; no assertion is assumed at a call site. + +|C. Julia compiler adapter +|Not started +|Add a Julia-minor-versioned adapter layer over `code_typed` and narrowly + isolated `Core.Compiler` APIs. Capture concrete argument tuple, return type, + `CodeInfo`, world bounds if obtainable, call edges, SSA types, and compiler + version. Do not couple contract parser to private compiler structs. +|Golden IR tests run on each declared Julia minor; adapter returns + `UNSUPPORTED` on `Any`, dynamic dispatch, unknown intrinsic, unmodeled + `invoke`, or absent/stale world data. New methods/dependency hashes invalidate + prior analysis. + +|D. Closed calls and typed subset +|Not started +|Resolve method instances recursively under one captured world; add + allowlisted summaries for a handful of pure Base operations; reject open + dispatch, reflection, global writes, exceptions not in the model, and + unverified callees. Represent CFG/phi nodes in a small stable Apodeixis IR. +|Negative tests demonstrate no `Any` or unknown edge leaks into an accepted IR; + dispatch ambiguity and world mismatch are rejected; summary contracts are + independently unit-tested. + +|E. Tier 1 scalar proof slice +|Not started +|Implement affine expressions and branch conditions; separate integer + Presburger constraints from rational LRA; range-lift machine `Int` only with + explicit no-overflow VCs. Generate deterministic VCs and route to ECHIDNA's + supported Why3/SMT interface only after its request/response schema is fixed. +|Proof and counterexample fixtures; unsupported nonlinear terms report + `UNKNOWN`; replayable witnesses are checked independently. No successful + solver status alone is displayed as verified. + +|F. Tier 2 and loop/array contracts +|Not started +|Lower fixed-width operations to explicit signed/unsigned bitvectors; add + checked arithmetic semantics, vector bounds, affine footprints, loop + invariants, alias checking, and the first `@inbounds` VC discharge. +|Exhaustive small-width reference tests; overflow/bounds counterexamples; + aliasing SubArray adversarial cases; mutation test evidence recorded by CI; + bounds VCs still required regardless of mutation score. + +|G. Allocation and JET integration +|Not started +|Use JET.jl as a diagnostic reporter, plus a conservative typed-IR/escape + analysis for `@noalloc`; add warmed allocation regression tests and report + toolchain/target context. +|Reports are labeled diagnostic/test evidence, never proof. Unknown helper + summaries block a static no-allocation claim. Runtime measurement context is + in every report. + +|H. Idris2/Zig ABI contract +|Not started +|Define a generated ABI manifest with symbol, target, calling convention, + layout, ownership, lengths, aliasing, and no-retain. Generate C layout probes; + verify manifest against Idris2 proofs and ZigProve output; analyze + `GC.@preserve` spans and one-based-to-zero-based conversions. +|Mismatch, pointer escape, unsupported target, or missing no-retain proof + rejects the call. Negative integration tests cover each seam obligation; + no generic `ccall` is admitted. + +|I. IEEE Tier 3 and statistical Tier 4 +|Not started +|Introduce explicit IEEE IR and rounding/error nodes with `echo-types` residue + obligations; route only supported fragments to QF_FP/Gappa/interval checking. + Keep probabilistic outputs in a non-deterministic evidence namespace. +|Adversarial NaN/Inf/signed-zero/rounding tests; no Float-to-real coercion; + statistical warrants cannot satisfy deterministic verification gates. + +|J. ECHIDNA receipt and `echidnabot` +|Not started +|Canonicalize obligations, hash all source/compiler/ABI/solver dependencies + with BLAKE3, emit local `INCOMPLETE Warrant`, and batch-check Dedukti + witnesses in Coq + Lean before producing a `COMPLETE Receipt`. Add PR bot + with untrusted-cache isolation. +|A receipt is independently reproducible and invalidates on any bound input + change. Incomplete, stale, unknown, probabilistic, or untrusted-cache results + never become green verification status. +|=== + +== Engineering rules for every slice + +. *Status is a sum type, not a Boolean.* At minimum use `PROVED`, `REFUTED`, + `UNKNOWN`, `UNSUPPORTED`, and `POLICY_REJECTED`. Do not collapse timeouts and + unsupported constructs into success. +. *Keep adapters at the boundary.* JuliaSyntax and `Core.Compiler` data should + be translated to an internal normalized IR before checks are implemented. + Private compiler APIs live in one versioned module with tests; no private + compiler field is read throughout the whole codebase. +. *Every accepted feature has a negative test.* Test one valid case and + adversarial near-misses: malformed contract, changed dispatch, stale world, + overflow, alias, wrong ABI, solver unknown, missing proof witness. +. *Do not overstate tools.* JET, tests, mutation testing, benchmarking, and + runtime assertions are diagnostics/evidence. They may gate a proof feature, + but do not replace the semantic VC or its checked witness. +. *Version proof artifacts.* Include Julia version/build, target triple, + dependency manifest, method-instance/call graph fingerprints, contract + elaborator version, tier semantics, solver/checker versions, and ABI manifest + hash in any eventual receipt key. +. *Minimize trust.* Keep proof-producing search separate from witness checking; + run Coq and Lean checking in a trusted batch job. Treat Julia compiler output + as an untrusted input to the internal IR validator until its invariants are + checked. + +== Immediate next actions + +. Make Julia 1.9+ available in CI and run the current package suite; fix API or + syntax defects before adding semantic features. +. Expand CLI tests to invoke the executable itself and assert its exit status, + rather than testing only `audit_source`. +. Replace caller-supplied mutation-score trust with an explicit evidence + interface; until then use the score only for local policy experimentation. +. Add stable `AuditReport` serialization and version tags before downstream + integrations depend on the API. +. Implement the `ContractSpec` parser next; do not start solver dispatch until + there is a typed contract model and a single accepted scalar example can be + traced from source to a named VC. diff --git a/docs/architecture/APODEIXIS-ULTRAPLAN.adoc b/docs/architecture/APODEIXIS-ULTRAPLAN.adoc new file mode 100644 index 0000000..5beeed8 --- /dev/null +++ b/docs/architecture/APODEIXIS-ULTRAPLAN.adoc @@ -0,0 +1,677 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) Jonathan D.A. Jewell += Apodeixis.jl Ultra-Plan: A Buildable Route to a Verified Julia Subset +:toc: +:toclevels: 3 +:sectnums: + +== Mission and how to use this plan + +This is the execution plan for taking the current Apodeixis.jl repository from +its 0.1 source-policy audit to a small, useful, independently checkable Julia +verification toolchain. It is written so a future maintainer, contributor, or +coding agent can choose a bounded task, understand its prerequisites, implement +it without inventing trust claims, and leave a testable handoff. + +This plan is deliberately *not* a promise that the complete ambition can be +implemented in one pass. Build the smallest vertical slice that has a precise +semantics, an independent check, and adversarial tests. Do not begin downstream +solver, FFI, or bot integration while its prerequisites are still `UNKNOWN`. + +Use this document with: + +* link:APODEIXIS-VERIFICATION-DESIGN.adoc[Verification architecture] for the + semantic model and full trust boundaries. +* link:APODEIXIS-MVP-IMPLEMENTATION-PLAN.adoc[MVP implementation plan] for the + short roadmap and present feature breakdown. +* the current package: `Project.toml`, `src/Apodeixis.jl`, + `scripts/apodeixis.jl`, and `test/runtests.jl`. + +=== Project snapshot + +As of 2026-10-22, the repository has a Julia package using JuliaSyntax.jl, a +non-proving source-policy audit, a CLI, policy tests, an Idris2 ABI scaffold, +Zig build scaffolding, and architecture documents. Julia is not available in +the implementation environment recorded by the initial package work; run the +package tests in a Julia-enabled environment before relying on the code. The +source-policy report value `:policy_clean` is *not* `PROVED`, `VERIFIED`, or a +Warrant. The compiler adapter, contract elaborator, VC generator, ECHIDNA +transport, proof witnesses, ABI checker, and Receipt issuer do not exist yet. + +== Product boundary + +=== First real product target + +The first useful release target is not "verify Julia". It is: + +[quote] +____ +Given one annotated, closed, pure Julia function in a documented supported +subset, either produce a checked proof of its contract under explicit numeric +and compiler assumptions, produce a counterexample, or return an explicit +`UNKNOWN` / `UNSUPPORTED` result. +____ + +The first end-to-end proof should be a scalar Tier 1 affine function, with a +caller precondition, a postcondition, a named generated VC, and an independently +replayable proof result. Arrays, floating point, `@inbounds`, and FFI are later +milestones. + +=== Out of scope for early milestones + +* Sound verification of arbitrary Julia, dynamic dispatch, reflection, macros, + generated functions, world-age changes, tasks, or concurrent mutation. +* Trusting a solver's `unsat` string, a green test suite, JET silence, mutation + score, runtime assertion, or a `POLICY CLEAN` audit as a formal proof. +* Mapping `Float64` onto mathematical `Real` or conflating wrapping machine + arithmetic with unbounded integer arithmetic. +* Treating statistical/ML confidence as deterministic functional safety. +* Supporting arbitrary foreign calls, callbacks, retained pointers, or + unverified layout facts. + +Unsupported constructs must stop verification, not be ignored or erased. + +== Principles every contributor must preserve + +. *Fail closed:* each stage returns a typed status (`PROVED`, `REFUTED`, + `UNKNOWN`, `UNSUPPORTED`, or `POLICY_REJECTED`). Errors and timeouts are not + success. +. *One proof claim, one exact model:* every proof names its source hash, + specialized method/call graph, Julia version, target, dependency manifest, + tier semantics, assumptions, and checker versions. +. *No execution in the frontend:* JuliaSyntax parses the user's source; macro + contracts are parsed as restricted data. Do not `include`, `eval`, or expand + arbitrary user macros as part of analysis. +. *Separate syntax from compiler facts:* preserve source spans in the syntax + layer; isolate version-specific `Core.Compiler` / `CodeInfo` assumptions in + an adapter; lower both into a small internal IR. +. *Independent check:* proof search is outside the trusted checker. A local + Warrant remains `INCOMPLETE` until the independent Dedukti/Coq/Lean checking + pipeline has accepted the exact bound artifact. +. *Explicit arithmetic:* integer, rational, bitvector, IEEE, and probabilistic + semantics remain distinct in IR, VC, certificate, report, and cache key. +. *Negative tests are mandatory:* each admitted language feature needs tests + showing nearby unsupported or unsafe programs are rejected. +. *Small trusted base:* do not let solver APIs, compiler internals, or foreign + libraries leak across their adapter boundaries into general validation code. + +== Repository map for implementers + +[cols="1,2,3",options="header"] +|=== +|Path |Use it for |Do not use it for + +|`Project.toml` +|Package identity, dependency compatibility, test target. +|A generated or manually drifting dependency lock. Decide and document the + package's manifest/lock policy before claiming reproducible proof builds. + +|`src/Apodeixis.jl` +|Public package entry and the current policy-audit implementation. +|Permanent home for parser internals, compiler private APIs, or all future + passes in one large module. Split adapters as they become real. + +|`scripts/apodeixis.jl` +|Thin command-line parsing and presentation. +|Verification semantics or proof decisions duplicated outside the package. + +|`test/runtests.jl` +|Julia package tests, beginning with parser/policy behavior. +|A replacement for VC soundness tests, independent checker tests, or end-to-end + proof fixtures. + +|`src/interface/Abi/` +|Existing Idris2 types/layout scaffold; evolve into generated target-specific + contracts only after probing actual ABI facts. +|A claim that its template constants establish every target's ABI. + +|`src/interface/ffi/` +|Existing Zig integration scaffold. +|A claim that any Julia pointer is safe merely because Zig is used. + +|`verification/proofs/` +|Existing Agda, Coq, Idris2, Lean, and TLA+ scaffolding. Add proof packages + with explicit versions/manifests and runnable checks. +|A repository-wide certificate checker before its exact role and trust model + are proven. + +|`docs/architecture/` +|Architecture, roadmap, and handoff documents. +|A substitute for executable acceptance tests or verified behavior. +|=== + +Add generated output, caches, manifests, and temporary solver files only under +existing ignore/external-storage conventions. Do not commit build products or +proof databases unless a reviewed reproducibility design requires them. + +== Dependency graph and milestone gates + +[cols="1,2,2,3",options="header"] +|=== +|Milestone |Needs |Deliver |Cannot claim yet + +|M0. Runtime baseline +|Repository baseline +|Julia-enabled test/CI path, supported Julia versions, reproducible package + load, passing parser/policy suite. +|Any semantic verification result. + +|M1. Surface contract model +|M0 +|Non-executing parser for contracts, tiers, capabilities, source locations, + normalized serialization, explicit parser errors. +|A precondition is not yet assumed or a postcondition proved. + +|M2. Compiler facts adapter +|M0 + M1 +|Version-isolated typed-code adapter, specialization request model, type/call + graph facts, target/world/dependency fingerprint or explicit unsupported. +|A closed call graph until every reachable edge is accounted for. + +|M3. Internal IR and closed core +|M1 + M2 +|Small normalized IR, function boundary/CFG model, effects and supported call + summaries, typed result states. +|Any VC result until lowering is tested against defined semantics. + +|M4. Tier 1 end-to-end scalar proof +|M3 +|Affine integer/rational VC generation, Why3/SMT request, negative model, checked + proof witness and report for one closed kernel. +|Tier 2 machine integer, float, array, or FFI safety. + +|M5. Tier 2 arrays and loops +|M4 +|Explicit QF_BV semantics, checked overflow, vector bounds/borrow model, + invariants, proof-backed first `@inbounds`. +|Generic views/aliasing or allocation claims beyond supported model. + +|M6. FFI proof seam +|M5 + ABI facts + Idris2/Zig checker capability +|One target-specific manifest and Julia preserve/conversion + layout + Zig + no-retain proof for one wrapper. +|Arbitrary `ccall`, other target triples, callbacks, retained pointers. + +|M7. Tier 3 / Tier 4 separation +|M3 + proof checker path +|Strict IEEE operation/error model and a separate statistical evidence status. +|Float-to-real substitution or deterministic claims from statistical evidence. + +|M8. Receipts, cache, CI bot +|At least one verified vertical slice; stable proof wire protocol +|BLAKE3 dependency key, INCOMPLETE Warrant, independent COMPLETE Receipt, + cache invalidation and least-privilege PR reporting. +|A green bot check before independent receipt validation. +|=== + +Dependency order is a safety constraint. M6 may proceed in parallel with M7 +only after the internal IR and receipt contract are stable; it must not invent a +separate status or trust model. M8 comes after a proof can be independently +checked locally; do not build the bot first and retrofit trust later. + +== Work packages and execution checklists + +Each package has one primary output, a completion gate, and an explicit stop +condition. A PR may split a work package into smaller changes, but must not +claim the whole package complete while its gate is red. + +=== WP-00 — Runtime, environment, and current tests + +*State:* immediate; runtime validation outstanding. + +*Tasks:* + +. Run on Julia 1.9 (declared compatibility floor) and current stable Julia. +. Instantiate `Project.toml`, run `Pkg.test()`, the CLI help path, and a CLI + audit against positive and negative fixture files. +. Fix parser API or syntax issues; pin supported dependency ranges and decide + whether to commit a `Manifest.toml` for CI/dev tooling or keep the package as + a library without a committed lock. +. Add a Julia CI workflow using the repository's existing action pinning and + `actions.lock` conventions; include the Julia workflow in the lock file and + run the repository action-lock consistency check. +. Check formatter/linter policy after adding the workflow; do not bypass a red + mandatory job with `continue-on-error`. +. Record all commands, Julia build strings, OS and outcomes in the PR. + +*Completion gate:* tests pass on floor and current stable, CLI exit status and +messages are tested, action locks are current, no source or macro is executed +by the parser tests. + +*Stop if:* JuliaSyntax's API differs, package load fails, or a test reveals +macro expansion. Repair the base before adding contract semantics. + +=== WP-01 — Stabilize the audit/report API + +*Tasks:* + +. Define stable status and diagnostic types; keep `POLICY CLEAN` explicitly + distinct from proof statuses. +. Add report schema version, tool version, filename/source digest, parser version, + deterministic finding ordering and deterministic text/JSON serialization. +. Test qualified and unqualified calls/macros, nesting, line spans, parse error + nodes, quoted syntax, aliases/indirection limitations, and CLI exit codes. +. Correct scope rules so a finding only applies to the proof region it claims to + audit; document constructs a purely syntactic scan cannot soundly identify. +. Remove the CLI's trust in an arbitrary mutation score as a proof-like fact. + For now label it as a user-supplied local gate, not evidence. Design a CI + artifact schema before consuming a measured score. + +*Completion gate:* deterministic snapshots, stable diagnostic documentation, +full CLI integration test, and no `:policy_clean` wording that implies safety. + +*Stop if:* the syntax tree cannot identify a construct without executing code; +return `UNSUPPORTED` and preserve the source location. + +=== WP-02 — Contract and capability syntax model + +*Target API:* `parse_contracts(source)::ParseReport{ContractUnit}`. + +*Types to define:* `ContractUnit`, `FunctionDecl`, `ContractSpec`, `ExprTerm`, +`CapabilitySet`, `NumericTier`, `SourceSpan`, `ParseDiagnostic`. Keep the AST +independent of `JuliaSyntax` node layouts after normalization. + +*Tasks:* + +. Design grammar for only `@verified`, `@pre`, `@post`, `@invariant`, `@cap`, + `@tier`, `@noalloc`, and `@echo` forms. Specify whether declaration macros + attach to a function prefix or appear in a body; support one syntax initially. +. Accept only literals, local identifiers, approved operators, named logical + predicates, and finite type annotations. Reject interpolation, macro calls in + contract expressions, dynamic lookup, arbitrary function execution, malformed + names, duplicate tier declarations, and conflicting effect declarations. +. Normalize alpha-renamable binders, preserve source spans, and serialize a + deterministic structural form. Names may be removed for alpha-equivalence + only when binding structure and types remain intact. +. Add grammar fixtures for each accepted form and near miss. Assert no + `eval`, macro expansion, `include`, or method dispatch over user expressions. +. Add round-trip/canonicalization tests that show equivalent spelling has the + same normalized representation and inequivalent binding/type has a different + representation. + +*Completion gate:* parser is pure data transformation, diagnostics identify +source ranges, golden representation tests are stable across supported Julia +minors, every unsupported expression rejects the function from later analysis. + +*Stop if:* a contract expression needs ordinary Julia evaluation to interpret. +Defer it rather than introduce execution. + +=== WP-03 — Supported Julia version and compiler adapter + +*Target API:* `specialize(entry, argtypes, world_policy)::CompilerFacts`. + +*Tasks:* + +. Pick a narrow Julia compatibility matrix and explain what is stable public API + versus `Core.Compiler` private API. Pin at least one test runtime for each + adapter implementation. +. Build an adapter module per supported Julia minor or adapter family. It alone + may read version-specific `CodeInfo`, `MethodInstance`, inference results, + world counters, or call edges. +. Capture concrete method signature, return type, SSA IR, call targets, argument + and SSA slot types, source identity, compilation flags, target triple, and + applicable world data where obtainable. +. Never promise a globally frozen Julia world. Model a closed analysis snapshot: + capture world/dependency fingerprints, identify new applicable methods or + invalidations where possible, and re-run analysis when any dependency changes. +. Confirm whether `code_typed` can provide required facts without relying on + undocumented internals. If not, isolate the private adapter and prove its + output invariants before downstream passes consume it. +. Add fixtures for concrete dispatch, abstract `Any`, dynamic call, `invoke`, + keyword lowering, recursion, generated method, method ambiguity, dependency + change, and unsupported builtin/intrinsic. + +*Completion gate:* adapter returns facts plus version tag, not proof. Unknown +call edge, unresolved `Any`, unsupported intrinsic, incomplete world facts, or +unrecognized IR node produces `UNSUPPORTED` / `UNKNOWN`, never an empty graph. +Golden adapter tests run on every supported Julia version. + +*Stop if:* a compiler field/version change makes semantics unclear. Add an +adapter test/compatibility rule; do not scatter a fallback through core code. + +=== WP-04 — Closed call graph and typed internal IR + +*Tasks:* + +. Define normalized IR with explicit variables, SSA definitions, block/branch + edges, phi nodes, function calls, effects, numeric types and source spans. +. Validate SSA graph invariants before any proof pass: every use is defined, + block edges are consistent, value types are known, and all call edges are + accounted for. +. Resolve each concrete call edge to an analyzed body or reviewed summary. + Summaries specify input types, output type, effects, tier behavior, + preconditions, postconditions and summary version/hash. +. Support a tiny pure core initially: literals, local assignments, integer and + rational add/sub/negate/order, conditionals, returns, and explicitly modeled + comparisons. Reject exceptions and side effects until specified. +. Record method table/world fingerprint, specialization tuple, dependency + identity and compiler build in canonical analysis input. +. Cross-check a sample lowering against a second representation/reference + interpreter; test branch and phi semantics. + +*Completion gate:* IR validator accepts only explicit supported constructs; +programs containing hidden dynamic calls, unmodeled global reads/writes, open +world dispatch, reflection or `Any` fail closed. No obligation is generated for +an invalid IR. + +=== WP-05 — VC/status layer before solvers + +*Tasks:* + +. Define typed `Obligation`, assumptions, goal, source provenance, tier, and + expected result. Define `PROVED`, `REFUTED`, `UNKNOWN`, `UNSUPPORTED`, and + `POLICY_REJECTED` result variants. +. Define stable obligation IDs from canonical source/IR/contract identity, not + line number alone. Line changes must update provenance but not accidentally + conflate different goals. +. Implement a deliberately simple evaluator/reference semantics for the first + supported scalar IR and compare generated obligation meaning against it. +. Test counterexample extraction with hand-built models; distinguish solver + timeout, parser error, unsupported theory and satisfiable negated goal. +. Define a prover request interface independent of a specific solver, with + explicit theory/tier/version and bounded resource configuration. + +*Completion gate:* no claim word `PROVED` is constructible from process exit code +or text output. Only the proof-check path (added later) may construct it. + +=== WP-06 — Tier 1 affine integers/rationals + +*Tasks:* + +. Specify mathematical `Int` and `Rational` semantics separately. Julia `Int` + is fixed-width: admit it as mathematical integer only with range/no-overflow + VCs at every operation; otherwise reject or classify as Tier 2. +. Support affine addition, subtraction, negation, comparisons, and conjunction/ + disjunction of supported constraints. Separate integer Presburger from + rational LRA theories in the IR and VC serializer. +. Reject non-linear multiplication, non-constant division, unsupported floor, + modulo, conversion, rounding, and integer overflow behavior. +. Add a reference enumerator over bounded small domains for testing; do not use + it as the general proof method. +. Choose the ECHIDNA/Why3 transport schema only after the abstract obligation + API is stable. Ensure solver replies bind to the exact request digest. +. First demonstration: prove a simple affine postcondition; second demonstration: + show a false postcondition is `REFUTED` with a concrete counterexample. + +*Completion gate:* proofs have replayable/checkable witnesses; counterexamples +are validated by internal evaluation; unsupported theories stay explicit. + +=== WP-07 — Machine bitvectors, arrays, loops, and mutation + +*Tasks:* + +. Add explicit bit width, signedness, wrap/checked semantics for every + operation; implement Tier 2 mapping only after reference tests establish + Julia's exact behavior for the supported operations. +. Add vector facts (axes, length, element type) and 1-based index semantics; + prove index arithmetic before converting to a bounds-free access. +. Implement loop CFG/invariant obligations with induction; initially restrict to + simple counted loops over vectors and constant/affine ranges. +. Model read/write footprints by backing object identity and intervals. Reject + overlapping mutable borrows; do not infer `SubArray` disjointness from wrapper + identity. Add slices/views only with precise parent/index-map semantics. +. Add `@inbounds` only after corresponding bound VC is proved. Require the + project mutation-testing gate >=95% for CI policy, but never treat score as a + substitute for proof. The score input must come from trusted CI evidence + before release use. +. Test alias counterexamples, boundary indices, empty arrays, negative steps, + checked overflow, wraparound, and view-parent overlap. + +*Completion gate:* Tier 2 operation-by-operation reference suite passes; +accepted unchecked load/store is dominated by proof of in-bounds; every +mutation has a unique proven footprint. + +=== WP-08 — `@noalloc` and JET evidence + +*Tasks:* + +. Define scope of a no-allocation claim: compiled normal path, target, Julia + build, warmup, exceptional paths, and runtime allocations included/excluded. +. Make typed-IR escape/allocation analysis conservative. Unknown helper, + boxing, captured closure, dynamic dispatch, or unmodeled runtime call means + `UNKNOWN` / rejected claim. +. Integrate JET as diagnostics only. Do not elevate a clean JET report to proof. +. Add warmed `@allocated` regression tests for selected kernels and retain + complete measurement context. + +*Completion gate:* report static findings and dynamic measurements separately; +unknown behavior blocks a static no-allocation claim. + +=== WP-09 — Idris2/Zig `ccall` vertical slice + +*Tasks:* + +. Choose one supported target ABI and one non-retaining, synchronous, read-only + function. Do not begin with arbitrary `ccall` conversion. +. Define one generated ABI manifest: symbol, calling convention, parameter and + return types, `sizeof`, `alignof`, field offsets, endianness, alias rules, + nullability, pointer extent, error/result values, ownership, and no-retain. +. Generate target C probes for layout facts. Check Julia `isbits` type facts + against those probes and the Idris2 layout proof; never treat the illustrative + constants currently in the scaffold as universal target facts. +. Define the Idris2 lifetime/borrow specification and a checkable ZigProve + result showing the pointer is not stored, returned, or used asynchronously. +. Analyze the lexical `GC.@preserve` region: pointer derivation inside the + region; owner preserved through the full `ccall`; no escaping pointer. +. Prove Julia 1-based to Zig 0-based offset conversion, slice count, empty-range + behavior, byte-size overflow, bounds, alignment and alias conditions. +. Write adversarial ABI integration tests: wrong signature, layout mismatch, + index 0, last-index off-by-one, empty buffer, escaped pointer, retained pointer, + wrong platform, missing preservation. + +*Completion gate:* one target, one helper, one complete independent proof seam. +All other FFI calls remain rejected. `GC.@preserve` is necessary but never +presented as sufficient for pointer safety. + +=== WP-10 — Strict IEEE and statistical tier boundary + +*Tier 3 tasks:* + +. Specify strict IEEE-754 operations by format, rounding mode and operation + ordering; forbid `@fastmath` in a strict proof unit. +. Preserve NaN, infinity, signed zero, subnormals, exceptions and fused-operation + behavior where in scope. Do not rewrite float terms as reals. +. Require finite/non-NaN assumptions only when needed and state them at the + function boundary. Add rounding-error/residue obligations and certificate + format, using QF_FP, Gappa or intervals only where the semantics line up. +. Test special values, halfway rounding, cancellation, overflow, underflow, + signed zero, NaN comparisons and fused-vs-unfused behavior. + +*Tier 4 tasks:* + +. Define a distinct probabilistic/statistical result type with distribution, + assumptions, sample process, confidence level, and runtime/monitor metadata. +. Keep ML ranking and Axiology policy estimates out of deterministic + postcondition proof channels. State explicitly what empirical warrant means. + +*Completion gate:* no Float64-to-Real cast without an explicit abstraction +proof; no Tier 4 status satisfies deterministic functional-safety gates. + +=== WP-11 — Warrant, Receipt, cache, and `echidnabot` + +*Tasks:* + +. Define a canonical proof bundle containing source/contract hashes, normalized + IR, Julia/compiler/world and target identity, dependencies, solver requests, + witnesses, ABI manifest, assumptions, checker versions, and evidence status. +. Compute BLAKE3 cache identity over every semantic input; prove invalidation + with tests changing each input independently. +. Local search may emit `INCOMPLETE Warrant` only. Build an independent batch + checker for Dedukti witnesses plus configured Coq and Lean checks. Only this + path may issue `COMPLETE Receipt`. +. Store artifacts content-addressed; verify cache content and provenance before + use. Pull-request workspaces and cache writes are untrusted. +. Add a read-only least-privilege bot to report statuses and attach obligation + bundles. The bot must distinguish proof status from policy/test/JET status. +. Test stale witness, forged status string, missing checker, compiler-version + mismatch, changed ABI, solver `unknown`, invalid BLAKE3 key, cache poisoning, + fork PR permissions and network failure. + +*Completion gate:* receipt is independently reproducible; the bot cannot mint +or upgrade one; every mismatch returns non-green `UNKNOWN`/invalid. + +== Release gates and definition of done + +A milestone is done only when all applicable checks pass: + +[cols="1,3",options="header"] +|=== +|Gate |Evidence required + +|Build and package +|Clean instantiate/load and `Pkg.test()` on supported floor + current stable; + reproducible lock decision; no generated artifacts committed. + +|Parser safety +|No macro execution; parse errors rejected; adversarial macro fixtures; source + spans and canonical form tested. + +|Compiler boundary +|Supported Julia matrix; adapter golden tests; unknown IR/call/world facts + rejected; dependency/world invalidation regression. + +|Semantics +|Reference semantics and negative/counterexample tests for every operator and + control-flow construct admitted. + +|Proof +|Named obligations, checked witnesses, independent checker; no solver-only + `unsat` promotion. + +|Memory and ABI +|Target-specific layout probes and mismatch negatives; lifetime, bounds, + conversion, no-alias and no-retain obligations independently accounted. + +|Numerics +|Separate tier; boundary/special-value tests; no coercion across arithmetic + theories without a proof obligation. + +|Documentation +|README, quickstart, design, plan, and feature status agree with actual code. + Every planned/incomplete status remains labeled. + +|Security/reproducibility +|Trusted workflow boundaries, least privilege, complete cache keys, no + untrusted receipt/cache acceptance. +|=== + +No milestone may waive a failing mandatory gate by changing a status label, +using `continue-on-error`, hiding an unsupported construct, or broadening a +precondition without recording it in the function contract and proof bundle. + +== First three pull requests to execute + +=== PR 1 — Validate the existing package and establish Julia CI + +* Run the present code on Julia 1.9 and current stable, fix actual runtime + defects, add CLI subprocess tests, and check formatting. +* Add a focused Julia workflow following the checked-in action-lock convention; + regenerate/check its lock as part of the same change. +* Add the test result and actual tested versions to the implementation status. +* No semantic feature expansion in this PR. + +=== PR 2 — Introduce contract data structures and parser + +* Add only data types and pure parser from WP-02; do not generate VCs. +* Parse `@verified`, `@pre`, `@post`, `@invariant`, `@cap`, `@tier`, + `@noalloc`, `@echo` from fixtures and preserve spans. +* Reject unsupported contract expressions, duplicate annotation, unknown tier, + dynamic expressions, unknown macros and malformed syntax. +* Document exact grammar; add canonicalization and adversarial tests. + +=== PR 3 — First specialized typed-IR probe + +* Select one pure scalar Julia function with concrete signature and no external + dependencies. +* Write an adapter proof-of-concept for floor and stable Julia. Capture typed + return/SSA/call facts and report adapter version; do not claim world freeze + until the adapter can evidence it. +* Validate all nodes/call edges or return `UNSUPPORTED`; add versioned snapshots. +* Keep result labeled compiler diagnostics; do not send to solver yet. + +Only after PR 1–3 are merged and stable should a contributor define the minimal +internal IR and first scalar VC in PR 4+. + +== Task selection and agent handoff protocol + +Before starting a task, every contributor/agent should: + +. Read README, this plan's mission/principles, the current implementation-plan + status, and relevant source/tests. +. Confirm branch/status and working tree; never overwrite unrelated changes. +. Select one WP/checklist item and state prerequisites. Do not silently expand + scope into a later milestone. +. Write a failing regression test or fixture first for a bug/feature whenever + practical. +. Implement the smallest change. Keep version-specific code and external + integration behind named adapters. +. Run relevant focused tests, then package/repository checks. Record commands, + versions, skipped checks and failures honestly. +. Update status/docs only to reflect code that exists; separate planned, + experimental, tested, and verified labels. +. Finish with this handoff record in the PR description or issue: + +[source,text] +---- +Work package / task: +Behavior added or changed: +Files touched: +Semantics and assumptions: +Tests run (exact commands and versions): +Tests not run and why: +Proof/trust status (never infer from tests): +Unsupported cases / residual risks: +Next unblocked task: +---- + +== Risks and decision log to maintain + +[cols="1,3,3",options="header"] +|=== +|Risk |Why it matters |Required mitigation / decision record + +|Julia compiler internals drift +|Private IR and inference details change across Julia minors. +|Version-specific adapter, golden tests, pinned support matrix, fail closed on + unknown nodes; no general use of private fields. + +|Method-table/world openness +|New methods or invalidations can change dispatch after analysis. +|Bounded snapshot with fingerprints and invalidation policy; do not claim + globally frozen dispatch without a real mechanism. + +|Unsound lowering +|An incorrect IR/VC translation can certify a false theorem. +|Small IR, reference semantics, differential/adversarial tests, checker-verified + witnesses, publish TCB. + +|Solver proof not checkable +|Solver status alone may be untrusted or buggy. +|Require certificate/witness checked independently; `UNKNOWN` otherwise. + +|Julia GC/FFI mismatch +|Preservation, ABI layout and pointer retention are separate properties. +|Target probes + Idris2 layout/lifetime contracts + Zig proof + Julia-side + preserve/bounds/alias checks; one target at a time. + +|False zero-allocation claim +|Compiler/runtime/target changes affect allocations. +|State exact scope; combine conservative static analysis with contextual runtime + regression tests; never promise all targets based on one measurement. + +|Feature creep +|Four tiers and many proof systems create broad integration surface. +|Prioritize Tier 1 scalar vertical slice; every new feature needs an exit gate + and known unsupported set. +|=== + +Maintain a dated decision log whenever support matrix, tier semantics, witness +format, trusted checker, ABI target, cache-key components, or status vocabulary +changes. Update architecture + tests in the same change; a plan-only edit cannot +change an implementation claim. + +== Navigation + +* link:APODEIXIS-VERIFICATION-DESIGN.adoc[Full verification architecture] +* link:APODEIXIS-MVP-IMPLEMENTATION-PLAN.adoc[Current MVP plan and status] +* link:../../README.adoc[Project README] diff --git a/docs/architecture/APODEIXIS-VERIFICATION-DESIGN.adoc b/docs/architecture/APODEIXIS-VERIFICATION-DESIGN.adoc new file mode 100644 index 0000000..0f821b3 --- /dev/null +++ b/docs/architecture/APODEIXIS-VERIFICATION-DESIGN.adoc @@ -0,0 +1,613 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) Jonathan D.A. Jewell += Apodeixis.jl: Verification Architecture and MVP Design +:toc: +:toclevels: 3 +:sectnums: + +== Status and scope + +This document is the technical design for Apodeixis.jl. The checkout supplies +the repository, Idris2 ABI, and Zig scaffolding, plus an initial Julia package +and source-policy CLI added as the first implementation slice. It does *not* yet +implement compiler-IR analysis, VC generation, solver integration, or receipts. +The design makes that boundary explicit: `POLICY CLEAN` is not proof; a result +is *proved* only when the verifier emits a checkable obligation/certificate and +the configured trusted checker accepts it. Tests, JET reports, mutation scores, +and statistical evidence are valuable gates, but are not substitutes for proof. + +=== Implementation status (0.1.0 bootstrap) + +Implemented in the current tree: a Julia package (`Project.toml`, +`src/Apodeixis.jl`) using JuliaSyntax.jl to parse source without evaluating +macros; a fail-closed source policy audit for forbidden dynamic escapes, +`@inbounds` context plus the 95% mutation-score gate, unsupported `ccall`, and +unelaborated macros inside `@verified`; a CLI at `scripts/apodeixis.jl`; and focused +`Pkg.test()` cases. This is a *policy linter*, not a contract prover. The Julia +runtime is not installed in the current development environment, so the package +tests have not yet been executed here; the first implementation CI job should +run them on the declared Julia compatibility matrix before treating the slice +as runtime-validated. + +Not implemented: contract elaboration/VC semantics, typed SSA inspection, +monomorphized call-graph closure, world-age fingerprinting, numeric-tier +checking, alias proofs, allocation proof, ABI manifest validation, solver +witnesses, ECHIDNA transport, or Warrant/Receipt issuance. The current +`AuditReport` returns only `:policy_clean` or `:rejected`; neither status +establishes these capabilities. `UNSUPPORTED` describes the future verifier's +behavior for these unimplemented features. + +Apodeixis is a source-to-obligation compiler for a deliberately restricted, +closed Julia program. It is not a theorem prover for arbitrary Julia. A verified +unit has a declared input domain, contract, effect/capability footprint, +numeric tier, dependency world, and proof status. Unsupported syntax, unknown +calls, unresolved dispatch, stale dependencies, or solver `unknown` cause a +reject/unknown result; they never silently weaken the claim. + +== Architecture at a glance + +[source,text] +---- + Julia source + | + +--> JuliaSyntax.jl surface pass: macros, syntax policy, source spans + | -> normalized contract/effect AST (not executable macro expansion) + | + +--> Julia compiler: method instance + typed SSA IR, pinned Julia version + -> closed call graph, dataflow/effect/alias/alloc checks + -> typed Apodeixis IR (ANF, explicit overflow/rounding/memory) + | + VC generation and dependency hashing + | + +--------------+-----------------------+ + | | | + SMT/Why3 Agda/Idris/Zig seam JET + runtime test evidence + | | | + Strict Dedukti witness + checked batch Receipt diagnostics only + | + +--> Warrant (INCOMPLETE) --> external batch Coq/Lean check + -> Receipt (COMPLETE) + -> BLAKE3-keyed Proof Burrower cache +---- + +=== Compiler boundary and trust model + +* *JuliaSyntax.jl* is the source-facing parser, syntax tree, macro-contract + recognizer, and source-span provider. It parses `@pre`, `@post`, `@invariant`, + `@cap`, `@tier`, and `@noalloc` declarations without executing arbitrary + macro expansion. Contract expressions are parsed into a small allowlisted + logic (comparisons, Boolean connectives, affine arithmetic, array indexing, + and approved predicates). A macro whose expansion would be required for + semantics is rejected unless registered with a reviewed, versioned + elaborator. This prevents `eval` or a malicious macro from becoming part of + the proof frontend. +* *Julia's compiler* supplies the concrete dispatch instance and typed SSA IR. + The adapter uses public introspection such as `code_typed`/`Base.return_types` + where possible, and a narrowly isolated `Core.Compiler` adapter where exact + `CodeInfo`, `MethodInstance`, call-edge, or world information is needed. Those + internals are version-specific: every supported Julia minor gets its own + adapter and golden IR tests. The verifier does not patch the compiler, alter + inferred IR, or assume a private field is stable. +* Each entry point is specialized over concrete argument types and a captured + Julia world. Recursively resolve every reachable call at that world. Require + one applicable `MethodInstance` for each call edge (or an explicitly + modeled finite dispatch split), and fail closed on `Any`, `invoke`, dynamic + `apply`, `invokelatest`, reflection, unresolved `ccall`, or a call into an + unverified package method. World-age freezing is a *reproducibility and + closed-world* condition, not a promise that Julia cannot load new methods: + record the world interval and dependency method fingerprints, reject + invalidation/newer methods that can change the graph, and re-verify when the + package image or dependency set changes. +* SSA checks reject `Any`-typed values at proof-relevant operations and reject + boxed/dynamic calls on the verified path. This is distinct from proving + allocation freedom: boxing analysis, inferred IR, LLVM/native code checks, + and runtime allocation tests are separate checks. `JET.jl` is an excellent + diagnostic and CI signal, but its absence of reports is not a soundness + theorem. The MVP certifies only a conservative typed-SSA subset and records + the Julia version, target triple, flags, method hashes, and dependency lock. + +The semantic translation is explicit: SSA control flow becomes a CFG with +phi-nodes; checked arithmetic becomes a value plus overflow condition; array +operations become bounds and alias obligations; floating-point operations +retain IEEE operations and rounding nodes; and calls become either inlined +verified summaries or separately proven contracts. No optimization is allowed +to erase distinctions in the selected numeric tier. + +=== Surface contract semantics + +Contract macros are declarations, not arbitrary Julia code hooks. A normalized +contract bundle is attached to the function's source identity and specialized +method instance. Preconditions are assumptions only at a verified call site +where their proof is discharged. Postconditions and invariants are goals. +Runtime contract checks can be emitted in debug mode but do not upgrade a +static proof status. `@cap` declares an upper bound on effects; inferred effects +must be a subset. Capabilities include heap reads/writes by region, IO, random +state, task/world mutation, and foreign calls. `eval`, `@generated`, +`Base.invokelatest`, global mutable state, and unverified `ccall` are forbidden +in the MPR-style safe footprint. + +Example surface shape (illustrative API; macro implementation is part of the +MVP): + +[source,julia] +---- +@verified function row_bound!(out::Vector{Int64}, row::Vector{Int64}, + incumbent::Int64) + @pre length(out) == length(row) + @pre all(x -> x >= 0, row) + @post length(out) == length(row) + @cap(read(row), write(out), foreign(:apx_max_scan)) + @tier MachineBV + @noalloc + # body follows below +end +---- + +== Four numeric and decidability tiers + +A tier is part of a function's proof interface. Calls may move to a *more +restricted* tier only with explicit conversion obligations; they may not +silently reinterpret values. In particular, mathematical real numbers and +`Float64` are different domains in both the IR and certificates. + +[cols="1,1,2,3",options="header"] +|=== +|Tier | Domain / encoding | Decidable fragment / obligations | Claim and boundaries + +|`ExactLinear` +|Mathematical integers and rationals. Julia `Rational{T}` may be admitted when + canonical and non-overflowing; arbitrary mathematical integers are represented + by `BigInt` or a proved-safe lift. +|Linear integer arithmetic (Presburger arithmetic) and linear rational + arithmetic (LRA). The two theories are not conflated. Addition, negation, + order, linear constraints, and affine branch bounds are supported. Nonlinear + products, division with variable denominator, and unsupported floor/mod + produce unknown or a different tier. +|For a machine `Int`, an additional no-overflow proof is mandatory before + interpreting it as a mathematical integer. Otherwise Julia `Int` is fixed + width and belongs to `MachineBV`. Supports exact skip/branch-and-bound + warrants, e.g. a RapidNJ row lower bound proves no candidate can improve the + incumbent. + +|`MachineBV` +|Fixed-width `Int8`…`Int128`, `UInt*`, and pointer-sized `Int`/`UInt`, with + explicit width and signedness. +|QF_BV; distinguish Julia wrapping operations from checked operations, checked + intrinsics, and `Base.Checked` semantics. Shifts, signed comparisons, + widening/narrowing, and reinterpretation are explicit BV operators. +|The proof states whether wraparound is intended. No appeal to unbounded + integer arithmetic is permitted without range obligations at every operation. + +|`StrictIEEE754` +|IEEE-754 `Float32` / `Float64` with exact format, rounding mode, and operation + sequence. `@fastmath` is rejected. +|QF_FP where supported; otherwise Gappa/interval certificates with directed + rounding. Preconditions prove operands/results are finite and non-NaN when + required. Rounding is modeled per operation, not by replacing floats with + reals. An `echo-types` residue/error bound is mandatory for every lossy result. +|NaN, signed zero, infinities, subnormals, exceptions, and fused operations are + specified explicitly. A real-arithmetic theorem is not a Float64 theorem. + Interval proof fallback may return unknown rather than silently assume a + solver's unsupported semantics. + +|`Probabilistic/Statistical` +|Random variables, distributions, sampled observations, learned rankings, + or statistical model outputs. +|Statistical tests, concentration bounds, calibration, runtime monitors, or + probabilistic proof systems with explicit assumptions and confidence levels. +|Produces a runtime/statistical `Warrant` only. It is hard-banned from claiming + deterministic functional safety, memory safety, or a universal postcondition. + `Axiology.jl` policy constraints and ML ranking can contribute evidence, but + cannot discharge Tier 1–3 safety VCs. +|=== + +`@echo(safe)` is restricted to exact `Int` operations with established range +bounds and exact rationals. `@echo(neutral)` records a bounded-residue float +conversion/truncation, with units, input domain, rounding mode, and a proved +residue bound. `@echo(breaking)` records irreversible loss and cannot flow into +a safety-critical postcondition unless an explicit, separately proved +abstraction justifies it. These annotations refine a tier; they do not change +the underlying arithmetic theory. + +A proof certificate includes theory, format, rounding mode, overflow mode, +solver/version, assumptions, and exact operation graph. Solver `sat` for the +negated goal is a counterexample; `unsat` is only a proof ingredient accepted +when the checker validates its witness. `unknown`, timeout, unsupported theory, +or missing residue bound means no proof. + +== Mutation, arrays, allocation, and capabilities + +=== Array and view discipline + +The MVP adopts a conservative separation-logic-like footprint model: + +* An input has a read borrow; a mutating argument has a unique write borrow for + the duration of the call. Simultaneous mutable borrows must have a statically + proved disjoint region. `Vector{T}` regions are object identity plus a + half-open index interval. `SubArray` footprints are derived from parent + identity, axes, strides, and index mapping; unknown/indirect index sets are + rejected unless a runtime disjointness guard is inserted and its branch + separately verified. +* If `A` and `B` may share a parent or backing storage, mutation through one and + observation/mutation through the other is rejected unless the declared + footprints are disjoint. `===` on wrappers is insufficient to prove backing + storage disjointness. `copy` creates a separate region but is incompatible + with `@noalloc` unless allocation is outside the measured kernel. +* Loop invariants state initialized prefix/suffix, bounds, and preservation of + elements outside the write footprint. Mutation cannot invalidate an active + read borrow. Global arrays and unmodeled `unsafe_load`/`unsafe_store!` are not + in the safe subset. + +=== `@inbounds` policy + +`@inbounds` is permitted *only* in an `@verified` function after the verifier +has generated and discharged bounds VCs for every affected access (including +loop preconditions and index arithmetic). It is rejected for unchecked or +unknown paths. In addition, the project policy requested for this toolchain +requires the covering `mutation.rs` mutation-testing score to be at least 95% +before a function containing `@inbounds` can pass the release/CI gate. The +score is computed from the relevant safety test suite, with surviving mutants +reviewed and excluded mutants documented. Mutation score is a test-strength +gate, not a proof rule: 95% cannot make an undischarged bounds VC acceptable. + +=== `@noalloc` policy + +`@noalloc` is checked on the specialized hot path, not inferred from source +appearance. Reject escaping closures, boxing, heap construction, dynamic +dispatch, growth operations, and helper calls without allocation summaries. +Use typed SSA / compiler allocation analysis as a conservative static filter, +then validate with warmed-up allocation tests (`@allocated` or BenchmarkTools) +on supported Julia versions. Record compiler version, target, compilation state, +and measurement method. A runtime zero-allocation result is regression evidence, +not a universal proof across targets. No allocation claim is made for compilation, +exceptional exits, or unmodeled runtime services unless explicitly covered. + +== Idris2 + Zig `ccall` memory-safety proof seam + +Foreign calls are opaque unless tied to a versioned ABI manifest and verified +Idris2 specification plus Zig implementation. Each entry declares exact symbol, +calling convention, target ABI, parameter widths, pointer mutability, lengths, +nullability, alignment, alias relation, ownership/lifetime, error codes, and +retention policy. The seam checker establishes four independent obligations: + +. *Preservation and lifetime:* the Julia owner remains strongly reachable for + the full dynamic extent of the foreign call. `GC.@preserve` encloses every + pointer derivation and the `ccall`; no pointer escapes the region. Pointer + conversion before entering the preserve block is rejected by the source + checker. A borrowed pointer is invalid after return unless ownership is + explicitly transferred under a separately verified allocator protocol. +. *Layout:* only `isbits` Julia values cross by value. For each `isbits` + `struct`, compare compiler-reported size, alignment, field offsets, field + sizes, signedness, and endian assumptions against the generated C ABI + manifest and the Idris2 `Layout` proof. The build runs target-specific + `sizeof`/`alignof`/`offsetof` probes; Idris2 proofs validate the manifest + arithmetic. A mismatch is a hard error. The template `Layout.idr` example is + not a universal platform layout proof; target facts must be generated and + checked for each supported triple. +. *Index and slice conversion:* Julia arrays are 1-based, while the Zig slice + contract is 0-based with a pointer plus element count. For Julia inclusive + interval `lo:hi`, prove `1 <= lo <= hi <= length(A)` (or handle the empty + case separately), then pass offset `lo - 1` and length `hi - lo + 1` using a + checked unsigned conversion. Prove multiplication by element size and pointer + offset cannot overflow, and prove alignment and bounds against the actual + array length. Do not pass Julia's `pointer(A)` for an empty range without a + separately specified empty-slice convention. +. *No retention:* Zig's verified function is specified to use the borrowed + pointer only during the call and not retain it, store it globally, spawn an + asynchronous use, or return it. Idris2 carries the borrowed lifetime in the + function type/specification; ZigProve checks the implementation against that + contract. A C ABI alone cannot encode non-retention, so this obligation is + proved by the Zig verification and exposed as a named trust boundary in the + manifest. + +`GC.@preserve` proves reachability/liveness only; it does not by itself prove +bounds, aliasing, alignment, layout, or Zig non-retention. Those are separate +VCs. Similarly, Zig proofs do not prove Julia's `ccall` declaration matches the +symbol unless the generated ABI manifest is checked against both sides. + +=== Example ABI declaration + +Illustrative Idris2 specification for the scanner's primitive operation (the +actual Idris syntax/package API should track the repository's Idris2 version): + +[source,idris] +---- +%default total + +||| Borrowed slice is valid only for this call; implementation retains no pointer. +public export +record SliceSpec where + constructor MkSliceSpec + base : Bits64 + offset : Bits64 + count : Bits64 + (0 nonNull : So (base /= 0)) + (0 positiveCount : So (count > 0)) + (0 inBounds : offset + count <= maxElements) + +public export +maxScan : SliceSpec -> Int64 -> Int64 +-- Postcondition in the interface package: +-- result == maximum of exactly [base + offset, count] elements, +-- count > 0; reads only; no pointer survives return. +---- + +The production ABI package must additionally prove that the types are +platform-correct; the sketch above communicates the logical contract, not a +portable pointer representation. + +== Worked end-to-end kernel: row bound scanner + +This example scans a nonnegative Int64 row and writes suffix lower bounds. It +uses a verified Zig helper to compute the row maximum, then Julia writes a +suffix accumulation combined with that maximum: each output is the maximum of +the suffix sum and the row maximum. `Int64` arithmetic is Tier 2: every add is +checked, not assumed mathematical. To keep the example readable, the shown +pseudocode helper `checked_add` returns `(value, ok)` and has a verified summary. Macro names are +proposed surface syntax. The caller supplies non-overlapping buffers; the +verifier establishes their full-array disjointness, not merely distinct Julia +wrapper objects. + +[source,julia] +---- +# Assumed generated wrapper from the Idris2/Zig ABI package: +# apx_max_scan(ptr::Ptr{Int64}, n::Csize_t) -> Int64 +# Its manifest asserts read-only, no-retain, no-throw C ABI semantics. + +@verified function suffix_bounds!(out::Vector{Int64}, row::Vector{Int64}) + @pre length(out) == length(row) + @pre !mayalias(out, row) + @pre all(x -> x >= 0, row) + # Mathematical (unbounded) sum in the contract logic; prevents overflow + # for every suffix, without allocating in the verified kernel. + @pre sum_wide(row) <= typemax(Int64) + @post length(out) == length(row) + @post all(i -> 1 <= i <= length(out) ==> out[i] >= 0, + 1:length(out)) + @cap(read(row), write(out), foreign(:apx_max_scan)) + @tier MachineBV + @noalloc + + n = length(row) + if n == 0 + return out + end + + m::Int64 = 0 + GC.@preserve row begin + p = pointer(row, 1) # pointer derived inside preserve region + m = ccall((:apx_max_scan, libapodeixis), Int64, + (Ptr{Int64}, Csize_t), p, Csize_t(n)) + end + + # Reverse suffix accumulation; no new arrays and no unchecked arithmetic. + acc::Int64 = 0 + @inbounds for i in n:-1:1 + @invariant acc == sum_wide(row[i+1:n]) + @invariant m == max_wide(row) + s, ok = checked_add(acc, row[i]) + ok || return out # defensive fallback; precondition proves unreachable + acc = s + out[i] = max(acc, m) + end + return out +end +---- + +The `sum_wide` and `max_wide` names are logical specifications, not Julia +runtime helpers. The sum precondition makes every nonnegative suffix fit in +`Int64`; the checked-add failure branch is retained as a defensive runtime +fallback but is proved unreachable on the verified entry path. The loop +invariant ties `acc` to the mathematical suffix sum, while `m` from Zig is +checked against the helper's verified maximum specification and combined with +`acc` in each output value. A production API may instead return an explicit +status and state initialized-output guarantees for a reachable failure path. + +=== Generated VCs and evidence + +The verifier lowers the function and emits obligations similar to these +(numbering is illustrative and stable IDs are derived from source + IR hashes): + +[cols="1,2,2",options="header"] +|=== +|VC | Goal / assumptions | Discharge path + +|`PRE-01` shape +|`length(out) == length(row)` at entry. +|Caller contract; otherwise caller VC fails. + +|`ALIAS-01` separation +|`region(out) ∩ region(row) = ∅` during writes. +|Ownership/borrow proof or explicit runtime guard with verified branch. + +|`FFI-PRESERVE-01` +|The owner of `row` remains live from pointer derivation through return from + `apx_max_scan`; pointer use is within `GC.@preserve`. +|JuliaSyntax source-span rule plus SSA lifetime analysis. + +|`FFI-ABI-01` +|Julia `(Ptr{Int64}, Csize_t) -> Int64` agrees with target C ABI and Idris2 + symbol declaration, sizes, alignment, and calling convention. +|Generated ABI probes + Idris2 layout proof + Zig exported signature. + +|`FFI-BOUNDS-01` +|For `n > 0`, pointer to Julia index 1 and count `n` covers exactly the array; + byte-size and pointer-offset arithmetic do not overflow. +|Julia array facts + checked arithmetic + seam manifest. + +|`FFI-NORETAIN-01` +|Zig does not save, return, or asynchronously use the borrowed Julia pointer. +|ZigProve proof checked against Idris2 lifetime specification. + +|`LOOP-01` invariant +|At loop head, `acc` is the checked sum of the processed suffix and all written + cells contain the maximum of their suffix sum and the row maximum, hence are + initialized and nonnegative. +|Induction over reverse loop; Tier 2 QF_BV obligations. + +|`BOUNDS-01` +|Every `row[i]` and `out[i]` access has `1 <= i <= n`. +|Induction from loop range; must pass before `@inbounds` is accepted. + +|`OVERFLOW-01` +|Each `checked_add` reports success iff the mathematical sum fits Int64; on the + success branch the result is the exact BV addition with no overflow. +|QF_BV + checked-add summary. + +|`ALLOC-01` +|No heap allocation/boxing/dynamic dispatch on the specialized normal path. +|Typed SSA effect/escape analysis + warmed allocation regression test. + +|`POST-01` postcondition +|For successful return, all stated output values satisfy the contract. +|Composition of loop invariant, checked arithmetic, and helper summary. +|=== + +`@inbounds` is not admitted until `BOUNDS-01` and all related bounds VCs are +proved and the relevant `mutation.rs` score is at least 95%. If the implementation +returns early on overflow, `POST-01` must be guarded by the success result or +state the weaker failure postcondition explicitly; the simplified example +intentionally exposes this API-design decision rather than hiding it. + +=== Warrant to Receipt lifecycle + +. The frontend stores a canonical normalized AST, specialized typed SSA + fingerprint, Julia version/world, ABI manifest hash, source map, assumptions, + and test/mutation evidence. It generates VCs and a deterministic BLAKE3 + dependency key. +. ECHIDNA sends supported obligations to Why3/SMT. A successful local run + creates a *Warrant* marked `INCOMPLETE`; this is evidence that proof search + succeeded, not a completed verification claim. +. Strict Dedukti `.dk` witnesses are emitted for the accepted proof steps. The + batch checker independently checks the witnesses in Coq and Lean. Any missing, + stale, inconsistent, or rejected witness prevents completion. +. On complete checking, ECHIDNA issues a *Receipt* marked `COMPLETE`, bound to + the exact BLAKE3 key. Proof Burrower may cache that receipt. Any source, + compiler version, world fingerprint, target ABI, contract, solver configuration, + or dependency change invalidates the key and requires re-checking. +. `Probabilistic/Statistical` obligations are labeled statistical warrants and + are never promoted to deterministic receipts for functional safety claims. + +Reports distinguish `PROVED`, `REFUTED` (counterexample), `UNKNOWN`, and +`UNSUPPORTED`. Only `PROVED` with a valid `COMPLETE` receipt satisfies a strict +verification gate. + +== Integration and developer workflow + +=== Julia package and test model + +The eventual package should be a normal Julia package with `Project.toml`, +`src/Apodeixis.jl`, and tests run by `Pkg.test()`. Pin compatible JuliaSyntax.jl, +JET.jl, and solver/client versions in the project/manifest; compiler internals +are gated by an explicit Julia compatibility matrix. Tests include parser golden +fixtures, typed-SSA fixtures, soundness regressions for dispatch/world changes, +unit tests for each VC lowering rule, ABI layout probes, FFI integration tests, +and end-to-end certificate checks. Test helpers must not be mistaken for +verified library code. + +Suggested developer loop: + +[source,bash] +---- +julia --project -e 'using Pkg; Pkg.test()' +julia --project -e 'using JET; @report_opt target(args...)' +apodeixis check --tier MachineBV --receipt target(args...) +apodeixis explain --vc FFI-PRESERVE-01 +---- + +JET reports are triage: every report is fixed or explicitly classified, but a +clean JET report alone does not prove the call graph closed or safe. `Pkg.test` +validates implementation behavior; SMT and certificate checking validate +formal obligations. CI keeps these statuses separate. + +=== `echidnabot` + +`echidnabot` runs on PRs with least-privilege permissions. It parses changed +Julia files, checks macro allowlists and policy, discovers annotated entry +points, runs parser/type/alias/VC checks, requests local ECHIDNA proof search, +and uploads reproducible obligation bundles. It comments with per-tier status, +VC IDs, counterexample/reason for unknown, compiler + dependency fingerprints, +mutation score, JET/test results, and receipt hash. It must not publish a +`COMPLETE` badge from local `INCOMPLETE Warrant` output. Receipt verification +runs in a separate trusted batch job; untrusted PR code cannot mint or alter +trusted receipts. Cache keys are content-addressed and include toolchain and +proof-checker versions; untrusted cache entries are never accepted as verified +receipts. + +== MVP roadmap + +[cols="1,2,3,2",options="header"] +|=== +|Phase |Deliverable |Exit criteria |Explicit non-goals + +|0. Foundations +|Julia package skeleton; supported-version policy; JuliaSyntax contract + parser; typed SSA adapter; diagnostic format and trust-boundary register. +|CI parses fixtures on every supported Julia minor; rejects `Any`, unknown + dispatch, forbidden syntax, and stale world/dependency fingerprints; golden + IR tests detect compiler drift. +|No whole-language Julia support, no claims based on JET alone. + +|1. Exact core +|Pure scalar subset; pre/post/invariant; closed calls; Tier 1 linear integers + and rationals; Why3/SMT VC generation and checked witness pipeline. +|Soundness tests for affine arithmetic/branches; counterexample tests; accepted + certificates independently check; unsupported nonlinear terms fail closed. +|No arrays, floating point, or foreign calls. + +|2. Machine arithmetic + arrays +|Tier 2 QF_BV; owned `Vector{T}` and affine loops; interval footprints, alias + checks, loop invariants, `@inbounds` gate, `@noalloc` diagnostics. +|Overflow/bounds/alias regression suite; all accepted unsafe accesses have + proven bounds VCs; mutation score gate at 95%; no unknown call on proof path. +|No arbitrary SubArray indexing or concurrent mutation. + +|3. Verified FFI seam +|Generated target ABI manifest; Julia preservation and lifetime analysis; + Idris2 layout and function contract; ZigProve-backed no-retain proof. +|Cross-check size/alignment/offset/signature on every target; negative tests + for escaped pointers, wrong index conversion, ABI mismatch, and pointer + retention; one end-to-end `ccall` receipt. +|No arbitrary third-party `ccall`, callbacks, or asynchronous borrowing. + +|4. IEEE and effects +|Tier 3 strict FP IR, QF_FP/Gappa/interval backend, `echo-types` residue + certificates; MPR capability footprints; statistical warrants segregated. +|NaN/Inf/rounding/fastmath adversarial tests; certified error bounds; no + deterministic-safety promotion of Tier 4 results. +|No proof of unrestricted numerical algorithms or statistical certainty. + +|5. Ecosystem hardening +|Pkg release workflow, JET + runtime allocation suite, `echidnabot`, receipt + cache, docs and migration tooling. +|Reproducible clean build; independent Receipt verification; cache invalidation + tests; documented support matrix and security audit. +|No guarantee across Julia compiler versions or targets not tested and pinned. +|=== + +== Soundness obligations and open decisions + +The first release must publish its trusted computing base: Julia parser/compiler +adapter, contract elaborator, IR lowerer, solver translation, Dedukti checker, +Idris2/Zig verifiers, ABI manifest generator, and any runtime guards. A verifier +bug is possible even when a solver is sound. Keep translations small, use +checker-validated certificates, test translations against independent +semantics, and never treat an external system's status string as a proof. + +Before implementation freezes, decide and document: supported Julia minors and +target triples; the exact Idris2/ZigProve versions and ABI generator format; +whether `mutation.rs` is a mandatory CI executable or a project-local adapter; +which SMT/FP certificate formats are independently checked; and how Julia +world fingerprints are captured without depending on unstable internals. Until +resolved, the corresponding feature remains `UNKNOWN`/experimental rather than +implicitly trusted. + +== References within this repository + +* `docs/architecture/APODEIXIS-MVP-IMPLEMENTATION-PLAN.adoc`: implementation + slices, current package entry points, acceptance gates, and immediate next steps. +* `src/interface/Abi/Types.idr` and `Layout.idr`: initial ABI type/layout + scaffolding; platform constants there are examples, not target-wide proofs. +* `src/interface/ffi/build.zig`: initial Zig build integration. +* `verification/proofs/`: existing proof-language scaffolding and manifests. +* `docs/ARCHITECTURE.adoc`: repository-level architecture overview. diff --git a/docs/architecture/REPOSITORY-MAP.adoc b/docs/architecture/REPOSITORY-MAP.adoc index ff28fb0..501efbb 100644 --- a/docs/architecture/REPOSITORY-MAP.adoc +++ b/docs/architecture/REPOSITORY-MAP.adoc @@ -113,6 +113,10 @@ predecessors did. | yes | REUSE licence texts, dual-licence model (code MPL-2.0 / docs CC-BY-SA-4.0) +| `Project.toml` +| optional +| julia-library archetype: Pkg reads the package manifest from the package root only + | `README.adoc` | yes | - @@ -181,6 +185,10 @@ predecessors did. | yes | - +| `test/` +| optional +| julia-library archetype: Pkg.test runs test/runtests.jl, a fixed path (the spine keeps tests/) + | `tests/` | yes | - diff --git a/scripts/apodeixis.jl b/scripts/apodeixis.jl new file mode 100755 index 0000000..0caa787 --- /dev/null +++ b/scripts/apodeixis.jl @@ -0,0 +1,66 @@ +#!/usr/bin/env julia +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) Jonathan D.A. Jewell + +using Apodeixis + +function usage(io=stdout) + println(io, "Usage: julia --project=. scripts/apodeixis.jl audit [--mutation-score PERCENT] FILE.jl") + println(io, " julia --project=. scripts/apodeixis.jl --help") + println(io, "Audits source policy only; POLICY CLEAN is not a verification proof.") +end + +function main(args) + if isempty(args) || args == ["--help"] || args == ["-h"] + usage() + return isempty(args) ? 2 : 0 + end + args[1] == "audit" || (usage(stderr); return 2) + + score = nothing + file = nothing + i = 2 + while i <= length(args) + arg = args[i] + if arg == "--mutation-score" + i == length(args) && (println(stderr, "missing percentage after --mutation-score"); return 2) + i += 1 + score = tryparse(Float64, args[i]) + score === nothing && (println(stderr, "invalid mutation score: ", args[i]); return 2) + elseif startswith(arg, "-") + println(stderr, "unknown option: ", arg) + usage(stderr) + return 2 + elseif file === nothing + file = arg + else + println(stderr, "expected exactly one source file") + usage(stderr) + return 2 + end + i += 1 + end + + file === nothing && (usage(stderr); return 2) + isfile(file) || (println(stderr, "file not found: ", file); return 2) + report = try + audit_file(file; mutation_score=score) + catch err + println(stderr, "Apodeixis could not read ", file, ": ", sprint(showerror, err)) + return 2 + end + + if isempty(report.findings) + println("POLICY CLEAN (NOT VERIFIED): ", report.filename) + return 0 + end + println("REJECTED: ", report.filename) + for finding in report.findings + println(" ", finding.code, " [line ", finding.line, "]: ", finding.message) + end + return 1 +end + +if abspath(PROGRAM_FILE) == @__FILE__ + exit(main(ARGS)) +end diff --git a/src/Apodeixis.jl b/src/Apodeixis.jl new file mode 100644 index 0000000..b38cc68 --- /dev/null +++ b/src/Apodeixis.jl @@ -0,0 +1,204 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) Jonathan D.A. Jewell + +""" + Apodeixis + +Initial, deliberately non-proving frontend for the Apodeixis verification +compiler. The 0.1 API parses Julia with JuliaSyntax.jl and audits a small set of +source-policy constraints. `:policy_clean` is not a verification result. +""" +module Apodeixis + +using JuliaSyntax + +export Finding, AuditReport, audit_source, audit_file, is_policy_clean + +"""One source-policy diagnostic. `line` is 1-based when known.""" +struct Finding + code::Symbol + line::Int + message::String +end + +"""Result of the fail-closed source-policy audit.""" +struct AuditReport + filename::String + status::Symbol + findings::Vector{Finding} +end + +"""True when the source passed this policy audit (not a proof of correctness).""" +is_policy_clean(report::AuditReport) = report.status === :policy_clean + +const _CONTRACT_MACROS = Set(( + Symbol("@verified"), Symbol("@pre"), Symbol("@post"), + Symbol("@invariant"), Symbol("@cap"), Symbol("@tier"), + Symbol("@noalloc"), Symbol("@echo"), +)) + +const _FORBIDDEN_MACROS = Set(( + Symbol("@generated"), Symbol("@eval"), Symbol("@fastmath"), +)) + +const _FORBIDDEN_CALLS = Set(( + :eval, :invokelatest, :ccall, :unsafe_load, :unsafe_store!, +)) + +function _push_once!(findings::Vector{Finding}, code::Symbol, line::Int, message::String) + # A malformed or deeply nested syntax tree can encounter the same policy + # violation through multiple wrappers. Keep reports deterministic and tidy. + any(f -> f.code === code && f.line == line && f.message == message, findings) || + push!(findings, Finding(code, max(line, 1), message)) + return nothing +end + +function _callee_symbol(x) + x isa Symbol && return x + if x isa GlobalRef + return x.name + elseif x isa Expr && x.head === :. && !isempty(x.args) + lastarg = last(x.args) + lastarg isa QuoteNode && return lastarg.value isa Symbol ? lastarg.value : nothing + lastarg isa Symbol && return lastarg + end + return nothing +end + +function _is_short_function_definition(x) + x isa Expr && x.head === :(=) && !isempty(x.args) || return false + signature = first(x.args) + # Return types and type parameters can wrap the call signature in either order. + while signature isa Expr && signature.head in (:(::), :where) && !isempty(signature.args) + signature = first(signature.args) + end + return signature isa Expr && signature.head === :call +end +_is_function_expr(x) = x isa Expr && (x.head === :function || _is_short_function_definition(x)) +_macro_symbol(x) = x isa Symbol ? x : _callee_symbol(x) + +"""Walk parsed Julia Expr nodes and report policy violations.""" +function _walk!(x, verified::Bool, mutation_score, line::Int, + findings::Vector{Finding}; nested_function::Bool=false) + x isa LineNumberNode && return Int(x.line) + x isa QuoteNode && return line + x isa Expr || return line + + if x.head in (:error, :incomplete) + _push_once!(findings, :APX_PARSE_ERROR, line, + "JuliaSyntax returned an incomplete or erroneous syntax node") + elseif x.head === :global + _push_once!(findings, :APX_GLOBAL_MUTATION, line, + "global declarations are outside the verified capability subset") + elseif x.head === :foreigncall + _push_once!(findings, :APX_UNMODELED_CCALL, line, + "lowered foreign calls require a checked Idris2/Zig ABI manifest") + elseif x.head === :call && !isempty(x.args) + callee = _callee_symbol(first(x.args)) + if callee in _FORBIDDEN_CALLS + code = callee === :ccall ? :APX_UNMODELED_CCALL : :APX_DYNAMIC_ESCAPE + message = callee === :ccall ? + "ccall is not yet verified; use a checked ABI wrapper only after the FFI phase" : + "$(callee) is forbidden in the closed verified subset" + _push_once!(findings, code, line, message) + end + end + + if x.head === :macrocall && !isempty(x.args) + macro_name = _macro_symbol(first(x.args)) + line_arg = findfirst(arg -> arg isa LineNumberNode, x.args) + macro_line = line_arg === nothing ? line : Int(x.args[line_arg].line) + if macro_name in _FORBIDDEN_MACROS + _push_once!(findings, :APX_FORBIDDEN_MACRO, macro_line, + "$(macro_name) is forbidden in the verified subset") + elseif macro_name === Symbol("@inbounds") + if !verified + _push_once!(findings, :APX_INBOUNDS_OUTSIDE_VERIFIED, macro_line, + "@inbounds is allowed only inside an @verified function") + end + if mutation_score === nothing || mutation_score < 95 + _push_once!(findings, :APX_MUTATION_GATE, macro_line, + "@inbounds requires mutation score >= 95%; supplied score is " * + (mutation_score === nothing ? "missing" : string(mutation_score, "%"))) + end + elseif !(macro_name in _CONTRACT_MACROS) && verified + _push_once!(findings, :APX_UNMODELED_MACRO, macro_line, + "macro $(macro_name) has no reviewed verifier elaborator") + end + + # @verified is only a marker when it directly wraps a function. It is + # never expanded/evaluated by this package. + if macro_name === Symbol("@verified") + payload = Any[arg for arg in x.args[2:end] if !(arg isa LineNumberNode)] + if length(payload) != 1 || !_is_function_expr(only(payload)) + _push_once!(findings, :APX_INVALID_VERIFIED_MARKER, macro_line, + "@verified must directly annotate one function definition") + for arg in x.args[2:end] + if arg isa LineNumberNode + line = Int(arg.line) + continue + end + line = _walk!(arg, false, mutation_score, line, findings) + end + return line + end + target = only(payload) + return _walk!(target, true, mutation_score, line, findings; nested_function=true) + end + end + + # A nested function is a new proof boundary: an outer @verified annotation + # does not implicitly certify locally defined methods. + is_function_definition = x.head === :function || _is_short_function_definition(x) + child_verified = is_function_definition && !nested_function ? false : verified + current_line = line + for arg in x.args + if arg isa LineNumberNode + current_line = Int(arg.line) + else + current_line = _walk!(arg, child_verified, mutation_score, current_line, findings) + end + end + return current_line +end + +""" + audit_source(source; filename="", mutation_score=nothing) + +Parse Julia source with JuliaSyntax.jl and enforce the initial fail-closed +source policy. `mutation_score` is an optional percentage in `0:100`; an +`@inbounds` expression requires a supplied score of at least 95. This is only a +policy gate: it does not discharge bounds VCs or establish a proof. + +The audit intentionally does not execute macros or source code. Unknown macros +inside `@verified` bodies and unmodeled foreign calls are rejected. +""" +function audit_source(source::AbstractString; filename::AbstractString="", + mutation_score::Union{Nothing,Real}=nothing) + if mutation_score !== nothing && !(0 <= mutation_score <= 100) + throw(ArgumentError("mutation_score must be a percentage between 0 and 100")) + end + + findings = Finding[] + expr = try + JuliaSyntax.parseall(Expr, String(source)) + catch err + _push_once!(findings, :APX_PARSE_ERROR, 1, + "JuliaSyntax could not parse source: " * sprint(showerror, err)) + nothing + end + + if expr !== nothing + _walk!(expr, false, mutation_score, 1, findings) + end + + status = isempty(findings) ? :policy_clean : :rejected + return AuditReport(String(filename), status, findings) +end + +"""Read and audit a Julia source file.""" +function audit_file(path::AbstractString; kwargs...) + return audit_source(read(path, String); filename=String(path), kwargs...) +end + +end # module Apodeixis diff --git a/test/runtests.jl b/test/runtests.jl new file mode 100644 index 0000000..705fc36 --- /dev/null +++ b/test/runtests.jl @@ -0,0 +1,423 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) Jonathan D.A. Jewell + +using Test +using Apodeixis + +codes(report) = Set(f.code for f in report.findings) + +@testset "Apodeixis source-policy MVP" begin + @testset "admitted declarations are parsed, not expanded" begin + report = audit_source(""" + @verified function positive(x::Int) + @pre x > 0 + @post x > 0 + @tier ExactLinear + @cap(pure) + x + end + """) + @test report.status === :policy_clean + @test isempty(report.findings) + @test is_policy_clean(report) + end + + @testset "short function signature wrappers preserve verification boundaries" begin + for signature in ( + "f(A)", + "f(A)::Int", + "f(A::T) where T", + "f(A::T)::Int where T", + "(f(A::T) where T)::Int", + "f(A::Vector{T})::T where T<:Integer", + "f(A::Vector{T}, x::S)::T where T where S", + ) + body = "$signature = (@inbounds A[1])" + + annotated = audit_source("@verified $body"; mutation_score=100) + @test is_policy_clean(annotated) + @test isempty(annotated.findings) + + nested = audit_source(""" + @verified function outer(A) + $body + f(A) + end + """; mutation_score=100) + @test codes(nested) == Set((:APX_INBOUNDS_OUTSIDE_VERIFIED,)) + + nested_annotated = audit_source(""" + @verified function outer(A) + @verified $body + f(A) + end + """; mutation_score=100) + @test is_policy_clean(nested_annotated) + end + + # A typed variable assignment is not a short function definition. + invalid = audit_source("@verified x::Int = 1") + @test codes(invalid) == Set((:APX_INVALID_VERIFIED_MARKER,)) + end + + @testset "inbounds needs both policy gates" begin + source = """ + @verified function getfirst(A::Vector{Int}) + @inbounds A[1] + end + """ + missing_score = audit_source(source) + @test :APX_INBOUNDS_OUTSIDE_VERIFIED ∉ codes(missing_score) + @test :APX_MUTATION_GATE in codes(missing_score) + @test !is_policy_clean(missing_score) + + passing_gate = audit_source(source; mutation_score=95) + @test passing_gate.status === :policy_clean + + low_score = audit_source(source; mutation_score=94.99) + @test :APX_MUTATION_GATE in codes(low_score) + qualified_macro = audit_source(""" + @verified function getfirst(A::Vector{Int}) + Base.@inbounds A[1] + end + """; mutation_score=94) + @test :APX_MUTATION_GATE in codes(qualified_macro) + + unverified = audit_source("function f(A); @inbounds A[1]; end"; + mutation_score=100) + @test :APX_INBOUNDS_OUTSIDE_VERIFIED in codes(unverified) + end + + @testset "unsafe escape hatches fail closed" begin + for source in ( + "@eval const x = 1", + "Base.invokelatest(identity, 1)", + "function f(p); ccall(:f, Cvoid, (), p); end", + "@generated function f(x); x; end", + "@fastmath 1.0 + 2.0", + "Base.@fastmath 1.0 + 2.0", + "@verified function f(); global mutable_state = 1; end", + ) + @test !is_policy_clean(audit_source(source)) + end + @test :APX_UNMODELED_CCALL in codes( + audit_source("function f(p); ccall(:f, Cvoid, (), p); end")) + for source in ( + "global mutable_state = 1", + "global mutable_state", + "@verified function f(); global mutable_state = 1; end", + ) + report = audit_source(source) + @test report.status === :rejected + @test codes(report) == Set((:APX_GLOBAL_MUTATION,)) + end + end + + @testset "unelaborated macros and nested verification boundaries" begin + unmodeled = audit_source(""" + @verified function f(x) + @mystery x + end + """) + @test :APX_UNMODELED_MACRO in codes(unmodeled) + + # Parsing must never execute user macro definitions or invocations. + no_expansion = audit_source(""" + macro explosive() + error(\"macro was expanded\") + end + @verified function f(x) + @explosive x + end + """) + @test :APX_UNMODELED_MACRO in codes(no_expansion) + + nested = audit_source(""" + @verified function outer(A) + inner(B) = (@inbounds B[1]) + inner(A) + end + """; mutation_score=100) + @test :APX_INBOUNDS_OUTSIDE_VERIFIED in codes(nested) + end + + @testset "parse errors and score validation are explicit" begin + @test :APX_INVALID_VERIFIED_MARKER in codes(audit_source("@verified begin; 1; end")) + @test :APX_PARSE_ERROR in codes(audit_source("function (")) + @test_throws ArgumentError audit_source("x = 1"; mutation_score=100.1) + @test_throws ArgumentError audit_source("x = 1"; mutation_score=-0.1) + end +end + +@testset "Audit API and policy regressions" begin + @testset "clean input and report metadata" begin + for source in ("", " \n\t", "# eval(:x) and @fastmath are comments", + "message = \"eval(:x); @inbounds A[1]\"", + "evaluation(x) = x; invokelatest_value = :eval") + report = audit_source(source) + @test report isa AuditReport + @test report.filename == "" + @test report.status === :policy_clean + @test isempty(report.findings) + @test is_policy_clean(report) + end + source = SubString("x = 1", 1, 5) + filename = SubString("α source.jl", 1) + report = audit_source(source; filename=filename) + @test report.filename == String(filename) + @test is_policy_clean(report) + end + + @testset "each unsafe call and macro, including qualified names" begin + for call in ("eval(:x)", "invokelatest(identity, 1)", + "unsafe_load(p)", "unsafe_store!(p, 1)", + "ccall(:f, Cvoid, ())") + expected = startswith(call, "ccall") ? :APX_UNMODELED_CCALL : :APX_DYNAMIC_ESCAPE + for prefix in ("", "Base."), verified in (false, true) + expression = prefix * call + source = verified ? "@verified f(p) = ($expression)" : expression + @testset "$source" begin + report = audit_source(source) + @test report.status === :rejected + @test !is_policy_clean(report) + @test codes(report) == Set([expected]) + @test all(f -> f isa Finding && f.line >= 1 && !isempty(f.message), + report.findings) + end + end + end + for invocation in ("@eval x = 1", "@generated function f(x); x; end", + "@fastmath 1.0 + 2.0") + for prefix in ("", "Base.") + expression = prefix * invocation + for source in (expression, "@verified function f(); $expression; end") + @test codes(audit_source(source)) == Set([:APX_FORBIDDEN_MACRO]) + end + end + end + end + + @testset "contract syntax and annotation boundaries" begin + for marker in ("@pre x > 0", "@post x > 0", "@invariant x > 0", + "@cap(pure)", "@tier ExactLinear", "@noalloc x", "@echo x") + for prefix in ("", "Contracts.") + @test is_policy_clean(audit_source( + "@verified function f(x); $(prefix)$(marker); x; end")) + end + end + for source in ("@verified f(A) = (@inbounds A[1])", + "Contracts.@verified function f(A); @inbounds A[1]; end") + @test is_policy_clean(audit_source(source; mutation_score=95)) + end + for source in ("@verified", "@verified x", "@verified f(x)", + "@verified 1 2", "@verified begin; f(x) = x; end") + @test codes(audit_source(source)) == Set([:APX_INVALID_VERIFIED_MARKER]) + end + # An invalid marker must still audit its payload without granting scope. + invalid = audit_source("@verified begin; @inbounds A[1]; eval(:x); end") + @test codes(invalid) == Set([:APX_INVALID_VERIFIED_MARKER, + :APX_INBOUNDS_OUTSIDE_VERIFIED, + :APX_MUTATION_GATE, :APX_DYNAMIC_ESCAPE]) + + for definition in ("inner(B) = (@inbounds B[1])", + "function inner(B); @inbounds B[1]; end") + source = "@verified function outer(A); $definition; inner(A); end" + @test codes(audit_source(source; mutation_score=100)) == + Set([:APX_INBOUNDS_OUTSIDE_VERIFIED]) + # A nested method can establish its own independent boundary. + annotated = "@verified function outer(A); @verified $definition; inner(A); end" + @test is_policy_clean(audit_source(annotated; mutation_score=100)) + end + siblings = "@verified f(A) = (@inbounds A[1])\ng(A) = (@inbounds A[1])" + @test codes(audit_source(siblings; mutation_score=100)) == + Set([:APX_INBOUNDS_OUTSIDE_VERIFIED]) + + # The MVP rejects global declarations only within the annotated body. + @test is_policy_clean(audit_source("global mutable_state = 1")) + @test is_policy_clean(audit_source("function f(); global mutable_state = 1; end")) + @test codes(audit_source("@verified f() = (global mutable_state = 1)")) == + Set([:APX_GLOBAL_MUTATION]) + @test is_policy_clean(audit_source("@mystery 1")) + @test codes(audit_source("@verified f(x) = (Other.@mystery x)")) == + Set([:APX_UNMODELED_MACRO]) + end + + @testset "mutation gate endpoints and non-finite inputs" begin + source = "@verified f(A) = (@inbounds A[1])" + for score in (nothing, 0, 94, prevfloat(95.0)) + @test codes(audit_source(source; mutation_score=score)) == Set([:APX_MUTATION_GATE]) + end + for score in (95, 95.0, nextfloat(95.0), 95//1, big"95", 100) + @test is_policy_clean(audit_source(source; mutation_score=score)) + end + for score in (0, 100) + @test is_policy_clean(audit_source("x = 1"; mutation_score=score)) + end + for score in (-eps(), nextfloat(100.0), NaN, Inf, -Inf) + @test_throws ArgumentError audit_source("x = 1"; mutation_score=score) + end + # The score cannot compensate for a missing @verified boundary. + for (score, expected) in ((nothing, Set([:APX_INBOUNDS_OUTSIDE_VERIFIED, + :APX_MUTATION_GATE])), + (95, Set([:APX_INBOUNDS_OUTSIDE_VERIFIED]))) + @test codes(audit_source("@inbounds A[1]"; mutation_score=score)) == expected + end + end + + @testset "diagnostic locations, deduplication, and parse failures" begin + source = "\n@eval x = 1\nBase.eval(:x)\n@fastmath 1.0 + 2.0\n" + report = audit_source(source; filename="diagnostics.jl") + @test report.filename == "diagnostics.jl" + @test [(f.code, f.line) for f in report.findings] == + [(:APX_FORBIDDEN_MACRO, 2), (:APX_DYNAMIC_ESCAPE, 3), (:APX_FORBIDDEN_MACRO, 4)] + repeated = audit_source(source) + @test [(f.code, f.line, f.message) for f in report.findings] == + [(f.code, f.line, f.message) for f in repeated.findings] + duplicates = audit_source("eval(:x); eval(:y)\neval(:z)") + @test [(f.code, f.line) for f in duplicates.findings] == + [(:APX_DYNAMIC_ESCAPE, 1), (:APX_DYNAMIC_ESCAPE, 2)] + distinct = audit_source("eval(:x); unsafe_load(p)") + @test length(distinct.findings) == 2 + @test length(Set(f.message for f in distinct.findings)) == 2 + for source in ("function (", "@verified function f(x)\n x", "x = [1,", "\"unterminated") + report = audit_source(source; filename="broken.jl") + @test report.status === :rejected + @test !is_policy_clean(report) + @test codes(report) == Set([:APX_PARSE_ERROR]) + @test report.filename == "broken.jl" + @test all(f -> f.line >= 1 && !isempty(f.message), report.findings) + end + end + + @testset "source, macro definitions, and files are never executed" begin + mktempdir() do dir + marker = joinpath(dir, "executed") + effect = "write($(repr(marker)), \"executed\")" + for source in (effect, "macro touch_marker(); $effect; :(nothing); end\n@touch_marker()") + @test is_policy_clean(audit_source(source)) + @test !ispath(marker) + end + path = joinpath(dir, "source α with spaces.jl") + source = "@verified f(A) = (@inbounds A[1])\n$effect" + write(path, source) + report = audit_file(path; mutation_score=95) + @test report.filename == path + @test is_policy_clean(report) + @test codes(audit_file(path)) == Set([:APX_MUTATION_GATE]) + @test read(path, String) == source + @test !ispath(marker) + write(path, "eval(:x)") + @test codes(audit_file(path)) == Set([:APX_DYNAMIC_ESCAPE]) + write(path, "function (") + @test codes(audit_file(path)) == Set([:APX_PARSE_ERROR]) + @test_throws ArgumentError audit_file(path; mutation_score=NaN) + @test_throws SystemError audit_file(joinpath(dir, "missing.jl")) + end + end +end + +# Including the CLI exercises main directly and must not exit the test runner. +module CLIUnderTest +include(joinpath(@__DIR__, "..", "scripts", "apodeixis.jl")) + +function invoke(args) + mktemp() do _, output + mktemp() do _, errors + status = redirect_stdout(output) do + redirect_stderr(errors) do + main(args) + end + end + seekstart(output) + seekstart(errors) + return (status=status, out=read(output, String), err=read(errors, String)) + end + end +end +end + +@testset "CLI argument handling and audit output" begin + for flag in ("--help", "-h") + result = CLIUnderTest.invoke([flag]) + @test result.status == 0 + @test occursin("Usage:", result.out) + @test occursin("not a verification proof", result.out) + @test isempty(result.err) + end + result = CLIUnderTest.invoke(String[]) + @test result.status == 2 + @test occursin("Usage:", result.out) + @test isempty(result.err) + + mktempdir() do dir + path = joinpath(dir, "source with spaces.jl") + write(path, "identity(1)\n") + result = CLIUnderTest.invoke(["audit", path]) + @test result == (status=0, out="POLICY CLEAN (NOT VERIFIED): $path\n", err="") + + for (args, diagnostic) in ((["verify", path], "Usage:"), + (["audit"], "Usage:"), + (["audit", "--mutation-score"], "missing percentage"), + (["audit", "--mutation-score", "oops", path], "invalid mutation score"), + (["audit", "--unknown", path], "unknown option"), + (["audit", path, "second.jl"], "expected exactly one source file"), + (["audit", joinpath(dir, "missing.jl")], "file not found"), + (["audit", dir], "file not found")) + @testset "$args" begin + result = CLIUnderTest.invoke(args) + @test result.status == 2 + @test isempty(result.out) + @test occursin(diagnostic, result.err) + end + end + for score in ("-0.1", "100.1", "NaN", "Inf", "-Inf") + result = CLIUnderTest.invoke(["audit", "--mutation-score", score, path]) + @test result.status == 2 + @test isempty(result.out) + @test occursin("mutation_score must be a percentage", result.err) + end + + write(path, "\nBase.eval(:x)\n@fastmath 1.0 + 2.0\n") + result = CLIUnderTest.invoke(["audit", path]) + @test result.status == 1 + @test startswith(result.out, "REJECTED: $path\n") + @test occursin("APX_DYNAMIC_ESCAPE [line 2]", result.out) + @test occursin("APX_FORBIDDEN_MACRO [line 3]", result.out) + @test !occursin("POLICY CLEAN", result.out) + @test isempty(result.err) + + write(path, "@verified f(A) = (@inbounds A[1])") + for args in (["audit", "--mutation-score", "95", path], + ["audit", path, "--mutation-score", "97.5"]) + result = CLIUnderTest.invoke(args) + @test result.status == 0 + @test startswith(result.out, "POLICY CLEAN (NOT VERIFIED):") + @test isempty(result.err) + end + for args in (["audit", path], ["audit", "--mutation-score", "94.99", path]) + result = CLIUnderTest.invoke(args) + @test result.status == 1 + @test occursin("APX_MUTATION_GATE", result.out) + @test isempty(result.err) + end + write(path, "function (") + result = CLIUnderTest.invoke(["audit", path]) + @test result.status == 1 + @test occursin("APX_PARSE_ERROR", result.out) + @test isempty(result.err) + + # Check the executable guard propagates main's success, rejection, + # and usage statuses to the operating system. + script = joinpath(@__DIR__, "..", "scripts", "apodeixis.jl") + project = dirname(@__DIR__) + for (args, status, output) in ((["--help"], 0, "Usage:"), + (["audit", path], 1, "REJECTED:"), + (String[], 2, "Usage:")) + command = `$(Base.julia_cmd()) --startup-file=no --project=$project $script $args` + io = IOBuffer() + process = run(pipeline(ignorestatus(command); stdout=io, stderr=io)) + @test process.exitcode == status + @test occursin(output, String(take!(io))) + end + end +end