Skip to content

backlog(B-0142): Code Contracts revival — design-by-contract primitives at compile/runtime (Aaron 2026-05-01; sibling of B-0141; second B-0177 audit hit)#1349

Merged
AceHack merged 4 commits intomainfrom
backlog/B-0142-code-contracts-design-by-contract-revival-aaron-2026-05-01
May 3, 2026
Merged

backlog(B-0142): Code Contracts revival — design-by-contract primitives at compile/runtime (Aaron 2026-05-01; sibling of B-0141; second B-0177 audit hit)#1349
AceHack merged 4 commits intomainfrom
backlog/B-0142-code-contracts-design-by-contract-revival-aaron-2026-05-01

Conversation

@AceHack
Copy link
Copy Markdown
Member

@AceHack AceHack commented May 3, 2026

Summary

Files `B-0142` — sibling of B-0141, both IDs reserved by Aaron 2026-05-01 in the parallelism-scaling-ladder memo's mechanized-guardrail table:

| Pre-condition violation | Code Contracts (B-0142, not yet filed) throws at runtime | Compiler-time refinement-types reject the build |

Both rows were named with B-NNNN IDs but never had per-row files filed. Otto 2026-05-03 audit pass (post-B-0141 filing) found B-0142 also missing.

Empirical evidence FOR B-0177 audit hypothesis

This row is the second concrete hit for B-0177's audit hypothesis ("a lot of backlog lost in our memories"). Pattern emerging:

  • B-0141 (filed 2026-05-03): brittle-pointer auto-rewriter — first hit
  • B-0142 (filed 2026-05-03): Code Contracts revival — second hit
  • B-0157: detect-changes pattern — third candidate (deferred to next-tick)

All three referenced in 2026-05-01 memos with B-NNNN IDs but never had files until 2026-05-03 audit.

Row scope

Design-by-contract primitives integrated into F#/C# codebase:

  • `requires(condition, message)` — pre-condition at function entry
  • `ensures(condition, message)` — post-condition at function exit
  • `invariant(condition, message)` — class/object lifetime invariants
  • Compile-time mode (refinement types) reject at build
  • Runtime mode (assertions) catch at execution
  • Composes with Result-over-exception per CLAUDE.md (structured error flow)

L-effort due to: library selection (PostSharp / Fody / Roslyn analyzers / F# type providers / source-generators), Result-flow composition, prose-contract migration, CI integration.

Composes with

  • B-0141 (brittle-pointer): sibling-instance of mechanization at substrate-cross-reference layer; this row is at code-boundary layer
  • B-0130 (verify-before-state-claim): claim-integrity discipline
  • B-0170 (substrate-claim-checker): data-claim verification; this row's tool is code-claim verification
  • B-0177 (audit memos): this row's existence IS the second empirical hit

Test plan

  • Backlog row format follows existing P2 convention
  • BACKLOG.md regenerated to include B-0142
  • markdownlint passes locally
  • Composes-with chain references B-0141, B-0130, B-0170, B-0177

Copilot AI review requested due to automatic review settings May 3, 2026 07:43
@AceHack AceHack enabled auto-merge (squash) May 3, 2026 07:43
…es at compile/runtime (Aaron 2026-05-01; reserved ID never filed; sibling of B-0141)

Aaron 2026-05-01 named "B-0142, not yet filed" in the parallelism-
scaling-ladder memo's mechanized-guardrail table — alongside B-0141
(brittle-pointer). Both IDs were reserved; per-row files were never
filed. Otto 2026-05-03 audit pass post-B-0141 filing found B-0142
also missing.

This is the second concrete hit for B-0177's audit hypothesis. The
parallelism-scaling-ladder memo named two B-NNNN IDs; both rows
materialized only after Aaron 2026-05-03 surfaced the gap during
B-0176 review.

Row scope: design-by-contract primitives (requires/ensures/invariant)
at function boundaries, mechanizing pre/post-condition + invariant
enforcement that's currently review-time-only. Compile-time mode
(refinement types) rejects violations at build; runtime mode catches
at execution. Composes with Result-over-exception per CLAUDE.md.

L-effort due to library/tooling selection (PostSharp, Fody, Roslyn
analyzers, F# type providers) + Result-flow composition + migration
of existing prose-documented contracts.

Composes with: B-0141 (sibling-instance of mechanization), B-0130
(claim-integrity), B-0170 (substrate-claim-checker), B-0177 (audit
hypothesis empirical hit #2).
@AceHack AceHack force-pushed the backlog/B-0142-code-contracts-design-by-contract-revival-aaron-2026-05-01 branch from ca87082 to f301ba3 Compare May 3, 2026 07:44
Copy link
Copy Markdown

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: ca87082e29

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

…— remove throw/panic options from row spec

Real review finding: B-0142 spec mentioned "throws / panics / returns
Result-error" as contract-violation handling options. This conflicts
with CLAUDE.md's hard Result-over-exception invariant ("user-visible
errors surface as Result<_, DbspError> or AppendResult-style values;
exceptions break the referential-transparency the operator algebra
depends on").

Backlog rows act as implementation guidance — admitting throw/panic
in the row spec could cause future contract tooling to reintroduce
exception-based control flow.

Fixes:
- Editorial note added after the verbatim quote (Aaron 2026-05-01
  memo's "throws at runtime" wording predates the spec; preserved
  verbatim, normalized to Result-flow in the spec)
- Pre-condition primitives: only Result-error flow, no throw/panic
- Open design questions updated: contract-violation handling within
  Result-flow (not "throw vs Result-error")
- Carved sentence: explicit Result-over-exception, NO throw/panic

The verbatim Aaron quote stays unchanged per preservation discipline;
the editorial note bridges to Result-flow.
Copy link
Copy Markdown

Copilot AI left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Pull request overview

This PR adds a new P2 backlog row for B-0142 and updates the generated backlog index so the design-by-contract research item is tracked in the repo’s per-row backlog system. It fits the codebase’s ongoing migration from implicit memo references to explicit docs/backlog/** entries with stable B-IDs.

Changes:

  • Adds docs/backlog/P2/B-0142-...md to capture the “Code Contracts revival” research/design row with origin, scope, effort, and composition notes.
  • Regenerates docs/BACKLOG.md to include the new B-0142 entry in the P2 section.

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated 4 comments.

File Description
docs/backlog/P2/B-0142-code-contracts-design-by-contract-revival-aaron-2026-05-01.md New per-row backlog file describing the design-by-contract / code-contracts research item and its provenance.
docs/BACKLOG.md Regenerated backlog index entry adding B-0142 to the P2 listing.

Comment thread docs/BACKLOG.md Outdated
Copy link
Copy Markdown

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 022ada008d

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

Copilot AI review requested due to automatic review settings May 3, 2026 07:52
@AceHack AceHack merged commit 9c4d247 into main May 3, 2026
24 checks passed
@AceHack AceHack deleted the backlog/B-0142-code-contracts-design-by-contract-revival-aaron-2026-05-01 branch May 3, 2026 07:53
Copy link
Copy Markdown

Copilot AI left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Pull request overview

Copilot reviewed 2 out of 2 changed files in this pull request and generated 4 comments.

AceHack added a commit that referenced this pull request May 3, 2026
…n + partial pre-existence acknowledged (#1357)

Three substantive review findings absorbed:

1. Cross-workflow `needs:` is invalid — `needs:` works only within
   single workflow file. Architecture corrected to specify three
   options (Architecture A: reusable workflow via workflow_call;
   Architecture B: per-workflow detect-job; Architecture C: single
   consolidated workflow). Architecture A recommended (matches
   sibling-repo pattern + preserves separation).

2. .yaml → .yml extension throughout — repo's existing workflows
   consistently use .yml; one-off .yaml suffix would create drift.

3. Problem-statement acknowledged partial pre-existence — gate.yml
   already skips on docs-only via path-gate; codeql.yml
   short-circuits pure docs; backlog-only changes have
   backlog-index-integrity. Row generalizes the partial pattern
   into uniform mechanism, NOT from-zero gating.

The B-0142-stale-cross-references in some threads were
merge-ordering false positives (B-0142 not present at PR-eval time;
merged later as #1349) — handled in resolve-thread comments.
AceHack added a commit that referenced this pull request May 3, 2026
…n (4 review threads absorbed) (#1356)

* fix(#1349 post-merge): B-0142 migration concerns + scope clarification (4 review threads absorbed)

Four substantive post-merge review findings on B-0142:

1. Existing invalidArg/exception-based code in src/Core/** —
   programmer-error preconditions historically use exceptions in F#
   idiom; CLAUDE.md Result-over-exception applies to user-visible
   failures. Scope refinement: B-0142 targets recoverable user-facing
   failures (Result-flow); programmer-error preconditions stay as
   invalidArg until a separate decision migrates them. NO blanket-ban
   exceptions.

2. Plain-returning APIs (bool/Stream/ValueTask) — contract primitives
   returning Result aren't drop-in. Scope refinement: two-mode
   primitive — requires_result() (Result-returning) vs requires_assert()
   (assertion-only).

3. TreatWarningsAsErrors=true makes warning vs error a false dichotomy.
   Scope refinement: contract-layer severity field; build-gate
   disposition is uniform (any reaching build = break); per-contract-
   class CI gating is separate future design question.

4. Dangling reference: memory/parallelism-scaling-ladder memo replaced
   with full filename for grep-ability.

New "Migration concerns + scope clarification" section absorbs the
findings. Open-design-questions updated with build-gate disposition
question replacing the warning-vs-error false dichotomy.

* fix(#1356 review): B-0142 internal-consistency reconciliation — scope no-throw rule explicitly to recoverable-user-facing-failures + Stream type precision
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants