Clarify LOGOS guides and preserve source safely

docs/AUTODEDUCT.md

@@ -0,0 +1,111 @@
+# AutoDeduct Integration
+
+[Documentation index](../README.md#documentation)
+
+LOGOS supplies the contract-generation skill and verification wrapper used by
+AutoDeduct's [`llm-skill-mode` branch](https://github.com/rse-verification/auto-deduct/tree/llm-skill-mode).
+The compatible LOGOS changes are on `llm-host-runtime`.
+
+Follow AutoDeduct's [LLM setup and usage guide](https://github.com/rse-verification/auto-deduct/blob/llm-skill-mode/docs/LLM.md)
+for host installation, the supported LOGOS revision, and Docker image builds.
+Its [usage index](https://github.com/rse-verification/auto-deduct/blob/llm-skill-mode/docs/USAGE.md)
+separates LLM and deductive commands; its
+[installation guide](https://github.com/rse-verification/auto-deduct/blob/llm-skill-mode/docs/INSTALLATION.md)
+covers the traditional toolchain.
+
+## Choose Where Verification Runs
+
+| Requirement | `--llm-runtime local` | `--llm-runtime docker` |
+|---|---|---|
+| Host Python and AutoDeduct launcher | Required | Required |
+| Host Codex CLI and login | Required | Required |
+| Local LOGOS checkout and skill path | Required | Skill extracted from verifier image |
+| Wrapper, libclang, Frama-C/WP, and provers | Installed on host | Packaged in verifier image |
+| Docker | Unnecessary | Required |
+
+Both modes start from your host terminal. `local` is the default. Docker runs
+only when selected explicitly.
+
+The host needs the AutoDeduct executable available through `PATH` to use the
+name `autodeduct`. A separate package installation is unnecessary: clone the
+repository and use `./bin/autodeduct`, or add its `bin/` directory to `PATH`.
+
+From the AutoDeduct checkout, after configuring the chosen runtime:
+
+```bash
+./bin/autodeduct llm --llm-runtime local \
+  --llm-skill /absolute/path/to/logos/skill/SKILL.md \
+  --output-dir /project/results/autodeduct /project/input/program.c
+```
+
+For Docker verification:
+
+```bash
+./bin/autodeduct llm --llm-runtime docker \
+  --output-dir /project/results/autodeduct /project/input/program.c
+```
+
+For local verification, you can set `AUTODEDUCT_LLM_SKILL` to the absolute skill
+path instead of repeating `--llm-skill`. Global skill installation is unnecessary.
+
+Docker verification uses the skill packaged at `/opt/logos/skill/SKILL.md` in
+the prepared image. AutoDeduct resolves the image to an immutable image ID,
+extracts its skill into a temporary host cache, and gives that path to Codex.
+The wrapper runs from the same image ID. Users of a prepared image need no
+local LOGOS checkout or `--llm-skill` flag.
+
+Building that image from source still requires a LOGOS checkout as the named
+Docker build context. This is a build requirement, separate from the runtime
+requirements of someone using an already prepared image. Follow
+[AutoDeduct's image build instructions](https://github.com/rse-verification/auto-deduct/blob/llm-skill-mode/docs/LLM.md#build-the-verifier-image).
+
+## Why the Launcher Runs on the Host
+
+The launcher coordinates host Codex and the verification tools. Codex uses the
+host's existing login and sandbox. In Docker mode, AutoDeduct mounts the input
+and headers read-only, mounts outputs writable, and runs the wrapper in the
+verifier container. The agent does not need Docker access.
+
+Running Codex inside the AutoDeduct container is unsupported and rejected by
+the LLM launcher. Earlier attempts encountered nested sandbox restrictions and
+introduced container authentication setup. The supported verifier image has no
+Codex installation or model credentials and runs without network access.
+
+Docker mode supports Linux/macOS and Windows through WSL. Native Windows
+Frama-C verification is not validated. The extracted skill and wrapper come
+from the same pinned image; use a compatible image from AutoDeduct's setup guide.
+
+## The Contract and Report Handoff
+
+1. AutoDeduct selects the local skill or extracts the Docker image's skill,
+   checks verification dependencies, and writes `llm-task.json` with
+   source/output paths, verification options, and `workflow: "generate-only"`.
+2. Host Codex reads the selected LOGOS skill and source, then writes
+   `llm-contracts.json`, including the source hash. It stops after generation.
+3. AutoDeduct checks that handoff, then explicitly invokes
+   `skill/scripts/generate_acsl.py` with the contracts, annotated output path,
+   `--verify`, `--verification-json`, and requested Frama-C options.
+4. The wrapper annotates the source, runs Frama-C WP, and writes verification
+   JSON plus text/PDF reports.
+5. AutoDeduct reads the wrapper's JSON evidence, checks source changes and
+   proof results, and writes its final `report.json`.
+
+The LLM writes contract JSON. The wrapper writes verification evidence. The
+text/PDF reports support human review; AutoDeduct consumes the JSON evidence.
+Generating contract JSON alone is insufficient for a successful verification.
+
+Docker runs retain an `llm-skill.md` snapshot for review. The recorded image ID
+and skill hash identify the packaged instructions and verifier used for that run.
+
+Standalone LOGOS and older tasks without the generation-only marker retain the
+skill's complete generation, annotation, and optional verification workflow.
+
+## Scope of This Mode
+
+The current AutoDeduct runner uses Codex-specific CLI arguments. Changing
+`--llm-runner` to an arbitrary LLM executable is insufficient to support another
+provider; it needs an adapter that produces the same contract handoff.
+
+LLM mode does not run Saida/TriCera, ISP/Eva, or the traditional ISP
+reachable-helper check. See [verification and scope](VERIFICATION.md) for LOGOS
+limitations and proof interpretation.

docs/SETUP.md

@@ -0,0 +1,122 @@
+# Setup
+
+[Documentation index](../README.md#documentation)
+
+Choose [standalone usage](USAGE.md) or [AutoDeduct integration](AUTODEDUCT.md)
+before installing dependencies. AutoDeduct's Docker runtime supplies the wrapper
+dependencies in its verifier image; the host still needs Python, authenticated
+Codex CLI, AutoDeduct, and Docker. The launcher extracts the skill from the
+prepared verifier image for the host agent. A local LOGOS checkout is required
+for standalone use and AutoDeduct's local runtime; it is unnecessary when
+running AutoDeduct with an already prepared Docker image.
+
+## Standalone and Local Verification Requirements
+
+- Python 3.10 or newer.
+- The libclang shared library, loadable by Python, for C parsing.
+- Codex or manually authored contract JSON for undocumented functions. The
+  wrapper does not infer contract semantics.
+- Frama-C with the WP plugin and configured provers when verification is requested.
+
+LOGOS loads libclang directly with `ctypes`. The `clang` executable alone is
+insufficient; the Python `clang` package is unnecessary.
+
+## Install libclang
+
+| Platform | Installation |
+|---|---|
+| macOS | `xcode-select --install` for Apple Command Line Tools, or `brew install llvm` |
+| Debian/Ubuntu | `sudo apt install libclang-dev` |
+| Windows x64 | `winget install --id LLVM.LLVM --exact`, or the [official LLVM installer](https://github.com/llvm/llvm-project/releases) |
+
+On Windows, use x64 Python with x64 LLVM and confirm that
+`C:\Program Files\LLVM\bin\libclang.dll` exists.
+
+LOGOS searches standard Apple Command Line Tools, Xcode, and Homebrew LLVM
+locations on macOS, and shared-library locations on Linux. On Windows it checks
+`%ProgramFiles%\LLVM\bin\libclang.dll` and Python's library discovery.
+
+For a custom installation or a discovery failure, set `LIBCLANG_FILE` to the
+compatible shared library before starting a new LOGOS process:
+
+```bash
+# Homebrew LLVM on macOS:
+export LIBCLANG_FILE="$(brew --prefix llvm)/lib/libclang.dylib"
+
+# Linux: adjust this path to your installed version.
+# export LIBCLANG_FILE=/usr/lib/llvm-19/lib/libclang.so
+```
+
+PowerShell:
+
+```powershell
+$env:LIBCLANG_FILE = 'C:\Program Files\LLVM\bin\libclang.dll'
+```
+
+`LIBCLANG_FILE` overrides automatic discovery. Its library must match the
+architecture of the Python process. A missing or unloadable library is an
+installation error; LOGOS stops before writing output instead of falling back
+to partial function detection.
+
+## Verification Tools
+
+Install Frama-C with WP and configure suitable provers, such as Alt-Ergo, using
+the instructions for your Frama-C distribution. The wrapper resolves `frama-c`
+from `PATH`. Check the executable before requesting verification:
+
+```bash
+frama-c -version
+frama-c -wp-help
+```
+
+The default wrapper command is `frama-c -wp <annotated-file>`. Additional
+verification options can be forwarded as described in
+[Verification and scope](VERIFICATION.md#verification-options).
+
+## Check the Installation
+
+From the LOGOS checkout:
+
+```bash
+python3 skill/scripts/generate_acsl.py --help
+python3 -m unittest discover -s tests -v
+```
+
+On Windows, use `python` if `python3` is unavailable. The tests check parsing,
+contract rendering, annotation, and verification-report handling. They do not
+replace a proof run against your program.
+
+Before verification, check its runtime dependencies:
+
+```bash
+python3 skill/scripts/generate_acsl.py --check-dependencies
+```
+
+This checks libclang and the `frama-c` executable without reading a source file
+or calling a model. Annotation-only use does not require Frama-C or this
+verification preflight. AutoDeduct uses it before generation because both LLM
+runtimes also verify. It does not establish that the prover setup can complete
+a proof.
+
+## Platform Coverage
+
+The native Windows x64 workflow runs the Python suite with automatic libclang
+discovery and an explicit DLL path. Tests include CRLF input, paths with spaces,
+and missing-library errors.
+
+Native Windows Frama-C verification, Windows ARM64, and 32-bit installations are
+not validated. Use WSL for AutoDeduct's Docker verification runtime. Full local
+AutoDeduct verification has not been validated end to end on every platform.
+
+## Skill Access
+
+An agent must actually read [SKILL.md](../skill/SKILL.md) to follow its workflow;
+having the repository on disk alone does not activate it. You can install the
+skill in your agent's skill directory or give the agent its full path explicitly.
+AutoDeduct supplies that path through `--llm-skill` or `AUTODEDUCT_LLM_SKILL`, so
+global skill installation is unnecessary for its local runtime. Its Docker
+runtime extracts `/opt/logos/skill/SKILL.md` from the selected image into a
+temporary host cache and uses the same pinned image for verification.
+`--llm-skill` and a separate local LOGOS checkout are unnecessary for Docker
+execution. Building the image from source still needs the LOGOS checkout as
+the build context; see [AutoDeduct integration](AUTODEDUCT.md).

docs/USAGE.md

@@ -0,0 +1,98 @@
+# Standalone Usage
+
+[Documentation index](../README.md#documentation) · [Setup](SETUP.md)
+
+Use this workflow when asking an agent to run LOGOS directly. For AutoDeduct's
+host launcher and runtime choices, see [AutoDeduct integration](AUTODEDUCT.md).
+
+## Prepare the External Project
+
+Keep input C files, contract JSON, annotated copies, and proof reports in your
+own project directory. The names `input/`, `contracts/`, and `results/` below are
+suggested folders in that external project; they are not shipped LOGOS content.
+
+The source must already contain at least one ACSL marker (`/*@` or `//@`) and
+must be valid C for the supported parser setup. Contracts must be provided for
+every detected function definition that lacks an existing function contract.
+The wrapper also recognizes existing contracts on prototypes and preserves them.
+
+## Ask Codex to Author Contracts
+
+Give Codex the full path to the skill and use paths from your project:
+
+```text
+Read /absolute/path/to/logos/skill/SKILL.md and use it on /project/input/program.c.
+Read the existing ACSL style, author structured contracts for undocumented
+functions, and save them to /project/contracts/program.contracts.json. Apply
+them with the LOGOS wrapper into /project/results/program.annotated.c, then
+verify with Frama-C WP and produce the reports.
+```
+
+This prompt requests verification. If you only want generation and annotation,
+say so; the skill otherwise asks before verification unless it was already
+requested. The LLM determines contract meaning. The wrapper requires explicit
+contracts and does not generate missing semantics on its own.
+
+## Contract JSON
+
+Prefer the structured `acsl-contracts-v2` schema defined in
+[the skill](../skill/SKILL.md#contract-schema). It maps function names to clause
+lists such as `requires`, `assigns`, and `ensures`. Additional fields support
+behaviors and other ACSL clauses. The wrapper renders those fields into ACSL.
+
+Legacy JSON mappings to raw ACSL strings are accepted by the wrapper, but the
+skill authors structured fields. Contracts for unknown functions or functions
+that already have ACSL are rejected, as are missing contracts for detected
+undocumented functions.
+
+Optional metadata records the intended source path and source hash. See
+[source matching](VERIFICATION.md#source-matching) for its exact behavior.
+
+## Apply Contracts Manually
+
+Use an absolute path to the LOGOS wrapper so the working directory can remain
+your external project:
+
+```bash
+python3 /absolute/path/to/logos/skill/scripts/generate_acsl.py \
+  /project/input/program.c \
+  --contracts /project/contracts/program.contracts.json \
+  -o /project/results/program.annotated.c \
+  --no-verify-prompt
+```
+
+`--no-verify-prompt` makes this annotation-only command suitable for automation.
+Without `-o`, the default output is `results/<input-stem>.annotated.c` relative
+to the current working directory. Use `--explain` to print how each detected
+function was handled.
+
+To overwrite the input deliberately, replace `-o` with `--in-place`:
+
+```bash
+python3 /absolute/path/to/logos/skill/scripts/generate_acsl.py \
+  /project/input/program.c \
+  --contracts /project/contracts/program.contracts.json \
+  --in-place --no-verify-prompt
+```
+
+Keep a recoverable copy before using `--in-place`.
+
+## Apply and Verify
+
+```bash
+python3 /absolute/path/to/logos/skill/scripts/generate_acsl.py \
+  /project/input/program.c \
+  --contracts /project/contracts/program.contracts.json \
+  -o /project/results/program.annotated.c \
+  --verify \
+  --verification-json /project/results/verification.json
+```
+
+The wrapper writes the annotated source, runs WP, and generates text and PDF
+reports. `--verification-json` is optional for standalone use and requires
+`--verify`. See [reports and success criteria](VERIFICATION.md#reports-and-success-criteria)
+before interpreting a successful process exit.
+
+In an interactive terminal, omitting both `--verify` and `--no-verify-prompt`
+causes the wrapper to ask whether to verify after annotation. Noninteractive
+commands do not prompt. Use `--verify` explicitly when verification is required.