OAI/Analysis/MatrixSigning/Machines/
1042 declarations, 0 contain sorry, 0 declared as axioms; 91 files
Files
- BinaryAccumulator.lean 16 declarations
- BinaryExpressionEvaluator.lean 13 declarations
- BinaryFloorBridge.lean 4 declarations
- BinaryMachine.lean 35 declarations
- BinaryNormalize.lean 20 declarations
- BinaryStackDeterministic.lean 2 declarations
- BinaryStackMoves.lean 30 declarations
- BinaryToUnary.lean 8 declarations
- BinaryToUnaryDeterministic.lean 3 declarations
- BinaryToUnaryMachine.lean 17 declarations
- BinaryToUnaryRun.lean 7 declarations
- BinaryTrimMachine.lean 12 declarations
- BisectionCommands.lean 13 declarations
- BorrowActivity.lean 2 declarations
- CanonicalUnarySpec.lean 1 declarations
- CleanupDeterministic.lean 4 declarations
- CommonDenominatorLift.lean 4 declarations
- ComplexBridge.lean 17 declarations
- ControllerReachable.lean 10 declarations
- ControllerReplayBound.lean 3 declarations
- ControllerRuntime.lean 5 declarations
- ControllerTerminalBound.lean 5 declarations
- CopyInput.lean 18 declarations
- DenseFieldCounter.lean 27 declarations
- Deterministic.lean 11 declarations
- DeterministicCombinators.lean 7 declarations
- DirectedRounding.lean 12 declarations
- EntryPoint.lean 6 declarations
- ExpressionPrimitives.lean 27 declarations
- ExpressionSyntax.lean 31 declarations
- FiniteControl.lean 9 declarations
- FiniteDispatch.lean 9 declarations
- FixedBranch.lean 26 declarations
- FixedCanonicalize.lean 6 declarations
- FixedCompare.lean 8 declarations
- FixedCopyRestore.lean 12 declarations
- FixedCopySpec.lean 1 declarations
- FixedDotBody.lean 10 declarations
- FixedDotBounds.lean 12 declarations
- FixedDotControl.lean 12 declarations
- FixedDotMachine.lean 19 declarations
- FixedDotModel.lean 15 declarations
- FixedDotPrimitives.lean 9 declarations
- FixedLoop.lean 23 declarations
- FixedPortRunSpec.lean 2 declarations
- FixedRun.lean 5 declarations
- FixedSequential.lean 39 declarations
- FixedStackMachine.lean 63 declarations
- FixedStackPortLift.lean 29 declarations
- InputHeaderPrimitives.lean 3 declarations
- InverseBounds.lean 6 declarations
- InverseHeight.lean 7 declarations
- LiteralProgram.lean 9 declarations
- LittleEndianCompare.lean 20 declarations
- MachineCombinators.lean 6 declarations
- MachineRoundTrip.lean 2 declarations
- MachineTransport.lean 1 declarations
- MagnitudeProgram.lean 9 declarations
- NestedSchur.lean 2 declarations
- NormalizeOutput.lean 5 declarations
- ProgramTable.lean 1 declarations
- Realification.lean 17 declarations
- RealificationSPD.lean 8 declarations
- SchurBounds.lean 9 declarations
- SchurCellMachine.lean 19 declarations
- SchurColumnLoop.lean 5 declarations
- SchurCounters.lean 5 declarations
- SchurDimension.lean 9 declarations
- SchurEntryMachine.lean 8 declarations
- SchurInputLength.lean 5 declarations
- SchurOperands.lean 10 declarations
- SchurReadStage.lean 17 declarations
- SchurRowLoop.lean 7 declarations
- SchurTableCorrectness.lean 10 declarations
- SchurTableInvariant.lean 9 declarations
- SchurTableMachine.lean 15 declarations
- SchurTablePorts.lean 2 declarations
- Sequential.lean 27 declarations
- SignedFloorMachine.lean 23 declarations
- SignedFloorModel.lean 7 declarations
- SignedFloorSize.lean 2 declarations
- SignedSerializePrimitives.lean 5 declarations
- SparseCoefficientStage.lean 11 declarations
- StackTransfer.lean 3 declarations
- StackTransferSpecs.lean 4 declarations
- TerminalInputBounds.lean 5 declarations
- TerminalReadStage.lean 8 declarations
- TerminalSparseAssembly.lean 12 declarations
- TerminalVectorReplace.lean 12 declarations
- TerminalZeroVector.lean 9 declarations
- UnaryLengthMachine.lean 9 declarations