Skip to content

GF8/20/24/32 specs: prose invariants are discarded by the parser and check nothing #5698

Description

@dmitrii-f-t27

t27c parse-complete (master 8fdf715) reports four GF format specs whose invariants are partly prose, so the parser drops them and the generated code checks nothing for them:

spec tokens discarded lines
specs/numeric/gf8.t27 37 456, 459, 477, 519
specs/numeric/gf20.t27 31 427, 430, 438
specs/numeric/gf24.t27 31 427, 430, 438
specs/numeric/gf32.t27 31 438, 441, 449

The dropped lines are assert pow(x, 0.0) == 1.0 for all positive x, assert pow(x, 1.0) == x for all valid x, assert floor(x) == i32 for all f32 x and (gf8) assert PHI_DISTANCE == 0.132 within 0.001. Each invariant keeps its name, so it looks checked, while its body is gone.

Boundary

  • specs/numeric/gf8.t27
  • specs/numeric/gf20.t27
  • specs/numeric/gf24.t27
  • specs/numeric/gf32.t27
  • .trinity/seals/GF8.json, .trinity/seals/GF20.json, .trinity/seals/GF24.json, .trinity/seals/GF32.json
  • .trinity/seals/numeric_GF8.json, .trinity/seals/numeric_GF20.json, .trinity/seals/numeric_GF24.json, .trinity/seals/numeric_GF32.json

User Scenarios & Testing

  • Given specs/numeric/gf8.t27, When t27c parse-complete --show reads it, Then it reports nothing discarded.
  • Given the rewritten invariants, When t27c gen emits Zig, Then each invariant body is an executable check at concrete points.

Requirements

  • FR-001: Every invariant in the four specs must be written in t27 the parser consumes, with no discarded tokens.
  • FR-002: A quantified claim must be checked at concrete points, and the comment must say which.
  • FR-003: The seals of the four specs must be regenerated with the t27c built from the PR's own tree.

Success Criteria

  • t27c parse-complete --show specs/numeric/gf8.t27 prints nothing discarded (today: 37 token(s) DISCARDED).
  • t27c parse-complete --show specs/numeric/gf32.t27 prints nothing discarded (today: 31 token(s) DISCARDED).
  • t27c gen specs/numeric/gf8.t27 | grep -c 'abs(pow(x1, 0.0) - 1.0)' prints at least 1 (today: 0).
  • t27c typecheck specs/numeric/gf8.t27 prints Typecheck OK (0 errors, 12 warnings) (today: the same).

Activity

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

    No labels
    No labels

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions