1. Top
  2. 6.5610-project
  3. Commits
6.5610-project

Cryptography final project

Commits at 5165d72597bd24d77213bf3c7e4fae2619fb9466

  1. 5165d725 toString for new type checker Anthony Wang authored at Anthony Wang comitted at
  2. 9e5da10a Better notation Anthony Wang authored at Anthony Wang comitted at
  3. 23dd54fb demo Rey Li authored at Rey Li comitted at
  4. 0cb4fc63 Commit more bad code Anthony Wang authored at Anthony Wang comitted at
  5. 3ff64e64 Cursed dependent type stuff Anthony Wang authored at Anthony Wang comitted at
  6. 631afd86 Fix bug in Lurk port as well Anthony Wang authored at Anthony Wang comitted at
  7. 2150026d Prove that uLean type checker is as consistent as Lean Dan Klishch authored at Dan Klishch comitted at
  8. e7a247de Lean type checker bug fix Dan Klishch authored at Dan Klishch comitted at
  9. b699a330 Move Lurk files to root dir, try with a larger proof, delete old garbage Anthony Wang authored at Anthony Wang comitted at
  10. c5d06832 More slightly nontrivial proofs Anthony Wang authored at Anthony Wang comitted at
  11. e0867123 Small tweaks to Lean impl of μLean Anthony Wang authored at Anthony Wang comitted at
  12. 3bb5cccf successful (inelegant) protocol implementation Rey Li authored at Rey Li comitted at
  13. bcb71a24 set up factoring example for better running Rey Li authored at Rey Li comitted at
  14. b4984fc0 factoring test proof made Rey Li authored at Rey Li comitted at
  15. a8be2654 significant partial working progress towards creating a hiding protocol Rey Li authored at Rey Li comitted at
  16. 6716245a Fix stupid typo (thanks Claude) Anthony Wang authored at Anthony Wang comitted at
  17. 183ddaad de Bruijn indices (Lurk version is still broken) Anthony Wang authored at Anthony Wang comitted at
  18. e84b5aa9 Name it μLean Anthony Wang authored at Anthony Wang comitted at
  19. ec83994f Use field elements instead of strings for variable names Anthony Wang authored at Anthony Wang comitted at
  20. 80ffed3a Swap Term and Typ to match the usual convention Anthony Wang authored at Anthony Wang comitted at
  21. e18f6136 Use finite field elements instead of strings for better perf Actually I have no idea if this actually improves perf or not... Anthony Wang authored at Anthony Wang comitted at
  22. 1aef3614 Bump Lean version Anthony Wang authored at Anthony Wang comitted at
  23. 09248633 Add Lurk dir patch Anthony Wang authored at Anthony Wang comitted at
  24. 7e531a32 Broken protocol code Anthony Wang authored at Anthony Wang comitted at
  25. 7731f06c Passing all test cases now Anthony Wang authored at Anthony Wang comitted at
  26. 786a1c9e Type checker in Lurk finally works!!! Anthony Wang authored at Anthony Wang comitted at
  27. 26daa600 Lurk port almost somewhat works now I guess Anthony Wang authored at Anthony Wang comitted at
  28. 041cf99d Implement natural numbers Anthony Wang authored at Anthony Wang comitted at
  29. 6ee71b22 Generate Lurk s-expressions from `Term`s Anthony Wang authored at Anthony Wang comitted at
  30. 320e2c47 Oops use boolean or instead of prop or Anthony Wang authored at Anthony Wang comitted at