Repository navigation
Expand file tree
/
Copy pathSemantics.lean
More file actions
7004 lines (6596 loc) · 357 KB
/
Copy pathSemantics.lean
File metadata and controls
7004 lines (6596 loc) · 357 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
-- PARTLY LEGACY, and the split matters: this file holds BOTH the pre-rebuild
-- INTERPRETER (evalExpr/execStmt/callIn/execGen…) — legacy, the statement
-- target of pre-rebuild theorems, no new consumers, deleted when re-founded —
-- AND every PURE WORKER (evalBinOp, indexValH, sliceVal, truthyH, assignToH,
-- the string/render/sort workers). The workers are NOT legacy: the monadic
-- interpreter imports them, deliberately, so the rebuild owns the control and
-- the trunk owns the arithmetic. Marking the whole file legacy would be false.
import LeanModels.Python.Runtime
/-!
# Fuel-based definitional interpreter (`LeanModels.Python`)
Implements the Python semantic tier of `docs/DESIGN.md` ("Semantic
decisions", normative), re-shaped over the H1 runtime core of
`docs/memory-model.md` v2 (normative for the heap layer):
* the interpreter runs over **runtime values** (`RVal`, which may contain
heap refs) and threads a **`FrameState`** (shared `World` + this frame's
locals) through the `Run σ α` outcome type — state is retained on `.ok`
AND on `.exn`;
* `callIn` is the mutual-recursion point (and the frozen recursion point of
the proof doctrine): nested Python-to-Python calls share the caller's
`World`;
* `callFunction` is the isolated public observation — fresh world, **thaw**
the boundary arguments (`Val → RVal`), run `callIn`, **deep-freeze** the
result (`RVal → Res Val`) — with its signature UNCHANGED
(`Module → String → Array Val → Nat → Res Val`), so `CallsTo` and every
public theorem statement are untouched.
H1-proper (the dict tier, docs/memory-model.md §dict semantics) is LIVE:
dict literals allocate on the heap (`.ref` values), subscript stores
mutate it (aliasing-visible), reads/membership/`len`/`.get`/truthiness
resolve through it, `==` walks it (`heapEq` — a frozen recursion point;
ref-free pairs take the pure `valEq` fast path), identity is decided
dynamically, and the G1 module-init pass allocates top-level dict
literals into `initWorld`'s heap. The remaining `.ref` refusals below are
the loud H1 frontier (live iteration, value-container membership,
methods beyond `.get`, `del`, `.ref` operands of value-only helpers).
The v0 discipline is unchanged:
* **Fuel discipline** (normative): every function in the mutual block takes
`fuel : Nat` and starts `match fuel with | 0 => .timeout | fuel + 1 => …`,
passing the *decremented* fuel to **every** recursive call (expressions
included). Termination is structural on fuel; proofs do induction on fuel.
Fuel is a *depth* bound, not a step count: sibling calls receive the same
(already decremented) fuel.
* **Loud failure**: anything outside the tier yields `unsupported` with a
message naming the construct — never a silently wrong value. Real Python
runtime errors yield `exn` with the corresponding `PyErr`. `.timeout` is
fuel exhaustion ONLY; `unsupported` is the fuel-INDEPENDENT frontier.
* **Provability**: the semantics is factored into small, pure, fuel-free
helpers (`truthy`, `asInt`, `valEq`, `evalBinOp`, `evalUnaryOp`,
`evalCompareOp`, `Env.lookup`, `Env.set`, `indexVal`, `lenVal`,
`sortedVal`, `assignTo`, and the dict tier's heap readers) that proofs
can `simp`-unfold — the heap-aware steps (`truthyH`, `evalCompareOpH`,
`evalUnaryOpH`, `lenValH`, `indexValH`) delegate to the pure ones on
non-ref values, which is what keeps the proof-layer vocabulary pure —
plus a mutual block of the normative functions (`evalExpr`, `execStmt`,
`execStmts`, `callIn`) and the fueled chain helpers (`evalExprs`,
`evalBoolChain`, `evalCompareChain`, `evalDictItems`, `execWhile`,
`execFor`). The fueled `heapEq` block is a FROZEN recursion point.
Tier-boundary decisions refining DESIGN.md (Python supports these, the
tier does not — so they are `unsupported`, never a fake `TypeError`):
sequence repetition (`"a" * 2`), `%` string formatting, `str` unpacking
(`a, b = "xy"`), nested/starred unpacking targets, `break`/`continue`
escaping a function body, negative `**` exponents (incl. `0 ** -1`),
referencing a function (or a builtin — `len`/`sorted`) as a value, calling a
non-`Name` expression, `is`/`is not` without a `None` side (identity is not
value-determined), non-literal parameter defaults, `sorted` on anything but
an all-int list (see `sortedVal`), and the `.ref` arms noted above (the loud
H1 frontier — every operation on a heap object that is not in the dict
inventory).
In tier since the F1/F2 sprint: LITERAL parameter defaults (missing trailing
arguments filled in `mkCallEnv`; arity window `arityOk`) and `is`/`is not`
against the literal `None` (`evalCompareOp`). In tier since the
call:sorted sprint: the builtin `sorted` on all-int lists (`sortedVal`,
`sortInts`).
`Env` is an abbrev for `REnv = List (String × RVal)`, so `Env.lookup` /
`Env.set` must be called by their full names (dot notation on an `Env`
value resolves into the `List` namespace). They are polymorphic in the
value type (the G1 accumulator uses them at `Val`).
-/
namespace LeanModels.Python
/-! ## Pure helpers (fuel-free; proofs `simp`-unfold these) -/
/-- Python type name of a boundary value, as used in CPython error
messages. -/
def Val.typeName : Val → String
| .none => "NoneType"
| .bool _ => "bool"
| .int _ => "int"
| .str _ => "str"
| .list _ => "list"
| .tuple _ => "tuple"
/-- Python type name of a runtime value. A `.ref`'s real type name lives in
the heap (H1-proper resolves it there); the `"object"` placeholder is never
part of a *decided* outcome — every helper refuses `.ref` operands loudly
BEFORE building an error message from `typeName`. A namedtuple names its
own class (`Move`), exactly as CPython error messages do. -/
def RVal.typeName : RVal → String
| .none => "NoneType"
| .bool _ => "bool"
| .int _ => "int"
| .str _ => "str"
| .listV _ => "list"
| .tuple _ => "tuple"
| .ntuple tn _ _ => tn
| .rangeV .. => "range"
| .ref _ => "object"
/-- Is this runtime value one of the value-sequence types
(`str`/`listV`/`tuple`/namedtuple)? Namedtuples ARE tuples in CPython
(sequence protocol included), so they answer `true` — which routes
repetition to the loud sequence-repetition arm, never a fake `TypeError`. -/
def RVal.isSeq : RVal → Bool
| .str _ | .listV _ | .tuple _ => true
| .ntuple _ _ _ => true
| _ => false
/-! ### Ranges (pass 3, docs/memory-model.md §module-init execution)
A range is an IMMUTABLE, re-iterable sequence, carried as the immediate
`RVal.rangeV` and MATERIALIZED per use — exact because nothing can
mutate it between uses. The materialization budget is a FIXED constant
(never the fuel), so refusing an over-budget range is `unsupported` —
fuel-independent, per the loudness doctrine — and the helpers stay
fuel-free (`Run.le_refl` in every meta-proof arm). -/
/-- Elements a range yields (CPython's exact length formula — the
`sliceCount` shape; `step ≠ 0` by construction of `rangeV`). -/
def rangeLen (lo hi step : Int) : Nat :=
if 0 < step then
if lo < hi then ((hi - lo - 1) / step).toNat + 1 else 0
else
if hi < lo then ((lo - hi - 1) / (-step)).toNat + 1 else 0
/-- Collect `n` ints from `cur`, stepping. Structural (kernel-reducible). -/
def rangeValsAux : Nat → Int → Int → List RVal
| 0, _, _ => []
| n + 1, cur, step => .int cur :: rangeValsAux n (cur + step) step
/-- The fixed materialization budget (a million elements). A constant on
purpose: budget-refusals must be fuel-INDEPENDENT (`unsupported`, never
a fuel-varying outcome). -/
def seqBudget : Nat := 1048576
/-- The left-shift budget: the largest shift COUNT `<<` will build, so the
widest result is about a million bits (128 KB). Its own constant rather
than a reuse of `seqBudget` — they bound different resources and the
backlog recorded this as its own budget decision — but the same
discipline: fixed, therefore fuel-INDEPENDENT.
Why any bound at all (docs/memory-model.md §left shift and bitwise or):
`x << n` is `x * 2^n` with nothing limiting `n`, and the arm was reachable
with an arbitrary `n`. Measured 2026-08-15 on this toolchain,
`1 << (10^30)` did not compute and did not refuse — it died
`INTERNAL PANIC: Nat.pow exponent is too big`, a runner abort rather than
an answer. Below the budget nothing changes and CPython is matched
exactly; above it the model says so LOUDLY. Note this refuses some shifts
CPython performs happily (`1 << 10^9` is a real 125 MB integer there): a
declared tier gap, never a claim that CPython raises. -/
def shiftBudget : Nat := 1048576
/-- Materialize a range value, budget-guarded (see the section comment). -/
def rangeVals (lo hi step : Int) : Res (List RVal) :=
let n := rangeLen lo hi step
if n ≤ seqBudget then .ok (rangeValsAux n lo step)
else .unsupported "materializing a range beyond seqBudget is outside the tier (docs/memory-model.md §module-init execution)"
/-- Is this runtime value Python's `None` singleton? (The value-level test
behind `is None` / `is not None` — see `evalCompareOp`.) A heap object is
never `None`, so the `.ref` arm is a faithful `false`, not a refusal. -/
def RVal.isNone : RVal → Bool
| .none => true
| _ => false
/-- Python surface syntax of a binary operator (error messages). -/
def BinOp.symbol : BinOp → String
| .add => "+"
| .sub => "-"
| .mult => "*"
| .floorDiv => "//"
| .mod => "%"
| .pow => "**"
| .lshift => "<<"
| .rshift => ">>"
| .bitOr => "|"
| .bitXor => "^"
| .bitAnd => "&"
/-- Python surface syntax of a comparison operator (error messages). -/
def CmpOp.symbol : CmpOp → String
| .eq => "=="
| .notEq => "!="
| .lt => "<"
| .ltE => "<="
| .gt => ">"
| .gtE => ">="
| .is => "is"
| .isNot => "is not"
| .inOp => "in"
| .notIn => "not in"
/-- Schema `kind` name of an expression node (error messages). For
`unsupported` nodes this is the recorded CPython class name. -/
def Expr.kindName : Expr → String
| .namedExpr .. => "NamedExpr"
| .constant .. => "Constant"
| .name .. => "Name"
| .binOp .. => "BinOp"
| .unaryOp .. => "UnaryOp"
| .boolOp .. => "BoolOp"
| .compare .. => "Compare"
| .call .. => "Call"
| .list .. => "List"
| .tuple .. => "Tuple"
| .subscript .. => "Subscript"
| .dict .. => "Dict"
| .attribute .. => "Attribute"
| .ifExp .. => "IfExp"
| .slice .. => "Slice"
| .genExp .. => "GeneratorExp"
| .unsupported pyKind _ _ => pyKind
/-- Schema `kind` name of a statement node (error messages) — the
`Expr.kindName` counterpart. -/
def Stmt.kindName : Stmt → String
| .ret .. => "Return"
| .assign .. => "Assign"
| .augAssign .. => "AugAssign"
| .whileLoop .. => "While"
| .forStmt .. => "For"
| .ifStmt .. => "If"
| .exprStmt .. => "Expr"
| .yieldStmt .. => "Yield"
| .yieldFromStmt .. => "YieldFrom"
| .defStmt .. => "NestedDef"
| .raiseStmt .. => "Raise"
| .assertStmt .. => "Assert"
| .tryStmt .. => "Try"
| .importFrom .. => "ImportFrom"
| .delStmt .. => "Delete"
| .pass _ => "Pass"
| .brk _ => "Break"
| .cont _ => "Continue"
| .unsupported pyKind _ _ => pyKind
/-- A CLOSURE CELL reached a VALUE position (H7 cells,
docs/memory-model.md §nested defs and closures). A cell is an
interpreter-internal heap slot: it is created by a `def` with a
late-bound capture, addressed ONLY through a frame's `<cell>x` env key,
and read ONLY by `cellsFor`, at the closure call. No Python expression
can produce one, so every value-position consumer says so LOUDLY rather
than inventing a type for it. -/
def cellInternal : String :=
"internal: a closure CELL reached a value position — a cell is never a Python value (unreachable through ingestion; report this)"
/-- Python truthiness `bool(x)`: `None` → false; `bool` → itself;
`int` → `≠ 0`; `str`/`listV`/`tuple` → nonempty. `Res`-valued since H1:
a `.ref`'s truthiness lives in the heap (`bool(d)` is `len(d) != 0`) —
loud until the dict tier reads it there. -/
def truthy : RVal → Res Bool
| .none => .ok false
| .bool b => .ok b
| .int n => .ok (n != 0)
| .str s => .ok (!s.isEmpty)
| .listV xs => .ok (xs.size != 0)
| .tuple xs => .ok (xs.size != 0)
| .ntuple _ _ xs => .ok (xs.size != 0)
| .rangeV lo hi step => .ok (rangeLen lo hi step != 0)
| .ref _ => .unsupported
"truthiness of a heap object lives in the heap (`truthyH` decides it; this pure helper is the proof-layer vocabulary)"
/-- Heap-resolving type name (H2): a `.ref` names its referent's type.
The `"object"` fallback is the dangling arm — unreachable from WF worlds,
and never part of a decided outcome that isn't already loud.
Deliberately OUT of `py_simp`/`interpUnfolds` (recorded H2 finding, the
`sortInts`/`heapEq` freeze family): it occurs only inside error-message
interpolations of undecided helper arms, so as a simp member it buys
nothing — and with it in the set a plain symbolic run whnf-storms
(≈740k `List.rec` / 1.5M `Array.toList` unfoldings on `sf_bound_rec`'s
exit lemma before timing out; message-position `String.append` chains
keep re-offering the pattern). A raise-theorem that needs a heap-named
message passes it explicitly. -/
def RVal.typeNameH (h : Heap) : RVal → String
| .ref a =>
match Heap.get? h a with
| some (.dict _ _) => "dict"
| some (.list _) => "list"
-- H3: the class NAME lives in the module, not the heap — "object" is
-- the message-only placeholder (the harness compares exception CLASS
-- names, never messages).
| some (.instance _ _) => "object"
| some (.generator ..) => "generator"
-- a CELL is interpreter-internal and never names a Python type; the
-- message-only placeholder keeps this total (the value-position
-- consumers all refuse with `cellInternal`).
| some (.cell _) => "cell"
| some (.closure ..) => "function"
| some (.pyset _) => "set"
| Option.none => "object"
| v => v.typeName
/-- bool→int coercion (Python's `bool` is an `int` subtype): `int` passes
through, `True`/`False` become `1`/`0`, everything else is `none`. -/
def asInt : RVal → Option Int
| .int n => some n
| .bool b => some (if b then 1 else 0)
| _ => Option.none
/-- `range(…)` construction from evaluated arguments: 1–3 int args
(bool coerces, CPython's `__index__` on bool), `step = 0` the faithful
`ValueError`, wrong arity/types the faithful `TypeError`s. -/
def rangeMake (h : Heap) (vs : List RVal) : Res RVal :=
-- CPython names the OFFENDING OBJECT's type, never range's requirements,
-- and it names the FIRST bad argument left to right (measured 3.9.19:
-- `range([1],[2],[3])` and `range(1,[2],[3])` are both `'list' object
-- cannot be interpreted as an integer`). The three-argument arm used to
-- answer `range() arguments must be integers`, which is not a sentence
-- CPython 3.9 produces. `typeNameH` and not `typeName`: a heap operand
-- is reachable here (`range({1: 2})` is `'dict' object …`) and the bare
-- `typeName` would put the `"object"` placeholder into a decided
-- outcome, which the recorded rule forbids.
let bad := fun (v : RVal) =>
Res.exn (α := RVal)
(.typeError s!"'{RVal.typeNameH h v}' object cannot be interpreted as an integer")
match vs with
| [] => .exn (.typeError "range expected at least 1 argument, got 0")
| [v] =>
(match asInt v with
| some n => .ok (.rangeV 0 n 1)
| Option.none => bad v)
| [a, b] =>
(match asInt a, asInt b with
| some x, some y => .ok (.rangeV x y 1)
| Option.none, _ => bad a
| some _, Option.none => bad b)
| [a, b, c] =>
(match asInt a, asInt b, asInt c with
| some x, some y, some z =>
if z == 0 then .exn (.valueError "range() arg 3 must not be zero")
else .ok (.rangeV x y z)
| Option.none, _, _ => bad a
| some _, Option.none, _ => bad b
| some _, some _, Option.none => bad c)
| vs => .exn (.typeError s!"range expected at most 3 arguments, got {vs.length}")
mutual
/-- Python `==` on runtime values. Numeric (`int`/`bool`) compare by
value after bool→int coercion (`True == 1`); `str` by string equality;
`listV`/`tuple` elementwise (recursively, so `[True] == [1]`);
`None == None`; any cross-type combination (after coercion) is `False`.
`Res`-valued since H1: `==` on a `.ref` is the heap-walking dict equality
(identity shortcut, size check, left-order traversal, active-pair cycle
detection — docs/memory-model.md) — loud until the dict tier implements
it. On ref-free values it never fails. -/
def valEq : RVal → RVal → Res Bool
| .none, .none => .ok true
| .bool a, .bool b => .ok (a == b)
| .bool a, .int m => .ok ((if a then (1 : Int) else 0) == m)
| .int n, .bool b => .ok (n == (if b then (1 : Int) else 0))
| .int n, .int m => .ok (n == m)
| .str s, .str t => .ok (s == t)
| .listV xs, .listV ys => valEqList xs.toList ys.toList
| .tuple xs, .tuple ys => valEqList xs.toList ys.toList
-- namedtuples compare as plain tuples (CPython: tuple.__eq__ — the
-- class is IGNORED, even across two different namedtuple classes)
| .ntuple _ _ xs, .ntuple _ _ ys => valEqList xs.toList ys.toList
| .ntuple _ _ xs, .tuple ys => valEqList xs.toList ys.toList
| .tuple xs, .ntuple _ _ ys => valEqList xs.toList ys.toList
| .ref _, _ => .unsupported
"'==' on a heap object lives in the heap (`heapEq` decides it; this pure helper is the proof-layer vocabulary)"
| _, .ref _ => .unsupported
"'==' on a heap object lives in the heap (`heapEq` decides it; this pure helper is the proof-layer vocabulary)"
-- pass 3: `==` with a range operand stays LOUD — CPython compares
-- ranges as SEQUENCES (`range(0) == range(2, 2)` is `True`), and the
-- cross-type `False` would invite guessing half the protocol
| .rangeV .., _ => .unsupported
"'==' on a range is outside the tier (CPython compares ranges as sequences; docs/memory-model.md §module-init execution)"
| _, .rangeV .. => .unsupported
"'==' on a range is outside the tier (CPython compares ranges as sequences; docs/memory-model.md §module-init execution)"
| _, _ => .ok false
/-- Elementwise `valEq`, short-circuiting on the first mismatch;
`false` on length mismatch. -/
def valEqList : List RVal → List RVal → Res Bool
| [], [] => .ok true
| a :: as, b :: bs => do
let e ← valEq a b
if e then valEqList as bs else return false
| _, _ => .ok false
end
/-- Ordering comparison on `Int` (only called with `.lt/.ltE/.gt/.gtE`;
the equality and identity cases are handled by `valEq`/`RVal.isNone` in
`evalCompareOp` and never reach here, but are given a by-value meaning
(`is` on identical-valued ints would be `True` under CPython's small-int
cache; the arms exist for totality only). -/
def intCmp : CmpOp → Int → Int → Bool
| .eq, x, y => x == y
| .notEq, x, y => x != y
| .lt, x, y => x < y
| .ltE, x, y => x ≤ y
| .gt, x, y => y < x
| .gtE, x, y => y ≤ x
| .is, x, y => x == y
| .isNot, x, y => x != y
| .inOp, _, _ => false -- unreachable: membership never reaches intCmp
| .notIn, _, _ => false -- (evalCompareOp handles it first; totality arm)
/-- Ordering comparison on `String` (lexicographic by Unicode code points,
which is Lean's `String` `<`). See `intCmp` for the equality/identity cases. -/
def strCmp : CmpOp → String → String → Bool
| .eq, s, t => s == t
| .notEq, s, t => s != t
| .lt, s, t => s < t
| .ltE, s, t => s < t || s == t
| .gt, s, t => t < s
| .gtE, s, t => t < s || s == t
| .is, s, t => s == t
| .isNot, s, t => s != t
| .inOp, _, _ => false -- unreachable: membership never reaches strCmp
| .notIn, _, _ => false -- (evalCompareOp handles it first; totality arm)
mutual
/-- CPython strict `<` on immediate values (H6 draining consumers,
docs/memory-model.md §draining consumers): int/bool numeric, str
code-point lexicographic, tuple/namedtuple/value-list lexicographic and
CLASS-ERASED (`valEq` walks elementwise ties, `rvalLt` decides the
first difference; exhaustion → the shorter is smaller — CPython's
`tuple.__lt__`). Refs and mixed value kinds refuse LOUDLY, mirroring
`evalCompareOp`'s ordering arm — never a guessed `TypeError`. This is
THE ordering relation: the `<` operator and `sorted`/`max`/`min` all
decide through it. A worker of the `sortInts` freeze family — OUT of
the simp sets. -/
def rvalLt : RVal → RVal → Res Bool
| .bool a, .bool b => .ok ((if a then (1 : Int) else 0) < (if b then (1 : Int) else 0))
| .bool a, .int m => .ok ((if a then (1 : Int) else 0) < m)
| .int n, .bool b => .ok (n < (if b then (1 : Int) else 0))
| .int n, .int m => .ok (n < m)
| .str s, .str t => .ok (strCmp .lt s t)
| .tuple xs, .tuple ys => rvalLtList xs.toList ys.toList
| .tuple xs, .ntuple _ _ ys => rvalLtList xs.toList ys.toList
| .ntuple _ _ xs, .tuple ys => rvalLtList xs.toList ys.toList
| .ntuple _ _ xs, .ntuple _ _ ys => rvalLtList xs.toList ys.toList
| .listV xs, .listV ys => rvalLtList xs.toList ys.toList
| .ref _, b =>
.unsupported s!"ordering comparison '<' on a heap object is outside the tier ({b.typeName} rhs; docs/memory-model.md)"
| a, .ref _ =>
.unsupported s!"ordering comparison '<' on a heap object is outside the tier ({a.typeName} lhs; docs/memory-model.md)"
| a, b =>
.unsupported s!"comparison '<' between '{a.typeName}' and '{b.typeName}' is outside the tier"
/-- Elementwise lexicographic `<`: `valEq` walks the common prefix,
`rvalLt` decides the first difference, length breaks ties. -/
def rvalLtList : List RVal → List RVal → Res Bool
| [], [] => .ok false
| [], _ :: _ => .ok true
| _ :: _, [] => .ok false
| a :: as, b :: bs => do
let e ← valEq a b
if e then rvalLtList as bs else rvalLt a b
end
/-- The four ordering operators derived from strict `<` — exact within
the tier: on comparable pairs the order is total, so `a <= b` is
`¬(b < a)`; incomparable pairs refuse inside `rvalLt` before the
negation can lie. -/
def ordFromLt (op : CmpOp) (a b : RVal) : Res Bool :=
match op with
| .lt => rvalLt a b
| .gt => rvalLt b a
| .ltE => do let g ← rvalLt b a; return !g
| .gtE => do let l ← rvalLt a b; return !l
| _ => .unsupported "ordFromLt: non-ordering operator (report this)"
/-- One comparison step. `==`/`!=` are `valEq` (`Res`-valued since H1 — see
there). `is`/`is not` (F2): the extractor admits these ONLY when one side of
the link is the literal `None`, whose runtime value is always `RVal.none` —
so identity here is against the `None` singleton and IS value-determined:
`x is None ⟺ x = RVal.none` (a heap `.ref` is faithfully not `None`). When
at least one operand is `.none` the result is `a.isNone && b.isNone`; if
NEITHER side is `.none` — unreachable through the extractor, but reachable
by hand-built ASTs — identity between two non-None values is
CPython-implementation-defined (small-int caching, str interning) and
refused loudly (H1-proper adds the faithful two-ref address equality).
Ordering: int/bool by value (bool→int coercion), str lexicographic;
ordering any other type combination is outside the tier. -/
def evalCompareOp (op : CmpOp) (a b : RVal) : Res Bool :=
match op with
| .eq => valEq a b
| .notEq => do let e ← valEq a b; return !e
| .is =>
if a.isNone || b.isNone then .ok (a.isNone && b.isNone)
else
.unsupported
s!"'is' between '{a.typeName}' and '{b.typeName}' (identity is not value-determined) is outside the v0 tier"
| .isNot =>
if a.isNone || b.isNone then .ok (!(a.isNone && b.isNone))
else
.unsupported
s!"'is not' between '{a.typeName}' and '{b.typeName}' (identity is not value-determined) is outside the v0 tier"
| .inOp =>
.unsupported
s!"'in' on '{b.typeName}' is outside this tier (dict membership lands with H1-proper, docs/memory-model.md)"
| .notIn =>
.unsupported
s!"'not in' on '{b.typeName}' is outside this tier (dict membership lands with H1-proper, docs/memory-model.md)"
| op =>
match asInt a, asInt b with
| some x, some y => .ok (intCmp op x y)
| _, _ =>
match a, b with
| .str s, .str t => .ok (strCmp op s t)
-- H6: tuple/namedtuple ordering, class-erased and lexicographic —
-- ONE relation with `sorted` (`rvalLt`, via `ordFromLt`)
| .tuple _, .tuple _ => ordFromLt op a b
| .tuple _, .ntuple _ _ _ => ordFromLt op a b
| .ntuple _ _ _, .tuple _ => ordFromLt op a b
| .ntuple _ _ _, .ntuple _ _ _ => ordFromLt op a b
| .ref _, b =>
.unsupported
s!"ordering comparison '{op.symbol}' on a heap object is outside the H1 tier ({b.typeName} rhs; docs/memory-model.md)"
| a, .ref _ =>
.unsupported
s!"ordering comparison '{op.symbol}' on a heap object is outside the H1 tier ({a.typeName} lhs; docs/memory-model.md)"
| a, b =>
.unsupported
s!"comparison '{op.symbol}' between '{a.typeName}' and '{b.typeName}' is outside the v0 tier"
/-- Tuple repetition `xs * n` (pass 3): `n ≤ 0` is empty (CPython), the
result budget-guarded like `rangeVals` (fuel-independent refusal). -/
def tupleRepeat (xs : Array RVal) (n : Int) : Res RVal :=
if xs.size * n.toNat ≤ seqBudget then
.ok (.tuple ((List.replicate n.toNat xs.toList).flatten.toArray))
else
.unsupported "tuple repetition beyond seqBudget is outside the tier (docs/memory-model.md §module-init execution)"
/-- `a &&& ~m` over `Nat`. `Nat.ldiff` does not exist in v4.33.0-rc1, and
none is needed: every bit of `a` either is or is not in `m`, so removing
the ones that are IS the difference. Never underflows (the grid instrument
in docs/backlog.md §construct 4 checked 0 underflows over 22201 pairs). -/
def ndiff (a m : Nat) : Nat := a - (a &&& m)
/-- `&` over `Int`, EXACT on negative operands. Nothing is guessed:
Lean's `Int.negSucc n` IS `-(n+1)`, so for a negative `x` the number
`-x-1` — whose bits are the complement of `x`'s — is the constructor's own
argument, available by matching and requiring no arithmetic at all
(docs/memory-model.md §bitwise `&`). -/
def intAnd : Int → Int → Int
| .ofNat a, .ofNat b => .ofNat (a &&& b)
| .negSucc a, .ofNat b => .ofNat (ndiff b a)
| .ofNat a, .negSucc b => .ofNat (ndiff a b)
| .negSucc a, .negSucc b => .negSucc (a ||| b)
/-- `|` over `Int`, the same construction. This REPLACES pass 5's negative
refusal, which was a design-time prediction rather than a measurement:
`-1 | 4` has a value (`-1`), it is exact here, and keeping the refusal
would be manufacturing one for a case known to be right. -/
def intOr : Int → Int → Int
| .ofNat a, .ofNat b => .ofNat (a ||| b)
| .negSucc a, .ofNat b => .negSucc (ndiff a b)
| .ofNat a, .negSucc b => .negSucc (ndiff b a)
| .negSucc a, .negSucc b => .negSucc (a &&& b)
/-- `^` over `Int`, the same construction — and the simplest of the three,
because XOR commutes with complement. `.negSucc a` IS `~a`, and
`~p ^ q = ~(p ^ q)`, `~p ^ ~q = p ^ q`, so every arm is one `Nat` XOR
whose sign is read off the operands' parity: no `ndiff`, no subtraction,
nothing to underflow. (§L39 rung 1: the tail batch landed `|` and `&`
and left `^` out, with nothing recorded about the omission.) -/
def intXor : Int → Int → Int
| .ofNat a, .ofNat b => .ofNat (a ^^^ b)
| .negSucc a, .ofNat b => .negSucc (a ^^^ b)
| .ofNat a, .negSucc b => .negSucc (a ^^^ b)
| .negSucc a, .negSucc b => .ofNat (a ^^^ b)
/-! ### Scalar rendering (`str()` and a str's `repr`)
These sit HERE, above the operator block, because both users need them
and one of the users is the `%` operator below: `evalBinOp` precedes
§rendering in this file and Lean has no forward references. Moved
verbatim from §rendering, which keeps the heap-recursive `reprVal`/
`printOne`/`strOfValH` built on top of them. -/
/-- `str(…)` — value-only (docs/memory-model.md §the cast tier): the
exact decimal for ints, `True`/`False`, identity on strs, `None`;
containers and refs refuse loudly (repr recursion is not guessed). -/
def strOfVal : RVal → Res RVal
| .int n => .ok (.str (toString n))
| .bool b => .ok (.str (if b then "True" else "False"))
| .str s => .ok (.str s)
| .none => .ok (.str "None")
| v => .unsupported s!"str() of '{v.typeName}' is outside the tier (repr recursion is not guessed; docs/memory-model.md §the cast tier)"
/-- Lowercase hex digit. -/
def hexDigit (n : Nat) : Char :=
if n < 10 then Char.ofNat (48 + n) else Char.ofNat (87 + n)
/-- Two-digit lowercase hex (`\xNN` escapes). -/
def hex2 (n : Nat) : String :=
String.mk [hexDigit (n / 16 % 16), hexDigit (n % 16)]
/-- The quote CPython picks for a string's `repr`: `'` unless the string
contains one and no `"`. -/
def reprQuote (s : String) : Char :=
if s.contains '\'' && !s.contains '"' then '"' else '\''
/-- `repr` of one character inside a string literal; `none` = non-ASCII
(printability is a Unicode table this model does not guess). -/
def reprChar (q : Char) : Char → Option String
| '\\' => some "\\\\"
| '\n' => some "\\n"
| '\r' => some "\\r"
| '\t' => some "\\t"
| c =>
if c == q then some (String.mk ['\\', c])
else if c.val < 0x20 || c.val == 0x7f then some ("\\x" ++ hex2 c.val.toNat)
else if c.val < 0x7f then some (String.mk [c])
else Option.none
/-- `reprChar` over a character list. -/
def reprChars (q : Char) : List Char → Option String
| [] => some ""
| c :: cs => do
let a ← reprChar q c
let rest ← reprChars q cs
return a ++ rest
/-- CPython `repr` of a str: the quote choice above, backslash/quote/
`\n`/`\r`/`\t` escapes, `\xNN` for the other C0 controls and DEL, and a
LOUD refusal on anything non-ASCII. -/
def reprStr (s : String) : Option String := do
let q := reprQuote s
let body ← reprChars q s.data
return String.mk [q] ++ body ++ String.mk [q]
/-! ### `%`-formatting (docs/memory-model.md §`%`-formatting on strings)
`str % args` is CPython's `unicode_mod`: ONE left-to-right pass over the
format string. This operator is a pure function of two VALUES and cannot
see the heap, so the admitted arguments are exactly the scalars whose
rendering is heap-independent — everything else refuses loudly rather
than guessing a `repr` the heap holds. -/
/-- `%s` of an argument: `strOfVal` verbatim (a str raw; int/bool/None
their digits/`True`/`False`/`None`). `none` = outside the inventory. -/
def strFormatStr (v : RVal) : Option String :=
match strOfVal v with
| .ok (.str s) => some s
| _ => Option.none
/-- `%r` of an argument. Only a str differs from `%s` — CPython's `repr`
and `str` COINCIDE on int/bool/None — and its quoting/escaping IS the
shipped `reprStr`, so a non-ASCII string refuses here exactly as it
refuses inside `print([…])`. -/
def strFormatRepr (v : RVal) : Option String :=
match v with
| .str s => reprStr s
| v => strFormatStr v
/-- One admitted conversion applied to one argument. A `.ref` argument
(reachable only nested inside a tuple, since an operand-position `.ref`
is refused before this arm) is LOUD, never a `TypeError` built from
`RVal.typeName`'s `"object"` placeholder. -/
def strFormatConv (c : Char) (v : RVal) : Res String :=
match v with
| .ref _ =>
.unsupported "a heap object as a '%'-format argument is outside the tier (its repr lives in the heap, which the operator cannot see; docs/memory-model.md §`%`-formatting on strings)"
| v =>
if c == 'd' then
match asInt v with
| some n => .ok (toString n)
-- CPython leaves this type name UNQUOTED (measured against 3.9)
| Option.none => .exn (.typeError s!"%d format: a number is required, not {v.typeName}")
else
match (if c == 'r' then strFormatRepr v else strFormatStr v) with
| some s => .ok s
| Option.none =>
.unsupported s!"'%{c}' of a '{v.typeName}' is outside the tier (only int/bool/str/None render here; docs/memory-model.md §`%`-formatting on strings)"
/-- CPython's `ctx.dict` test, verbatim: `PyMapping_Check(args) &&
!PyTuple_Check(args) && !PyUnicode_Check(args)` (`PyUnicode_Format`,
Objects/unicodeobject.c). `PyMapping_Check` is `tp_as_mapping->mp_subscript
≠ NULL` — MEASURED true on str/tuple/list/dict/range/bytes/bytearray and
false on None/bool/int/float/set (3.9.19, through `ctypes.pythonapi`), so
inside this tier the mapping right operand is exactly `listV` and `rangeV`:
str and tuple are struck out by the two `!` clauses, a namedtuple by
`PyTuple_Check` on the subclass, and a `.ref` never arrives at all
(`evalBinOp`'s heap-operand refusal fires first — the invariant §`%`-
formatting states, and the thing to revisit when lists move to the heap).
It decides ONE observable, and that is why it is here: with a mapping RHS
the trailing `not all arguments converted` check DOES NOT RUN (the check
is guarded `argidx < arglen && !dict`), so `' x ' % [1, 3, 5]` is
`' x '` and not a `TypeError`. The other half of the mapping path, the
`%(key)s` protocol, is refused LOUDLY by the walker below and stays so. -/
def strFormatMappingRhs : RVal → Bool
| .listV _ => true
| .rangeV _ _ _ => true
| _ => false
/-- The single left-to-right pass. Literals copy; `%%` emits one `%` and
consumes NOTHING; `%s`/`%r`/`%d` consume the next argument. Running out
mid-walk is CPython's `not enough arguments` verbatim, and so are
leftover arguments at the end — EXCEPT under `mapping`, the `ctx.dict`
flag above, which is exactly the condition CPython guards that second
check with. Anything else after a `%` — a flag, a width, a precision, a
mapping key, another conversion character, or the end of the string — is
LOUD: the format minilanguage is a second tier, and the forms CPython
itself rejects (`%q`, a trailing `%`) get a refusal rather than a
fabricated `ValueError` (recorded restriction). -/
def strFormatWalk : List Char → List RVal → Bool → String → Res String
| [], args, mapping, acc =>
if args.isEmpty || mapping then .ok acc
else .exn (.typeError "not all arguments converted during string formatting")
| '%' :: '%' :: cs, args, mapping, acc => strFormatWalk cs args mapping (acc ++ "%")
| '%' :: c :: cs, args, mapping, acc =>
if c == 's' || c == 'r' || c == 'd' then
match args with
| [] => .exn (.typeError "not enough arguments for format string")
-- the conversion is matched OPEN, not bound through `Res`'s
-- `bind`: a recursive call under the bind's lambda is invisible
-- to structural recursion, and this walker must stay
-- kernel-reducible (the mergeSort trap, AGENTS.md)
| a :: rest =>
match strFormatConv c a with
| .ok piece => strFormatWalk cs rest mapping (acc ++ piece)
| .exn e => .exn e
| .timeout => .timeout
| .unsupported msg => .unsupported msg
else
.unsupported s!"the '%{c}' conversion is outside the tier (only bare %s/%r/%d/%% — no flags, width, precision, or mapping key; docs/memory-model.md §`%`-formatting on strings)"
| ['%'], _, _, _ =>
.unsupported "a format string ending in '%' is outside the tier (CPython's `incomplete format` ValueError is not modelled; docs/memory-model.md §`%`-formatting on strings)"
| c :: cs, args, mapping, acc => strFormatWalk cs args mapping (acc ++ String.mk [c])
/-- `str % args`. The argument LIST is the RHS spread when it is a tuple
— and a NAMEDTUPLE spreads too, because `PyTuple_Check` succeeds on the
subclass (`'%s %s' % Move(1,2)` is `'1 2'`, measured): treating it as one
argument would fabricate an arity error for a program CPython runs.
Everything else is the one-element list — which is CPython's `arglen = -1,
argidx = -2` state exactly: the first conversion gets the whole object,
the second is `not enough arguments`. Whether a LEFTOVER is an error is
the separate `ctx.dict` question `strFormatMappingRhs` answers. -/
def strFormat (fmt : String) (rhs : RVal) : Res RVal := do
let args : List RVal :=
match rhs with
| .tuple xs => xs.toList
| .ntuple _ _ xs => xs.toList
| v => [v]
let s ← strFormatWalk fmt.data args (strFormatMappingRhs rhs) ""
return .str s
/-- Binary operator on already-evaluated operands. int/bool operands are
coerced to `Int`; arithmetic results are always `int`, never `bool`.
`//`/`%` floor (`Int.fdiv`/`Int.fmod`); divisor 0 → `ZeroDivisionError`.
`**` requires a nonnegative exponent (float result otherwise → unsupported).
`+` concatenates matching sequence types. Python-valid combinations outside
the tier (sequence repetition) → unsupported; `%` on a str is the format
operator (`strFormat`, §`%`-formatting above); Python-invalid
combinations → `TypeError`. A `.ref` operand is refused loudly BEFORE the
`TypeError` fallback (its type name lives in the heap). -/
def evalBinOp (op : BinOp) (a b : RVal) : Res RVal :=
match asInt a, asInt b with
| some x, some y =>
match op with
| .add => .ok (.int (x + y))
| .sub => .ok (.int (x - y))
| .mult => .ok (.int (x * y))
| .floorDiv =>
if y = 0 then .exn .zeroDivisionError else .ok (.int (Int.fdiv x y))
| .mod =>
if y = 0 then .exn .zeroDivisionError else .ok (.int (Int.fmod x y))
| .pow =>
if y < 0 then
-- CPython: 0 ** -1 raises (no float involved); other negative
-- exponents produce floats, which are outside the v0 tier.
-- Same CLASS as `//`/`%` but a different TEXT, so it carries its
-- own constructor (Ast.lean `zeroDivisionPow`) — measured
-- `0.0 cannot be raised to a negative power`.
if x = 0 then .exn .zeroDivisionPow
else .unsupported "'**' with a negative exponent (float result) is outside the v0 tier"
else .ok (.int (x ^ y.toNat))
-- pass 5 (docs/memory-model.md §left shift and bitwise or):
-- `x << n` is EXACT on all ints as `x * 2^n` (unbounded ints, sign
-- carries through); the negative count is the faithful ValueError.
| .lshift =>
if y < 0 then .exn (.valueError "negative shift count")
else if y.toNat > shiftBudget then
.unsupported "a left shift beyond shiftBudget is outside the tier (docs/memory-model.md §left shift and bitwise or)"
else .ok (.int (x * (2 : Int) ^ y.toNat))
-- `>>` is `<<`'s mirror and is CPython's ARITHMETIC shift: it rounds
-- toward -inf, which is exactly `Int.fdiv` by `2^n` (`-5 >> 1 == -3`).
-- The budget is `<<`'s, for the same reason and not a weaker one:
-- forming `2 ^ y` to divide by would hit the very `Nat.pow exponent
-- is too big` abort the budget exists to prevent. CPython SATURATES
-- there (a shift past the operand's bit length is 0, or -1 when
-- negative) and answers instantly; saturating here would be exact
-- only under a bound on `x`'s bit length that this tier does not
-- have, so the honest answer is the same loud, fuel-independent
-- refusal `<<` gives — never a claim that CPython raises. Recorded
-- as owed: saturation behind a width argument.
| .rshift =>
if y < 0 then .exn (.valueError "negative shift count")
else if y.toNat > shiftBudget then
.unsupported "a right shift beyond shiftBudget is outside the tier (docs/memory-model.md §left shift and bitwise or)"
else .ok (.int (Int.fdiv x ((2 : Int) ^ y.toNat)))
-- `|` and `&` decide BOOLNESS first (`bool.__or__(bool)` returns a
-- BOOL, any int operand makes it an int), then compute over `Int` —
-- negative operands INCLUDED (docs/memory-model.md §bitwise `&`; the
-- pass-5 refusal was measured wrong and is retired here, in the same
-- landing that admits `&`, so the family cannot drift apart).
| .bitOr =>
(match a, b with
| .bool p, .bool q => .ok (.bool (p || q))
| _, _ => .ok (.int (intOr x y)))
| .bitXor =>
(match a, b with
| .bool p, .bool q => .ok (.bool (p != q))
| _, _ => .ok (.int (intXor x y)))
| .bitAnd =>
(match a, b with
| .bool p, .bool q => .ok (.bool (p && q))
| _, _ => .ok (.int (intAnd x y)))
| _, _ =>
match op, a, b with
| .add, .str s, .str t => .ok (.str (s ++ t))
| .add, .listV xs, .listV ys => .ok (.listV (xs ++ ys))
| .add, .tuple xs, .tuple ys => .ok (.tuple (xs ++ ys))
-- namedtuple `+` concatenates as tuples and yields a PLAIN tuple
-- (CPython: tuple.__add__ — the class does not survive concatenation)
| .add, .ntuple _ _ xs, .tuple ys => .ok (.tuple (xs ++ ys))
| .add, .tuple xs, .ntuple _ _ ys => .ok (.tuple (xs ++ ys))
| .add, .ntuple _ _ xs, .ntuple _ _ ys => .ok (.tuple (xs ++ ys))
| op, .ref _, _ =>
.unsupported
s!"binary '{op.symbol}' on a heap object is outside the H1 tier (dict operators beyond the inventory; docs/memory-model.md)"
| op, _, .ref _ =>
.unsupported
s!"binary '{op.symbol}' on a heap object is outside the H1 tier (dict operators beyond the inventory; docs/memory-model.md)"
-- pass 3: TUPLE repetition (`(0,) * 20`) — in-model allocation-free
-- (immediate values); a namedtuple repeats as a PLAIN tuple
-- (tuple.__mul__); non-int right/left operands keep CPython's
-- `can't multiply sequence by non-int` class through the arm below.
-- List/str repetition stays loud (a list result allocates; recorded).
| .mult, .tuple xs, v =>
(match asInt v with
| some n => tupleRepeat xs n
| Option.none =>
.exn (.typeError s!"can't multiply sequence by non-int of type '{v.typeName}'"))
| .mult, .ntuple _ _ xs, v =>
(match asInt v with
| some n => tupleRepeat xs n
| Option.none =>
.exn (.typeError s!"can't multiply sequence by non-int of type '{v.typeName}'"))
| .mult, v, .tuple xs =>
(match asInt v with
| some n => tupleRepeat xs n
| Option.none =>
.exn (.typeError s!"can't multiply sequence by non-int of type '{v.typeName}'"))
| .mult, v, .ntuple _ _ xs =>
(match asInt v with
| some n => tupleRepeat xs n
| Option.none =>
.exn (.typeError s!"can't multiply sequence by non-int of type '{v.typeName}'"))
| .mult, a, b =>
if (a.isSeq && (asInt b).isSome) || ((asInt a).isSome && b.isSeq) then
.unsupported
s!"sequence repetition ('{a.typeName}' * '{b.typeName}') is outside the v0 tier"
else
.exn (.typeError s!"unsupported operand type(s) for *: '{a.typeName}' and '{b.typeName}'")
| .mod, .str fmt, rhs => strFormat fmt rhs
| op, a, b =>
.exn (.typeError
s!"unsupported operand type(s) for {op.symbol}: '{a.typeName}' and '{b.typeName}'")
/-- Unary operator: `not` is truthiness negation (`Res`-valued through
`truthy` since H1); `-`, `+` and `~` need an int/bool operand and all
three DROP boolness the way CPython does (`-True == -1`, `+True == 1`,
`~True == -2` — `bool` has no `__neg__`/`__pos__`/`__invert__`, so the
int slots run); a `.ref` operand is refused loudly (its dunder lives in
the heap). `+` is the identity on an int and `~x` is `-x - 1`, which is
two's complement by definition, not a bit-level guess. -/
def evalUnaryOp (op : UnaryOp) (v : RVal) : Res RVal :=
match op with
| .not => do let b ← truthy v; return .bool (!b)
| .usub =>
match v with
| .ref _ =>
.unsupported "unary '-' on a heap object is outside the H1 tier (docs/memory-model.md)"
| v =>
match asInt v with
| some n => .ok (.int (-n))
| Option.none => .exn (.typeError s!"bad operand type for unary -: '{v.typeName}'")
| .uadd =>
match v with
| .ref _ =>
.unsupported "unary '+' on a heap object is outside the H1 tier (docs/memory-model.md)"
| v =>
match asInt v with
| some n => .ok (.int n)
| Option.none => .exn (.typeError s!"bad operand type for unary +: '{v.typeName}'")
| .invert =>
match v with
| .ref _ =>
.unsupported "unary '~' on a heap object is outside the H1 tier (docs/memory-model.md)"
| v =>
match asInt v with
| some n => .ok (.int (-n - 1))
| Option.none => .exn (.typeError s!"bad operand type for unary ~: '{v.typeName}'")
/-- First match wins (shadowing is by position in the list). Polymorphic in
the value type: runtime envs bind `RVal`, the G1 accumulator binds `Val`. -/
def Env.lookup : List (String × α) → String → Option α
| [], _ => Option.none
| (k, v) :: rest, name => if k == name then some v else Env.lookup rest name
/-- Replace an existing binding in place, else append at the end. -/
def Env.set : List (String × α) → String → α → List (String × α)
| [], name, v => [(name, v)]
| (k, w) :: rest, name, v =>
if k == name then (name, v) :: rest else (k, w) :: Env.set rest name v
/-- Remove the first binding of `name` (the one `Env.lookup` sees) — the
`del` statement's primitive (docs/memory-model.md §the del statement).
Structural recursion beside `lookup`/`set`; a missing name removes
nothing (the CALLERS decide the miss — the two arms decide it
differently, and neither reaches here on a miss). -/
def Env.remove : List (String × α) → String → List (String × α)
| [], _ => []
| (k, w) :: rest, name =>
if k == name then rest else (k, w) :: Env.remove rest name
/-- Fold `del`'s targets LEFT TO RIGHT over an env — the PARTIAL effect
(CPython really removes `x` before raising on `nosuch` in
`del x, nosuch`): the env after every successful removal, plus the first
missing name if any. Pure; both runtime arms dispatch on the pair. -/
def delNames : List (String × α) → List String → List (String × α) × Option String
| env, [] => (env, Option.none)
| env, n :: rest =>
match Env.lookup env n with
| some _ => delNames (Env.remove env n) rest
| Option.none => (env, some n)
/-- Constant literal → boundary value (G1 freeze side). -/
def Const.toVal : Const → Val
| .none => .none
| .bool b => .bool b
| .int n => .int n
| .str s => .str s
/-- Constant literal → runtime value (constants are scalars — no
allocation). -/
def Const.toRVal : Const → RVal
| .none => .none
| .bool b => .bool b
| .int n => .int n
| .str s => .str s
/-- `len(v)` for `str`/`listV`/`tuple` (str counts code points), else
`TypeError`; `len` of a `.ref` is a heap read (dicts) — loud until
H1-proper. -/
def lenVal : RVal → Res RVal
| .str s => .ok (.int s.length)
| .listV xs => .ok (.int xs.size)
| .tuple xs => .ok (.int xs.size)
| .ntuple _ _ xs => .ok (.int xs.size)
| .rangeV lo hi step => .ok (.int (rangeLen lo hi step))
| .ref _ =>
.unsupported "len() of a heap object lives in the heap (`heapLen` via `lenValH` decides it)"
| v => .exn (.typeError s!"object of type '{v.typeName}' has no len()")
/-- Insert `x` into an (ascending) list — the step function of `sortInts`.
Structural recursion on purpose: the kernel reduces it, which `#py_check` /
`py_check` / `py_vcgen`'s captured runs need. (Core's `List.mergeSort` is
well-founded recursion and does NOT kernel-reduce — verified on this
toolchain; `by rfl` on a concrete `mergeSort` run fails.) -/
def insertLe (x : Int) : List Int → List Int
| [] => [x]
| y :: ys => if x ≤ y then x :: y :: ys else y :: insertLe x ys
/-- Ascending insertion sort on `Int` — the value-level meaning of the
builtin `sorted` (tier: all-int lists only, see `sortedVal`). Stability
is vacuous at this type: `.int`s have no identity, so equal elements are
interchangeable. The proof layer bridges to Mathlib's `List.insertionSort`
(`sortInts_eq` in `Examples/python/bench_statistics/proof.lean`) to harvest
`Pairwise`/`Perm` lemmas; only the Mathlib-free `sortInts_length` lives
in-tree (Logic.lean), because symbolic execution needs it. -/
def sortInts : List Int → List Int
| [] => []