Skip to content

Sysfs streq - #13

Closed
SetSplin wants to merge 11 commits into
evdenis:masterfrom
SetSplin:sysfs_streq
Closed

SetSplin wants to merge 11 commits into
evdenis:masterfrom
SetSplin:sysfs_streq

Conversation

@SetSplin

Copy link
Copy Markdown
Contributor

added lemma functions for sysfs_streq

@evdenis
evdenis force-pushed the master branch 4 times, most recently from 4541855 to e5926d1 Compare September 7, 2020 22:49
@evdenis
evdenis force-pushed the master branch 4 times, most recently from 120a130 to 440fee7 Compare October 7, 2020 14:59
evdenis added a commit that referenced this pull request Sep 18, 2026
Replace the incorrect normalized-length behaviors with an exact common
prefix and termination predicate. This covers unequal strings and the
repeated-newline case: "x\n" and "x\n\n" compare equal. Remove the unused
sysfs_strlen helpers and preserve the repaired shared strncmp definitions.

WP proves 166/166 goals with RTE under the documented unsigned-wraparound
policy; all 25 smoke tests pass. The executable algorithm is unchanged.
The goal count drops because the old contract and helper chain are gone.

PR: #13
evdenis added a commit that referenced this pull request Sep 18, 2026
Replace the incorrect normalized-length behaviors with an exact common
prefix and termination predicate. This covers unequal strings and the
repeated-newline case: "x\n" and "x\n\n" compare equal. Remove the unused
sysfs_strlen helpers and preserve the repaired shared strncmp definitions.

WP proves 166/166 goals with RTE under the documented unsigned-wraparound
policy; all 25 smoke tests pass. The executable algorithm is unchanged.
The goal count drops because the old contract and helper chain are gone.

PR: #13
evdenis added a commit that referenced this pull request Sep 18, 2026
Replace the incorrect normalized-length behaviors with an exact common
prefix and termination predicate. This covers unequal strings and the
repeated-newline case: "x\n" and "x\n\n" compare equal. Remove the unused
sysfs_strlen helpers and preserve the repaired shared strncmp definitions.

WP proves 166/166 goals with RTE under the documented unsigned-wraparound
policy; all 25 smoke tests pass. The executable algorithm is unchanged.
The goal count drops because the old contract and helper chain are gone.

PR: #13
@evdenis

evdenis commented Sep 18, 2026

Copy link
Copy Markdown
Owner

Superseded by #19.

@evdenis evdenis closed this Sep 18, 2026
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