mirror of
https://github.com/rosenpass/rosenpass.git
synced 2026-02-28 06:23:08 -08:00
65 lines
2.9 KiB
Markdown
65 lines
2.9 KiB
Markdown
# TODO for the project of rewriting Marzipan
|
|
|
|
## Done
|
|
|
|
* ~~figure out why ProVerif is started on the non-processed mpv file~~
|
|
* ~~rework rebound warnings (`clean_warnings` Bash function)~~
|
|
```bash
|
|
rosenpass$ rosenpass-marzipan run-proverif target/proverif/03_identity_hiding_responder.entry.o.pv target/proverif/03_identity_hiding_responder.entry.log
|
|
```
|
|
* ~~provide log parameter to `rosenpass-marzipan`-call~~ (no, it was intentionally not used)
|
|
* ~~cpp pre-processing stuff~~
|
|
* ~~awk pre-processing stuff~~
|
|
* ~~`pretty_output` Bash function~~
|
|
* ~~pretty_output_line~~
|
|
* ~~click function intervention weirdness~~
|
|
* ~~why is everything red in the pretty output? (see line 96 in __init__.py)~~
|
|
* ~~awk RESULT flush in marzipan()~~
|
|
* ~~move the whole metaverif function to Python~~
|
|
* ~move the whole analyze function to Python~
|
|
* ~find the files~
|
|
* ~start subprocesses in parallel~
|
|
* ~wait for them to finish~
|
|
* ~~rebase from main~~
|
|
* ~~see if we still need the `extra_args is None` check in `_run_proverif`~`
|
|
* ~~set colors differently to prevent injection attack~~
|
|
* ~~by calling a function~~
|
|
* ~~by prepared statements~~
|
|
* ~~standalone function parse_result_line is no longer necessary~~
|
|
* ~~is the clean function still necessary?~~
|
|
* ~~implement better main function for click~~
|
|
* ~~why does analyze fail when the target/proverif directory is not empty?~~
|
|
* ~~return an exit status that is meaningful for CI~~
|
|
* ~~exception handling in analyze() and in run_proverif()~~
|
|
* ~~refactor filtering in run_proverif (see karo's comment)~~
|
|
* ~configurable target directory~
|
|
* ~lark parser: multiline comments, how???~
|
|
|
|
## Next Steps
|
|
|
|
* integrate marzipan.awk into Python, somehow
|
|
* options term special cases (c.f. manual page 133, starting with "fun" term)
|
|
* complete with CryptoVerif options
|
|
* error when trying with: `nix run .# -- parse ../target/proverif/01_secrecy.entry.i.pv`
|
|
* `in(C, Cinit_conf(Ssskm, Spsk, Sspkt, ic));`
|
|
* ^
|
|
* rewrite marzipan.awk into Python/LARK
|
|
* define a LARK grammar for marzipan.awk rules
|
|
* write python code for processing marzipan rules, e.g. alias replacement (step: i.pv->o.pv)
|
|
* do not assume that the repo path has subdir marzipan
|
|
* do not assume that the repo path has subdir analysis
|
|
* rewrite cpp into Python/LARK (step: mpv->i.pv)
|
|
* integrate the Nix flake into the main Nix flake
|
|
* pull the gawk dependency into the Nix flake
|
|
* think about next steps
|
|
* integrate this upstream, into the CI?
|
|
* “make it beautiful” steps? more resiliency to working directory?
|
|
* rewrite our awk usages into Python/…?
|
|
* yes, possibly as extension to the LARK grammar
|
|
* and rewrite the AST within Python
|
|
* reconstruct ProVerif input file for ProVerif
|
|
* rewrite our CPP usages into Python/…?
|
|
* low priority: nested comments in ProVerif code
|
|
|
|
“it replaces the Bash script and is idiomatic Python code”
|