Repository navigation
Add Fledge verification and north-delivery model-checking skills - #1743
Open
FelixHelin wants to merge 3 commits into
Open
FelixHelin wants to merge 3 commits into
FelixHelin wants to merge 3 commits into
Conversation
Project-local skill at .github/skills/verify: a stdlib helper builds fledge-local:dev from the checkout via .ci/local, launches labelled per-run containers with their own port and data volume, drives the REST API with recorded evidence in .verify-evidence/<run>/, and cleans up without touching unrelated containers. Seeds a feature map for health, auth/users, configuration, schedules/tasks, and backup, each checked against a live instance. Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com>
TLA+ model of the north service's delivery position (streams.last_object) across the load thread, send thread and shutdown, checked with TLC by scripts/check.py. The model reproduces three defects in today's code where the saved position can pass readings that were never sent: partial plugin_send counts, pipelineEnd advancing on a fully filtered block, and the sender advancing to getLastFetched() on an empty block. No product code is changed. Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com>
Keep the skill free of tooling other contributors may not have. Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com>
There was a problem hiding this comment.
🟡 Changes recommended
Cleanup can delete another checkout’s containers and volumes because repository ownership checks are incomplete or absent.
5 open issues
What changed in this PR
Adds two repository-local agent skills for REST verification and north-delivery model checking without changing Fledge runtime code.
Changes:
- Adds a Docker-backed REST driver with evidence capture, cleanup, and five feature recipes.
- Adds a bounded TLA+ delivery-position model, seven configurations, and a TLC runner that checks expected outcomes.
- Excludes generated verification evidence from Git and Docker build contexts.
| File | Description |
|---|---|
.gitignore |
Ignores generated verification evidence. |
.github/skills/verify/SKILL.md |
Documents verification workflow and proof standards. |
.github/skills/verify/scripts/fledge_verify.py |
Implements container lifecycle, API calls, and evidence capture. |
.github/skills/verify/features/schedules-tasks.md |
Provides schedule and task verification steps. |
.github/skills/verify/features/README.md |
Defines recipe structure and shared preconditions. |
.github/skills/verify/features/health.md |
Covers health, services, and anonymous access checks. |
.github/skills/verify/features/configuration.md |
Covers configuration changes, validation, and audit evidence. |
.github/skills/verify/features/backup.md |
Covers backup creation, completion, and file evidence. |
.github/skills/verify/features/auth-users.md |
Covers authentication, roles, users, and logout. |
.github/skills/north-delivery/SKILL.md |
Documents model scope, assumptions, and known modeled defects. |
.github/skills/north-delivery/scripts/check.py |
Runs TLC and reports expected outcomes and mapped traces. |
.github/skills/north-delivery/model/witness-send.cfg |
Checks reachability of complete delivery. |
.github/skills/north-delivery/model/witness-filter.cfg |
Checks reachability of complete filtering. |
.github/skills/north-delivery/model/today.cfg |
Enables all three modeled defect paths. |
.github/skills/north-delivery/model/sender-filtered.cfg |
Isolates sender-side empty-block advancement. |
.github/skills/north-delivery/model/partial-send.cfg |
Isolates partial-send position advancement. |
.github/skills/north-delivery/model/NorthDelivery.tla |
Models delivery-position updates and thread interleavings. |
.github/skills/north-delivery/model/fixed.cfg |
Checks the proposed corrected model. |
.github/skills/north-delivery/model/filter-end.cfg |
Isolates load-side filtered-block advancement. |
.dockerignore |
Excludes verification evidence from image builds. |
Review effort: Balanced
Comment on lines
+398
to
+400
| if lbl.get(LABEL_RUN) != name: | ||
| die("container {} lacks label {}={}; not removing what this script did not start".format( | ||
| inst["container"], LABEL_RUN, name)) |
Comment on lines
+408
to
+409
| if run(["docker", "volume", "inspect", inst["volume"]], check=False).returncode == 0: | ||
| run(["docker", "volume", "rm", inst["volume"]], check=False) |
|
|
||
| def tla2tools() -> Path: | ||
| if os.environ.get("TLA2TOOLS"): | ||
| jar = Path(os.environ["TLA2TOOLS"]) |
| def next_evidence_path(name, label): | ||
| d = run_dir(name) | ||
| d.mkdir(parents=True, exist_ok=True) | ||
| nums = [int(m.group(1)) for p in d.iterdir() for m in [re.match(r"^(\d{3})-", p.name)] if m] |
Comment on lines
+251
to
+253
| run(["docker", "run", "-d", "--name", cname, | ||
| "--label", "{}={}".format(LABEL_RUN, name), "--label", "{}={}".format(LABEL_REPO, str(REPO)), | ||
| "-p", "127.0.0.1:{}:8081".format(port), "-v", "{}:{}".format(volume, FLEDGE_DATA), IMAGE]) |
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Add two repository-local agent skills without changing Fledge runtime code:
verify: a standard-library Python driver that builds this checkout with the existing local Docker setup, launches isolated Fledge instances, drives the authenticated REST API, records evidence, and cleans up its containers. Includes recipes for health, authentication/users, configuration, schedules/tasks, and backup.north-delivery: a bounded TLA+ model of delivery-position updates, seven TLC configurations, and a Python runner with expected outcomes and source-mapped counterexample traces.Review order
87e4f7036— REST verification skill, driver, feature recipes, and ignore rules.2795ba21e— north-delivery model, configurations, runner, assumptions, and findings.Start with each skill's
SKILL.mdfor its scope and run commands.Portability and prerequisites
All project-specific skill sources, recipes, model files, and runners are committed. The Docker/Compose build files they reference already exist on
develop; neither runner depends on this conversation or its scratch files.Running the REST driver needs Python 3.8+, Git, Docker with Compose v2, and access to build dependencies. The model checker needs Python and either Java 11+ or Docker; it downloads a pinned, SHA-256-checked TLC JAR unless
TLA2TOOLSis supplied.This PR does not vendor pstack or publish personal Copilot model choices/routing instructions. Those remain user-local. The two runners work without pstack; optional
/statechartand maintenance commands require the separately installed pstack plugin. Generated images, caches, evidence, and diagrams are not committed and can be recreated.Verification
A TLC
PASSmeans the expected outcome occurred, not that today's Fledge implementation is defect-free. Four configurations reproduce modeled delivery-position violations, two are intentional reachability witnesses, andfixedchecks a proposed corrected model. The documented F1/F2a/F2b findings are not fixed here. This model does not automatically track C++ edits; its source mapping must be maintained.The REST image does not include device-facing south/north plugins, so these recipes do not claim device-to-destination coverage.