Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
thanhnguyen-aws wants to merge 14 commits into
base: main2
Choose a base branch
from
Open

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

Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
6b20af8
add basic support for del key word
thanhnguyen-aws Apr 27, 2026
a247211
Merge branch 'main' into supportdel
thanhnguyen-aws Apr 27, 2026
4d0db12
Add del support for list negative index and slice
keyboardDrummer-bot Apr 27, 2026
312c974
Merge branch 'main' into supportdel
thanhnguyen-aws Apr 27, 2026
a2cb07c
Merge remote-tracking branch 'bot/supportdel-negative-index-and-slice…
keyboardDrummer-bot Apr 27, 2026
228dd05
Merge branch 'main' into supportdel
tautschnig May 4, 2026
dff2df9
Merge branch 'main' into supportdel
thanhnguyen-aws May 5, 2026
fec063c
merge conflict
thanhnguyen-aws May 5, 2026
8b41562
Update Strata/Languages/Python/PythonRuntimeLaurelPart.lean
thanhnguyen-aws May 8, 2026
5c39ff9
Update Strata/Languages/Python/PythonRuntimeLaurelPart.lean
thanhnguyen-aws May 8, 2026
080b72b
add exception for del statements
thanhnguyen-aws May 8, 2026
4627fe1
Merge branch 'main' into supportdel
thanhnguyen-aws May 8, 2026
e6cfede
add theorems
thanhnguyen-aws May 8, 2026
a61b257
import proof
thanhnguyen-aws May 8, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
57 changes: 56 additions & 1 deletion Strata/Languages/Python/PythonRuntimeLaurelPart.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -398,7 +398,6 @@ function List_slice_non_neg (l : ListAny, start : int, stop: int) : ListAny
else List_take (List_drop (l, start), int_min(stop, List_len(l)) - start)
};


function List_slice (l : ListAny, start : int, stop: int) : ListAny
{
List_slice_non_neg (l,
Expand All @@ -407,6 +406,26 @@ function List_slice (l : ListAny, start : int, stop: int) : ListAny
)
};

function List_remove_non_neg(l: ListAny, i: int) : ListAny
requires i >= 0 && i < List_len(l)
{
List_extend(List_take(l, i),List_drop(l, i + 1))
};

function List_remove(l: ListAny, i: int) : ListAny
requires i >= - List_len(l) && i < List_len(l)
{
if i >= 0 then List_remove_non_neg(l, i)
else List_remove_non_neg(l, List_len(l) + i)
};

function List_remove_slice(l: ListAny, start: int, stop: int) : ListAny
{
List_extend(
List_take(l, if start >= 0 then int_min(start, List_len(l)) else int_max(List_len(l) + start, 0)),
List_drop(l, if stop >= 0 then int_min(stop, List_len(l)) else int_max(List_len(l) + stop, 0)))
};
Comment thread
thanhnguyen-aws marked this conversation as resolved.
Comment on lines +418 to +437

@tautschnig tautschnig May 8, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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:

  1. DictStrAny_remove_contains_false:

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

  2. 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 thanhnguyen-aws May 8, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.


function List_set_non_neg (l : ListAny, i : int, v: Any) : ListAny
requires i >= 0 && i < List_len(l)
{
Expand Down Expand Up @@ -465,6 +484,13 @@ function DictStrAny_insert (d : DictStrAny, key: string, val: Any) : DictStrAny
else DictStrAny_cons(DictStrAny..key!(d), DictStrAny..val!(d), DictStrAny_insert(DictStrAny..tail!(d), key, val))
};

function DictStrAny_remove (d : DictStrAny, key: string) : DictStrAny
{
if DictStrAny..isDictStrAny_empty(d) then DictStrAny_empty()
else if DictStrAny..key!(d) == key then DictStrAny..tail!(d)
else DictStrAny_cons(DictStrAny..key!(d), DictStrAny..val!(d), DictStrAny_remove(DictStrAny..tail!(d), key))
};

function Any_get (dictOrList: Any, index: Any): Any
requires (Any..isfrom_DictStrAny(dictOrList) && Any..isfrom_str(index) && DictStrAny_contains(Any..as_Dict!(dictOrList), Any..as_string!(index))) ||
(Any..isfrom_ListAny(dictOrList) && Any..isfrom_int(index) && Any..as_int!(index) >= - List_len(Any..as_ListAny!(dictOrList)) && Any..as_int!(index) < List_len(Any..as_ListAny!(dictOrList)))
Expand Down Expand Up @@ -535,6 +561,35 @@ function Any_sets! (indices: ListAny, dictOrList: Any, val: Any): Any
Any_sets!(ListAny..tail!(indices), Any_get!(dictOrList, ListAny..head!(indices)), val))
};

function Any_remove (dictOrList: Any, index: Any): Any
{
if Any..isexception(dictOrList) then dictOrList
else if Any..isexception(index) then index
else if !(Any..isfrom_DictStrAny(dictOrList) && Any..isfrom_str(index)) && !(Any..isfrom_ListAny(dictOrList) && Any..isfrom_int(index)) then
exception (TypeError("Invalid subscription type"))
else if Any..isfrom_DictStrAny(dictOrList) && Any..isfrom_str(index) && DictStrAny_contains(Any..as_Dict!(dictOrList), Any..as_string!(index)) then
from_DictStrAny(DictStrAny_remove(Any..as_Dict!(dictOrList), Any..as_string!(index)))
else if Any..isfrom_ListAny(dictOrList) && Any..isfrom_int(index) && Any..as_int!(index) >= - List_len(Any..as_ListAny!(dictOrList)) && Any..as_int!(index) < List_len(Any..as_ListAny!(dictOrList)) then
from_ListAny(List_remove(Any..as_ListAny!(dictOrList), Any..as_int!(index)))
else
exception (IndexError("Invalid subscription"))
};
Comment thread
thanhnguyen-aws marked this conversation as resolved.

function Any_remove_slice (list: Any, index: Any): Any
{
if Any..isexception(list) then list
else if Any..isexception(index) then index
else if !(Any..isfrom_ListAny(list) && Any..isfrom_Slice(index)) then
exception (TypeError("Invalid subscription type"))
else
from_ListAny(List_remove_slice(
Any..as_ListAny!(list),
Any..start!(index),
if OptionInt..isOptSome(Any..stop!(index))
then OptionInt..unwrap!(Any..stop!(index))
else List_len(Any..as_ListAny!(list))))
};

function Any_len (v: Any) : int;

function Any_len_to_Any (v: Any) : Any {
Expand Down
18 changes: 18 additions & 0 deletions Strata/Languages/Python/PythonToLaurel.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1417,6 +1417,20 @@ def withExceptionChecks (ctx : TranslationContext)
let exceptionCheck := rhs_exprs.flatMap $ getExceptionAssertions ctx
(newctx, exceptionCheck ++ stmts)

def translateDel (ctx : TranslationContext) (md: MetaData) (e: Python.expr SourceRange) : Except TranslationError StmtExprMd := do
Comment thread
tautschnig marked this conversation as resolved.
Outdated
match e with
| .Subscript _ (.Name _ n _) slice _ =>
match slice with
| .Slice _ start stop step =>
let index ← translateSlice ctx start.val stop.val step.val
let rhs := mkStmtExprMd $ .StaticCall "Any_remove_slice" [freeVar n.val, index]
return mkStmtExprMdWithLoc (.Assign [freeVar n.val] rhs) md
| _ =>
let slice ← translateExpr ctx slice
let rhs := mkStmtExprMd $ .StaticCall "Any_remove" [freeVar n.val, slice]
return mkStmtExprMdWithLoc (.Assign [freeVar n.val] rhs) md
| _ => throw (.unsupportedConstruct "Only support del statement for list[index] and dict[key] where list and dict are variables, unsupported: " (toString (repr e)))
Comment thread
thanhnguyen-aws marked this conversation as resolved.

mutual

partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRange)
Expand Down Expand Up @@ -1768,6 +1782,10 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
let (ctx, assignStmt) ← translateStmt ctx pyNormalAssign
return (ctx, tempVarDecls ++ assignStmt)

| .Delete _ targets =>
let delStmts ← targets.val.toList.mapM $ translateDel ctx md
return (ctx, delStmts)

| _ => throw (.unsupportedConstruct "Statement type not yet supported" (toString (repr s)))

partial def translateStmtList (ctx : TranslationContext) (stmts : List (Python.stmt SourceRange))
Expand Down
4 changes: 4 additions & 0 deletions StrataTest/Languages/Python/expected_laurel/test_del_dict_key.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
test_del_dict_key.py(4, 4): ✅ pass - assert_assert(56)_calls_PNotIn_0
test_del_dict_key.py(4, 4): ✅ pass - key deleted
DETAIL: 2 passed, 0 failed, 0 inconclusive
RESULT: Analysis success
6 changes: 6 additions & 0 deletions StrataTest/Languages/Python/expected_laurel/test_del_list_item.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
test_del_list_item.py(4, 4): ✅ pass - assert_assert(49)_calls_Any_get_0
test_del_list_item.py(4, 4): ✅ pass - first unchanged
test_del_list_item.py(5, 4): ✅ pass - assert_assert(90)_calls_Any_get_0
test_del_list_item.py(5, 4): ✅ pass - second shifted
DETAIL: 4 passed, 0 failed, 0 inconclusive
RESULT: Analysis success
8 changes: 8 additions & 0 deletions StrataTest/Languages/Python/expected_laurel/test_del_list_negative_index.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
test_del_list_negative_index.py(4, 4): ✅ pass - assert_assert(53)_calls_Any_get_0
test_del_list_negative_index.py(4, 4): ✅ pass - first unchanged
test_del_list_negative_index.py(5, 4): ✅ pass - assert_assert(94)_calls_Any_get_0
test_del_list_negative_index.py(5, 4): ✅ pass - second unchanged
test_del_list_negative_index.py(6, 4): ✅ pass - assert_assert(136)_calls_Any_get_0
test_del_list_negative_index.py(6, 4): ✅ pass - third unchanged
DETAIL: 6 passed, 0 failed, 0 inconclusive
RESULT: Analysis success
8 changes: 8 additions & 0 deletions StrataTest/Languages/Python/expected_laurel/test_del_list_slice.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
test_del_list_slice.py(4, 4): ✅ pass - assert_assert(57)_calls_Any_get_0
test_del_list_slice.py(4, 4): ✅ pass - first unchanged
test_del_list_slice.py(5, 4): ✅ pass - assert_assert(98)_calls_Any_get_0
test_del_list_slice.py(5, 4): ✅ pass - fourth shifted
test_del_list_slice.py(6, 4): ✅ pass - assert_assert(138)_calls_Any_get_0
test_del_list_slice.py(6, 4): ✅ pass - fifth shifted
DETAIL: 6 passed, 0 failed, 0 inconclusive
RESULT: Analysis success
0 ...Python/tests/pending/test_del_dict_key.py → ...nguages/Python/tests/test_del_dict_key.py
View file
Open in desktop
File renamed without changes.
0 ...ython/tests/pending/test_del_list_item.py → ...guages/Python/tests/test_del_list_item.py
View file
Open in desktop
File renamed without changes.
7 changes: 7 additions & 0 deletions StrataTest/Languages/Python/tests/test_del_list_negative_index.py
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
def test():
xs = [1, 2, 3, 4]
del xs[-1]
assert xs[0] == 1, "first unchanged"
assert xs[1] == 2, "second unchanged"
assert xs[2] == 3, "third unchanged"
test()
7 changes: 7 additions & 0 deletions StrataTest/Languages/Python/tests/test_del_list_slice.py
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
def test():
xs = [1, 2, 3, 4, 5]
del xs[1:3]
assert xs[0] == 1, "first unchanged"
assert xs[1] == 4, "fourth shifted"
assert xs[2] == 5, "fifth shifted"
test()
Comment thread
thanhnguyen-aws marked this conversation as resolved.
Outdated
Loading