Repository navigation
Expand file tree
/
Copy pathVerified.lean
More file actions
114 lines (114 loc) · 3.45 KB
/
Copy pathVerified.lean
File metadata and controls
114 lines (114 loc) · 3.45 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
import Verified.Source
import Verified.Tree
import Verified.TreeHeader
import Verified.TreeDetach
import Verified.TreeAttach
import Verified.TreeStorage
import Verified.TreeRestore
import Verified.TreeInitialize
import Verified.TreeCopy
import Verified.TreeHeaderCopyCode
import Verified.TreeFieldsStore
import Verified.TreeFieldsLoad
import Verified.TreeFieldsState
import Verified.TreeFieldValues
import Verified.TreeFieldLocs
import Verified.FieldsExpr
import Verified.CoercedRelease
import Verified.FieldsAdvance
import Verified.BindPrefix
import Verified.ContextHEq
import Verified.TreeMatchBlocks
import Verified.TreeFieldPositions
import Verified.VarCorrect
import Verified.FieldsArgs
import Verified.TreeAssembleCode
import Verified.TreePackedBlocks
import Verified.TreeRelease
import Verified.TreeLayout
import Verified.TreeCopyWork
import Verified.TreeNodeLayout
import Verified.Compile
import Verified.State
import Verified.Correct
import Verified.BoundFacts
import Verified.LoopCostLast
import Verified.ChargeFacts
import Verified.Reflect.Lemmas
import Verified.Reflect.BoundLemmas
import Verified.Reflect.FitsLemmas
import Verified.Reflect.Command
import Verified.Examples.Poly
import Verified.Examples.Mix
import Verified.Examples.Lets
import Verified.Examples.Select
import Verified.Examples.Calls
import Verified.Examples.Frontend
import Verified.Examples.Fold
import Verified.Examples.TreeCopy
import Verified.Examples.TreeCore
import Verified.Examples.Lists
import Verified.Examples.Composition
import Verified.Examples.CompositionPure
import Verified.Examples.ScalarComposition
import Verified.Examples.Relocation
import Verified.WGSL.Compile
import Verified.Examples.WgslProof
import Verified.Examples.ListRecursion
import Verified.Examples.ListLoops
import Verified.Examples.ListTail
import Verified.Examples.RecursiveTypes
import Verified.Examples.TaggedTypes
import Verified.Examples.TailCore
import Verified.Examples.Tail
import Verified.Examples.TailConditions
import Verified.Examples.TailReflection
import Verified.ArrayFold
import Verified.TailRun
import Verified.TailArgs
import Verified.TailCorrect
import Verified.TailNext
import Verified.TailBranch
import Verified.TailBind
import Verified.TailCode
import Verified.TailStep
import Verified.TailWhile
import Verified.TailEntryFacts
import Verified.TailEntry
import Verified.FunRenameBound
import Verified.TailExpand
import Verified.TailAllocExpand
import Verified.TailTransport
import Verified.Reflect.TailModes
import Verified.Reflect.TailLemmas
import Verified.Reflect.TailBoundLemmas
import Verified.Examples.Pairs
import Verified.Examples.Loops
import Verified.Examples.Arrays
import Verified.Examples.Owned
import Verified.Examples.Bytes
import Verified.Examples.Updates
import Verified.Examples.Grow
import Verified.Examples.Modes
import Verified.Examples.Floats
import Verified.Examples.Floats32
import Verified.Examples.Sums
import Verified.Examples.HeapSums
import Verified.Examples.TypedTrees
import Verified.Examples.Elements
import Verified.Examples.Tuples
import Verified.Examples.Records
import Verified.Examples.Grids
import Verified.Examples.Repeat
import Verified.Examples.Enums
import Verified.Examples.Recursion
import Verified.Examples.Fields
import Verified.Examples.Insert
import Verified.Examples.Tables
import Demos.Verified
import Verified.Wasi
import Verified.Examples.Literals
import Verified.ProgramLiterals
import Verified.Examples.WasiDepth
import Verified.Examples.WasiRetainTotal
import Verified.Examples.WasiStdio