OAI/Analysis/MatrixSigning/Encoding/FramedArrayRetrieval.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W11.FramedArray.decoderPorts line 11
2. def OAI.KS.W11.FramedArray.decoderProgram line 12
3. theorem OAI.KS.W11.FramedArray.run_decoder line 14
4. def OAI.KS.W11.FramedArray.lookupProgram line 28
5. theorem OAI.KS.W11.FramedArray.lookupProgram_states line 30
6. theorem OAI.KS.W11.FramedArray.lookupProgram_table_length line 32
7. def OAI.KS.W11.FramedArray.lookupFuel line 41
8. theorem OAI.KS.W11.FramedArray.run_lookup_prefix line 44
9. theorem OAI.KS.W11.FramedArray.lookupFuel_linear line 67
10. theorem OAI.KS.W11.FramedArray.run_lookup line 74
11. theorem OAI.KS.W11.FramedArray.lookup_linear_time line 97