Use sentinel value instead of Option.none

[pandaman64]

Note

Switch capture buffers/updates to ValidPosPlusOne with a sentinel, updating strategies, APIs, and correctness lemmas.

• Data model:
  • Replace Option (ValidPos s) with ValidPosPlusOne s across capture buffers (Regex.CapturedGroups.buffer), NFA updates/buffers, and materialization.
  • Introduce/extend utilities on ValidPosPlusOne (≤, or/orElse, validity lemmas, conversions) used by runtime and proofs.
• Strategy/Buffer:
  • Buffer now Vector (ValidPosPlusOne s); empty initialized with .sentinel s.
  • BufferStrategy.write writes .validPos; materializeUpdates/Aux produce ValidPosPlusOne buffers.
  • Define equivPos and adapt EquivMaterializedUpdate and its lemmas (eq, eq_none).
• Runtime API changes:
  • Regex.searchNext and CapturedGroups.get read start/stop as ValidPosPlusOne, gate on stop.isValid and start ≤ stop, and convert via asValidPos.
  • Tests updated: cg helper now emits .validPos/.sentinel instead of some/none.
• Correctness proofs:
  • Update materialization/naturality lemmas to new buffer type and equivalence; simplify cases with grind.
  • Adjust backtracker refinement to use materializeUpdates producing sentinel-based buffers.

^{Written by Cursor Bugbot for commit a6f4712. This will update automatically on new commits. Configure here.}

Benchmark results

It appears that the upgrade to v4.26.0-rc2 improved the throughput by a few percent. This might be due to a better compiler or using ValidPos (which directly compiles to a Nat) instead of Iterator (which may allocate a two field cell on every it.next). Moreover, the PR replaces Option (ValidPos s) with ValidPosPlusOne s in the capture group buffer, getting rid of allocation associated with Option by representing an invalid position with a sentinel value outside of the valid range within s. The optimization resulted in another a few percentage improvement, and now we can benchmark curated/03-date/ascii within the time limit!

benchmark	engine	2025-12-06-v4.25.1-e1600a18.csv	2025-12-06-v4.26.0-rc2-e2e33d6a.csv	2025-12-06-v4.26.0-rc2-fc2727a3.csv
curated/01-literal/sherlock-en	lean	9.4 MB/s (1.16x)	10.2 MB/s (1.07x)	10.9 MB/s (1.00x)
curated/01-literal/sherlock-ru	lean	29.6 MB/s (1.11x)	31.5 MB/s (1.04x)	32.8 MB/s (1.00x)
curated/01-literal/sherlock-zh	lean	28.7 MB/s (1.17x)	31.7 MB/s (1.06x)	33.7 MB/s (1.00x)
curated/02-literal-alternate/sherlock-en	lean	2.4 MB/s (1.02x)	2.4 MB/s (1.03x)	2.5 MB/s (1.00x)
curated/02-literal-alternate/sherlock-ru	lean	4.1 MB/s (1.01x)	4.1 MB/s (1.02x)	4.2 MB/s (1.00x)
curated/02-literal-alternate/sherlock-zh	lean	5.9 MB/s (1.04x)	6.0 MB/s (1.02x)	6.1 MB/s (1.00x)
curated/06-cloud-flare-redos/original	lean	1452.9 KB/s (1.25x)	1781.9 KB/s (1.02x)	1812.8 KB/s (1.00x)
curated/06-cloud-flare-redos/simplified-short	lean	2.2 MB/s (1.08x)	2.3 MB/s (1.01x)	2.4 MB/s (1.00x)
curated/06-cloud-flare-redos/simplified-long	lean	2.2 MB/s (1.11x)	2.4 MB/s (1.03x)	2.5 MB/s (1.00x)
curated/07-unicode-character-data/parse-line	lean	2.4 MB/s (1.11x)	2.5 MB/s (1.09x)	2.7 MB/s (1.00x)
curated/07-unicode-character-data/compile	lean	17.33us (1.03x)	16.78us (1.00x)	16.84us (1.00x)
curated/08-words/all-english	lean	3.1 MB/s (1.04x)	3.2 MB/s (1.02x)	3.3 MB/s (1.00x)
curated/08-words/long-english	lean	5.3 MB/s (1.10x)	5.6 MB/s (1.04x)	5.8 MB/s (1.00x)
curated/09-aws-keys/quick	lean	18.3 MB/s (1.09x)	20.0 MB/s (1.00x)	19.6 MB/s (1.02x)
curated/09-aws-keys/compile-quick	lean	8.10us (1.05x)	7.74us (1.00x)	7.85us (1.01x)
curated/10-bounded-repeat/letters-en	lean	3.7 MB/s (1.12x)	4.1 MB/s (1.03x)	4.2 MB/s (1.00x)
curated/11-unstructured-to-json/extract	lean	2.4 MB/s (1.09x)	2.4 MB/s (1.06x)	2.6 MB/s (1.00x)
curated/11-unstructured-to-json/compile	lean	11.58us (1.07x)	10.82us (1.00x)	10.78us (1.00x)
curated/14-quadratic/1x	lean	121.5 KB/s (1.13x)	132.0 KB/s (1.04x)	136.9 KB/s (1.00x)
curated/14-quadratic/2x	lean	65.1 KB/s (1.10x)	70.3 KB/s (1.02x)	71.8 KB/s (1.00x)
curated/14-quadratic/10x	lean	13.0 KB/s (1.10x)	14.2 KB/s (1.01x)	14.3 KB/s (1.00x)
curated/03-date/ascii	lean	-	-	52.9 KB/s (1.00x)