example: specification of a left pad string padding function

[crodriguezvega]

This is a sample specification of a left pad string padding function. After addressing any feedback and merging this PR, I plan to open a PR to hwayne/lets-prove-leftpad to add it there as well.

• Tests added for any new code
• Documentation added for any new functionality
• Entries added to the respective CHANGELOG.md for any new functionality
• Feature table on README.md updated for any listed functionality

[crodriguezvega]

I've run make examples, but it seems to hang and the README.md doesn't get updated...

echo "<!-- DO NOT EDIT: THIS FILE IS GENERATED FROM examples/.scripts/README-text.md VIA 'make examples' -->" > examples/README.md
cat examples/.scripts/README-text.md >> examples/README.md
./examples/.scripts/run-examples.sh >> examples/README.md
Academic tradition requires you to cite works you base your article on.
If you use programs that use GNU Parallel to process data for an article in a
scientific publication, please cite:

  Tange, O. (2025, February 22). GNU Parallel 20250222 ('Grete Tange').
  Zenodo. https://doi.org/10.5281/zenodo.14911163

This helps funding further development; AND IT WON'T COST YOU A CENT.
If you pay 10000 EUR you should feel free to use GNU Parallel without citing.

More about funding GNU Parallel and the citation notice:
https://www.gnu.org/software/parallel/parallel_design.html#citation-notice

To silence this citation notice: run 'parallel --citation' once.

[bugarela]

I've run make examples, but it seems to hang and the README.md doesn't get updated...

This takes a few minutes to run, but it might be the case that you are hitting #1609

Don't worry, I can run this for you and update the dashboard

[bugarela]

Hi! Sorry for the late review.

I looked at Hillel's repo and all the examples I checked had actual proofs in them, while here we:

1. Use only a simulator, which won't check all scenarios
2. Constrain the input in several ways

I tweaked the spec a bit so we can use model checkers, and also removed one of the input constraints were the input string was always repeated chars. I still couldn't get rid of the size constraints, and I'm not sure whether it is possible: I asked here apalache-mc/apalache#3093

If we don't manage to get rid of the size constraint, this does not qualify as a proof as Hillel is proposing. We can potentially submit it as a weaker case where we only prove up to a bound, but the repo doesn't seem to be about those. We can still have it in the Quint examples, and I can add a write up explaining why this isn't as good of a proof as the ones you can do with tools from that repo.

A good thing is that there are some talks about embedding Quint into Lean, which would enable such proofs. See https://protocols-made-fun.com/lean/2025/04/25/lean-two-phase.html and https://verse-lab.github.io/papers/veil-cav25.pdf (one of the authors said they want to add support for Quint)

[bugarela]

You can add // -*- mode: Bluespec; -*- to the first line of a Quint file to tell GitHub to use syntax highlighting for "bluespec", which is the closest one to Quint while we don't have it at GitHub.

Suggested change

	/**
	// -*- mode: Bluespec; -*-
	/**