Skip to content

[v0.4] Plant evidence states what it shows: generator refusals by locus, SP-16's forged-program plant, the SM-32 records (follow-up to #167) #184

Closed as not planned

Description

@humuhumu33

Follow-up to #167 (reviews of #157, #163 and #151).

  1. assert_targeted (crates/conformance/src/cases/preservation.rs:91-101) counts any generator refusal as a caught lowering plant. It checks only that the function owns a relation, not that the refusal names the mutated function and site. The SP-15 record (VERIFICATION.md:1471-1530) shows that the six observed refusals do name the site, but the case does not assert it. Both Buffer plants are refused by the generator, so no Buffer mutation reaches the kernel.
  2. SP-16's plant "forged program literal" forges the crate term, not the program row.
  3. VERIFICATION.md:8870-8885: the two SM-32 plants cite bit_contribution, is_fixed_integer() and is_unsigned_fixed_integer(), which exist in no version of the code, and an output ("check fails with LLT4001: ()") the harness does not print.

Definition of done:

  • A refusal counts as caught only when its message names the mutated function and site, and the case asserts it.
  • At least one Buffer mutation is carried to the kernel by a plant that bypasses the lockstep refusal, or the SP-02 statement says which kinds the generator alone refuses.
  • SP-16 gains a plant on the program row, or the plant is renamed.
  • Both SM-32 plants are re-run against widen.rs and semantic.rs, with the real edit and the real output recorded.
  • just vv green.

Activity

  1. added this to the LexLean v0.4 milestone on Oct 18, 2026
  2. humuhumu33 commented on Oct 18, 2026

    @humuhumu33
    ContributorAuthor

    Duplicate of #179, filed twice by mistake; #179 is the one the #167 approval links.

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

    bugSomething isn't working

    Type

    No type

    Projects

    No projects

      Milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions