Skip to content

AFFIRMATION.adoc

Latest commit

 

History

History
166 lines (134 loc) · 7.89 KB

AFFIRMATION.adoc

File metadata and controls

166 lines (134 loc) · 7.89 KB
Raw

AFFIRMATION — trigger, as of 2026-10-07

Table of Contents

What this is, and how it works

This file is a dated, signed snapshot of what can honestly be claimed about trigger at one exact commit. It is the third file of the README / EXPLAINME / AFFIRMATION trio. The README says where the project is going. EXPLAINME says how it is built. This file says what was true and checkable at the anchor below.

Every claim here comes from running the project’s own checks in the session that wrote this file. Where the README, the Justfile or memory disagree with a live run, the live run wins and the disagreement is recorded.

The owner lands this file with a signed git commit. That signature over this content, at the anchored commit, is what makes the affirmation attributable.

The epistemic contract

This document records best belief at the timestamp below. It is not a guarantee of correctness. The only guarantee is no intentional overclaim. Where something was checked, it says how. Where something was not checked, it says so. A claim that later proves false is an error to fix, not a lie.

You are invited to refute any claim here with a failing run, a counter-example or a contradicting source.

Verifiable anchor

Field Value

Repo

https://github.com/hyperpolymath/trigger

Branch

main

Commit (HEAD)

0755f3b99b0ee103b554aa1c3d5fd515dcca301b

Permalink

https://github.com/hyperpolymath/trigger/tree/0755f3b99b0ee103b554aa1c3d5fd515dcca301b

Verified (UTC)

2026-10-07T12:02:03Z

Working-tree delta at verification

none (git status --porcelain --ignored empty)

Toolchain

GNAT 14.2.0 + gprbuild (Debian); Zig 0.16.0; Idris 2 0.7.0; Agda 2.7.0.1 with agda-stdlib 2ffa8b7d; just 1.56.0. Not available: gnatprove, alr.

If you are reading this at a later commit, the claims may have drifted. Re-run the reproduction steps and write a fresh affirmation; do not trust a stale one.

Companion documents and repo metadata (cross-check)

  • README.adoc describes an Ada/SPARK implementation with Zig FFI bindings and an Idris2 API layer. The runs below show that none of those three layers builds at the anchor with the toolchain listed.

  • The GitHub repository description, as of the anchor, calls trigger a social media reporting utility with multi-account management, persistent sessions, proxy support, FloodWait handling and a TUI. That is a feature statement. Nothing below verifies any of those features.

  • This file replaces an earlier AFFIRMATION.adoc that was the unfilled estate template (placeholder heading and anchor fields). It made no claims, so it is replaced in place rather than archived. Git history keeps it.

The honest state (one breath)

At the anchor, trigger does not build. The Ada project file is rejected, the Justfile does not parse, every Zig FFI module fails to compile, every Idris2 module fails to resolve an import, and both Agda proof modules are rejected. Nothing about runtime behaviour was or could be verified.

What is solid (and how we checked)

  • The repository is clean at the anchor and its history is intact.

  • Six of the ten check contexts on the anchor commit concluded SUCCESS (read from the commit’s status check rollup over the GitHub GraphQL API): Hypatia neurosymbolic analysis, panic-attack assail, the rust-secrets and shell-secrets scans, Patch Bridge CVE triage, and the gitbot-fleet deposit. These are scanners over the tree, not evidence that the code works.

The honest nuance you must not lose

  • "Fails here" is not "never worked". Each failure below is measured at the toolchain versions in the anchor. Two of them look like code written for an older toolchain:

    • The Zig telegram module calls @ptrCast and @alignCast with two arguments. Current Zig takes one.

    • Every Idris2 module imports Control.Monad.Effect, which is the Idris 1 Effects library and does not ship with Idris 2.

  • Some failures do not depend on the version:

    • The Agda modules declare --safe and also contain postulates (8 in Trigger/API.agda, 5 in Trigger/Epistemic.agda). Agda rejects that combination in every version.

    • Four Zig modules fail at the parser, for example @null, in crypto/crypto.zig:121.

  • SPARK proofs were not checked, rather than found failing. gnatprove is not installed here, and the project file does not process, so the SPARK layer is untested at this anchor.

  • The Ada tests were not runnable. The test target goes through the same project file that fails to process.

Known-incomplete but honestly fenced

  • The two Hypatia contexts on the anchor disagree: "Hypatia / Hypatia Neurosymbolic Analysis" concluded SUCCESS and "Hypatia neurosymbolic scan" concluded FAILURE. Their logs were not read for this file.

  • scan / gitleaks concluded FAILURE. The job’s log was not read, so this file makes no claim about whether it found anything.

Outstanding / weak / refuted (no spin)

Check Result at the anchor

just build

Refuted. just cannot parse the Justfile: Justfile:223:1, an indented test-harness: recipe header.

gprbuild -P trigger.gpr -XLIBRARY_TYPE=static (the command the Justfile and ada-ci.yml both run)

Refuted. rc=5, "trigger.gpr" processing failed, for example trigger.gpr:18:08: undefined attribute "executable" and trigger.gpr:101:08: undefined attribute "build_profiles".

Ada/SPARK CI workflow on the anchor commit

Concluded FAILURE (GitHub check suite), consistent with the local run.

Zig FFI, zig build-lib -fno-emit-bin on each of the five modules

Refuted, 5 of 5. Parse errors in crypto.zig:121, discord.zig:98, social_media/common.zig:185 and twitter.zig:36. Seven errors in telegram.zig.

Idris2 API, idris2 --check on each of the five ffi/idris2/*.idr

Refuted, 5 of 5: Error: Module Control.Monad.Effect not found. Note: idris2 --check exited 0 while printing this error. Read the output, not the exit code.

Agda, Trigger/API.agda and Trigger/Epistemic.agda

Refuted, 2 of 2, rc=42: Cannot postulate …​ with safe flag.

Other CI on the anchor

Rollup contexts at FAILURE: openssf-compliance, scan / gitleaks, lint-workflows, Hypatia neurosymbolic scan. Check suites at FAILURE but absent from the rollup: Static Analysis Gate, Ada/SPARK CI. STARTUP_FAILURE: Dogfood Gate (no jobs ran).

Reproduce it yourself

From a clone checked out at the anchor commit:

git checkout 0755f3b99b0ee103b554aa1c3d5fd515dcca301b
just build                                     # Justfile parse error at 223
gprbuild -P trigger.gpr -XLIBRARY_TYPE=static  # rc=5, project file rejected
for d in crypto discord social_media twitter telegram; do
  (cd ffi/zig/$d && for f in *.zig; do zig build-lib -fno-emit-bin "$f"; done)
done
(cd ffi/idris2 && for f in *.idr; do idris2 --check "$f"; done)  # look for "Error:"
(cd proofs/agda && agda Trigger/API.agda && agda Trigger/Epistemic.agda)

Agda needs agda-stdlib. Point AGDA_DIR at a directory whose libraries file names the stdlib’s .agda-lib and whose defaults file says standard-library.

One-line characterisation (quote this)

At 0755f3b, trigger is an unbuilt Ada/SPARK, Zig and Idris2 codebase: every language layer and both Agda proofs fail their own checks, so no functional claim is affirmed.

Joint attestation

Engineering party (AI). Claude (claude-opus-5-5), session run at 2026-10-07T12:02:03Z, ran every check above and wrote this file. The wording is a faithful report of those runs. Nothing was copied forward from an earlier affirmation.

Owner. Jonathan D.A. Jewell signs by committing this file with an SSH signing key:

git commit -S -s AFFIRMATION.adoc -m "docs: affirm state at 0755f3b9"
git log --show-signature -1