Support host generation and AutoDeduct-owned verification

README.md

@@ -138,7 +138,37 @@ python3 skill/scripts/generate_acsl.py input/main.c -o results/main.annotated.c
 
 ## AutoDeduct Integration
 
-LOGOS implements the skill interface used by AutoDeduct's [`llm-skill-mode` branch](https://github.com/rse-verification/auto-deduct/tree/llm-skill-mode). Point `AUTODEDUCT_LLM_SKILL` at the absolute path of `skill/SKILL.md`; global skill installation is unnecessary when AutoDeduct supplies this path. The complete skill directory, Python, libclang, Frama-C WP, and configured provers must be available to the runner.
+LOGOS implements the skill interface used by AutoDeduct's [`llm-skill-mode` branch](https://github.com/rse-verification/auto-deduct/tree/llm-skill-mode). Point `AUTODEDUCT_LLM_SKILL` at the absolute path of `skill/SKILL.md`; global skill installation is unnecessary when AutoDeduct supplies this path.
+
+AutoDeduct is the host launcher. It runs authenticated Codex locally with a
+`workflow: "generate-only"` task; Codex writes contract JSON and stops.
+AutoDeduct then invokes this repository's Python wrapper, checks the resulting
+source and proof evidence, and writes its final report. The model does not
+launch verification or write the verification report.
+
+```shell
+# Host Python, Codex, libclang, Frama-C/WP and provers installed locally:
+autodeduct llm --llm-runtime local \
+  --llm-skill /absolute/path/to/logos/skill/SKILL.md path/to/program.c
+
+# Host Python and authenticated Codex; LOGOS wrapper and tools in Docker:
+autodeduct llm --llm-runtime docker \
+  --llm-skill /absolute/path/to/logos/skill/SKILL.md path/to/program.c
+```
+
+Docker is optional. With Docker, build AutoDeduct's `auto-deduct:logos` image
+from this checkout, then invoke the launcher on the host. The container includes
+Python, libclang, the LOGOS wrapper, Frama-C/WP and provers. It contains no Codex
+installation or login credentials. Inputs/headers are mounted read-only, outputs
+are writable, and the verifier container has no network access. Host libclang or
+Frama-C installations are unnecessary for this runtime. Running Codex inside a
+container is unsupported by this integration. Docker mode supports Linux/macOS
+and Windows through WSL; native Windows Frama-C verification is not validated.
+See AutoDeduct's [setup instructions](https://github.com/rse-verification/auto-deduct/blob/llm-skill-mode/docs/INSTALLATION.md#logos-for-llm-mode).
+
+Standalone LOGOS usage still requires local Python and libclang, and local
+Frama-C/WP with provers when verification is requested. Older AutoDeduct tasks
+without the generation-only marker retain the skill's full workflow.
 
 The wrapper accepts repeated `--frama-c-option=VALUE` arguments and writes process evidence with `--verification-json FILE` (requires `--verify`):
 

skill/SKILL.md

@@ -13,6 +13,9 @@ Use this skill when:
 
 ## Prerequisites
 
+- When AutoDeduct sets `workflow: "generate-only"` in its task, the host agent
+  only reads the source and writes contract JSON. Python/libclang/Frama-C are
+  wrapper dependencies and may live inside AutoDeduct's verifier container.
 - Python 3 and the libclang shared library are required. The `clang` executable alone is insufficient; Python loads libclang directly without additional Python bindings.
 - macOS: install Apple Command Line Tools with `xcode-select --install`, or LLVM with `brew install llvm`. Standard Apple and Homebrew library paths are detected automatically.
 - Debian/Ubuntu: install `libclang-dev` with `sudo apt install libclang-dev`.
@@ -38,6 +41,23 @@ Use this skill when:
 
 When AutoDeduct supplies `llm-task.json`, read its absolute artifact paths and use them instead of the default `contracts/` and `results/` paths. Invoke `scripts/generate_acsl.py` relative to this SKILL.md's directory, even when the working directory is the task output directory.
 
+For tasks with `workflow: "generate-only"`:
+
+1. Read the source and existing ACSL; author contracts for undocumented functions.
+2. Write only the specified `contracts` JSON, including `metadata.source_sha256`
+   computed from Python's UTF-8 source text as described below.
+3. Stop after generation. AutoDeduct runs the Python wrapper and verification;
+   do not invoke the wrapper, Docker, or Frama-C, or write annotated source or
+   verification JSON. Report generation issues accurately in your final message.
+
+The supported AutoDeduct launcher runs Codex on the host. Its `local` runtime
+executes the wrapper locally; its `docker` runtime executes the wrapper and
+Frama-C/provers in a container without Codex or login credentials. Running
+AutoDeduct's Codex workflow inside a container is unsupported.
+
+For older tasks without `workflow: "generate-only"`, follow the complete
+workflow below. Standalone interactive use also retains the default flow.
+
 - Include `metadata.source_sha256` computed from the UTF-8 source text read by Python (`Path(source).read_text(encoding="utf-8").encode("utf-8")`).
 - Author structured function contracts, then run the wrapper with the task's `source`, `--contracts`, `-o`, `--verify`, and `--verification-json` paths.
 - Forward **each** item of `verification_options` as a separate `--frama-c-option=VALUE`, in order (including option values such as the entry function name).