Skip to content

PVB-6: B2 — extend pv kani to generate from rust: predicates #6460

Closed as not planned
Closed as not planned
PVB-6: B2 — extend pv kani to generate from rust: predicates#6460
Labels
P1High prioritykind:codeWork is a code change (derived rule, #4159)owner:aprender-wsweepowner session
Milestone
0.80.0

Description

@noahgift
noahgift
opened on Oct 27, 2026

Sub-issue of #6452. Row BR-6 of PVB-001 Appendix A (docs/specifications/PVB-001-proof-code-bridge.md, once #6451 lands). depends_on: BR-5.

Scope, done-when and falsifier are the BR-6 entry in Appendix A. Do not start before its dependency is closed.

🤖 Generated with Claude Code

Activity

  1. noahgift
    added this to the 0.74.0 milestone on Oct 27, 2026
  2. noahgift
    added
    P1High priority
    kind:codeWork is a code change (derived rule, #4159)
    owner:aprender-wsweepowner session
    on Oct 27, 2026
  3. noahgift
    added a parent issue on Oct 27, 2026
  4. noahgift
    modified the milestones: 0.74.0, 0.75.0, 0.80.0 on Oct 30, 2026

  5. noahgift commented on Oct 30, 2026

    @noahgift
    noahgift
    on Oct 30, 2026
    MemberAuthor

    Closing as not planned (iceboxed): this ticket is outside milestones 0.72.x-0.76.0 in the 2026-10-30 date-driven release plan, and the open-ticket cap needs it off the board. Tracked in the icebox epic #6521. Reopen it and give it a milestone to bring it back. (release planning worker, PMAT-5306, operator rulings 11:17Z)

  6. noahgift
    closed this as not plannedon Oct 30, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    P1High prioritykind:codeWork is a code change (derived rule, #4159)owner:aprender-wsweepowner session

    Type

    No type

    Projects

    No projects

      Milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions