Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

EverParse+Pulse: Verified parsing and serialization with separation logic #155

Open
wants to merge 89 commits into
base: master
Choose a base branch
from
Open

EverParse+Pulse: Verified parsing and serialization with separation logic #155

wants to merge 89 commits into from

Commits on Oct 25, 2024

  1. pts_to_serialized, validator, jumper, peek, CPS reader, read

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    638269a View commit details
    Browse the repository at this point in the history

  2. WIP LowParse.Pulse.Combinators

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    9777ccf View commit details
    Browse the repository at this point in the history

  3. integer readers

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    573761d View commit details
    Browse the repository at this point in the history

  4. validate, jump int

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    b084439 View commit details
    Browse the repository at this point in the history

  5. switch to CPS validators

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    de8c900 View commit details
    Browse the repository at this point in the history

  6. synth, filter

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    2e9bf08 View commit details
    Browse the repository at this point in the history

  7. validate_nonempty

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    cf0534c View commit details
    Browse the repository at this point in the history

  8. validate_nondep_then

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    7209ceb View commit details
    Browse the repository at this point in the history

  9. common validate_dtuple2 and nondep_then

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    cbf928e View commit details
    Browse the repository at this point in the history

  10. split_dtuple2, simplified split_nondep_then

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    6352265 View commit details
    Browse the repository at this point in the history

  11. jump_nondep_then, jump_dtuple2

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    53d8e8b View commit details
    Browse the repository at this point in the history

  12. validate_and_read

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    4fd8c75 View commit details
    Browse the repository at this point in the history

  13. validate_filter -> validate_and_read_filter

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    ad30058 View commit details
    Browse the repository at this point in the history

  14. validate_dtuple2 with validate_and_read tag, remove validate_nondep_then

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    dc5e56b View commit details
    Browse the repository at this point in the history

  15. restore validate_nondep_then

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    fd887c5 View commit details
    Browse the repository at this point in the history

  16. validate_and_read_dtuple2

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    cb95617 View commit details
    Browse the repository at this point in the history

  17. read_synth, read_filter

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    14f5bac View commit details
    Browse the repository at this point in the history

  18. validate_and_read_synth

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    b44c18b View commit details
    Browse the repository at this point in the history

  19. bitsum

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    9383b8c View commit details
    Browse the repository at this point in the history

  20. validate_and_read integers; ret, empty; etc.

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    4b29d00 View commit details
    Browse the repository at this point in the history

  21. ifthenelse_jumper, jump_ret, jump_empty

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    944b32d View commit details
    Browse the repository at this point in the history

  22. some extraction fixes: avoid pure lets in F* assemblies, replace reco… 

    …rd field accesses, normalize with postprocess_with, etc.
    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    769d3b1 View commit details
    Browse the repository at this point in the history

  23. mark more combinators inline_for_extraction

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    376403d View commit details
    Browse the repository at this point in the history

  24. Karamel chokes on tuples. Use a custom slice_pair type instead

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    9d360cb View commit details
    Browse the repository at this point in the history

  25. Karamel chokes on local ghost functions, hoist them instead (mainly f… 

    …or intro_stick)
    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    92f6343 View commit details
    Browse the repository at this point in the history

  26. slice_pair moved to Pulse

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    5e76a3f View commit details
    Browse the repository at this point in the history

  27. read then pure cont

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    39a4638 View commit details
    Browse the repository at this point in the history

  28. read with pure continuation

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    f9a36f3 View commit details
    Browse the repository at this point in the history

  29. pure_read_ext, empty, dtuple, ifthenelse

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    b5f83df View commit details
    Browse the repository at this point in the history

  30. properly normalize integer readers

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    ff928b0 View commit details
    Browse the repository at this point in the history

  31. replace CPS reader with pure_reader

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    5d088a0 View commit details
    Browse the repository at this point in the history

  32. restore validate_and_read_intro, jump_dtuple2, with leaf_reader this … 

    …time
    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    cf0a5ba View commit details
    Browse the repository at this point in the history

  33. revert to non-CPS validators; jumpers with offsets instead of sizes

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    626d975 View commit details
    Browse the repository at this point in the history

  34. eta-expand validate_synth because of the pure bind

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    f85e1c0 View commit details
    Browse the repository at this point in the history

  35. ifthenelse_validator

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    0238383 View commit details
    Browse the repository at this point in the history

  36. bound offset on validator failure

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    fc169dd View commit details
    Browse the repository at this point in the history

  37. jump_vclist; dtuple2, nondep_then, nlist accessors

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    d75f3b6 View commit details
    Browse the repository at this point in the history

  38. pts_to_serialized_nlist_1, pts_to_serialized_length, etc.

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    4c57be3 View commit details
    Browse the repository at this point in the history

  39. Util: stick -> trade

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    a8eb400 View commit details
    Browse the repository at this point in the history

  40. move all trade lemmas to Pulse.Lib.Trade.Util

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    6dee4b9 View commit details
    Browse the repository at this point in the history

  41. LowParse.Pulse: stick -> trade

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    65945cb View commit details
    Browse the repository at this point in the history

  42. LowParse.Pulse: remove now implicit arguments to trade operations

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    e93bb12 View commit details
    Browse the repository at this point in the history

  43. LowParse.Pulse: stick -> trade in names

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    709bf3b View commit details
    Browse the repository at this point in the history

  44. LowParse.Pulse: vprop -> slprop

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    e1ff2c4 View commit details
    Browse the repository at this point in the history

  45. WIP write

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    1dc81c2 View commit details
    Browse the repository at this point in the history

  46. WIP ghost parsers

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    f922d50 View commit details
    Browse the repository at this point in the history

  47. convert LowParse.Pulse back to ghost parsers, serializers (WIP impl_p… 

    …red_recursive)
    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    50ebfeb View commit details
    Browse the repository at this point in the history

  48. WIP serialize

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    bd2955d View commit details
    Browse the repository at this point in the history

  49. writer, size lenses

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    a723657 View commit details
    Browse the repository at this point in the history

  50. compute_remaining_size_constant_size

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    0e7e174 View commit details
    Browse the repository at this point in the history

  51. fuse Write into Base

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    6986044 View commit details
    Browse the repository at this point in the history

  52. compose writing lenses, write ints

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    26891a1 View commit details
    Browse the repository at this point in the history

  53. WIP l2r_write_dtuple2

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    caea2d3 View commit details
    Browse the repository at this point in the history

  54. write dtuple2, nondep_then

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    6d47866 View commit details
    Browse the repository at this point in the history

  55. l2r_write_synth

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    6b86b7a View commit details
    Browse the repository at this point in the history

  56. l2r_write_filter

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    eca27ba View commit details
    Browse the repository at this point in the history

  57. l2r_leaf_writer_ext

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    5917d64 View commit details
    Browse the repository at this point in the history

  58. l2r_leaf_write_filter

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    05e9b22 View commit details
    Browse the repository at this point in the history

  59. WHY WHY WHY are lambdas no longer usable in slprops?

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    8ca9313 View commit details
    Browse the repository at this point in the history

  60. lowparse: remove LowParse.Pulse.Util

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    59e59a0 View commit details
    Browse the repository at this point in the history

  61. WIP more l2r_writer combinators

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    24f2db9 View commit details
    Browse the repository at this point in the history

  62. serialization combinators with reverse handling of vmatch

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    88251c3 View commit details
    Browse the repository at this point in the history

  63. l2r_writer_ifthenelse

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    4d569ba View commit details
    Browse the repository at this point in the history

  64. serialize seqbytes by copy

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    a3ba19f View commit details
    Browse the repository at this point in the history

  65. extensionality with explicit type equality in vmatch

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    deb455c View commit details
    Browse the repository at this point in the history

  66. vmatch should act on low-level data bundled with perm

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    ef51cfd View commit details
    Browse the repository at this point in the history

  67. WIP l2r_write_nlist_as_array

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    bc979a7 View commit details
    Browse the repository at this point in the history

  68. l2r_write_nlist_as_array

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    a03661d View commit details
    Browse the repository at this point in the history

  69. nlist_match_array: make varray partial

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    e771aa9 View commit details
    Browse the repository at this point in the history

  70. move nlist_match_array_intro to LowParse.Pulse.VCList

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    7dd28f6 View commit details
    Browse the repository at this point in the history

  71. nlist_sorted

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    19ea2f5 View commit details
    Browse the repository at this point in the history

  72. l2r_leaf_writer_ifthenelse

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    a74cccc View commit details
    Browse the repository at this point in the history

  73. test extraction of CBOR serializer

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    c9e131f View commit details
    Browse the repository at this point in the history

  74. write_header

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    430fac5 View commit details
    Browse the repository at this point in the history

  75. adjust proofs to new official Pulse slices

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    ac651f1 View commit details
    Browse the repository at this point in the history

  76. move lemmas to LowParse.Pulse

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    da4929e View commit details
    Browse the repository at this point in the history

  77. WIP serialize tagged

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    4caa9b9 View commit details
    Browse the repository at this point in the history

  78. compute_remaining_size combinators

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    6bd6456 View commit details
    Browse the repository at this point in the history

  79. extract the validator, the parser and the serializer

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    1c6683f View commit details
    Browse the repository at this point in the history

  80. towards sharing of Makefiles

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    367716a View commit details
    Browse the repository at this point in the history

  81. ignore response files

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    9a15bae View commit details
    Browse the repository at this point in the history

  82. recover build of lowparse/pulse

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    1b08afc View commit details
    Browse the repository at this point in the history

  83. use --ext context_pruning with new Makefiles

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    9b78c60 View commit details
    Browse the repository at this point in the history

  84. CI: install pulse, build lowparse/pulse

    @tahina-pro
    tahina-pro committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    2c3edcc View commit details
    Browse the repository at this point in the history

Commits on Oct 26, 2024

  1. also install Pulse to build the binary package (even though it's not … 

    …used yet)
    @tahina-pro
    tahina-pro committed Oct 26, 2024
    Configuration menu
    Copy the full SHA
    2ae077b View commit details
    Browse the repository at this point in the history

Commits on Oct 28, 2024

  1. fix standalone CI

    @tahina-pro
    tahina-pro committed Oct 28, 2024
    Configuration menu
    Copy the full SHA
    bfeaa30 View commit details
    Browse the repository at this point in the history

Commits on Oct 29, 2024

  1. (TEMP) use FStarLang/pulse#247

    @tahina-pro
    tahina-pro committed Oct 29, 2024
    Configuration menu
    Copy the full SHA
    3593766 View commit details
    Browse the repository at this point in the history

  2. remove slice_pair

    @tahina-pro
    tahina-pro committed Oct 29, 2024
    Configuration menu
    Copy the full SHA
    28f4e3b View commit details
    Browse the repository at this point in the history

Commits on Oct 30, 2024

  1. Revert "(TEMP) use FStarLang/pulse#247" 

    This reverts commit 3593766.
    @tahina-pro
    tahina-pro committed Oct 30, 2024
    Configuration menu
    Copy the full SHA
    848ec7a View commit details
    Browse the repository at this point in the history