fix: complete WP proofs for five string algorithms

Makefile

@@ -2,7 +2,7 @@ export TIMEOUT   ?= 10
 export PROCESSES ?= 4
 
 CC               := gcc
-CFLAGS           := -Wall -Werror
+CFLAGS           := -Wall -Werror -fno-builtin
 CLANG            := clang
 CLANGFLAGS       := -g -O1
 GEN_CFLAGS       := -w
@@ -187,7 +187,7 @@ fuzz-%: $(FUZZDIR) $(FUZZDIR)/%
 	$(FUZZDIR)/$*
 
 run: build ## Run each program. You can also type run-<target>.
-	@for i in $(BINFILES); do echo $$i; ./$$i; done
+	@for i in $(BINFILES); do echo $$i; ./$$i || exit $$?; done
 
 run-%: $(BINDIR) $(BINDIR)/%
 	$(BINDIR)/$*

README.md

@@ -21,7 +21,7 @@ has been re-proved with WP so far.
 | ID | Function      | AstraVer | WP | Logic function | libfuzzer | Comment |
 |----|---------------|----------|----|----------------|-----------|---------|
 | 1  | check\_bytes8 | proved |    | proved         | yes       |         |
-| 2  | match\_string | proved |    | not required   |           |         |
+| 2  | match\_string | proved | proved | not required   |           |         |
 | 3  | memchr        | proved | proved |                | yes       |         |
 | 4  | memcmp        | proved | proved |                | yes       |         |
 | 5  | memscan       | proved | proved | not required   | yes       |         |
@@ -42,14 +42,14 @@ has been re-proved with WP so far.
 | 20 | strncmp       | proved | proved |                | yes       | -warn-unsigned-downcast off |
 | 21 | strncpy       |        | proved | not required   |           |         |
 | 22 | strnlen       | proved | proved | proved         | yes       |         |
-| 23 | strnstr       |        |    |                | yes       | memory safety and termination only; no functional postcondition yet |
+| 23 | strnstr       |        | proved |                | yes       |         |
 | 24 | strpbrk       | proved | proved | proved         | yes       |         |
 | 25 | strrchr       | proved | proved |                | yes       |         |
 | 26 | strreplace    | proved | proved | not required   | !const    |         |
 | 27 | strsep        | proved | proved | not required   | !const    |         |
 | 28 | strspn        | proved | proved | proved         | yes       |         |
 | 29 | strstr        |        |    |                | yes       |         |
-| 30 | sysfs\_streq  | proved |    |                | yes       |         |
+| 30 | sysfs\_streq  | proved | proved |                | yes       |         |
 | 31 | strlcat       |        | proved | not required   |           |         |
 | 32 | strlcpy       | proved | proved | not required   |           | use strncmp lf in ensures |
 | 33 | memmove       | proved\*| proved | not required   |           | use memcmp logic function at ensures |
@@ -102,6 +102,10 @@ $ make wp-status          # only the goals that are still unproved
 $ make wp-gui-strlen      # the same run in the Frama-C GUI
 ```
 
+```make run``` also runs boundary assertions in the algorithms' existing main functions:
+truncation, first matches, embedded NULs, trailing newlines and NULL-terminated arrays.
+CI runs these examples alongside the committed proof replay.
+
 ```TIMEOUT``` (seconds per goal) and ```PROCESSES``` (parallel provers) are environment
 knobs: ```make TIMEOUT=30 wp-strcmp```. Raising ```TIMEOUT``` alone has no effect on a goal
 whose timeout is already cached — use ```make wp-rebuild``` to force the provers to run
@@ -212,10 +216,11 @@ Criteria to develop a logical function:
 1. It is possible to write a logical function only for a pure C function;
 2. It is rational to write logical functions if they are useful for developing specifications of other functions. For example, in the memcpy contract, you can express the equality of src and dest by calling the memcmp logical function.
 
-A ```lemma``` in an active axiomatic is a proof obligation, not an assumption: WP generates
-a goal for it like any other. The corpus has 27 such goals and discharges 26; the exception
-is ```strcmp_corollary```, which times out. Under AstraVer the inductive ones were discharged
-by the plugin's ```lemma``` functions; they now live in the headers as ordinary ACSL ghost
+A ```lemma``` has its own proof obligation. WP can also use it as a hypothesis for other
+goals before it has been proved, so those dependent goals are not sufficient evidence.
+The previously unresolved ```strcmp_corollary``` is now a proved ghost function in
+**match_string.h**. Under AstraVer the inductive lemmas were discharged by the plugin's
+```lemma``` functions; they now live in the headers as ordinary ACSL ghost
 functions whose contract WP proves and which a caller instantiates from ghost code — see the
 block after each axiomatic in **strlen.h**, **strnlen.h** and friends.
 

README_ru.md

@@ -121,9 +121,10 @@ $ extricate -m ~/linux-stable/lib/string.c -k ~/linux-stable --double -f strim -
 1) Обычной функции можно сопоставить логическую функцию (один-в-один), только если функция на языке Си "чистая" (pure).
 2) Логическую функцию рационально писать в том случае, если они пригодится для разработки спецификаций в том числе и для других функций. Например, в функциональных требованиях к memcpy можно выразить "одинаковость" src и dest посредством вызова логической функции memcmp.
 
-```lemma``` в действующей аксиоматике — это цель доказательства, а не постулат: WP
-порождает для неё обычную цель. В корпусе таких целей 27, доказываются 26; исключение —
-```strcmp_corollary```, который не укладывается в таймаут. Под AstraVer индуктивные из них
+Для каждой ```lemma``` WP порождает отдельную цель доказательства. При этом WP может
+использовать её как гипотезу в других целях ещё до доказательства самой леммы, поэтому
+одних зависимых целей недостаточно. Ранее недоказанная ```strcmp_corollary``` теперь
+доказана как ghost-функция в **match_string.h**. Под AstraVer индуктивные леммы
 доказывались лемма-функциями плагина; теперь они лежат в заголовочных файлах как обычные
 ghost-функции ACSL, контракт которых доказывает WP, а вызывающий код инстанцирует их из
 ghost-кода — см. блок после каждой аксиоматики в **strlen.h**, **strnlen.h** и других.