Soundness bug: `PNot` returns `exception` for `None` and `DictStrAny` inputs instead of computing `not`

[keyboardDrummer-bot]

Bug

PNot in PythonRuntimeLaurelPart.lean is unsound for None and DictStrAny inputs. It falls through to exception(UndefinedError(...)) for these types, but Python's not operator works on all types (it's equivalent to not bool(x)) and never raises an exception for non-exception inputs.

Affected cases

Expression	Python behavior	Strata (PNot) result
not None	True	❌ exception(UndefinedError(...))
not {}	True	❌ exception(UndefinedError(...))

PNot currently handles bool, int, float, str, and ListAny, but is missing branches for None and DictStrAny.

Related issue in Any_to_bool

Any_to_bool (around line 309) has a similar gap — it handles None and DictStrAny but is missing float. These two functions should be kept in sync since not x is semantically not bool(x).

Proposed fix

1. Add None and DictStrAny branches to PNot
2. Change the else branch from exception to hole (to be safe for types not yet modeled, e.g. datetime, bytes, ClassInstance)
3. Add the missing float branch to Any_to_bool
4. Align PNot and Any_to_bool so they cover the same set of types

Sketch for PNot:

function PNot (v: Any) : Any
{
  if Any..isexception(v) then v
  else if Any..isfrom_bool(v) then from_bool(!(Any..as_bool!(v)))
  else if Any..isfrom_int(v) then from_bool(!(Any..as_int!(v) == 0))
  else if Any..isfrom_float(v) then from_bool(!(Any..as_float!(v) == 0.0))
  else if Any..isfrom_str(v) then from_bool(!(Any..as_string!(v) == ""))
  else if Any..isfrom_ListAny(v) then from_bool(!(List_len(Any..as_ListAny!(v)) == 0))
  else if Any..isfrom_None(v) then from_bool(true)
  else if Any..isfrom_DictStrAny(v) then from_bool(!(Any..as_Dict!(v) == DictStrAny_empty()))
  else hole
};

Context

Discovered during review of #926 (bitwise operators PR). See this review thread for the full discussion.

[olivier-aws]

@keyboardDrummer-bot Please have a look. Do not go straight to implementation but create a design here first. Look beyond the PNot function but think of all other functions from our Python runtime and see if the same problem could happen as well

[olivier-aws]

@keyboardDrummer-bot Please have a look. Do not go straight to implementation but create a design here first. Look beyond the PNot function but think of all other functions from our Python runtime and see if the same problem could happen as well

[keyboardDrummer-bot]

Design: Align truthiness handling across the Python runtime

I audited every function in PythonRuntimeLaurelPart.lean that depends on Python's truthiness semantics or dispatches over Any type variants. Here's the full analysis and proposed fix.

---

1. The Any datatype — reference set of types

The Any datatype defines these non-exception variants:

Variant	Python type
from_None	None
from_bool	bool
from_int	int
from_float	float
from_str	str
from_datetime	datetime
from_bytes	bytes
from_DictStrAny	dict
from_ListAny	list
from_ClassInstance	class instances
from_Slice	slices

---

2. Functions affected and their current gaps

Any_to_bool (line 309) — the canonical truthiness function

Currently handles: bool, None, str, int, DictStrAny, ListAny
Missing: float (falsy when 0.0)

This is the root function. PAnd and POr delegate to it, so fixing it here fixes them too.

Fix: Add a float branch: if (Any..isfrom_float(v)) then !(Any..as_float!(v) == 0.0), and add Any..isfrom_float(v) to the requires clause.

PNot (line 612) — not x

Currently handles: bool, int, float, str, ListAny
Missing: None (always truthy under not), DictStrAny (truthy when non-empty)
Else branch: Returns exception(UndefinedError(...)) — unsound because Python's not never raises on non-exception inputs.

Fix: Add None and DictStrAny branches. Change the else to hole (safe over-approximation for types not yet modeled like datetime, bytes, ClassInstance, Slice).

PAnd / POr (lines 897, 904) — and / or

Currently handles (via requires): exception, bool, None, str, int
Missing from requires: float, DictStrAny, ListAny

In Python, and/or work on all types — they evaluate truthiness of the left operand and return one of the two operands. The requires clause artificially restricts the input types.

Fix: Expand the requires to match Any_to_bool's domain (add float, DictStrAny, ListAny). Once Any_to_bool handles float, these automatically work.

PNeg (line 599) — unary -

Currently handles: bool, int, float
Else branch: exception(UndefinedError(...))

This is correct. Python's unary - raises TypeError for non-numeric types (-None, -"hello", -[], -{} all raise). The exception fallthrough is the right behavior here. No change needed.

Comparison operators: PLt, PLe, PGt, PGe (lines 761–884)

Currently handles: bool, int, float (cross-type), str, ListAny, datetime
Missing: None, DictStrAny

This is correct. Python raises TypeError for < > <= >= on None and dict. The exception fallthrough is sound. No change needed.

PEq / PNEq (lines 885–891)

These use normalize_any and work on all types via structural equality. No change needed.

Arithmetic: PAdd, PSub, PMul, PFloorDiv, PMod, PPow

These correctly raise exceptions for unsupported type combinations (Python does the same). No change needed.

PIn / PNotIn (lines 539–560)

These have requires restricting to DictStrAny or ListAny, which matches Python (in only works on iterables/containers). No change needed.

---

3. Summary of proposed changes

Function	Change	Rationale
Any_to_bool	Add float branch + update requires	bool(0.0) is False in Python
PNot	Add None branch, add DictStrAny branch, change else from exception to hole	not works on all types in Python
PAnd	Expand requires to include float, DictStrAny, ListAny	and works on all types in Python
POr	Expand requires to include float, DictStrAny, ListAny	or works on all types in Python

---

4. Why hole instead of exception in the PNot else branch

For types we haven't modeled yet (datetime, bytes, ClassInstance, Slice), Python's not still works — it just calls __bool__ or __len__ on the object. Using exception is unsound because it claims Python raises an error when it doesn't. Using hole is a sound over-approximation: the verifier treats the result as unknown, which may produce inconclusive results but never unsound ones.

The same argument applies to Any_to_bool's final else false — but since it's guarded by a requires clause that restricts inputs to known types, the else branch is unreachable and thus not unsound. Still, for defense-in-depth, we could consider changing it to hole as well, but that's a separate discussion.

---

5. Sketch of the changes

Any_to_bool:

function Any_to_bool (v: Any) : bool
  requires (Any..isfrom_bool(v) || Any..isfrom_None(v) || Any..isfrom_str(v) || Any..isfrom_int(v) || Any..isfrom_float(v) || Any..isfrom_DictStrAny(v) || Any..isfrom_ListAny(v))
{
  if (Any..isfrom_bool(v)) then Any..as_bool!(v) else
  if (Any..isfrom_None(v)) then false else
  if (Any..isfrom_str(v)) then !(Any..as_string!(v) == "") else
  if (Any..isfrom_int(v)) then !(Any..as_int!(v) == 0) else
  if (Any..isfrom_float(v)) then !(Any..as_float!(v) == 0.0) else
  if (Any..isfrom_DictStrAny(v)) then !(Any..as_Dict!(v) == DictStrAny_empty()) else
  if (Any..isfrom_ListAny(v)) then !(Any..as_ListAny!(v) == ListAny_nil()) else
  false
};

PNot:

function PNot (v: Any) : Any
{
  if Any..isexception(v) then v
  else if Any..isfrom_bool(v) then from_bool(!(Any..as_bool!(v)))
  else if Any..isfrom_int(v) then from_bool(!(Any..as_int!(v) == 0))
  else if Any..isfrom_float(v) then from_bool(!(Any..as_float!(v) == 0.0))
  else if Any..isfrom_str(v) then from_bool(!(Any..as_string!(v) == ""))
  else if Any..isfrom_ListAny(v) then from_bool(!(List_len(Any..as_ListAny!(v)) == 0))
  else if Any..isfrom_None(v) then from_bool(true)
  else if Any..isfrom_DictStrAny(v) then from_bool(!(Any..as_Dict!(v) == DictStrAny_empty()))
  else hole
};

PAnd:

function PAnd (v1: Any, v2: Any) : Any
  requires (Any..isexception(v1) || Any..isfrom_bool(v1) || Any..isfrom_None(v1) || Any..isfrom_str(v1) || Any..isfrom_int(v1) || Any..isfrom_float(v1) || Any..isfrom_DictStrAny(v1) || Any..isfrom_ListAny(v1))
{
  if Any..isexception(v1) then v1 else
  if ! Any_to_bool (v1) then v1 else v2
};

POr: (same requires expansion as PAnd)

---

6. Questions for the team

1. Should we also add datetime truthiness? In Python, datetime objects are always truthy. This would mean adding datetime to Any_to_bool, PNot, PAnd/POr requires. I'd lean toward leaving it out for now and letting hole handle it, but wanted to flag it.

2. For PNot's hole fallthrough — should we do the same for PNeg? PNeg currently returns exception for unsupported types, which is correct for Python (unary - does raise TypeError). But if we ever model __neg__ on custom classes, we'd want hole there too. I think exception is fine for PNeg today.

3. Should Any_to_bool's unreachable else false also become hole for defense-in-depth?

Let me know if this design looks right and I'll proceed with implementation.

[olivier-aws]

@keyboardDrummer-bot Regarding your questions:

1. Let's leave datetime aside for now
2. The hole seems fine for PNot
3. Let's keep false for the else branch in Any to book

Please start the implementation. Start by writing a Python test that shows all these edge cases. The test should be executable in Python

[keyboardDrummer-bot]

Started the implementation. Here's what I've done so far:

Python test file added: test_truthiness_edge_cases.py — executable with plain python3, all 28 tests pass. It covers every edge case from the design:

Category	What's tested	Key edge cases (the bugs)
bool()	None, bool, int, float, str, list, dict	bool(0.0) == False, bool(-0.0) == False
not	All 7 types above	not None == True, not {} == True
and	All 7 types	0.0 and "x" == 0.0, [] and 1 == [], {} and 1 == {}
or	All 7 types	0.0 or "x" == "x", [] or 1 == 1, {} or 1 == 1

Draft PR: #936

Per the decisions:

1. ✅ Leaving datetime aside
2. ✅ Using hole for PNot else branch
3. ✅ Keeping false for Any_to_bool else branch

I'll proceed with the Lean runtime changes next (PythonRuntimeLaurelPart.lean).

[keyboardDrummer-bot]

Implementation complete. PR #936 now has both commits:

Commit 1 — Python test: test_truthiness_edge_cases.py with 28 tests covering all edge cases. All pass with python3.

Commit 2 — Lean runtime fix: PythonRuntimeLaurelPart.lean with these changes:

Function	Change
Any_to_bool	Added float to requires and added if (Any..isfrom_float(v)) then !(Any..as_float!(v) == 0.0) branch
PNot	Added None → from_bool(true) and DictStrAny → from_bool(!(... == DictStrAny_empty())) branches; changed else from exception(UndefinedError(...)) to hole
PAnd	Expanded requires to include float, DictStrAny, ListAny
POr	Expanded requires to include float, DictStrAny, ListAny

Build verified: lake build Strata succeeds ✅, lake build StrataTest has only pre-existing failures (unrelated Java jar + AnalyzeLaurelTest — both fail identically on main).

PR is in draft — ready for review when you'd like.