[Integration of Porridge] Generalized POR#19

Open

LCBH wants to merge 61 commits into

DeepSec-prover:masterfrom

Commits on Jan 22, 2018

import interface with Porridge from Apte's integration
Lucca Hirschi
committed

Commits on Jan 24, 2018

compilation Deepsec.expansed_process -> Porridge.process
Lucca Hirschi
committed
fix HEAD^1 (channels are constants)
Lucca Hirschi
committed
Merge branch 'master' into POR2
Lucca Hirschi
committed
first complete integration, need to fix action-selection though
Lucca Hirschi
committed
WIP: debug criterion for stopping explorations
Lucca Hirschi
committed
progress with argument trs, still a bug to fix
Lucca Hirschi
committed

Commits on Jan 25, 2018

fix the bug (missing calls to the continuation of f_next)
Lucca Hirschi
committed
trs should now be correctly propagated in the distributed mode
Lucca Hirschi
committed

Commits on Jan 26, 2018

[POR and distributed] POR options and hashtables are marshaled -> it works now
Lucca Hirschi
committed

Commits on Jan 27, 2018

no stats in distributed mode
Lucca Hirschi
committed
Add examples: feldhofer for different sizes
Lucca Hirschi
committed

Commits on Jan 28, 2018

Detect inpt of the form P'+Q ~ P and call Porridge on P~Q when
Lucca Hirschi
committed
Fix detection of inclusion verification.
Lucca Hirschi
committed
Disable detection_inclusion by default.
Lucca Hirschi
committed
added BAC examples
Lucca Hirschi
committed
Private Auth examples
Lucca Hirschi
committed
Script for launching benchmarks
Lucca Hirschi
committed
moving around scripts
Lucca Hirschi
committed
fix script: get version name
Lucca Hirschi
committed
launch_benchmark and extract_res work !!
Lucca Hirschi
committed
minors
Lucca Hirschi
committed
minors
Lucca Hirschi
committed
minor
Lucca Hirschi
committed
update data.py with more examples
Lucca Hirschi
committed

Commits on Jan 29, 2018

more sized for PA ANO and UK
Lucca Hirschi
committed
more sizes for BAC and BAC_FR
Lucca Hirschi
committed
fix typo in models of BAC
Lucca Hirschi
committed
add version without plus (when >= 4 agents, should be equivalent)
Lucca Hirschi
committed
Enforce limit on memory usage. Correct timing constraints.
Lucca Hirschi
committed
fix parsing of logs
Lucca Hirschi
committed
allow to fetch direct version of logs
Lucca Hirschi
committed
added PA version determinate
Lucca Hirschi
committed
feldhofer ANO and ANO+determinate
Lucca Hirschi
committed
update scripts
Lucca Hirschi
committed
Merge branch 'POR2-bench' of github.com:LCBH/deepsec into POR2-bench
Lucca Hirschi
committed
update scripts
Lucca Hirschi
committed
update scripts
Lucca Hirschi
committed

Commits on Jan 30, 2018

display stats for determinate as well
Lucca Hirschi
committed
Merge branch 'POR2-bench' of github.com:LCBH/deepsec into POR2-bench
Lucca Hirschi
committed
minor
Lucca Hirschi
committed
first set of benchmarks
Lucca Hirschi
committed
improved scripts (nb. explos, time without Porridge)
Lucca Hirschi
committed
Update bench without colors
Lucca Hirschi
committed
display both time
Lucca Hirschi
committed
print CSV
Lucca Hirschi
committed
Write CSV file with our benchs
Lucca Hirschi
committed
option for creating CSV and table auto
Lucca Hirschi
committed
resuls
Lucca Hirschi
committed

Commits on Jan 31, 2018

Address all warnings
Lucca Hirschi
committed
Merge branch 'POR2-bench' of github.com:LCBH/deepsec into POR2-bench
Lucca Hirschi
committed

Commits on Jul 23, 2018

Merge branch 'master' into POR2-bench
Lucca Hirschi
committed
remove benchmark utlities
Lucca Hirschi
committed
better help messages + rename POR2 -> generalized POR
Lucca Hirschi
committed
cleaning
Lucca Hirschi
committed
Update installation instructions
Lucca Hirschi
committed
Add Porride sources (v0.0.0).
Lucca Hirschi
committed
fix Porridge installation
Lucca Hirschi
committed
more cleaning
Lucca Hirschi
committed
fix a clash with Make targets for Porridge
Lucca Hirschi
committed
Remove nb. of explorations information when POR gen. is disabled
Lucca Hirschi
committed