-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathProject.lean
More file actions
153 lines (151 loc) · 5.73 KB
/
Copy pathProject.lean
File metadata and controls
153 lines (151 loc) · 5.73 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
import Project.Gcd.Spec
import Project.AssocList.Spec
import Project.OrderBook.Spec
import Project.Validate.Spec
import Project.AppendBang.Spec
import Project.PushSize.Spec
import Project.PushTwice.Spec
import Project.SharedPair.Spec
import Project.PairFree.Spec
import Project.BoxFree.Spec
import Project.FoldSum.Spec
import Project.F64MulBits.Spec
import Project.F64SubBits.Spec
import Project.F64DivBits.Spec
import Project.F64SqrtBits.Spec
import Project.F64Dot2CheckedBits.Spec
import Project.F64DotCheckedBits.Spec
import Project.F64Horner2CheckedBits.Spec
import Project.EulerRusanov.Spec
import Project.EulerRusanov.RealMathematics
import Project.EulerRusanov.StencilNumerical
import Project.EulerRusanov.StencilAdmissibility
import Project.EulerRusanovStep.Spec
import Project.EulerRusanovStep.StepData
import Project.LebU32.Spec
import Project.ClobQuote.Spec
import Project.ClobCancel.Spec
import Project.ClobFindBest.Spec
import Project.ClobPostOnly.Spec
import Project.ClobMatchFuel.Spec
import Project.ClobLimit.Spec
import Project.ClobMarket.Spec
import Project.ClobDepth.Spec
import Project.Runtime.Checks
import Project.Runtime.Spec
import Project.ProofKit.F64Order
import Project.EulerConservative.Spec
import Project.EulerDynamicFlux.Spec
import Project.EulerCellStep.Spec
import Project.EulerGridStep.Outputs
import Project.EulerGridStep.Helpers
import Project.EulerGridStep.FieldMemory
import Project.EulerGridStep.FieldShape
import Project.EulerGridStep.FieldTail
import Project.EulerGridStep.FieldAllocationBump
import Project.EulerGridStep.FieldAllocationReuse
import Project.EulerGridStep.FieldPrefix
import Project.EulerGridStep.FieldCapacity
import Project.EulerGridStep.FieldFrame
import Project.EulerGridStep.FieldExecution
import Project.EulerGridStep.Release
import Project.EulerGridStep.ReleaseFramed
import Project.EulerGridStep.LiveBuffers
import Project.EulerGridStep.CellFieldCall
import Project.EulerGridStep.WriterCopies
import Project.EulerGridStep.WriterReleases
import Project.EulerGridStep.WriterAccepted
import Project.EulerGridStep.RejectedPrefix
import Project.EulerGridStep.RejectedFrame
import Project.EulerGridStep.WriterRejected
import Project.EulerGridStep.WriterProtected
import Project.EulerGridStep.WriterSequence
import Project.EulerGridStep.FreshBufferState
import Project.EulerGridStep.ArenaAllocation
import Project.EulerGridStep.FreshWriterAccepted
import Project.EulerGridStep.FreshWriterRejected
import Project.EulerGridStep.AdvanceReads
import Project.EulerGridStep.AdvanceAccepted
import Project.EulerGridStep.AdvanceRejected
import Project.EulerGridStep.WriterReleaseSequence
import Project.EulerGridStep.BufferResults
import Project.EulerGridStep.ReleaseHeap
import Project.EulerGridStep.FreshSpace
import Project.EulerGridStep.MixedCellState
import Project.EulerGridStep.CellReleaseHeap
import Project.EulerGridStep.WriterAcceptedSequence
import Project.EulerGridStep.AdvanceMixed
import Project.EulerGridStep.AdvanceArena
import Project.EulerGridStep.AdvanceFirstArena
import Project.EulerGridStep.AdvanceLaterRejected
import Project.EulerGridStep.AdvanceFirstRejected
import Project.EulerGridStep.ArenaAdvance
import Project.EulerGridStep.InitialAllocationBump
import Project.EulerGridStep.InitializationFill
import Project.EulerGridStep.InitialCapacity
import Project.EulerGridStep.InitialDimensions
import Project.EulerGridStep.InitialMemory
import Project.EulerGridStep.InitialOutput
import Project.EulerGridStep.InitialArena
import Project.EulerGridStep.EntryGuards
import Project.EulerGridStep.RejectedEntryExecution
import Project.EulerGridStep.ProtectedArenaAdvance
import Project.EulerGridStep.GridLoopModel
import Project.EulerGridStep.GridLoopStorage
import Project.EulerGridStep.GridLoopTransition
import Project.EulerGridStep.GridLoopAdvance
import Project.EulerGridStep.GridLoopShape
import Project.EulerGridStep.GridLoopFrame
import Project.EulerGridStep.GridLoop
import Project.EulerGridStep.GridFinalGeometry
import Project.EulerGridStep.GridFinalRelease
import Project.EulerGridStep.GridFinish
import Project.EulerGridStep.GridSetup
import Project.EulerGridStep.GridInitialFacts
import Project.EulerGridStep.GridValidBody
import Project.EulerGridStep.GridEntryReady
import Project.EulerGridStep.GridExecution
import Project.EulerGridStep.GridReset
import Project.EulerGridStep.Spec
import Project.EulerGridStep.Runner
import Project.EulerGridStep.RunnerExecution
import Project.EulerGridStep.Scan
import Project.EulerGridScan.Spec
import Project.ProofKit.F64StrictOrder
import Project.Euler2DConservative.Outputs
import Project.Euler2DConservative.Spec
import Project.Euler2DDynamicFlux.Spec
import Project.Euler2DCellStep.Spec
import Project.EulerRiemann.Spec
import Project.EulerOutwardSpeed.Spec
import Project.EulerReconstruction.Spec
import Project.EulerOutwardMaximum.Spec
import Project.EulerOutwardCfl.Spec
import Project.EulerOutwardGrid.Spec
import Project.EulerOutwardFlux.Spec
import Project.EulerOutwardFaceStep.Spec
import Project.EulerRiemann.OutwardFaceStepSpec
import Project.EulerRiemann.OutwardFaceStepResidual
import Project.EulerReconstructed.Spec
import Project.EulerCertificateFlux.Spec
import Project.EulerCertificate.Spec
import Project.ExpSmall.Spec
import Project.ExpWide.Spec
import Project.ExpNeg.Spec
import Project.Softmax.Spec
import Project.SoftmaxWide.Spec
import Project.LayerNorm.Spec
import Project.Gelu.Spec
import Project.GeluWide.Spec
import Project.TinyGpt2Hidden.Spec
import Project.TinyGpt2Infer.Spec
import Project.F64Clip.Spec
import Project.TinyGpt2Checked.Spec
import Project.SequenceSoftmax.Spec
import Project.PackedRead.Spec
import Project.PackedGenerate.Spec
import Project.Gpt2RowMean.Spec
import Project.Gpt2RowInvStd.Spec
import Project.Gpt2AttentionScore.Spec
import Project.Gpt2LinearRows.Spec
import Project.Gpt2CachedStep.Spec