OAI/Analysis/MatrixSigning/Machines/ExpressionPrimitives.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W13.ExpressionMachine.registers line 14
  2. def OAI.KS.W13.ExpressionMachine.boundary line 17
  3. def OAI.KS.W13.ExpressionMachine.firstPorts line 20
  4. def OAI.KS.W13.ExpressionMachine.leafPorts line 23
  5. def OAI.KS.W13.ExpressionMachine.rightPorts line 24
  6. def OAI.KS.W13.ExpressionMachine.leftPorts line 25
  7. def OAI.KS.W13.ExpressionMachine.framePorts line 26
  8. def OAI.KS.W13.ExpressionMachine.finalPorts line 27
  9. def OAI.KS.W13.ExpressionMachine.leafDecode line 28
  10. def OAI.KS.W13.ExpressionMachine.rightDecode line 29
  11. def OAI.KS.W13.ExpressionMachine.leftDecode line 30
  12. def OAI.KS.W13.ExpressionMachine.resultFrame line 31
  13. def OAI.KS.W13.ExpressionMachine.resultPush line 32
  14. def OAI.KS.W13.ExpressionMachine.leftPrepend line 33
  15. theorem OAI.KS.W13.ExpressionMachine.leafDecode_spec line 35
  16. theorem OAI.KS.W13.ExpressionMachine.rightDecode_spec line 42
  17. theorem OAI.KS.W13.ExpressionMachine.leftDecode_spec line 49
  18. theorem OAI.KS.W13.ExpressionMachine.leftPrepend_spec line 57
  19. theorem OAI.KS.W13.ExpressionMachine.resultFrame_spec line 65
  20. theorem OAI.KS.W13.ExpressionMachine.resultPush_spec line 72
  21. def OAI.KS.W13.ExpressionMachine.finishValue line 81
  22. theorem OAI.KS.W13.ExpressionMachine.finishValue_spec line 83
  23. inductive OAI.KS.W13.ExpressionMachine.BinaryOp line 88
  24. def OAI.KS.W13.ExpressionMachine.BinaryOp.eval line 90
  25. def OAI.KS.W13.ExpressionMachine.binaryArithmetic line 96
  26. def OAI.KS.W13.ExpressionMachine.binaryBudget line 102
  27. theorem OAI.KS.W13.ExpressionMachine.binaryArithmetic_spec line 104