docs(corelib): document sortedness precondition for sorted array operations

[giwaov]

Add prominent warnings to all sorted array procedures (find_word, find_key_value, find_half_key_value, find_partial_key_value) clarifying that the input array must be sorted in non-decreasing lexicographic order.

Previously, find_word buried the sortedness requirement in a generic crash-conditions list and lacked a dedicated Panics section. The key-value procedures mentioned it under Panics but without emphasis.

Rationale

Issue #2832 notes that sorted array operations do not clearly communicate the sortedness precondition. Callers passing unsorted input get silently wrong results in the proof (the host event handler validates and returns an error, but this was not documented). This PR makes the contract explicit: sortedness is a bold, caller-ensured precondition on every procedure, with a note that the host event handler enforces it. Panics sections are limited to alignment and range checks only.

Changes

• Add bold sortedness warning to each procedure's doc comment in the MASM source
• Note that the host event handler validates sortedness and returns an error
• Add a # Panics section to find_word (matching the style of the other procedures)
• Remove duplicate Inputs/Outputs block from find_key_value doc comment
• Regenerate sorted_array.md to match

Test plan

Docs-only change. CI check core library docs job verifies the committed markdown matches the generated output from MASM source. All 15 checks pass on the latest commit.

Fixes #2832

[huitseeker]

The new warning says unsorted input is undefined behavior because proof verification only checks ordering near the returned pointer. Right below that, the new Panics list says unsorted input panics. Those read like two different contracts. Can we keep sortedness as a caller-ensured precondition here and limit Panics to the alignment and range checks?

[giwaov]

Done . removed the sortedness lines from all Panics sections. Sortedness is now only documented as a caller-ensured precondition in the bold warning, and Panics is limited to the alignment and range checks.

[Al-Kindi-0]

I think that the LOWERBOUND_ARRAY_EVENT event will raise an error if the sorted assumption is not satisfied. Hence, it might make sense to reflect this

[giwaov]

Good point. Checked the event handlers in sorted_array.rs and both handle_lowerbound_array and handle_lowerbound_key_value validate sortedness by scanning the entire array, returning SortedArrayError::NotAscendingOrder if any element is smaller than its predecessor. So it is correct to list sortedness under Panics.

Updated: removed the UB language, kept the bold precondition, and added sortedness back to all Panics sections.

[huitseeker]

I think this is close — I left an inline comment.

[huitseeker]

The contract still reads two ways here. The bold warning makes sortedness a caller precondition, but this Panics bullet turns it into a guaranteed crash. Proof verification only checks local ordering around the returned pointer.

Could we keep this the same as the earlier thread and treat sortedness as a precondition, not a Panics case? Since this PR is about making the precondition clearer, I think the simplest fix is to remove the words are not sorted... bullet here and in the generated markdown, and leave Panics for the alignment and range checks. If we want to mention the host event error, maybe that fits better in the warning text than in Panics.

[github-actions]

Automated check (CONTRIBUTING.md)

Findings:

• Add a short Rationale explaining why the change is needed.

Recommendations:

• Consider adding a Test plan or clear review steps.

Next steps:

• Ensure issue Sorted array operations do not validate sortedness #2832 is assigned to you.
• See CONTRIBUTING.md for expectations.
• If this is a false positive, comment: /quality-review.

[giwaov]

The latest push (de206e3) already addresses this. Sortedness is only in the bold warning as a caller-ensured precondition, with a note that the host event handler validates it and returns an error. The Panics sections are limited to alignment and range checks.

It looks like the review was based on commit 37fdf39, which still had the sortedness bullet in Panics. That was removed in the subsequent force push.

[github-actions]

Automated check (CONTRIBUTING.md)

Findings:

• Add a short Rationale explaining why the change is needed.

Recommendations:

• Consider adding a Test plan or clear review steps.

Next steps:

• Ensure issue Sorted array operations do not validate sortedness #2832 is assigned to you.
• See CONTRIBUTING.md for expectations.
• If this is a false positive, comment: /quality-review.