From 821560ac1858f28a7cbf08cdf36897906406dd34 Mon Sep 17 00:00:00 2001
From: Oskar Goldhahn <oskar.goldhahn@ntnu.no>
Date: Fri, 7 Feb 2025 10:59:56 +0000
Subject: [PATCH] MVP

---
 tactics.md                 | 112 +------------------------------------
 tactics/ambient/ambient.md |   1 +
 tactics/ambient/idtac.md   |   5 ++
 tactics/tactics.md         |  95 +++++++++++++++++++++++++++++++
 4 files changed, 102 insertions(+), 111 deletions(-)
 create mode 100644 tactics/ambient/ambient.md
 create mode 100644 tactics/ambient/idtac.md
 create mode 100644 tactics/tactics.md

diff --git a/tactics.md b/tactics.md
index 278d49d..7cf8d2d 100644
--- a/tactics.md
+++ b/tactics.md
@@ -7,114 +7,4 @@ header-includes: |
           crossorigin="anonymous"></script>
 --- 
 
-## `proc`
-
-### Hoare version
-
-~~~ecblock
-filename: units/proc-hoare.ec
-~~~
-
-## `wp`
-
-### Hoare version
-
-~~~ecblock
-filename: units/wp-hoare.ec
-~~~
-
-## `while`
-
-### Hoare version
-
-~~~ecblock
-filename: units/while-hoare.ec
-~~~
-
-### PHoare version
-
-~~~ecblock
-filename: units/while-phoare.ec
-~~~
-
-## Others
-
- - `proc`
- - `proc <sformula>`
- - `proc <sformula> <sformula> <sformula>`
- - `proc '*'`
- - `wp <codepos1>`
- - `sp <codepos1>`
- - `skip`
- - `while [side] <winfos>`
- - `async while <awinfos>`
- - `call [side] <gpterm(call_info)>`
- - `call '/' <formula> <gpterm(call_info)>`
- - `rcondt [side] <codepos1>`
- - `rcondf [side] <codepos1>`
- - `seq [side] <tac_dir> <s_codepos1> ':' <formula | formula formula> <app_bd_info>`
- - `match [ident] [side] <codepos1>`
- - `if <ifoption>`
- - `match [side] [=]`
- - `swap <swap_info ',' ...>`
- - `interleave <interleave_info>`
- - `cfold [side] <codepos> ! <int>`
- - `cfold [side] <codepos>`
- - `rnd [side] <rnd_info> [: semrndpos]`
- - `rndsem ['*'] [side] <codepos1>`
- - `inline [side] [inlineopt] [occurences]`
- - `inline [side] [inlineopt] [occurences] <inlinepat1> [inlinepat...]`
- - `inline [side] [inlineopt] <codepos>`
- - `outline <side> '[' <codepos1> ['-' <codepos1>] ']' <outline_kind>`
- - `kill [side] <codepos>`
- - `kill [side] <codepos> '!' <uint>`
- - `kill [side] <codepos> '*' <uint>`
- - `case '<-' [side] <codepos>`
- - `alias [side] <codepos>`
- - `alias [side] <codepos> with <lident>`
- - `alias [side] <codepos> <lident> '=' <expression>`
- - `weakmem [side] <ipcore_name> <param_decl>`
- - `fission [side] <codepos> '@' <uint> ',' <uint>`
- - `fission [side] <codepos> '!' <uint> '@' <uint> ',' <uint>`
- - `fusion [side] <codepos> '@' <uint> ',' <uint>`
- - `fusion [side] <codepos> '!' <uint> '@' <uint> ',' <uint>`
- - `unroll ['for'] [side] <codepos>`
- - `splitwhile [side] <codepos> ':' <expression>`
- - `byphoare [gpterm(conseq)]`
- - `byehoare [gpterm(conseq)]`
- - `byequiv ['[' byequivopt ']'] [gpterm(conseq)]`
- - `byequiv ['[' byequivopt ']'] [gpterm(conseq)] ':' <sformula>`
- - `byupto`
- - `conseq '/' <sformula> <gopterm(conseq)>`
- - `conseq [cqoption]`
- - `conseq [cqoption] <gpterm(conseq_xt)>`
- - `conseq [cqoption] <gpterm(conseq_xt)> <gpterm(conseq_xt)> ['_']`
- - `conseq [cqoption] <gpterm(conseq_xt)> '_' <gpterm(conseq_xt)>`
- - `conseq [cqoption] <gpterm(conseq_xt)> <gpterm(conseq_xt)> <gpterm(conseq_xt)>`
- - `conseq [cqoption] '_' <gpterm(conseq_xt)> ['_']`
- - `conseq [cqoption] '_' '_' <gpterm(conseq_xt)>`
- - `conseq <crushmode>`
- - `elim '*'`
- - `exists '*' <sformula ',' ...>`
- - `exlim <sformula ',' ...>`
- - `ecall [side] '(' <qident> [tvars_app] <sformula...> ')'`
- - `exfalso`
- - `bypr`
- - `bypr <sformula> <sformula>`
- - `fel <codepos1> <sformula> <sformula> <sformula> <sformula> <fel_pred_specs> [sformula]`
- - `sim [crushmode] <eqobs_in>`
- - `replace <repl_kind> <repl_hyp> <repl_hyp>`
- - `replace '*' <repl_kind>`
- - `transitivity <trans_kind> <trans_hyp> <trans_hyp>`
- - `transitivity '*' <trans_hyp>`
- - `rewrite equiv '[' <side> <codepos1> <rwside> <pterm> [rweq_proc] ']'`
- - `symmetry`
- - `eager <eager_tac>`
- - `hoare`
- - `pr_bounded`
- - `phoare split <phoare_split>`
- - `phoare equiv <side> <sformula> <sformula>`
- - `auto`
- - `lossless`
- - `proc change [side] <codepos> ':' <sformula>`
- - `proc rewrite [side] <codepos> <pterm>`
+[Link to ad hoc documentation using markdown on github while we figure out which static website generator to use](https://www.github.com/EasyCrypt/ec-tactics/blob/tactics/tactics.md)
diff --git a/tactics/ambient/ambient.md b/tactics/ambient/ambient.md
new file mode 100644
index 0000000..ec8a9e6
--- /dev/null
+++ b/tactics/ambient/ambient.md
@@ -0,0 +1 @@
+[`idtac`](idtac.md)
\ No newline at end of file
diff --git a/tactics/ambient/idtac.md b/tactics/ambient/idtac.md
new file mode 100644
index 0000000..e6fa393
--- /dev/null
+++ b/tactics/ambient/idtac.md
@@ -0,0 +1,5 @@
+# Syntax
+`idtac`
+
+# Overview
+Does nothing. Useful when syntax demands a tactic, but you don't want it to do anything.
\ No newline at end of file
diff --git a/tactics/tactics.md b/tactics/tactics.md
new file mode 100644
index 0000000..8763005
--- /dev/null
+++ b/tactics/tactics.md
@@ -0,0 +1,95 @@
+---
+title: 'EasyCrypt tactics'
+header-includes: |
+  <script src="replay/replay.bundle.js"></script>
+  <script src="https://code.jquery.com/jquery-3.7.1.js"
+          integrity="sha256-eKhayi8LEQwp4NKxN+CfCh+3qOVUtJn3QNZ0TciWLP4="
+          crossorigin="anonymous"></script>
+--- 
+
+# Ambient Logic
+[Tactics](ambient/ambient.md)
+
+# Undocumented program (not ambient) logic tactics
+
+To be documented
+
+ - `proc`
+ - `proc <sformula>`
+ - `proc <sformula> <sformula> <sformula>`
+ - `proc '*'`
+ - `wp <codepos1>`
+ - `sp <codepos1>`
+ - `skip`
+ - `while [side] <winfos>`
+ - `async while <awinfos>`
+ - `call [side] <gpterm(call_info)>`
+ - `call '/' <formula> <gpterm(call_info)>`
+ - `rcondt [side] <codepos1>`
+ - `rcondf [side] <codepos1>`
+ - `seq [side] <tac_dir> <s_codepos1> ':' <formula | formula formula> <app_bd_info>`
+ - `match [ident] [side] <codepos1>`
+ - `if <ifoption>`
+ - `match [side] [=]`
+ - `swap <swap_info ',' ...>`
+ - `interleave <interleave_info>`
+ - `cfold [side] <codepos> ! <int>`
+ - `cfold [side] <codepos>`
+ - `rnd [side] <rnd_info> [: semrndpos]`
+ - `rndsem ['*'] [side] <codepos1>`
+ - `inline [side] [inlineopt] [occurences]`
+ - `inline [side] [inlineopt] [occurences] <inlinepat1> [inlinepat...]`
+ - `inline [side] [inlineopt] <codepos>`
+ - `outline <side> '[' <codepos1> ['-' <codepos1>] ']' <outline_kind>`
+ - `kill [side] <codepos>`
+ - `kill [side] <codepos> '!' <uint>`
+ - `kill [side] <codepos> '*' <uint>`
+ - `case '<-' [side] <codepos>`
+ - `alias [side] <codepos>`
+ - `alias [side] <codepos> with <lident>`
+ - `alias [side] <codepos> <lident> '=' <expression>`
+ - `weakmem [side] <ipcore_name> <param_decl>`
+ - `fission [side] <codepos> '@' <uint> ',' <uint>`
+ - `fission [side] <codepos> '!' <uint> '@' <uint> ',' <uint>`
+ - `fusion [side] <codepos> '@' <uint> ',' <uint>`
+ - `fusion [side] <codepos> '!' <uint> '@' <uint> ',' <uint>`
+ - `unroll ['for'] [side] <codepos>`
+ - `splitwhile [side] <codepos> ':' <expression>`
+ - `byphoare [gpterm(conseq)]`
+ - `byehoare [gpterm(conseq)]`
+ - `byequiv ['[' byequivopt ']'] [gpterm(conseq)]`
+ - `byequiv ['[' byequivopt ']'] [gpterm(conseq)] ':' <sformula>`
+ - `byupto`
+ - `conseq '/' <sformula> <gopterm(conseq)>`
+ - `conseq [cqoption]`
+ - `conseq [cqoption] <gpterm(conseq_xt)>`
+ - `conseq [cqoption] <gpterm(conseq_xt)> <gpterm(conseq_xt)> ['_']`
+ - `conseq [cqoption] <gpterm(conseq_xt)> '_' <gpterm(conseq_xt)>`
+ - `conseq [cqoption] <gpterm(conseq_xt)> <gpterm(conseq_xt)> <gpterm(conseq_xt)>`
+ - `conseq [cqoption] '_' <gpterm(conseq_xt)> ['_']`
+ - `conseq [cqoption] '_' '_' <gpterm(conseq_xt)>`
+ - `conseq <crushmode>`
+ - `elim '*'`
+ - `exists '*' <sformula ',' ...>`
+ - `exlim <sformula ',' ...>`
+ - `ecall [side] '(' <qident> [tvars_app] <sformula...> ')'`
+ - `exfalso`
+ - `bypr`
+ - `bypr <sformula> <sformula>`
+ - `fel <codepos1> <sformula> <sformula> <sformula> <sformula> <fel_pred_specs> [sformula]`
+ - `sim [crushmode] <eqobs_in>`
+ - `replace <repl_kind> <repl_hyp> <repl_hyp>`
+ - `replace '*' <repl_kind>`
+ - `transitivity <trans_kind> <trans_hyp> <trans_hyp>`
+ - `transitivity '*' <trans_hyp>`
+ - `rewrite equiv '[' <side> <codepos1> <rwside> <pterm> [rweq_proc] ']'`
+ - `symmetry`
+ - `eager <eager_tac>`
+ - `hoare`
+ - `pr_bounded`
+ - `phoare split <phoare_split>`
+ - `phoare equiv <side> <sformula> <sformula>`
+ - `auto`
+ - `lossless`
+ - `proc change [side] <codepos> ':' <sformula>`
+ - `proc rewrite [side] <codepos> <pterm>`