Specification of cstring#48

Closed

LennartATSkylabsAI wants to merge 11 commits intomainfrom

lennart/cstring

Commits on May 1, 2026

Added poject layout, md files for verification of cstring. Proved initial set of functions using ctring.R and a lower-level alternative cstringz.R
LennartATSkylabsAI
committed
First cut at step 3 of planning.md, ie functions strchr, strrchr, strspn, strcspn, strpbrk, and strstr
LennartATSkylabsAI
committed
Updated current state
LennartATSkylabsAI
committed
Specs for several more functions and their litmus tests (with first, non-ergonomic proofs)
LennartATSkylabsAI
committed
Added comments about candidate predicates for object_bytesR
LennartATSkylabsAI
committed
Split the litmus proof file, upstreamed predicate lemmas, slightly polished the model
LennartATSkylabsAI
committed
Moved remaining specs/proofs ofr embedded_null litmus tests to proofs_embedded_null
LennartATSkylabsAI
committed
Proof progrss in litmus tests proofs but proofs for mem{set|cmp|cpy|chr|move} remain ugly
LennartATSkylabsAI
committed
Updated md files; split proofs into string and memory-related functions
LennartATSkylabsAI
committed
Better usage of cancelx makes string proofs mostly-automatic
LennartATSkylabsAI
committed
Reviewed specs
LennartATSkylabsAI
committed