Repository navigation
Expand file tree
/
Copy pathDefinitions.lean
More file actions
5174 lines (4944 loc) · 285 KB
/
Copy pathDefinitions.lean
File metadata and controls
5174 lines (4944 loc) · 285 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
import Verified.Correct
import Verified.Instantiate
import Verified.Reflect.Lemmas
import Verified.Reflect.BoundPass
import Verified.Reflect.Modes
import Verified.Reflect.FoldLemmas
import Verified.Reflect.ListFoldLemmas
import Verified.Reflect.TreeLemmas
import Verified.Reflect.TreeNodeLemmas
import Verified.Reflect.NativeList
import Verified.Reflect.NativeTree
import Verified.Reflect.RecursiveLayout
import Verified.Reflect.TailBoundLemmas
import LeanExe.Encoding.RoundTrip
import LeanExe.Encoding.Completeness.Writes
/-! The reflector. `verified_compile p := [f, g, …]` reads the listed Lean definitions, writes
each as a source function, and proves its equation `denote (reflect f) = f` from the lemmas of
`Verified.Reflect.Lemmas`, composed term by term. It adds the program `p.program`, the meanings
`p.funs` of its functions with the proof `p.meaning` that they are, the module
`p.module := compile p.program`, in which the `k`-th definition is function `2 + k`, and for each
definition `f` the source function `p.f.func`, the equation `p.f.denote_eq`, and the theorem
`p.f.implements` that the module computes `f`, at the entry of `f` when its code takes the call
depth. A recursive definition is reflected from its unfolding equation, and its meaning
`p.f.meaning` is the definition at the inverses of the flattenings. `p.bytes` states that the
module's bytes decode to the module, which computes every listed definition.
The reflector is meta code and is not trusted: Lean's kernel checks every equation it builds, and
the theorem holds for the parameter modes that `Expr.paramChoice` chooses as for any others. A
definition's parameters and result are `UInt64`, `Bool`, `Float`, structures with a `Flat` instance
whose tuple is their fields, enumerations with a `Flat` instance to words, arrays of these, and
pairs, and structures whose `Flat` tuple holds arrays, which are represented as that tuple and split
as pairs are. Its body may also hold arrays of tuples, which have no `Represent` instance. A
structure's source value is its flattening `φ`, the source value of its `Flat` tuple, an array's is
the array of its elements' flattenings, and each equation states that the source expression means
`φ` of the Lean term, with `φ` the identity for the types without structures. The theorem follows
from the equation by `ImplementsA.transferAgree`, with proofs that Lean's instances agree with the
source instances along `φ`. Its body may use literals, its parameters, `let`, the word operations
`+`, `-`, `*`, `/`, `%`, `&&&`, `|||`, `^^^`, `<<<`, and `>>>`, the comparisons `==`, `!=`, `<`,
`≤`, `>`, `≥`, `=`, and `≠` as `Bool` values, `!`, `&&`, and `||`, `if` on a `Bool` or on a
comparison, also as `if h : c` with branches that do not use `h`, pairs built with `(a, b)` and
taken apart with `.1`, `.2`, or `match`, structures built with their constructor or `{ s with … }`
and taken apart with their fields or `match`, enumeration constructors, `Flat.flat` of enumerations,
`match` and comparisons on enumerations, Boolean equality and inequality, `LeanExe.loop`,
`LeanExe.repeatWhile`, whole-array `Array.foldl`, `#[]`, `xs.size.toUInt64`, `xs[i.toNat]!`,
`xs.set! i.toNat v`, `xs.push v`,
`xs ++ ys`, `LeanExe.build`, `LeanExe.insertAt xs i v`, `LeanExe.eraseAt xs i`, safe named
constants whose type holds no array, as their values, `setIfInBounds`, `insertIdxIfInBounds`,
`eraseIdxIfInBounds`, unfolded `@[inline]` helpers, calls of the listed definitions before it,
and, in a recursive definition, calls of itself. A definition
`f x := g T₁ … Tₖ x` that applies a listed definition `g` to constants `Tᵢ` of type `Array UInt64`
before its own parameters is a wrapper: the module holds the tables `Tᵢ` in data segments and
exports `f` as an entry that passes their addresses to `g`. -/
namespace Verified.Reflect
open Lean Meta Elab Command Term
initialize registerTraceClass `Verified.reflect
def elemOf? (type : Lean.Expr) : MetaM (Option Elem) := do
let type ← whnfR type
if type.isConstOf ``UInt64 then return some .word
if type.isConstOf ``Bool then return some .bool
if type.isConstOf ``Float then return some .float
if type.isConstOf ``Float32 then return some .float32
return none
def elemExpr : Elem → Lean.Expr
| .word => mkConst ``Elem.word
| .bool => mkConst ``Elem.bool
| .float => mkConst ``Elem.float
| .float32 => mkConst ``Elem.float32
| .prod a b => mkApp2 (mkConst ``Elem.prod) (elemExpr a) (elemExpr b)
def elemZero : Elem → MetaM Lean.Expr
| .word => pure (toExpr (0 : UInt64))
| .bool => pure (mkConst ``Bool.false)
| .float => mkAppM ``Float.ofBits #[toExpr (0 : UInt64)]
| .float32 => mkAppM ``Float32.ofBits #[toExpr (0 : UInt32)]
| .prod a b => do mkAppM ``Prod.mk #[← elemZero a, ← elemZero b]
def boolEqTerm (a b : Lean.Expr) : MetaM Lean.Expr := do
mkAppM ``ite #[← mkEq a (mkConst ``Bool.true), b, ← mkAppM ``not #[b]]
/-- The path along the steps `steps`, from the outside in, of a component of an element of type
`e`: `false` for the first part and `true` for the second. Also the component's type. -/
def pathExpr : Elem → List Bool → MetaM (Lean.Expr × Elem)
| e, [] => return (mkApp (mkConst ``Path.here) (elemExpr e), e)
| .prod a b, false :: rest => do
let (p, t) ← pathExpr a rest
return (mkApp4 (mkConst ``Path.fst) (elemExpr a) (elemExpr t) (elemExpr b) p, t)
| .prod a b, true :: rest => do
let (p, t) ← pathExpr b rest
return (mkApp4 (mkConst ``Path.snd) (elemExpr b) (elemExpr t) (elemExpr a) p, t)
| _, _ :: _ => throwError "verified_compile: a projection of an element that is not a tuple"
abbrev reflectedTreeShape (ctors : List (List TreeField)) (valid : shapeValid ctors = true) :
TreeShape :=
⟨ctors, valid⟩
/-- Record constructor `i` of a shape, with a proof that the kernel checks by evaluation. -/
abbrev reflectedRecord (shape : TreeShape) (i : Nat) (valid : decide (i < shape.records) = true) :
Fin shape.records :=
⟨i, of_decide_eq_true valid⟩
def trueRefl : Lean.Expr :=
mkApp2 (mkConst ``Eq.refl [Level.one]) (mkConst ``Bool) (mkConst ``Bool.true)
def treeShapeExpr (shape : TreeShape) : Lean.Expr :=
if shape = listShape then mkConst ``listShape else
mkApp2 (mkConst ``reflectedTreeShape) (toExpr shape.ctors) trueRefl
def recordExpr (shape : TreeShape) (r : Fin shape.records) : Lean.Expr :=
if shape = listShape then mkConst ``listCell else
mkApp3 (mkConst ``reflectedRecord) (treeShapeExpr shape) (mkNatLit r.val) trueRefl
def tyExpr : Ty → Lean.Expr
| .word => mkConst ``Ty.word
| .bool => mkConst ``Ty.bool
| .pair a b => mkApp2 (mkConst ``Ty.pair) (tyExpr a) (tyExpr b)
| .float => mkConst ``Ty.float
| .float32 => mkConst ``Ty.float32
| .elem e => mkApp (mkConst ``Ty.elem) (elemExpr e)
| .array e => mkApp (mkConst ``Ty.array) (elemExpr e)
| .bytes => mkConst ``Ty.bytes
| .tree shape => mkApp (mkConst ``Ty.tree) (treeShapeExpr shape)
| .treeHeader shape r => mkApp2 (mkConst ``Ty.treeHeader) (treeShapeExpr shape) (recordExpr shape r)
/-- How a Lean type is flattened into a source type: the source type, and the function `φ` from
the Lean type to the source type's meaning, `none` for the identity. A structure with a `Flat`
instance is the flattening of its `Flat` tuple, so nested structures are flattened in turn. -/
structure Shape where
ty : Ty
flat : Option Lean.Expr
/-- `φ e`, beta-reduced. -/
def Shape.apply (sh : Shape) (e : Lean.Expr) : Lean.Expr :=
match sh.flat with
| none => e
| some f => f.beta #[e]
/-- `φ` as a function from `type` to the source type's meaning, the identity when `flat` is
`none`. -/
def Shape.fn (sh : Shape) (type : Lean.Expr) : MetaM Lean.Expr := do
let f ← match sh.flat with
| some f => pure f
| none => withLocalDeclD `x type fun x => mkLambdaFVars #[x] x
mkExpectedTypeHint f (← mkArrow type (mkApp (mkConst ``Ty.denote) (tyExpr sh.ty)))
/-- The constructor and field names of a structure type other than `Prod`. -/
def structOf? (type : Lean.Expr) : MetaM (Option (ConstructorVal × Array Name)) := do
let type ← whnfR type
let .const n _ := type.getAppFn | return none
if n == ``Prod then return none
let env ← getEnv
unless isStructure env n do return none
let some (.ctorInfo ctor) := env.find? (getStructureCtor env n).name | return none
return some (ctor, getStructureFields env n)
/-- The tuple tree of a structure's `Flat` instance: `Flat.flat` of the structure built from fresh
variables, reduced down the tuple's pairs, has those variables at its leaves. Each leaf is the
index of a field, and a leaf is reached by steps `false` for a pair's first component and `true`
for its second. The command `command` rejects an instance whose leaves are not distinct fields. -/
partial def flatTree (command : String) (type β inst : Lean.Expr) (ctor : ConstructorVal) :
MetaM (List (Nat × List Bool)) := do
let type ← whnfR type
let ctorApp := mkAppN (mkConst ctor.name type.getAppFn.constLevels!) type.getAppArgs
forallBoundedTelescope (← inferType ctorApp) ctor.numFields fun ys _ => do
let t := mkApp4 (mkConst ``LeanExe.Pipeline.Flat.flat) type β inst (mkAppN ctorApp ys)
let rec descend (t ty : Lean.Expr) (steps : List Bool) : MetaM (List (Nat × List Bool)) := do
let ty ← whnfR ty
let t' ← whnf t
if let some i := ys.findIdx? (· == t') then return [(i, steps.reverse)]
if let (``Prod, #[a, b]) := ty.getAppFnArgs then
if let (``Prod.mk, #[_, _, x, y]) := t'.getAppFnArgs then
return (← descend x a (false :: steps)) ++ (← descend y b (true :: steps))
throwError "{command}: the `Flat` instance of {type} is not a tuple of its fields"
let leaves ← descend t β []
unless (leaves.map (·.1)).eraseDups.length == leaves.length do
throwError "{command}: the `Flat` instance of {type} repeats a field"
return leaves
/-- The name of a sum: an inductive type without parameters or indices that is neither recursive,
a structure, nor an enumeration. -/
def sumName? (type : Lean.Expr) : MetaM (Option Name) := do
let .const name _ ← whnfR type | return none
let some (.inductInfo info) := (← getEnv).find? name | return none
unless info.numParams == 0 && info.numIndices == 0 && !info.isRec &&
!isStructure (← getEnv) name do return none
if ← isEnumType name then return none
return some name
partial def shapeOf (type : Lean.Expr) : MetaM Shape := do
if let some e ← elemOf? type then return ⟨.elem e, none⟩
let type ← whnfR type
if type.isConstOf ``LeanExe.Bytes then return ⟨.bytes, none⟩
if let (``List, #[el]) := type.getAppFnArgs then
if (← whnfR el).isConstOf ``UInt64 then
return ⟨.tree listShape, some (mkConst ``Tree.ofList)⟩
if let some layout ← recursiveLayout? type then
let flatten := layout.decl `toTree
if (← getEnv).contains flatten then return ⟨.tree layout.shape, some (mkConst flatten)⟩
if let (``Prod, #[a, b]) := type.getAppFnArgs then
let sa ← shapeOf a
let sb ← shapeOf b
let ty := match sa.ty, sb.ty with
| .elem ea, .elem eb => Ty.elem (.prod ea eb)
| ta, tb => .pair ta tb
if sa.flat.isNone && sb.flat.isNone then return ⟨ty, none⟩
let f ← withLocalDeclD `p type fun p => do
mkLambdaFVars #[p] (← mkAppM ``Prod.mk
#[sa.apply (← mkAppM ``Prod.fst #[p]), sb.apply (← mkAppM ``Prod.snd #[p])])
return ⟨ty, some f⟩
if let (``Array, #[el]) := type.getAppFnArgs then
let se ← shapeOf el
let .elem e := se.ty | throwError "verified_compile: an array holds elements, not {el}"
if se.flat.isNone then return ⟨.array e, none⟩
let φ ← se.fn el
let f ← withLocalDeclD `xs type fun xs => do mkLambdaFVars #[xs] (← mkAppM ``Array.map #[φ, xs])
return ⟨.array e, some f⟩
if let some (β, inst) ← flatInstance? type then
let sβ ← shapeOf β
-- A sum whose tuple holds heap values is represented as its tuple, and `sumLayout` checks
-- the tuple where a constructor or a match needs it.
if !(sβ.ty matches .elem _) && (← sumName? type).isNone then
-- A structure that holds arrays is split as its tuple, which must be a pair of all its
-- fields.
let some (ctor, _) ← structOf? type
| throwError "verified_compile: {type} holds arrays and is not a structure"
let (``Prod, _) := (← whnfR β).getAppFnArgs
| throwError "verified_compile: the `Flat` instance of {type} holds arrays and is not a \
pair"
unless (← flatTree "verified_compile" type β inst ctor).length == ctor.numFields do
throwError "verified_compile: the `Flat` instance of {type} does not hold all its fields"
let f ← withLocalDeclD `x type fun x => do
mkLambdaFVars #[x] (sβ.apply (mkApp4 (mkConst ``LeanExe.Pipeline.Flat.flat) type β inst x))
return ⟨sβ.ty, some f⟩
throwError "verified_compile: the type {type} is not UInt64, Bool, Float, Float32, Bytes, a structure with a \
`Flat` instance, an array, or a pair"
def tyOf (type : Lean.Expr) : MetaM Ty := return (← shapeOf type).ty
/-- Whether `type` is a sum whose `Flat` tuple holds heap values. A variable of such a sum stays
whole, since the sum cannot be rebuilt from its tuple, and a match destructures it. -/
def heapSum? (type : Lean.Expr) : MetaM Bool := do
if (← sumName? type).isNone then return false
return !((← shapeOf type).ty matches .elem _)
/-- The steps to field `i` of a structure value in its flattening, if the type is a structure
with a `Flat` instance. -/
def fieldPath? (type : Lean.Expr) (i : Nat) : MetaM (Option (List Bool)) := do
let some (ctor, _) ← structOf? type | return none
let some (β, inst) ← flatInstance? type | return none
let tree ← flatTree "verified_compile" type β inst ctor
return (tree.find? (·.1 == i)).map (·.2)
/-- Field `i` and the structure value `p` of a structure projection `e`. -/
def structProj? (e : Lean.Expr) : MetaM (Option (Nat × Lean.Expr)) := do
if let .proj _ i p := e then return some (i, p)
let .const fn _ := e.getAppFn | return none
let some info ← getProjectionFnInfo? fn | return none
if info.fromClass then return none
let args := e.getAppArgs
unless args.size == info.numParams + 1 do return none
return some (info.i, args[info.numParams]!)
/-- The source value of a Lean term: its flattening. -/
def flatValue (e : Lean.Expr) : MetaM Lean.Expr := return (← shapeOf (← inferType e)).apply e
def listExpr (α : Lean.Expr) : List Lean.Expr → Lean.Expr
| [] => mkApp (mkConst ``List.nil [Level.zero]) α
| x :: xs => mkApp3 (mkConst ``List.cons [Level.zero]) α x (listExpr α xs)
def ctxExpr (Γ : List Ty) : Lean.Expr := listExpr (mkConst ``Ty) (Γ.map tyExpr)
def finiteFn (type : Lean.Expr) (values : List Lean.Expr) : MetaM Lean.Expr :=
mkAppOptM ``List.get #[some type, some (listExpr type values)]
def finiteIndex (n i : Nat) : MetaM Lean.Expr := do
mkAppM ``Fin.mk #[mkNatLit i, ← mkDecideProof (← mkLt (mkNatLit i) (mkNatLit n))]
partial def finiteForall (n : Nat) (P : Lean.Expr) (prove : Lean.Expr → MetaM Lean.Expr) :
MetaM Lean.Expr := do
if n == 0 then
withLocalDeclD `i (mkApp (mkConst ``Fin) (mkNatLit 0)) fun i => do
mkLambdaFVars #[i] (mkApp2 (mkConst ``Fin.elim0 [Level.zero]) (mkApp P i) i)
else
let first ← prove (← finiteIndex n 0)
let rest ← withLocalDeclD `i (mkApp (mkConst ``Fin) (mkNatLit (n - 1))) fun i => do
let shifted ← mkLambdaFVars #[i] (mkApp P (← mkAppM ``Fin.succ #[i]))
finiteForall (n - 1) shifted fun j => do prove (← mkAppM ``Fin.succ #[j])
mkAppOptM ``Fin.cases #[some (mkNatLit (n - 1)), some P, some first, some rest]
/-- The context `t :: Γ` for the expression `Γ` of a context, which it shares. -/
def consCtx (t : Ty) (Γ : Lean.Expr) : Lean.Expr :=
mkApp3 (mkConst ``List.cons [Level.zero]) (mkConst ``Ty) (tyExpr t) Γ
def modeExpr : Mode → Lean.Expr
| .borrowed => mkConst ``Mode.borrowed
| .owned => mkConst ``Mode.owned
def modesExpr (modes : List Mode) : Lean.Expr := listExpr (mkConst ``Mode) (modes.map modeExpr)
def sigExpr (g : Sig) : Lean.Expr :=
mkApp5 (mkConst ``Sig.mk) (ctxExpr g.params) (tyExpr g.result) (toExpr g.aborts)
(modesExpr g.modes) (toExpr g.depth)
/-- The allocation bound `p.g.bound` of a listed definition; when its code takes the call depth,
its frames condition `p.g.fits`, both of which then take the frames available before the
arguments; and the name of `p.g.bound_eq` when the equation gives a numeral, which a caller's bound
then shows. -/
structure CalleeBound where
bound : Name
fits? : Option Name := none
numeralEq : Option Name := none
/-- For a function with a paid parameter, whose entry `bound` is `base.cost`, `base.bound`: the
credits plus the entry. -/
credited? : Option Name := none
deriving Inhabited
/-- A listed definition that a later one may call: its name, its signature, its equation
`∀ args, Func.denote … = name args`, and its bound. -/
structure Callee where
name : Name
sig : Sig
denoteEq : Name
bound : CalleeBound
/-- The bounds and frames conditions of the functions that a definition's body may call, with
`fuel` frames available to the calls: those of the functions `prog` before the definition, with
signatures `sigs` and meanings `funs`, and, in a recursive definition, the definition's own first,
its signature with its bound and frames condition at `fuel`. -/
structure Tables where
sigs : Lean.Expr
prog : Lean.Expr
funs : Lean.Expr
fuel : Lean.Expr
self : Option (Lean.Expr × Lean.Expr × Lean.Expr) := none
/-- In a recursive definition, the flags of the definition and of the functions before it. -/
selfFlags : Option Lean.Expr := none
/-- `Prog.boundsAt` or `Prog.fitsAt` of the functions before the definition, at `fuel`. -/
def Tables.rest (t : Tables) (fits : Bool) : Lean.Expr :=
mkAppN (mkConst (if fits then ``Prog.fitsAt else ``Prog.boundsAt))
#[t.sigs, t.prog, t.funs, t.fuel]
/-- The flags of the functions that the body may call. -/
def Tables.flags (t : Tables) : Lean.Expr :=
t.selfFlags.getD (mkApp2 (mkConst ``Prog.flags) t.sigs t.prog)
/-- The bounds, or the frames conditions, of the functions that the body may call. -/
def Tables.table (t : Tables) (fits : Bool) : Lean.Expr :=
match t.self with
| none => t.rest fits
| some (g, b, fi) =>
mkAppN (mkConst (if fits then ``Fits.cons else ``Bounds.cons))
#[t.sigs, g, if fits then fi else b, t.rest fits]
/-- The functions an expression may call, the Lean functions they mean, the definitions behind
them, variable 0 of `sigs` first, the variables in scope with their types, variable 0 first, the
environment of their values, and the bounds and frames conditions of the functions. -/
structure Ctx where
/-- The program's name, under which the reflector adds the theorems it shares between
definitions. -/
base : Name
sigs : Lean.Expr
funs : Lean.Expr
callees : List Callee
vars : List (Lean.Expr × Ty)
env : Lean.Expr
ctx : Lean.Expr
tables : Tables
/-- `Expr.denote funs e env`. -/
def denoteExpr (c : Ctx) (e : Lean.Expr) : MetaM Lean.Expr :=
mkAppM ``Expr.denote #[c.funs, e, c.env]
/-- The proof by `rfl` that `e` means `lean`. -/
def rflProof (c : Ctx) (e lean : Lean.Expr) : MetaM Lean.Expr := do
mkExpectedTypeHint (← mkEqRefl lean) (← mkEq (← denoteExpr c e) lean)
def binOp? : Name → Option Lean.Expr
| ``HAdd.hAdd => some (mkConst ``BinOp.add)
| ``HSub.hSub => some (mkConst ``BinOp.sub)
| ``HMul.hMul => some (mkConst ``BinOp.mul)
| ``HDiv.hDiv => some (mkConst ``BinOp.div)
| ``HMod.hMod => some (mkConst ``BinOp.rem)
| ``HAnd.hAnd => some (mkConst ``BinOp.and)
| ``HOr.hOr => some (mkConst ``BinOp.or)
| ``HXor.hXor => some (mkConst ``BinOp.xor)
| ``HShiftLeft.hShiftLeft => some (mkConst ``BinOp.shl)
| ``HShiftRight.hShiftRight => some (mkConst ``BinOp.shr)
| _ => none
def fbinOp? : Name → Option Lean.Expr
| ``HAdd.hAdd => some (mkConst ``FBinOp.add)
| ``HSub.hSub => some (mkConst ``FBinOp.sub)
| ``HMul.hMul => some (mkConst ``FBinOp.mul)
| ``HDiv.hDiv => some (mkConst ``FBinOp.div)
| _ => none
def isFloat (α : Lean.Expr) : MetaM Bool := do
let α ← whnfR α
return α.isConstOf ``Float || α.isConstOf ``Float32
/-- A comparison of floats as a `Prop`: its operation and its operands, with `>` and `≥` as `<`
and `≤` on swapped operands. `=` and `≠` on floats compare bit patterns, which `==` and `!=` do
not, and the reflector rejects them. -/
def fcomparison? (p : Lean.Expr) : MetaM (Option (FCmpOp × Lean.Expr × Lean.Expr)) := do
match p.consumeMData.getAppFnArgs with
| (``LT.lt, #[α, _, a, b]) => if ← isFloat α then return some (.lt, a, b) else return none
| (``LE.le, #[α, _, a, b]) => if ← isFloat α then return some (.le, a, b) else return none
| (``GT.gt, #[α, _, a, b]) => if ← isFloat α then return some (.lt, b, a) else return none
| (``GE.ge, #[α, _, a, b]) => if ← isFloat α then return some (.le, b, a) else return none
| (``Eq, #[α, _, _]) | (``Ne, #[α, _, _]) =>
if ← isFloat α then
throwError "verified_compile: = and ≠ on {α} compare bit patterns; use == and !="
return none
| _ => return none
def fcmpExpr : FCmpOp → Lean.Expr
| .lt => mkConst ``FCmpOp.lt
| .le => mkConst ``FCmpOp.le
| .eq => mkConst ``FCmpOp.eq
/-- The value of a word literal. -/
def wordLit? (e : Lean.Expr) : MetaM (Option UInt64) := do
let (``OfNat.ofNat, #[α, n, _]) := e.consumeMData.getAppFnArgs | return none
unless (← whnfR α).isConstOf ``UInt64 do return none
return (natOf (← instantiateMVars n)).map UInt64.ofNat
def bytesLit? (e : Lean.Expr) : MetaM (Option (List UInt8)) := do
if e.hasFVar || e.hasLooseBVars then return none
unless (← whnfR (← inferType e)).isConstOf ``LeanExe.Bytes do return none
let (``LeanExe.Bytes.mk, #[data]) := (← whnfR e).getAppFnArgs | return none
let (``ByteArray.mk, #[data]) := (← whnfR data).getAppFnArgs | return none
return (← getArrayLitOf? data getUInt8Value?).map Array.toList
/-- The bit pattern of a float literal: a scientific or natural literal, `Float.ofBits` or
`UInt64.toFloat` of a word literal, or the negation of a float literal. Lean's model has one
NaN, so `Float.ofBits` and the negation give the canonical NaN for a NaN. The kernel checks the
bits. -/
partial def floatLit? (e : Lean.Expr) : MetaM (Option UInt64) := do
let canonical (w : UInt64) := if Wasm.IEEE64.isNaN w then Wasm.IEEE64.canonicalNaN else w
match e.consumeMData.getAppFnArgs with
| (``OfScientific.ofScientific, #[_, _, m, sgn, ex]) =>
let some m := natOf (← instantiateMVars m) | return none
let some ex := natOf (← instantiateMVars ex) | return none
if sgn.isConstOf ``Bool.true then return some (Float.ofScientific m true ex).toBits
if sgn.isConstOf ``Bool.false then return some (Float.ofScientific m false ex).toBits
return none
| (``OfNat.ofNat, #[_, n, _]) =>
let some n := natOf (← instantiateMVars n) | return none
return some (Float.ofNat n).toBits
| (``Float.ofBits, #[w]) => return (← wordLit? w).map canonical
| (``UInt64.toFloat, #[w]) => return (← wordLit? w).map Wasm.IEEE64.convertI64U
| (``Neg.neg, #[_, _, x]) =>
return (← floatLit? x).map fun b => canonical (b ^^^ 0x8000000000000000)
| _ => return none
def word32Lit? (e : Lean.Expr) : MetaM (Option UInt32) := do
let (``OfNat.ofNat, #[α, n, _]) := e.consumeMData.getAppFnArgs | return none
unless (← whnfR α).isConstOf ``UInt32 do return none
return (natOf (← instantiateMVars n)).map UInt32.ofNat
partial def float32Lit? (e : Lean.Expr) : MetaM (Option UInt32) := do
let canonical (w : UInt32) := if Wasm.IEEE32.isNaN w then Wasm.IEEE32.canonicalNaN else w
match e.consumeMData.getAppFnArgs with
| (``OfScientific.ofScientific, #[_, _, m, sgn, ex]) =>
let some m := natOf (← instantiateMVars m) | return none
let some ex := natOf (← instantiateMVars ex) | return none
if sgn.isConstOf ``Bool.true then return some (Float32.ofScientific m true ex).toBits
if sgn.isConstOf ``Bool.false then return some (Float32.ofScientific m false ex).toBits
return none
| (``OfNat.ofNat, #[_, n, _]) =>
let some n := natOf (← instantiateMVars n) | return none
return some (Float32.ofNat n).toBits
| (``Float32.ofBits, #[w]) => return (← word32Lit? w).map canonical
| (``UInt64.toFloat32, #[w]) => return (← wordLit? w).map Wasm.IEEE32.convertI64U
| (``Neg.neg, #[_, _, x]) =>
return (← float32Lit? x).map fun b => canonical (b ^^^ 0x80000000)
| _ => return none
/-- A comparison of words as a `Prop`: its operation and its operands, with `>` and `≥` as `<`
and `≤` on swapped operands. -/
def comparison? (p : Lean.Expr) : MetaM (Option (CmpOp × Lean.Expr × Lean.Expr)) := do
let p := p.consumeMData
let isWord (α : Lean.Expr) : MetaM Bool := return (← whnfR α).isConstOf ``UInt64
match p.getAppFnArgs with
| (``LT.lt, #[α, _, a, b]) => if ← isWord α then return some (.lt, a, b) else return none
| (``LE.le, #[α, _, a, b]) => if ← isWord α then return some (.le, a, b) else return none
| (``GT.gt, #[α, _, a, b]) => if ← isWord α then return some (.lt, b, a) else return none
| (``GE.ge, #[α, _, a, b]) => if ← isWord α then return some (.le, b, a) else return none
| (``Eq, #[α, a, b]) => if ← isWord α then return some (.eq, a, b) else return none
| (``Ne, #[α, a, b]) => if ← isWord α then return some (.ne, a, b) else return none
| _ => return none
def cmpExpr : CmpOp → Lean.Expr
| .eq => mkConst ``CmpOp.eq
| .ne => mkConst ``CmpOp.ne
| .lt => mkConst ``CmpOp.lt
| .le => mkConst ``CmpOp.le
def iteLemma : CmpOp → Name
| .eq => ``ite_eqP_eq
| .ne => ``ite_ne_eq
| .lt => ``ite_lt_eq
| .le => ``ite_le_eq
/-- The context of the variables `vars` and `Env.cons v₀ (… (Env.cons vₙ Env.nil))`, with each
context built once and shared by the longer ones. -/
def ctxEnvExpr : List (Lean.Expr × Ty) → MetaM (Lean.Expr × Lean.Expr)
| [] => return (ctxExpr [], mkConst ``Env.nil)
| (x, t) :: rest => do
let (ctx, env) ← ctxEnvExpr rest
return (consCtx t ctx,
← mkAppOptM ``Env.cons #[some ctx, some (tyExpr t), some (← flatValue x), some env])
/-- `Env.cons v₀ (… (Env.cons vₙ Env.nil))` for the variables `vars`. -/
def envExpr (vars : List (Lean.Expr × Ty)) : MetaM Lean.Expr :=
return (← ctxEnvExpr vars).2
/-- The word family of record constructor `r` with the values `values` of their elements: for a
shape whose fields are words and children, the list of the words, and otherwise
`TreeShape.wordsOf`, which states each word's element. -/
def wordFamily (shapeValue : TreeShape) (r : Fin shapeValue.records)
(values : List (Elem × Lean.Expr)) : MetaM Lean.Expr := do
let shape := treeShapeExpr shapeValue
let record := recordExpr shapeValue r
if shapeValue.allWords then
return ← mkExpectedTypeHint (← finiteFn (mkConst ``UInt64) (values.map (·.2)))
(← mkArrow (mkApp (mkConst ``Fin) (← mkAppM ``TreeShape.words #[shape, record]))
(mkConst ``UInt64))
let sigma := mkApp2 (mkConst ``Sigma [.zero, .zero]) (mkConst ``Elem) (mkConst ``Elem.denote)
let entries := values.map fun (e, v) =>
mkApp4 (mkConst ``Sigma.mk [.zero, .zero]) (mkConst ``Elem) (mkConst ``Elem.denote)
(toExpr e) v
return mkApp3 (mkConst ``TreeShape.wordsOf) shape record (listExpr sigma entries)
/-- The family of the word expressions `exprs` of a construction of record constructor `r`, of
the elements of the fields, in the form of `wordFamily`. -/
def exprFamily (c : Ctx) (shapeValue : TreeShape) (r : Fin shapeValue.records)
(exprs : List (Elem × Lean.Expr)) : MetaM Lean.Expr := do
let shape := treeShapeExpr shapeValue
let record := recordExpr shapeValue r
let sourceType (t : Ty) := mkApp3 (mkConst ``Expr) c.sigs c.ctx (tyExpr t)
if shapeValue.allWords then
-- The type that `Expr.treeNode` states, whose word types reduce to `Ty.word`.
let fin := mkApp (mkConst ``Fin) (← mkAppM ``TreeShape.words #[shape, record])
let type ← withLocalDeclD `i fin fun i => do
mkForallFVars #[i] (mkApp3 (mkConst ``Expr) c.sigs c.ctx
(← mkAppM ``TreeShape.wordTy #[shape, record, i]))
return ← mkExpectedTypeHint (← finiteFn (sourceType .word) (exprs.map (·.2))) type
let family ← withLocalDeclD `e (mkConst ``Elem) fun e => do
mkLambdaFVars #[e] (mkApp3 (mkConst ``Expr) c.sigs c.ctx (mkApp (mkConst ``Ty.elem) e))
let sigma := mkApp2 (mkConst ``Sigma [.zero, .zero]) (mkConst ``Elem) family
let entries := exprs.map fun (e, x) =>
mkApp4 (mkConst ``Sigma.mk [.zero, .zero]) (mkConst ``Elem) family (toExpr e) x
return mkAppN (mkConst ``TreeShape.exprsOf) #[c.sigs, c.ctx, shape, record,
listExpr sigma entries]
/-- `noFields` over the index type `Fin count`, which is empty, of the motive `motive`. -/
def emptyFamily (count motive : Lean.Expr) : MetaM Lean.Expr := do
mkAppOptM ``noFields
#[some count, some (← mkDecideProof (← mkEq count (mkNatLit 0))), some motive]
/-- The array family of record constructor `r` with the arrays `values` of their elements:
`TreeShape.arraysOf`, or `noFields` for a record constructor without array fields. -/
def arrayFamily (shapeValue : TreeShape) (r : Fin shapeValue.records)
(values : List (Elem × Lean.Expr)) : MetaM Lean.Expr := do
let shape := treeShapeExpr shapeValue
let record := recordExpr shapeValue r
let arrayOf (e : Lean.Expr) : Lean.Expr :=
mkApp (mkConst ``Array [.zero]) (mkApp (mkConst ``Elem.denote) e)
if values.isEmpty then
let count ← mkAppM ``TreeShape.arrays #[shape, record]
let motive ← withLocalDeclD `i (mkApp (mkConst ``Fin) count) fun i => do
mkLambdaFVars #[i] (arrayOf (← mkAppM ``TreeShape.arrayElem #[shape, record, i]))
return ← emptyFamily count motive
let family ← withLocalDeclD `e (mkConst ``Elem) fun e => mkLambdaFVars #[e] (arrayOf e)
let sigma := mkApp2 (mkConst ``Sigma [.zero, .zero]) (mkConst ``Elem) family
let entries := values.map fun (e, v) =>
mkApp4 (mkConst ``Sigma.mk [.zero, .zero]) (mkConst ``Elem) family (toExpr e) v
return mkApp3 (mkConst ``TreeShape.arraysOf) shape record (listExpr sigma entries)
/-- The buffer family of record constructor `r` with the buffers `values`, or `noFields` for a
record constructor without buffer fields. -/
def bufferFamily (shapeValue : TreeShape) (r : Fin shapeValue.records)
(values : List Lean.Expr) : MetaM Lean.Expr := do
let count ← mkAppM ``TreeShape.buffers #[treeShapeExpr shapeValue, recordExpr shapeValue r]
if values.isEmpty then
return ← emptyFamily count (← withLocalDeclD `i (mkApp (mkConst ``Fin) count) fun i =>
mkLambdaFVars #[i] (mkConst ``LeanExe.Bytes))
mkExpectedTypeHint (← finiteFn (mkConst ``LeanExe.Bytes) values)
(← mkArrow (mkApp (mkConst ``Fin) count) (mkConst ``LeanExe.Bytes))
/-- The family of the array expressions `exprs` of a construction of record constructor `r`, of
the elements of the fields, in the form of `arrayFamily`. -/
def arrayExprFamily (c : Ctx) (shapeValue : TreeShape) (r : Fin shapeValue.records)
(exprs : List (Elem × Lean.Expr)) : MetaM Lean.Expr := do
let shape := treeShapeExpr shapeValue
let record := recordExpr shapeValue r
if exprs.isEmpty then
let count ← mkAppM ``TreeShape.arrays #[shape, record]
let motive ← withLocalDeclD `i (mkApp (mkConst ``Fin) count) fun i => do
mkLambdaFVars #[i] (mkApp3 (mkConst ``Expr) c.sigs c.ctx
(← mkAppM ``TreeShape.arrayTy #[shape, record, i]))
return ← emptyFamily count motive
let family ← withLocalDeclD `e (mkConst ``Elem) fun e => do
mkLambdaFVars #[e] (mkApp3 (mkConst ``Expr) c.sigs c.ctx (mkApp (mkConst ``Ty.array) e))
let sigma := mkApp2 (mkConst ``Sigma [.zero, .zero]) (mkConst ``Elem) family
let entries := exprs.map fun (e, x) =>
mkApp4 (mkConst ``Sigma.mk [.zero, .zero]) (mkConst ``Elem) family (toExpr e) x
return mkAppN (mkConst ``TreeShape.arrayExprsOf) #[c.sigs, c.ctx, shape, record,
listExpr sigma entries]
/-- The family of the buffer expressions `exprs` of a construction of record constructor `r`, or
`noFields` for a record constructor without buffer fields. -/
def bufferExprFamily (c : Ctx) (shapeValue : TreeShape) (r : Fin shapeValue.records)
(exprs : List Lean.Expr) : MetaM Lean.Expr := do
let count ← mkAppM ``TreeShape.buffers #[treeShapeExpr shapeValue, recordExpr shapeValue r]
let exprType := mkApp3 (mkConst ``Expr) c.sigs c.ctx (mkConst ``Ty.bytes)
if exprs.isEmpty then
return ← emptyFamily count (← withLocalDeclD `i (mkApp (mkConst ``Fin) count) fun i =>
mkLambdaFVars #[i] exprType)
mkExpectedTypeHint (← finiteFn exprType exprs)
(← mkArrow (mkApp (mkConst ``Fin) count) exprType)
/-- The words of a field `x` of the kind `kind`, each with its element: the field itself for a
word field, and the leaves of its flattening for a flat field. -/
def nativeWords (x : Lean.Expr) : NativeField → MetaM (List (Elem × Lean.Expr))
| .child | .array _ | .bytes => pure []
| .leaf e => pure [(e, x)]
| .flat _ leaves => leaves.mapM fun (e, segments) => return (e, ← leafTerm x segments)
/-- The component of the flattening of `x` along `steps`: a pair takes a step, and a value of a
type with a `Flat` instance is its tuple, down to a word, a `Bool`, a float, or a pair. At a leaf
it is the leaf's term. -/
partial def componentTerm (x : Lean.Expr) (steps : List Bool) : MetaM Lean.Expr := do
let type ← withReducible (whnf (← inferType x))
if (fieldElem? type).isSome then return x
if let (``Prod, #[_, _]) := type.getAppFnArgs then
let step :: rest := steps | return x
return ← componentTerm (← mkAppM (if step then ``Prod.snd else ``Prod.fst) #[x]) rest
if (← flatInstance? type).isNone then return x
componentTerm (← flatTerm x) steps
/-- Runs `k` with the variables of a match's branch on record constructor `r`: the header, then
each word, then each child, then each array, then each buffer. The fields `natives` are the
constructor's fields with their types.
A flat field is one Lean variable, and the branch holds a variable for each leaf of its tuple,
keyed in the context by the leaf's projection of the field. -/
def withTreeCaseFields {α : Type} (c : Ctx) (shapeValue : TreeShape)
(r : Fin shapeValue.records) (natives : List (Lean.Expr × NativeField))
(k : Ctx → Array Lean.Expr → MetaM α) : MetaM α := do
let shape := treeShapeExpr shapeValue
let record := recordExpr shapeValue r
let ctx ← mkAppM ``TreeShape.context #[shape, record, c.ctx]
let marker ← mkAppOptM ``TreeHeader.unit #[some shape, some record]
let decls := natives.toArray.mapIdx fun i (type, _) => (Name.mkSimple s!"field{i}", type)
let rec bindFields (decls : List (Name × Lean.Expr)) (fields : Array Lean.Expr)
(body : Array Lean.Expr → MetaM α) : MetaM α :=
match decls with
| [] => body fields
| (name, type) :: rest =>
withLocalDeclD name type fun field => bindFields rest (fields.push field) body
bindFields decls.toList #[] fun fields => do
let values := fields.toList.zip (natives.map (·.2))
let words := (← values.mapM fun (x, kind) => do
return (← nativeWords x kind).map fun (e, w) => (w, e)).flatten
let children := values.filterMap fun (x, kind) =>
if kind matches .child then some x else none
let wordFn ← wordFamily shapeValue r (← words.mapM fun (w, e) => do
return (e, ← flatValue w))
let childFn ← mkExpectedTypeHint
(← finiteFn (mkApp (mkConst ``Tree) shape) (← children.mapM flatValue))
(← mkArrow (mkApp (mkConst ``Fin) (← mkAppM ``TreeShape.children #[shape, record]))
(mkApp (mkConst ``Tree) shape))
let arrays := values.filterMap fun (x, kind) => match kind with
| .array e => some (x, e)
| _ => none
let arrayFn ← arrayFamily shapeValue r (← arrays.mapM fun (x, e) => do
return (e, ← flatValue x))
let buffers := values.filterMap fun (x, kind) =>
if kind matches .bytes then some x else none
let bufferFn ← bufferFamily shapeValue r (← buffers.mapM flatValue)
let env ← mkAppM ``Env.treeFields
#[shape, record, wordFn, arrayFn, bufferFn, childFn, c.env]
let vars := [(marker, .treeHeader shapeValue r)] ++
words.map (fun (w, e) => (w, Ty.elem e)) ++ children.map (·, Ty.tree shapeValue) ++
arrays.map (fun (x, e) => (x, Ty.array e)) ++ buffers.map (·, Ty.bytes) ++ c.vars
let inner := { c with ctx, env, vars }
k inner fields
def withListCaseFields {α : Type} (c : Ctx) (xs : Lean.Expr)
(k : Ctx → Lean.Expr → Lean.Expr → MetaM α) : MetaM α := do
withTreeCaseFields c listShape listCell
[(mkConst ``UInt64, .leaf .word), (← inferType xs, .child)]
fun inner fields => k inner fields[0]! fields[1]!
def withRecursiveCaseFields {α : Type} (c : Ctx) (layout : RecursiveLayout)
(r : Fin layout.shape.records) (k : Ctx → Array Lean.Expr → MetaM α) : MetaM α :=
withTreeCaseFields c layout.shape r ((layout.recordCtor r).2.map fun
| .child => (mkConst layout.name, .child)
| .leaf e => (elemType e, .leaf e)
| .flat type leaves => (type, .flat type leaves)
| .array e => (mkApp (mkConst ``Array [.zero]) (elemType e), .array e)
| .bytes => (mkConst ``LeanExe.Bytes, .bytes)) k
/-- `e` with each projection of a pair `(a, b)` or of a structure's constructor at its head
replaced by the component, and each pair `(y.1, y.2)` of the components of `y` replaced by `y`,
from the inside out. Each step is a reduction or eta for pairs, so the result is equal to `e` by
`rfl`. -/
partial def projReduce (e : Lean.Expr) : MetaM Lean.Expr := do
let e := e.consumeMData.headBeta
match e.getAppFnArgs with
| (``Prod.fst, #[_, _, p]) => match (← projReduce p).getAppFnArgs with
| (``Prod.mk, #[_, _, a, _]) => projReduce a
| _ => return e
| (``Prod.snd, #[_, _, p]) => match (← projReduce p).getAppFnArgs with
| (``Prod.mk, #[_, _, _, b]) => projReduce b
| _ => return e
| (``Prod.mk, #[α, β, a, b]) =>
let a ← projReduce a
let b ← projReduce b
if let (``Prod.fst, #[_, _, y]) := a.getAppFnArgs then
if let (``Prod.snd, #[_, _, y']) := b.getAppFnArgs then
if y == y' then return y
return mkApp4 e.getAppFn α β a b
| _ =>
let some (i, p) ← structProj? e | return e
let p ← projReduce p
let .const k _ := p.getAppFn | return e
let some (.ctorInfo ctor) := (← getEnv).find? k | return e
unless p.getAppNumArgs == ctor.numParams + ctor.numFields do return e
projReduce (p.getArg! (ctor.numParams + i))
/-- The `Flat` tuple of the fields of `e`, an application of a structure's constructor, built
along the tuple tree of its instance. -/
partial def ctorTuple? (e : Lean.Expr) : MetaM (Option Lean.Expr) := do
let .const ctorName _ := e.getAppFn | return none
let some (.ctorInfo ctor) := (← getEnv).find? ctorName | return none
let type ← inferType e
let some (ctor', _) ← structOf? type | return none
unless ctor'.name == ctor.name do return none
let args := e.getAppArgs
unless args.size == ctor.numParams + ctor.numFields do return none
let some (β, inst) ← flatInstance? type | return none
let tree ← flatTree "verified_compile" type β inst ctor
let fields := args.extract ctor.numParams args.size
let rec build (pre : List Bool) (ty : Lean.Expr) : MetaM Lean.Expr := do
if let some (i, _) := tree.find? (·.2 == pre.reverse) then return fields[i]!
let ty ← whnfR ty
let (``Prod, #[a, b]) := ty.getAppFnArgs
| throwError "verified_compile: the `Flat` instance of {type} is not a tuple of its fields"
mkAppM ``Prod.mk #[← build (false :: pre) a, ← build (true :: pre) b]
return some (← build [] β)
/-- The leaf with segments `segments` of a value whose tuple is `tuple`, with the tuple of each
structure's constructor in place of its `Flat.flat`, so that the reflector reads the constructor's
fields. -/
partial def tupleLeaf (tuple : Lean.Expr) : List (List Bool) → MetaM Lean.Expr
| [] => pure tuple
| [steps] => do projReduce (← stepsTerm tuple steps)
| steps :: rest => do
let t ← projReduce (← stepsTerm tuple steps)
tupleLeaf (← match ← ctorTuple? t with
| some u => pure u
| none => flatTerm t) rest
/-- Whether a Lean term reflects to a place: a variable, a pair of places, or a structure's
constructor whose tuple of fields is a place, as `reflectStruct?` reflects it. -/
partial def isPlace (e : Lean.Expr) : MetaM Bool := do
let e ← projReduce e
if e.isFVar then return true
if let (``Prod.mk, #[_, _, a, b]) := e.getAppFnArgs then
return (← isPlace a) && (← isPlace b)
if let some tuple ← ctorTuple? e then return ← isPlace tuple
return false
/-- `fn args`, with each argument that `bind` marks bound by a `let` around the application, in
order. The result is equal to `fn args` by `zeta`. -/
def bindArgs (fn : Lean.Expr) : List Lean.Expr → List Bool → Array Lean.Expr → Array Lean.Expr →
MetaM Lean.Expr
| [], _, newArgs, fvars => mkLetFVars fvars (mkAppN fn newArgs)
| a :: as, b :: bs, newArgs, fvars => do
if b then
withLetDecl `a (← inferType a) a fun x => bindArgs fn as bs (newArgs.push x) (fvars.push x)
else bindArgs fn as bs (newArgs.push a) fvars
| a :: as, [], newArgs, fvars => bindArgs fn as [] (newArgs.push a) fvars
/-- The source variable whose key in the context is `key`, and its type. The key of a variable
is its Lean variable, or, for a leaf of a flat field of a matched record, the leaf's projection of
the field. -/
def keyVar? (c : Ctx) (key : Lean.Expr) : MetaM (Option (Lean.Expr × Ty)) := do
let some i := c.vars.findIdx? (·.1 == key) | return none
let some (_, t) := c.vars[i]? | return none
let proof ← mkEqRefl (mkApp (mkConst ``Option.some [Level.zero]) (mkConst ``Ty) |>.app
(tyExpr t))
return some (← mkAppOptM ``Var.ofIndex
#[some (tyExpr t), some c.ctx, some (toExpr i), some proof], t)
/-- The source variable for the Lean variable `e` in scope, and its type. -/
def varOf (c : Ctx) (e : Lean.Expr) : MetaM (Lean.Expr × Ty) := do
let some v ← keyVar? c e | throwError "verified_compile: {e} is not a variable in scope"
return v
/-- `Eq.trans p q` with the middle term of `p`. The elaborator does not unify the two middle
terms; the kernel checks that `q`'s left side is the same term, which the reflector arranges up to
beta reduction. -/
def transHint (p q : Lean.Expr) : MetaM Lean.Expr := do
let some (α, a, b) := (← inferType p).eq? | throwError "verified_compile: the equation {p}"
let some (_, _, c) := (← inferType q).eq? | throwError "verified_compile: the equation {q}"
return mkApp6 (mkConst ``Eq.trans [← getLevel α]) α a b c p
(← mkExpectedTypeHint q (← mkEq b c))
/-- The reference to function `j` of the signatures `sigs`, a list of `Sig` literals, as a chain
of `FVar.there` around `FVar.here`. -/
partial def fvarAt (sigs : Lean.Expr) (j : Nat) : MetaM Lean.Expr := do
let (``List.cons, #[_, h, rest]) := sigs.getAppFnArgs
| throwError "verified_compile: no function {j} in {sigs}"
if j == 0 then return mkApp2 (mkConst ``FVar.here) h rest
let inner ← fvarAt rest (j - 1)
let .app (.app _ _) g := (← inferType inner)
| throwError "verified_compile: the reference {inner}"
return mkApp4 (mkConst ``FVar.there) rest g h inner
/-- The proof that `funs.get fv env` is `F env` for the meaning `F` of the function that `fv`
names, by `Funs.get_there` and `Funs.get_here`, for `funs` a chain of `Funs.cons`. -/
partial def getChain (funs fv env : Lean.Expr) : MetaM Lean.Expr := do
let (``Funs.cons, #[S, h, F, rest]) := funs.getAppFnArgs
| throwError "verified_compile: the meanings {funs}"
match fv.getAppFnArgs with
| (``FVar.here, _) => return mkAppN (mkConst ``Funs.get_here) #[S, h, F, rest, env]
| (``FVar.there, #[_, g, _, v]) =>
transHint (mkAppN (mkConst ``Funs.get_there) #[S, g, h, F, rest, v, env])
(← getChain rest v env)
| _ => throwError "verified_compile: the function reference {fv}"
def addDefinition (name : Name) (type value : Lean.Expr) : CoreM Unit :=
addAndCompile <| .defnDecl <|
mkDefinitionValEx name [] type value (.regular 1) .safe [name]
def addTheorem (name : Name) (type value : Lean.Expr) : CoreM Unit :=
addDecl <| .thmDecl { name, levelParams := [], type, value }
/-- A definition for the kernel only, without compiled code, for the literal bytes of a module. -/
def addLiteral (name : Name) (type value : Lean.Expr) : CoreM Unit :=
addDecl <| .defnDecl <| mkDefinitionValEx name [] type value (.regular 1) .safe [name]
unsafe def evalModuleUnsafe (env : Environment) (opts : Options) (name : Name) :
Except String Wasm.Module :=
env.evalConst Wasm.Module opts name
/-- The module of the constant `name`, from its compiled code. -/
@[implemented_by evalModuleUnsafe]
opaque evalModule (env : Environment) (opts : Options) (name : Name) : Except String Wasm.Module
/-- The component of the tuple `x` along `steps`: `false` for a pair's first component and `true`
for its second. -/
def tuplePath (x : Lean.Expr) : List Bool → MetaM Lean.Expr
| [] => return x
| false :: rest => do tuplePath (← mkAppM ``Prod.fst #[x]) rest
| true :: rest => do tuplePath (← mkAppM ``Prod.snd #[x]) rest
/-- A pair or a record that holds arrays, viewed as a pair for its destructuring: the component
types `α` and `β` of `α × β` or of the record's `Flat` tuple, the value built from components `a`
and `b`, the pair `pair p` of a value `p`, `p` itself or `Flat.flat p`, and the proof `eta B v` of
`B (rebuild (pair v).1 (pair v).2) = B v`. -/
structure PairView where
α : Lean.Expr
β : Lean.Expr
rebuild : Lean.Expr → Lean.Expr → MetaM Lean.Expr
pair : Lean.Expr → Lean.Expr
eta : Lean.Expr → Lean.Expr → MetaM Lean.Expr
/-- The view of `type` as a pair. A pair's eta is `pair_eta`. A record's is the theorem
`base.flat_eta.R`, added once per program and record type and proved by `rfl` with `B` and `v`
free, so that the kernel unfolds only the `Flat` instance and structure eta, never the terms that
`B` and `v` stand for. A sum that holds heap values has the components of its tuple, for the costs
of its parts, and neither a rebuild nor an eta law. -/
def pairView (base : Name) (type : Lean.Expr) : MetaM PairView := do
let type ← whnfR type
if let (``Prod, #[α, β]) := type.getAppFnArgs then
return ⟨α, β, fun a b => mkAppM ``Prod.mk #[a, b], id, fun B v => mkAppM ``pair_eta #[B, v]⟩
if ← heapSum? type then
-- A sum's components are those of its tuple, and nothing rebuilds the sum from them.
let some (τ, inst) ← flatInstance? type
| throwError "verified_compile: the sum {type} has no `Flat` instance"
let (``Prod, #[α, β]) := (← whnfR τ).getAppFnArgs
| throwError "verified_compile: the `Flat` instance of {type} is not a pair"
let missing (what : String) : MetaM Lean.Expr :=
throwError "verified_compile: the sum {type} has no {what}; its variables stay whole"
return ⟨α, β, fun _ _ => missing "rebuild from its components",
fun p => mkApp4 (mkConst ``LeanExe.Pipeline.Flat.flat) type τ inst p,
fun _ _ => missing "eta law"⟩
let some (ctor, _) ← structOf? type
| throwError "verified_compile: {type} is not a pair or a record"
let some (τ, inst) ← flatInstance? type
| throwError "verified_compile: the record {type} has no `Flat` instance"
let (``Prod, #[α, β]) := (← whnfR τ).getAppFnArgs
| throwError "verified_compile: the `Flat` instance of {type} is not a pair"
let tree ← flatTree "verified_compile" type τ inst ctor
let rebuild (a b : Lean.Expr) : MetaM Lean.Expr := do
let fields ← (List.range ctor.numFields).mapM fun i => do
match tree.find? (·.1 == i) with
| some (_, false :: rest) => tuplePath a rest
| some (_, true :: rest) => tuplePath b rest
| _ => throwError "verified_compile: the `Flat` instance of {type} does not hold field {i}"
return mkAppN (mkConst ctor.name type.getAppFn.constLevels!) (type.getAppArgs ++ fields.toArray)
let pair (p : Lean.Expr) := mkApp4 (mkConst ``LeanExe.Pipeline.Flat.flat) type τ inst p
let .const n _ := type.getAppFn | throwError "verified_compile: the record {type}"
let name := base ++ `flat_eta ++ n
unless (← getEnv).contains name do
let (stmt, proof) ← withLocalDeclD `γ (mkSort Level.one) fun γ => do
withLocalDeclD `B (← mkArrow type γ) fun B => withLocalDeclD `v type fun v => do
let P := pair v
let lhs := mkApp B (← rebuild (← mkAppM ``Prod.fst #[P]) (← mkAppM ``Prod.snd #[P]))
let rhs := mkApp B v
let proof ← mkExpectedTypeHint (← mkEqRefl rhs) (← mkEq lhs rhs)
return (← mkForallFVars #[γ, B, v] (← mkEq lhs rhs), ← mkLambdaFVars #[γ, B, v] proof)
addTheorem name stmt proof
let eta (B v : Lean.Expr) : MetaM Lean.Expr := do
return mkApp3 (mkConst name) (← inferType (mkApp B v)) B v
return ⟨α, β, rebuild, pair, eta⟩
/-- Whether the kernel finds `a` and `b` definitionally equal, in the current local context. -/
def kernelDefEq (a b : Lean.Expr) : MetaM Bool := do
match Kernel.isDefEq (← getEnv) (← getLCtx) a b with
| .ok r => return r
| .error ex => throwKernelException ex
/-- The proof of `T = e` by `rfl`, for a term `T` that the reflector reflects in place of `e`:
the two differ by a `let` that `T` substitutes, a beta reduction, or a match on a constructor,
which the kernel reduces without evaluating either term's parts. -/
def bareEq (T e : Lean.Expr) : MetaM Lean.Expr := do
mkExpectedTypeHint (← mkEqRefl e) (← mkEq T e)
/-- The enumeration and its `Flat` instance, for a type other than `Bool` whose values are
enumeration constants with a `Flat` instance to words. -/
def enumFlat? (type : Lean.Expr) : MetaM (Option (Name × Lean.Expr)) := do
if (← elemOf? type).isSome then return none
let .const n _ ← whnfR type | return none
unless ← isEnumType n do return none
let some (β, inst) ← flatInstance? (mkConst n) | return none
unless (← whnfR β).isConstOf ``UInt64 do return none
return some (n, inst)
/-- `Flat.flat` of the enumeration `n` with the instance `inst`. -/
def enumFlat (n : Name) (inst : Lean.Expr) : Lean.Expr :=
mkApp3 (mkConst ``LeanExe.Pipeline.Flat.flat) (mkConst n) (mkConst ``UInt64) inst
/-- The theorem that the flattening of the enumeration `n` is injective, added once per program
under `base`. It follows from the decoder `fun w => bif w == flat K₁ then K₁ else …` and its
value at each constructor, which the kernel evaluates. The reflector checks each constructor
first, so that a flattening that maps two constructors to one word is reported by name. -/
def flatInjective (base n : Name) (inst : Lean.Expr) : MetaM Lean.Expr := do
let name := base ++ `flat_injective ++ n
if (← getEnv).contains name then return mkConst name
let .inductInfo info ← getConstInfo n | throwError "verified_compile: {n} is not an enumeration"
let E := Lean.mkConst n
let flat := enumFlat n inst
let ctors := info.ctors.map Lean.mkConst
let g ← withLocalDeclD `w (mkConst ``UInt64) fun w => do
let rec chain : List Lean.Expr → MetaM Lean.Expr
| [] => throwError "verified_compile: {n} has no constructors"
| [k] => return k
| k :: ks => do mkAppM ``cond #[← mkAppM ``BEq.beq #[w, mkApp flat k], k, ← chain ks]
mkLambdaFVars #[w] (← chain ctors)
let hgTy ← withLocalDeclD `x E fun x => do
mkForallFVars #[x] (← mkEq (mkApp g (mkApp flat x)) x)
let hg ← withLocalDeclD `x E fun x => do
let motive ← withLocalDeclD `y E fun y => do
mkLambdaFVars #[y] (← mkEq (mkApp g (mkApp flat y)) y)
let minors ← ctors.mapM fun k => do
let lhs := mkApp g (mkApp flat k)
unless ← kernelDefEq lhs k do
throwError "verified_compile: the flattening of {n} gives {k} the same word as an earlier \
constructor"
mkExpectedTypeHint (← mkEqRefl k) (← mkEq lhs k)
mkLambdaFVars #[x] (mkAppN (mkConst (n ++ `casesOn) [Level.zero]) (#[motive, x] ++ minors))
let hg ← mkExpectedTypeHint hg hgTy
let proof ← withLocalDeclD `a E fun a => withLocalDeclD `b E fun b => do
withLocalDeclD `h (← mkEq (mkApp flat a) (mkApp flat b)) fun h => do
mkLambdaFVars #[a, b, h] (← mkEqTrans (← mkEqSymm (mkApp hg a))
(← mkEqTrans (← mkCongrArg g h) (mkApp hg b)))
addTheorem name (← mkAppM ``Function.Injective #[flat]) proof
return mkConst name
/-- The word of an enumeration constant `e`, as a literal. -/
def enumWord? (e : Lean.Expr) : MetaM (Option Lean.Expr) := do
let .const k _ := e | return none
let some (.ctorInfo info) := (← getEnv).find? k | return none
let some (n, inst) ← enumFlat? (mkConst info.induct) | return none
let w ← match Kernel.whnf (← getEnv) (← getLCtx)
(mkApp (mkConst ``UInt64.toNat) (mkApp (enumFlat n inst) e)) with
| .ok w => pure w
| .error ex => throwKernelException ex
let some v := natOf w | throwError "verified_compile: the word of {e} is not a literal: {w}"