Add basic support for del key word in Python->Laurel

[thanhnguyen-aws]

This PR adds del statement support to handle list[index/slice] and dict[key] when list and dict are variables, which also supports:

1. Negative indices: del xs[-1] now correctly converts negative indices to positive before removal, following the same pattern as List_get.

2. Slice deletion: del xs[start:stop] removes a range of elements, keeping elements before start and from stop onwards. Supports both positive and negative slice bounds.

Changes

Runtime (PythonRuntimeLaurelPart.lean):

• Split List_remove into List_remove_non_neg (requires i >= 0) and List_remove (handles negative-to-positive conversion)
• Added List_remove_slice for removing a range of elements
• Added Any_remove_slice with exception handling and slice unpacking

Translator (PythonToLaurel.lean):

• translateDel now matches on .Slice to call Any_remove_slice, falling back to Any_remove for single-index deletion

Tests:

• test_del_list_negative_index.py: del xs[-1] on [1, 2, 3, 4]
• test_del_list_slice.py: del xs[1:3] on [1, 2, 3, 4, 5]

All existing del tests continue to pass.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[thanhnguyen-aws]

@keyboardDrummer-bot Please add similar support for list's negative index and slice.

[keyboardDrummer-bot]

@thanhnguyen-aws I've opened PR #1055 with support for list negative index and slice in del statements.

Changes:

• del xs[-1] — negative indices are now converted to positive before removal (matching List_get's pattern)
• del xs[1:3] — slice deletion removes a range of elements, supporting both positive and negative bounds

Both new tests pass verification, and all existing del tests continue to pass. The PR targets main since supportdel is on your fork.

[thanhnguyen-aws]

@keyboardDrummer-bot Please merge PR #1055 to this PR. Don't create a new one.

[tautschnig]

Proof coverage — four cheap theorems that would lock in Python semantics.

All four new runtime functions have closed-form element/length specifications. These can live in a new StrataTest/Languages/Python/PythonRuntimeLaurelPartProofs.lean or, more in keeping with the rest of the tree, in the existing Python runtime test file as #guard-style snapshots. rfl should handle most of them once the surface syntax is lowered.

1. List_remove_non_neg_length:

   ∀ l i, 0 ≤ i < List_len(l) → List_len(List_remove_non_neg(l, i)) = List_len(l) - 1
   

2. List_remove_non_neg_get (the element-preservation property — this is the one that catches accidental off-by-one in i+1):

   ∀ l i j, 0 ≤ i < List_len(l) → 0 ≤ j < List_len(l) - 1 →
     List_get(List_remove_non_neg(l, i), j) =
       if j < i then List_get(l, j) else List_get(l, j + 1)
   

3. List_remove_slice_length (the one that would catch concern (1) above as a proof failure):

   ∀ l start stop,
     let start_c = clamp(start, List_len(l))
     let stop_c  = clamp(stop,  List_len(l))
     List_len(List_remove_slice(l, start, stop)) =
       if start_c >= stop_c then List_len(l)
       else List_len(l) - (stop_c - start_c)
   

   With the current implementation, for l=[1,2,3,4,5], start=3, stop=1, LHS = 7 and RHS = 5 — the proof doesn't go through, forcing a rewrite.

4. List_remove_roundtrip (sanity check tying List_remove_non_neg and List_remove_slice together):

   ∀ l i, 0 ≤ i < List_len(l) →
     List_remove_non_neg(l, i) = List_remove_slice(l, i, i + 1)
   

Even if only (3) lands, that's the regression-proof version of the concern above, and is the highest-value theorem in the set.

Similarly worth adding for DictStrAny_remove:

5. DictStrAny_remove_contains_false:

   ∀ d k, DictStrAny_contains(DictStrAny_remove(d, k), k) = false
   

6. DictStrAny_remove_other (other keys preserved):

   ∀ d k k' v, k ≠ k' →
     DictStrAny_get(DictStrAny_remove(d, k), k') = DictStrAny_get(d, k')
     (when d contains k')
   

[thanhnguyen-aws]

I added the proofs for List's theorems in Laurel and add the guard test for them. The Dict theorems cannot be proved because it requires that the Dict is constructed by Dict_insert. The runtime is slow, so it is just a temporary approach. We need to have a Lean backend so that the theorems can be proved efficiently.