OAI/Analysis/MatrixSigning/Matrices/DenseMatrixSerialization.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W08.matrixEntryIndex line 14
2. theorem OAI.KS.W08.matrixEntryIndex_val line 16
3. theorem OAI.KS.W08.matrixEntryIndex_lt line 20
4. def OAI.KS.W08.denseMatrixPayloads line 23
5. theorem OAI.KS.W08.denseMatrixPayloads_length line 28
6. theorem OAI.KS.W08.denseMatrixPayloads_get line 31
7. def OAI.KS.W08.denseMatrixTape line 47
8. def OAI.KS.W08.denseMatrixCursor line 50
9. theorem OAI.KS.W08.denseMatrixCursor_length line 53
10. theorem OAI.KS.W08.denseMatrixTape_length line 56
11. theorem OAI.KS.W08.denseMatrixTape_length_le line 63
12. theorem OAI.KS.W08.denseMatrixScanSize_le line 79