diff --git a/cmd/vplogic/libcoq.go b/cmd/vplogic/libcoq.go
new file mode 100644
index 0000000..48f4e7e
--- /dev/null
+++ b/cmd/vplogic/libcoq.go
@@ -0,0 +1,1725 @@
+/* SPDX-FileCopyrightText: © 2019-2022 Nadim Kobeissi <nadim@symbolic.software>
+ * SPDX-License-Identifier: GPL-3.0-only */
+// 806d8db3ce9f3ded40fd35fdba02fb84
+
+package vplogic
+
+import "strings"
+
+var libcoq = strings.Join([]string{
+	"Require Import Coq.Lists.List Coq.Bool.Bool Coq.Arith.PeanoNat",
+	"        Lia Coq.Strings.String.",
+	"        Import ListNotations.",
+	"",
+	"Inductive generator :=",
+	"| G.",
+	"",
+	"Inductive guard_status: Type :=",
+	"| guarded",
+	"| unguarded.",
+	"",
+	"Inductive constant : Type :=",
+	"| Nil",
+	"| cnstn : string -> constant",
+	"with primitive : Type :=",
+	"| ENC : value -> value -> primitive",
+	"| DEC : value -> value -> primitive",
+	"| AEAD_ENC : value -> value -> value -> primitive",
+	"| AEAD_DEC : value -> value -> value -> primitive",
+	"| PKE_ENC : value -> value -> primitive",
+	"| PKE_DEC : value -> value -> primitive",
+	"| HASH1 : value -> primitive",
+	"| HASH2 : value -> value -> primitive",
+	"| HASH3 : value -> value -> value -> primitive",
+	"| HASH4 : value -> value -> value -> value -> primitive",
+	"| HASH5 : value -> value -> value -> value -> value -> primitive",
+	"| MAC : value -> value -> primitive",
+	"| HKDF1: value -> value -> value -> primitive",
+	"| HKDF2: value -> value -> value -> primitive",
+	"| HKDF3: value -> value -> value -> primitive",
+	"| HKDF4: value -> value -> value -> primitive",
+	"| HKDF5: value -> value -> value -> primitive",
+	"| PW_HASH1 : value -> primitive",
+	"| PW_HASH2 : value -> value -> primitive",
+	"| PW_HASH3 : value -> value -> value -> primitive",
+	"| PW_HASH4 : value -> value -> value -> value -> primitive",
+	"| PW_HASH5 : value -> value -> value -> value -> value -> primitive",
+	"| SIGN: value -> value -> primitive",
+	"| SIGNVERIF: value -> value -> value -> primitive",
+	"| RINGSIGN: value -> value -> value -> value -> primitive",
+	"| RINGSIGNVERIF: value -> value -> value -> value -> value -> primitive",
+	"| BLIND: value -> value -> primitive",
+	"| UNBLIND: value -> value -> value -> primitive",
+	"| SHAMIR_SPLIT1: value -> primitive",
+	"| SHAMIR_SPLIT2: value -> primitive",
+	"| SHAMIR_SPLIT3: value -> primitive",
+	"| SHAMIR_JOIN: value -> value -> primitive",
+	"| CONCAT2 : value -> value -> primitive",
+	"| CONCAT3 : value -> value -> value -> primitive",
+	"| CONCAT4 : value -> value -> value -> value -> primitive",
+	"| CONCAT5 : value -> value -> value -> value -> value -> primitive",
+	"| SPLIT1: value -> primitive",
+	"| SPLIT2: value -> primitive",
+	"| SPLIT3: value -> primitive",
+	"| SPLIT4: value -> primitive",
+	"| SPLIT5: value -> primitive",
+	"  with equation : Type :=",
+	"| PUBKEY : generator -> value -> equation",
+	"| DH : generator -> value -> value -> equation",
+	"  with value : Type :=",
+	"| pass : constant -> value",
+	"| const : constant -> value ",
+	"| eq : equation -> value",
+	"| prim : primitive -> value",
+	"| default.",
+	"",
+	"Inductive qualifier : Type :=",
+	"| public",
+	"| private.",
+	"",
+	"Inductive declaration : Type :=",
+	"| assignment",
+	"| generation",
+	"| knowledge.",
+	"",
+	"Inductive leak_status : Type :=",
+	"| leaked",
+	"| unleaked.",
+	"",
+	"Inductive expression : Type :=",
+	"| EXP: declaration -> qualifier -> value -> leak_status -> expression.",
+	"",
+	"(* if qualifier = public -> can learn*)",
+	"(* if leak_status = leaked -> can learn*)",
+	"(* if sent over the wire -> can learn*)",
+	"(* when learning, need to check if attacker already knows equivalent value,",
+	"    but maybe this isn't necessary *)",
+	"",
+	"(* ",
+	"Variable enc_dec :",
+	"  forall (k m : value), DEC k (ENC k m) = m. *)",
+	"",
+	"(* It has no axioms attached to Hash *)",
+	"",
+	"(* ",
+	"",
+	"Variable pke_enc_correcntess : ",
+	"   PKE_DEC k (PKE_ENC((PUBKEY G k), m)) = m *)",
+	"",
+	"(* Variable public : value -> Prop.",
+	"Variable encryption_constructor : value -> value -> value.",
+	"Variable hash_constructor : value -> value. *)",
+	"",
+	"Inductive knows : value -> Type :=",
+	"(*equations*)",
+	"| public_key_generation (a ga: value) : knows a -> ga = (eq(PUBKEY G a)) -> knows ga",
+	"| dh_agreement_primitive (ga b a gab: value) (p: primitive): knows ga -> ga = ",
+	"  (eq(PUBKEY G a)) -> knows b -> b = prim p -> gab = (eq(DH G a b)) -> knows gab",
+	"| dh_agreement_constant (ga b a gab: value) (c: constant): knows ga -> ga = ",
+	"  eq(PUBKEY G a) -> knows b -> b = const c -> gab = (eq(DH G a b)) -> knows gab",
+	"(*core primitives*)    ",
+	"      (* todo: assert*)",
+	"| concat2_constructor (a b out: value) : knows a -> knows b -> out = prim(CONCAT2 a b)",
+	"  -> knows out",
+	"| concat2_corerule_one (val a b : value) : knows val -> val = prim (CONCAT2 a b) -> knows a",
+	"| concat2_corerule_two (val a b : value) : knows val -> val = prim (CONCAT2 a b) -> knows b",
+	"",
+	"| concat3_constructor (a b c out: value) : knows a -> knows b -> knows c",
+	"  -> out = prim(CONCAT3 a b c) -> knows out",
+	"| concat3_corerule_one (val a b c : value) : knows val -> val = prim (CONCAT3 a b c) -> knows a",
+	"| concat3_corerule_two (val a b c : value) : knows val -> val = prim (CONCAT3 a b c) -> knows b",
+	"| concat3_corerule_three (val a b c : value) : knows val -> val = prim (CONCAT3 a b c) -> knows c",
+	"",
+	"| concat4_constructor (a b c d out: value) : knows a -> knows b -> knows c -> knows d",
+	"  -> out = prim(CONCAT4 a b c d) -> knows out",
+	"| concat4_corerule_one (val a b c d: value) : knows val -> val = prim (CONCAT4 a b c d) -> knows a",
+	"| concat4_corerule_two (val a b c d: value) : knows val -> val = prim (CONCAT4 a b c d) -> knows b",
+	"| concat4_corerule_three (val a b c d: value) : knows val -> val = prim (CONCAT4 a b c d) -> knows c",
+	"| concat4_corerule_four (val a b c d: value) : knows val -> val = prim (CONCAT4 a b c d) -> knows d",
+	"",
+	"| concat5_constructor (a b c d e out: value) : knows a -> knows b -> knows c -> knows d -> knows e",
+	"  -> out = prim(CONCAT5 a b c d e) -> knows out",
+	"| concat5_corerule_one (val a b c d e: value) : knows val -> val = prim (CONCAT5 a b c d e) -> knows a",
+	"| concat5_corerule_two (val a b c d e: value) : knows val -> val = prim (CONCAT5 a b c d e) -> knows b",
+	"| concat5_corerule_three (val a b c d e: value) : knows val -> val = prim (CONCAT5 a b c d e) -> knows c",
+	"| concat5_corerule_four (val a b c d e: value) : knows val -> val = prim (CONCAT5 a b c d e) -> knows d",
+	"| concat5_corerule_fives (val a b c d e: value) : knows val -> val = prim (CONCAT5 a b c d e) -> knows e",
+	"",
+	"(*hashing primitives*)",
+	"| hash1_constructor (a out: value) : knows a -> out = prim(HASH1 a) -> knows out",
+	"| hash2_constructor (a b out: value) : knows a -> knows b -> out = prim(HASH2 a b) -> knows out",
+	"| hash3_constructor (a b c out: value) : knows a -> knows b -> knows c -> out = prim(HASH3 a b c) -> knows out",
+	"| hash4_constructor (a b c d out: value) : knows a -> knows b -> knows c -> knows d -> out = prim(HASH4 a b c d) -> knows out",
+	"| hash5_constructor (a b c d e out: value) : knows a -> knows b -> knows c -> knows d -> knows e -> out = prim(HASH5 a b c d e) -> knows out",
+	"| mac_constructor (a b out: value) : knows a -> knows b -> out = prim(MAC a b) -> knows out",
+	"| hkdf1_constructor (salt ikm info out: value) : knows salt -> knows ikm -> knows info",
+	"  -> out = prim(HKDF1 salt ikm info) -> knows out",
+	"| hkdf2_constructor (salt ikm info out: value) : knows salt -> knows ikm -> knows info",
+	"  -> out = prim(HKDF2 salt ikm info) -> knows out",
+	"| hkdf3_constructor (salt ikm info out: value) : knows salt -> knows ikm -> knows info",
+	"  -> out = prim(HKDF3 salt ikm info) -> knows out",
+	"| hkdf4_constructor (salt ikm info out: value) : knows salt -> knows ikm -> knows info",
+	"  -> out = prim(HKDF4 salt ikm info) -> knows out",
+	"| hkdf5_constructor (salt ikm info out: value) : knows salt -> knows ikm -> knows info",
+	"  -> out = prim(HKDF5 salt ikm info) -> knows out",
+	"  |pw_hash1_constructor (a out: value) : knows a -> out = prim(PW_HASH1 a) -> knows out",
+	"  |pw_hash2_constructor (a b out: value) : knows a -> knows b -> out = prim(PW_HASH2 a b) -> knows out",
+	"  |pw_hash3_constructor (a b c out: value) : knows a -> knows b -> knows c -> out = prim(PW_HASH3 a b c) -> knows out",
+	"  |pw_hash4_constructor (a b c d out: value) : knows a -> knows b -> knows c -> knows d -> out = prim(PW_HASH4 a b c d) -> knows out",
+	"  |pw_hash5_constructor (a b c d e out: value) : knows a -> knows b -> knows c -> knows d -> knows e -> out = prim(PW_HASH5 a b c d e) -> knows out",
+	"",
+	"(*encryption primitives*)",
+	"    (*symmetric encryption*)",
+	"| enc_constructor (k m out: value) : knows k -> knows m -> out = prim(ENC k m) -> knows out",
+	"| enc_decomposerule (k c m : value) : knows k -> knows c -> c = prim(ENC k m) -> knows m",
+	"| dec_constructor (k c m out: value) : knows k -> knows c -> c = prim(ENC k m)",
+	"  -> out = prim(DEC k c) -> knows out",
+	"| dec_rewriterule (c k m: value) : knows c -> c = prim(DEC k (prim(ENC k m))) -> knows m",
+	"    (*authenticated encryption with additional data*)",
+	"| aead_enc_constructor (k m ad out: value) : knows k -> knows m -> knows ad",
+	"   -> out = prim(AEAD_ENC k m ad) -> knows out",
+	"| aead_enc_decomposerule (k c ad m: value): knows k -> knows c -> c = prim(AEAD_ENC k m ad)",
+	"  -> knows ad -> knows m",
+	"    (*public key encryption*)",
+	"| pke_enc_constructor (gk m k out: value): knows gk -> gk = eq(PUBKEY G k) -> knows m",
+	"  -> out = prim(PKE_ENC gk m) -> knows out",
+	"| pke_enc_decomposerule (k c gk m: value): knows k -> knows gk -> gk = eq(PUBKEY G k)",
+	"  -> knows c -> c = prim(PKE_ENC gk m) -> knows m",
+	"| pke_dec_constructor(k c gk m out: value): knows k -> knows c -> c = prim(PKE_ENC gk m)",
+	"  -> out = prim(PKE_DEC k (prim(PKE_ENC gk m))) -> knows out",
+	"| pke_dec_rewriterule(c k m: value): knows c -> c = prim(PKE_DEC k (prim(PKE_ENC (eq(PUBKEY G k))m)))",
+	"  -> knows m",
+	"",
+	"(*signature primitives*)",
+	"    (*classical digital signatures*)",
+	"| sign_constructor(k m out: value): knows k -> knows m -> out = prim(SIGN k m) -> knows out",
+	"| signverif_constructor(gk m s k out: value): knows gk -> gk = eq(PUBKEY G k) -> knows m -> knows s -> ",
+	"  s = prim(SIGN k m) -> out = prim(SIGNVERIF gk m s) -> knows out",
+	"| signverif_rewriterule(val k m s: value): knows val -> val = prim(SIGNVERIF (eq(PUBKEY G k)) m (prim(SIGN k m))) -> knows m",
+	"",
+	"    (*ring signatures*)",
+	"| ringsign_constructor(ka gkb gkc m kb kc out: value): knows ka -> knows gkb -> gkb = eq(PUBKEY G kb) ->",
+	"    knows gkc -> gkc = eq(PUBKEY G kc) -> knows m -> out = prim(RINGSIGN ka gkb gkc m) -> knows out",
+	"",
+	"      (*unsure about ringsignverif*)",
+	"      (*todo: ringsignverif_constructor*)",
+	"| ringsignverif_constructor(gka gkb gkc m s out ka kb kc: value): knows gka -> gka = eq(PUBKEY G ka)",
+	"  -> knows gkb -> gkb = eq(PUBKEY G kb) -> knows gkc -> gkc = eq(PUBKEY G kc) -> knows m",
+	"    -> knows s -> s = prim(RINGSIGN ka gkb gkc m) -> out = prim(RINGSIGNVERIF gka gkb gkc m s) -> knows out",
+	"| ringsignverif_rewriterule(gka gkb gkc m s ka kb kc: value): knows gka -> gka = eq(PUBKEY G ka) -> knows gkb -> gkb = eq(PUBKEY G kb)",
+	"  -> knows gkc -> gkc = eq(PUBKEY G kc) -> knows m -> knows s -> s = prim(RINGSIGN ka gkb gkc m) -> knows m",
+	"",
+	"    (*blind signatures*)",
+	"| blind_constructor(k m out: value): knows k -> knows m -> out = prim(BLIND k m) -> knows out",
+	"| blind_decomposerule(k b m: value): knows k -> knows b -> b = prim(BLIND k m) -> knows m",
+	"| unblind_constructor(k m s a out: value): knows k -> knows m -> knows s -> ",
+	"  s = prim(SIGN a (prim(BLIND k m))) -> out = prim(UNBLIND k m s) -> knows out",
+	"| unblind_rewriterule(u k m a out: value): knows u ->",
+	"  u = prim(UNBLIND k m (prim(SIGN a (prim(BLIND k m))))) -> out = prim(SIGN a m) -> knows out",
+	"",
+	"(*secret sharing*)",
+	"    (*unsure about shamir_split/shamir_join*)",
+	"| shamir_split1_constructor(k out: value): knows k -> out = prim(SHAMIR_SPLIT1 k) -> knows out",
+	"| shamir_split2_constructor(k out: value): knows k -> out = prim(SHAMIR_SPLIT2 k) -> knows out",
+	"| shamir_split3_constructor(k out: value): knows k -> out = prim(SHAMIR_SPLIT3 k) -> knows out",
+	"  (*todo: shamir_split_recomposerule*)",
+	"  (*todo: shamir_join_constructor*)",
+	"  (*todo: shamir_join_rebuildrule*).",
+	"",
+	"Lemma concat2_rule : forall (a b val : value),",
+	"    knows val -> val = prim (CONCAT2 a b) ->",
+	"    (knows a * knows b)%type.",
+	"Proof using.",
+	"  intros a b val Hk Hv.",
+	"  pose proof (concat2_corerule_one _ _ _ Hk Hv).",
+	"  pose proof (concat2_corerule_two _ _ _ Hk Hv).",
+	"  auto.",
+	"Qed.",
+	"",
+	"Lemma concat2_cons_rule : forall  (a b val : value), knows a -> knows b -> val = prim (CONCAT2 a b) ->",
+	"                                               knows val.",
+	"Proof using.",
+	"  intros.  apply concat2_constructor with (a := a) (b := b); assumption.",
+	"Qed.",
+	"",
+	"Theorem insecure : forall (a c m k : value), knows c -> knows a -> k = prim (HASH1 a) ->",
+	"                                        c = prim (ENC k m) -> knows m.",
+	"Proof using.",
+	"  intros.",
+	"  pose proof (hash1_constructor _ _ H0 H1).",
+	"  apply enc_decomposerule with (k := k) (c := c); assumption.",
+	"Qed.",
+	"",
+	"  (* the task is to come up with natural deduction style rules for \"knows\"*)",
+	"",
+	"Fixpoint value_beq (v1 v2: value) : bool := ",
+	"  match v1, v2 with",
+	"    | const c1, const c2 => match c1, c2 with",
+	"        | cnstn a, cnstn a' => eqb a a'",
+	"        | Nil, Nil => true",
+	"        | _, _ => false",
+	"      end",
+	"    | eq e1, eq e2 => match e1, e2 with",
+	"        | PUBKEY g1 k1, PUBKEY g2 k2 => value_beq k1 k2",
+	"        | DH _ exp1 exp2, DH _ exp1' exp2' => ((value_beq exp1 exp1') && (value_beq exp2 exp2')) || ((value_beq exp1 exp2') && (value_beq exp2 exp1'))",
+	"        | _, _ => false",
+	"      end",
+	"    | prim p1, prim p2 => match p1, p2 with",
+	"        | ENC k1 m1, ENC k2 m2 => (value_beq k1 k2) && (value_beq m1 m2)",
+	"        | DEC k1 e1, DEC k2 e2 => (value_beq k1 k2) && (value_beq e1 e2)",
+	"        | AEAD_ENC k1 m1 ad1, AEAD_ENC k2 m2 ad2 => ((value_beq k1 k2) && (value_beq m1 m2)) && (value_beq ad1 ad2)",
+	"        | AEAD_DEC k1 e1 ad1, AEAD_DEC k2 e2 ad2 => ((value_beq k1 k2) && (value_beq e1 e2)) && (value_beq ad1 ad2)",
+	"        | PKE_ENC gk1 m1, PKE_ENC gk2 m2 => (value_beq gk1 gk2) && (value_beq m1 m2)",
+	"        | PKE_DEC k1 e1, PKE_DEC k2 e2 => (value_beq k1 k2) && (value_beq e1 e2)",
+	"        | HASH1 a1, HASH1 a2 => value_beq a1 a2",
+	"        | HASH2 a1 b1, HASH2 a2 b2 => (value_beq a1 a2) && (value_beq b1 b2)",
+	"        | HASH3 a1 b1 c1, HASH3 a2 b2 c2 => ((value_beq a1 a2) && (value_beq b1 b2)) && (value_beq c1 c2)",
+	"        | HASH4 a1 b1 c1 d1, HASH4 a2 b2 c2 d2 => ((value_beq a1 a2) && (value_beq b1 b2)) && ((value_beq c1 c2) && (value_beq d1 d2))",
+	"        | HASH5 a1 b1 c1 d1 e1, HASH5 a2 b2 c2 d2 e2 => (((value_beq a1 a2) && (value_beq b1 b2)) && ((value_beq c1 c2) && (value_beq d1 d2))) && (value_beq e1 e2)",
+	"        | MAC a1 b1, MAC a2 b2 => (value_beq a1 a2) && (value_beq b1 b2)",
+	"        | HKDF1 s1 k1 i1, HKDF1 s2 k2 i2 => ((value_beq s1 s2) && (value_beq k1 k2)) && (value_beq i1 i2)",
+	"        | HKDF2 s1 k1 i1, HKDF2 s2 k2 i2 => ((value_beq s1 s2) && (value_beq k1 k2)) && (value_beq i1 i2)",
+	"        | HKDF3 s1 k1 i1, HKDF3 s2 k2 i2 => ((value_beq s1 s2) && (value_beq k1 k2)) && (value_beq i1 i2)",
+	"        | HKDF4 s1 k1 i1, HKDF4 s2 k2 i2 => ((value_beq s1 s2) && (value_beq k1 k2)) && (value_beq i1 i2)",
+	"        | HKDF5 s1 k1 i1, HKDF5 s2 k2 i2 => ((value_beq s1 s2) && (value_beq k1 k2)) && (value_beq i1 i2)",
+	"        | PW_HASH1 a1, PW_HASH1 a2 => value_beq a1 a2",
+	"        | PW_HASH2 a1 b1, PW_HASH2 a2 b2 => (value_beq a1 a2) && (value_beq b1 b2)",
+	"        | PW_HASH3 a1 b1 c1, PW_HASH3 a2 b2 c2 => ((value_beq a1 a2) && (value_beq b1 b2)) && (value_beq c1 c2)",
+	"        | PW_HASH4 a1 b1 c1 d1, PW_HASH4 a2 b2 c2 d2 => ((value_beq a1 a2) && (value_beq b1 b2)) && ((value_beq c1 c2) && (value_beq d1 d2))",
+	"        | PW_HASH5 a1 b1 c1 d1 e1, PW_HASH5 a2 b2 c2 d2 e2 => (((value_beq a1 a2) && (value_beq b1 b2)) && ((value_beq c1 c2) && (value_beq d1 d2))) && (value_beq e1 e2)",
+	"        | SIGN k1 m1, SIGN k2 m2 => (value_beq k1 k2) && (value_beq m1 m2)",
+	"        | SIGNVERIF gk m s, SIGNVERIF gk' m' s' => ((value_beq gk gk') && (value_beq m m')) && (value_beq s s')",
+	"        | RINGSIGN ka1 gkb1 gkc1 m1, RINGSIGN ka2 gkb2 gkc2 m2 => ((value_beq ka1 ka2) && (value_beq gkb1 gkb2)) && (",
+	"          (value_beq gkc1 gkc2) && (value_beq m1 m2))",
+	"        | RINGSIGNVERIF gka1 gkb1 gkc1 m1 s1, RINGSIGNVERIF gka2 gkb2 gkc2 m2 s2 => ",
+	"          (((value_beq gka1 gka2) && (value_beq gkb1 gkb2)) && ((value_beq gkc1 gkc2) && (value_beq m1 m2))) && (value_beq s1 s2)",
+	"        | SHAMIR_SPLIT1 k1, SHAMIR_SPLIT1 k2 => value_beq k1 k2",
+	"        | SHAMIR_SPLIT2 k1, SHAMIR_SPLIT2 k2 => value_beq k1 k2",
+	"        | SHAMIR_SPLIT3 k1, SHAMIR_SPLIT3 k2 => value_beq k1 k2",
+	"        | SHAMIR_JOIN sa1 sb1, SHAMIR_JOIN sa2 sb2 => (value_beq sa1 sa2) && (value_beq sb1 sb2)",
+	"        | CONCAT2 a1 b1, CONCAT2 a2 b2 => (value_beq a1 a2) && (value_beq b1 b2)",
+	"        | CONCAT3 a1 b1 c1, CONCAT3 a2 b2 c2 => ((value_beq a1 a2) && (value_beq b1 b2)) && (value_beq c1 c2)",
+	"        | CONCAT4 a1 b1 c1 d1, CONCAT4 a2 b2 c2 d2 => ((value_beq a1 a2) && (value_beq b1 b2)) && ((value_beq c1 c2) && (value_beq d1 d2))",
+	"        | CONCAT5 a1 b1 c1 d1 e1, CONCAT5 a2 b2 c2 d2 e2 => (((value_beq a1 a2) && (value_beq b1 b2)) && ((value_beq c1 c2) && (value_beq d1 d2))) && (value_beq e1 e2)",
+	"        | SPLIT1 a1, SPLIT1 a2 => value_beq a1 a2",
+	"        | SPLIT2 a1, SPLIT2 a2 => value_beq a1 a2",
+	"        | SPLIT3 a1, SPLIT3 a2 => value_beq a1 a2",
+	"        | SPLIT4 a1, SPLIT4 a2 => value_beq a1 a2",
+	"        | SPLIT5 a1, SPLIT5 a2 => value_beq a1 a2",
+	"        | _, _ => false",
+	"      end",
+	"    | pass a, pass b => match a, b with",
+	"        | cnstn a, cnstn b => eqb a b",
+	"        | Nil, Nil => true",
+	"        | _ , _ => false",
+	"      end",
+	"    | default, default => true",
+	"    | _, _ => false",
+	"  end.",
+	"",
+	"Fixpoint has_nested_value (main v: value) : bool :=",
+	"    match main with",
+	"    | default => false",
+	"    | const _ => value_beq v main",
+	"    | pass _ => value_beq v main",
+	"    | eq e => match e with",
+	"        | PUBKEY _ exp => has_nested_value exp v",
+	"        | DH _ exp1 exp2 => (has_nested_value exp1 v) || (has_nested_value exp2 v)",
+	"      end",
+	"    | prim p => match p with",
+	"        | ENC k m => (has_nested_value k v) || (has_nested_value m v)",
+	"        | DEC k c => (has_nested_value k v) || (has_nested_value c v)",
+	"        | AEAD_ENC k m ad => ((has_nested_value k v) || (has_nested_value m v)) || (has_nested_value ad v)",
+	"        | AEAD_DEC k c ad => ((has_nested_value k v) || (has_nested_value c v)) || (has_nested_value ad v)",
+	"        | PKE_ENC gk m => (has_nested_value gk v) || (has_nested_value m v)",
+	"        | PKE_DEC k m => (has_nested_value k v) || (has_nested_value m v)",
+	"        | HASH1 a => has_nested_value a v",
+	"        | HASH2 a b => (has_nested_value a v) || (has_nested_value b v)",
+	"        | HASH3 a b c => ((has_nested_value a v) || (has_nested_value b v)) || (has_nested_value c v)",
+	"        | HASH4 a b c d => ((has_nested_value a v) || (has_nested_value b v)) || ((has_nested_value c v) || (has_nested_value d v))",
+	"        | HASH5 a b c d e => ((has_nested_value a v) || (has_nested_value b v)) || ((has_nested_value c v) || (has_nested_value d v)) || (has_nested_value e v)",
+	"        | MAC a b => (has_nested_value a v) || (has_nested_value b v)",
+	"        | HKDF1 s k i => ((has_nested_value s v) || (has_nested_value k v)) || (has_nested_value i v)",
+	"        | HKDF2 s k i => ((has_nested_value s v) || (has_nested_value k v)) || (has_nested_value i v)",
+	"        | HKDF3 s k i => ((has_nested_value s v) || (has_nested_value k v)) || (has_nested_value i v)",
+	"        | HKDF4 s k i => ((has_nested_value s v) || (has_nested_value k v)) || (has_nested_value i v)",
+	"        | HKDF5 s k i => ((has_nested_value s v) || (has_nested_value k v)) || (has_nested_value i v)",
+	"        | PW_HASH1 a => has_nested_value a v",
+	"        | PW_HASH2 a b => (has_nested_value a v) || (has_nested_value b v)",
+	"        | PW_HASH3 a b c => ((has_nested_value a v) || (has_nested_value b v)) || (has_nested_value c v)",
+	"        | PW_HASH4 a b c d => ((has_nested_value a v) || (has_nested_value b v)) || ((has_nested_value c v) || (has_nested_value d v))",
+	"        | PW_HASH5 a b c d e => ((has_nested_value a v) || (has_nested_value b v)) || ((has_nested_value c v) || (has_nested_value d v)) || (has_nested_value e v)",
+	"        | SIGN k m => (has_nested_value k v) || (has_nested_value m v)",
+	"        | SIGNVERIF k m s => ((has_nested_value k v) || (has_nested_value m v)) || (has_nested_value s v)",
+	"        | RINGSIGN ka gkb gkc m => ((has_nested_value ka v) || (has_nested_value gkb v)) || ((has_nested_value gkc v) || (has_nested_value m v))",
+	"        | RINGSIGNVERIF ka gkb gkc m s => ((has_nested_value ka v) || (has_nested_value gkb v)) || ((has_nested_value gkc v) || (has_nested_value m v)) || (has_nested_value s v)",
+	"        | BLIND k m => (has_nested_value k v) || (has_nested_value m v)",
+	"        | UNBLIND k m s => ((has_nested_value k v) || (has_nested_value m v)) || (has_nested_value s v)  ",
+	"        | SHAMIR_SPLIT1 k => has_nested_value k v",
+	"        | SHAMIR_SPLIT2 k => has_nested_value k v",
+	"        | SHAMIR_SPLIT3 k => has_nested_value k v",
+	"        | SHAMIR_JOIN sa sb => (has_nested_value sa v) || (has_nested_value sb v)",
+	"        | CONCAT2 a b => (has_nested_value a v) || (has_nested_value b v)",
+	"        | CONCAT3 a b c => ((has_nested_value a v) || (has_nested_value b v)) || (has_nested_value c v)",
+	"        | CONCAT4 a b c d => ((has_nested_value a v) || (has_nested_value b v)) || ((has_nested_value c v) || (has_nested_value d v))",
+	"        | CONCAT5 a b c d e => ((has_nested_value a v) || (has_nested_value b v)) || ((has_nested_value c v) || (has_nested_value d v)) || (has_nested_value e v)",
+	"        | SPLIT1 a => has_nested_value a v",
+	"        | SPLIT2 a => has_nested_value a v",
+	"        | SPLIT3 a => has_nested_value a v",
+	"        | SPLIT4 a => has_nested_value a v",
+	"        | SPLIT5 a => has_nested_value a v",
+	"      end",
+	"  end.",
+	"Definition is_primitive (v: value): bool :=",
+	"  match v with",
+	"    | prim p => true",
+	"    | _ => false",
+	"  end.",
+	"",
+	"Definition is_constant (v: value): bool :=",
+	"  match v with",
+	"    | const c => true",
+	"    | _ => false",
+	"  end.",
+	"",
+	"Definition is_equation (v: value): bool :=",
+	"  match v with",
+	"    | eq e => true",
+	"    | _ => false",
+	"  end.",
+	"",
+	"Fixpoint shallow_search (l: list value) (v: value) : bool :=",
+	"    match l with",
+	"    | [] => false",
+	"    | h :: t => match value_beq h v with",
+	"        | true => true",
+	"        | false => shallow_search t v",
+	"      end",
+	"  end.",
+	"",
+	"Definition deep_search (l : list value) (v : value) := filter (fun x => has_nested_value x v) l.",
+	"Fixpoint remove_value_list (l: list value) (v: value) : list value :=",
+	"  match l with",
+	"      | [] => []",
+	"      | h :: t => match value_beq h v with ",
+	"          | true => t",
+	"          | false => [h] ++ (remove_value_list t v)",
+	"        end",
+	"    end.",
+	"",
+	"Fixpoint merge_lists (l1 l2: list value) : list value :=",
+	"  match l1 with",
+	"      | [] => l2",
+	"      | h :: t => [h] ++ (merge_lists t (remove_value_list l2 h))",
+	"  end.",
+	"",
+	"Inductive principal : Type :=",
+	"| PRINCIPAL : string -> list expression -> principal.",
+	"",
+	"Inductive message : Type :=",
+	"| MSG : guard_status -> value -> message.",
+	"",
+	"Inductive block : Type :=",
+	"| pblock : principal -> block",
+	"| mblock : message -> block.",
+	"",
+	"Inductive state : Type :=",
+	"| STATE: list block -> state.",
+	"",
+	"",
+	"Fixpoint absorb_expression (l: list expression) : list value :=",
+	"  match l with",
+	"    | [] => []  ",
+	"    | h :: t => match h with",
+	"        | EXP dec qual val ls => match qual, ls with",
+	"            | private, not_leaked => absorb_expression t",
+	"            | _, _ => [val] ++ absorb_expression t",
+	"          end",
+	"      end",
+	"  end.",
+	"",
+	"Fixpoint has_password (v: value) : list value :=",
+	"  match v with",
+	"  | prim p => match p with",
+	"      | CONCAT2 a b => has_password a ++ has_password b",
+	"      | CONCAT3 a b c => has_password a ++ has_password b ++ has_password c",
+	"      | CONCAT4 a b c d => has_password a ++ has_password b ++ has_password c ++ has_password d",
+	"      | CONCAT5 a b c d e => has_password a ++ has_password b ++ has_password c ++ has_password d ++ has_password e",
+	"      | SPLIT1 a => has_password a",
+	"      | SPLIT2 a => has_password a",
+	"      | SPLIT3 a => has_password a",
+	"      | SPLIT4 a => has_password a",
+	"      | SPLIT5 a => has_password a",
+	"      | PW_HASH1 a => []",
+	"      | PW_HASH2 a b => []",
+	"      | PW_HASH3 a b c => []",
+	"      | PW_HASH4 a b c d => []",
+	"      | PW_HASH5 a b c d e => []",
+	"      | HASH1 a => has_password a",
+	"      | HASH2 a b => has_password a ++ has_password b",
+	"      | HASH3 a b c => has_password a ++ has_password b ++ has_password c",
+	"      | HASH4 a b c d => has_password a ++ has_password b ++ has_password c ++ has_password d",
+	"      | HASH5 a b c d e => has_password a ++ has_password b ++ has_password c ++ has_password d ++ has_password e",
+	"      | HKDF1 salt ikm info => has_password salt ++ has_password ikm ++ has_password info",
+	"      | HKDF2 salt ikm info => has_password salt ++ has_password ikm ++ has_password info",
+	"      | HKDF3 salt ikm info => has_password salt ++ has_password ikm ++ has_password info",
+	"      | HKDF4 salt ikm info => has_password salt ++ has_password ikm ++ has_password info",
+	"      | HKDF5 salt ikm info => has_password salt ++ has_password ikm ++ has_password info",
+	"      | AEAD_ENC k m ad => has_password k ++ has_password ad",
+	"      | AEAD_DEC k c ad => has_password k ++ has_password c ++  has_password ad",
+	"      | ENC k m => has_password k",
+	"      | DEC k c => has_password k ++ has_password c",
+	"      | MAC k m => has_password k",
+	"      | SIGN k m => has_password k",
+	"      | SIGNVERIF k m s => has_password k ++ has_password m ++ has_password s ",
+	"      | PKE_ENC gk m => has_password gk",
+	"      | PKE_DEC k c => has_password k ++ has_password c",
+	"      | SHAMIR_SPLIT1 k => has_password k",
+	"      | SHAMIR_SPLIT2 k => has_password k",
+	"      | SHAMIR_SPLIT3 k => has_password k",
+	"      | SHAMIR_JOIN sa sb => has_password sa ++ has_password sb",
+	"      | RINGSIGN ka gkb gkc m => has_password ka ++ has_password gkb ++ has_password gkc",
+	"      | RINGSIGNVERIF gka gkb gkc m s => has_password gka ++ has_password gkb ++ has_password gkc ++ has_password m ++ has_password s",
+	"      | BLIND k m => has_password k",
+	"      | UNBLIND k m s => has_password k ++ has_password m ++ has_password s",
+	"    end",
+	"  | eq e => match e with",
+	"      | PUBKEY _ exp => has_password exp",
+	"      | DH _ exp1 exp2 => has_password exp1 ++ has_password exp2",
+	"    end",
+	"  | const c => match c with",
+	"      | Nil => []",
+	"      | cnstn c => []",
+	"    end",
+	"    | pass a => [v]",
+	"    | default => []",
+	"end.",
+	"",
+	"Fixpoint absorb_passwords_expression (l: list expression) : list value :=",
+	"  match l with",
+	"    | [] => []  ",
+	"    | h :: t => match h with",
+	"        | EXP dec qual val ls => has_password val ++ absorb_passwords_expression t",
+	"      end",
+	"  end.",
+	"",
+	"Definition absorb_principal (p: principal) : list value :=",
+	"  match p with",
+	"  | PRINCIPAL _ pk => merge_lists (absorb_expression pk) (absorb_passwords_expression pk)",
+	"end.",
+	"",
+	"Definition absorb_message (m: message) : value :=",
+	"  match m with",
+	"  | MSG _ val => val",
+	"end.",
+	"",
+	"Definition absorb_block (b: block) : list value :=",
+	"  match b with",
+	"    | pblock p => absorb_principal p",
+	"    | mblock m => [absorb_message m]",
+	"end.",
+	"",
+	"Fixpoint init_attacker (l: list block) : list value := ",
+	"  match l with",
+	"    | [] => []",
+	"    | h :: t => absorb_block h ++ init_attacker t",
+	"end.",
+	"",
+	"Fixpoint gather_principal_expressions (l: list block) (pname: string) : list expression :=",
+	"  match l with",
+	"    | [] => []",
+	"    | h :: t => match h with",
+	"      | mblock _ => gather_principal_expressions t pname",
+	"      | pblock pb => match pb with",
+	"          | PRINCIPAL hpname hplist => match eqb pname hpname with",
+	"                  | true => hplist ++ gather_principal_expressions t pname",
+	"                  | false => gather_principal_expressions t pname",
+	"              end",
+	"          end",
+	"      end",
+	"  end.",
+	"",
+	"Fixpoint gather_principals (pnames: list string) (l: list block) : list principal :=",
+	"  match pnames with ",
+	"    | [] => []",
+	"    | p1 :: r => [PRINCIPAL p1 (gather_principal_expressions l p1)] ++ gather_principals r l",
+	"  end.",
+	"",
+	"Fixpoint get_values_expression_list (l: list expression) : list value :=",
+	"  match l with",
+	"    | [] => []",
+	"    | h :: t => match h with",
+	"      | EXP _ _ v _  => [v] ++ get_values_expression_list t",
+	"      end",
+	"  end.",
+	"",
+	"Fixpoint gather_principal_values (l: list principal) : list (list value) :=",
+	"  match l with",
+	"    | [] => []",
+	"    | h :: t => match h with",
+	"        | PRINCIPAL pname plist => [get_values_expression_list plist] ++ gather_principal_values t",
+	"      end",
+	"  end.",
+	"",
+	"Definition rewrite_diff (old new: value) : value :=",
+	"  match old, new with",
+	"    | const c1, const c2 => match value_beq old new with",
+	"        | true => old",
+	"        | false => new",
+	"      end",
+	"    | pass a1, pass a2 => match value_beq old new with",
+	"        | true => old",
+	"        | false => new",
+	"      end",
+	"    | prim p1, prim p2 => match p1, p2 with",
+	"        | ENC k1 m1, ENC k2 m2 => match value_beq k1 k2, value_beq m1 m2 with",
+	"            | true, true => old",
+	"            | false, true => prim(ENC k2 m1)",
+	"            | true, false => prim(ENC k1 m2)",
+	"            | false, false => new",
+	"          end",
+	"        | DEC k1 c1, DEC k2 c2 => match value_beq k1 k2, value_beq c1 c2 with",
+	"            | true, true => old",
+	"            | false, true => prim(DEC k2 c1)",
+	"            | true, false => prim(DEC k1 c2)",
+	"            | false, false => new",
+	"          end",
+	"        | AEAD_ENC k1 m1 ad1, AEAD_ENC k2 m2 ad2 =>",
+	"           match value_beq k1 k2, value_beq m1 m2, value_beq ad1 ad2 with",
+	"            | true, true, true => old",
+	"            | false, true, true => prim(AEAD_ENC k2 m1 ad1)",
+	"            | true, false, true => prim(AEAD_ENC k1 m2 ad1)",
+	"            | true, true, false => prim(AEAD_ENC k1 m1 ad2)",
+	"            | true, false, false => prim(AEAD_ENC k1 m2 ad2)",
+	"            | false, true, false => prim(AEAD_ENC k2 m1 ad1)",
+	"            | false, false, true => prim(AEAD_ENC k2 m2 ad1)",
+	"            | false, false, false => new",
+	"          end",
+	"        | AEAD_DEC k1 c1 ad1, AEAD_DEC k2 c2 ad2 =>",
+	"           match value_beq k1 k2, value_beq c1 c2, value_beq ad1 ad2 with",
+	"            | true, true, true => old",
+	"            | false, true, true => prim(AEAD_DEC k2 c1 ad1)",
+	"            | true, false, true => prim(AEAD_DEC k1 c2 ad1)",
+	"            | true, true, false => prim(AEAD_DEC k1 c1 ad2)",
+	"            | true, false, false => prim(AEAD_DEC k1 c2 ad2)",
+	"            | false, true, false => prim(AEAD_DEC k2 c1 ad1)",
+	"            | false, false, true => prim(AEAD_DEC k2 c2 ad1)",
+	"            | false, false, false => new",
+	"          end",
+	"      | PKE_ENC gk1 m1, ENC gk2 m2 => match value_beq gk1 gk2, value_beq m1 m2 with",
+	"          | true, true => old",
+	"          | false, true => prim(PKE_ENC gk2 m1)",
+	"          | true, false => prim(PKE_ENC gk1 m2)",
+	"          | false, false => new",
+	"        end",
+	"      | PKE_DEC k1 c1, PKE_DEC k2 c2 => match value_beq k1 k2, value_beq c1 c2 with",
+	"          | true, true => old",
+	"          | false, true => prim(PKE_DEC k2 c1)",
+	"          | true, false => prim(PKE_DEC k1 c2)",
+	"          | false, false => new",
+	"        end",
+	"      | HASH1 a1, HASH1 a2 => match value_beq a1 a2 with",
+	"          | true => old",
+	"          | false => new",
+	"        end",
+	"      | HASH2 a1 b1, HASH2 a2 b2 => match value_beq a1 a2, value_beq b1 b2 with",
+	"          | true, true => old",
+	"          | false, true => prim(HASH2 a2 b1)",
+	"          | true, false => prim(HASH2 a1 b2)",
+	"          | false, false => new",
+	"        end",
+	"      | HASH3 a1 b1 c1, HASH3 a2 b2 c2 =>",
+	"        match value_beq a1 a2, value_beq b1 b2, value_beq c1 c2 with",
+	"         | true, true, true => old",
+	"         | false, true, true => prim(HASH3 a2 b1 c1)",
+	"         | true, false, true => prim(HASH3 a1 b2 c1)",
+	"         | true, true, false => prim(HASH3 a1 b1 c2)",
+	"         | true, false, false => prim(HASH3 a1 b2 c2)",
+	"         | false, true, false => prim(HASH3 a2 b1 c1)",
+	"         | false, false, true => prim(HASH3 a2 b2 c1)",
+	"         | false, false, false => new",
+	"       end",
+	"      | HASH4 a1 b1 c1 d1, HASH4 a2 b2 c2 d2 =>",
+	"        match value_beq a1 a2, value_beq b1 b2, value_beq c1 c2, value_beq d1 d2 with",
+	"         | true, true, true, true => old",
+	"         | false, true, true, true => prim(HASH4 a2 b1 c1 d1)",
+	"         | true, false, true, true => prim(HASH4 a1 b2 c1 d1)",
+	"         | true, true, false, true => prim(HASH4 a1 b1 c2 d1)",
+	"         | true, true, true, false => prim(HASH4 a1 b1 c1 d2)",
+	"         | false, false, true, true => prim(HASH4 a2 b2 c1 d1)",
+	"         | false, true, false, true => prim(HASH4 a2 b1 c2 d1)",
+	"         | false, true, true, false => prim(HASH4 a2 b1 c1 d2)",
+	"         | true, false, false, true => prim(HASH4 a1 b2 c2 d1)",
+	"         | true, false, true, false => prim(HASH4 a1 b2 c1 d2)",
+	"         | true, true, false, false => prim(HASH4 a1 b1 c2 d2)",
+	"         | true, false, false, false => prim(HASH4 a1 b2 c2 d2)",
+	"         | false, true, false, false => prim(HASH4 a2 b1 c2 d2)",
+	"         | false, false, true, false => prim(HASH4 a2 b2 c1 d2)",
+	"         | false, false, false, true => prim(HASH4 a2 b2 c2 d1)",
+	"         | false, false, false, false => new",
+	"       end",
+	"      | HASH5 a1 b1 c1 d1 e1, HASH5 a2 b2 c2 d2 e2=>",
+	"        match value_beq a1 a2, value_beq b1 b2, value_beq c1 c2, value_beq d1 d2, value_beq e1 e2 with",
+	"         | true, true, true, true, true => old",
+	"         | false, true, true, true, true => prim(HASH5 a2 b1 c1 d1 e1)",
+	"         | true, false, true, true, true => prim(HASH5 a1 b2 c1 d1 e1)",
+	"         | true, true, false, true, true => prim(HASH5 a1 b1 c2 d1 e1)",
+	"         | true, true, true, false, true => prim(HASH5 a1 b1 c1 d2 e1)",
+	"         | true, true, true, true, false => prim(HASH5 a1 b1 c1 d1 e2)",
+	"         | false, false, true, true, true => prim(HASH5 a2 b2 c1 d1 e1)",
+	"         | false, true, false, true, true => prim(HASH5 a2 b1 c2 d1 e1)",
+	"         | false, true, true, false, true => prim(HASH5 a2 b1 c1 d2 e1)",
+	"         | false, true, true, true, false => prim(HASH5 a2 b1 c1 d1 e2)",
+	"         | true, false, false, true, true => prim(HASH5 a1 b2 c2 d1 e1)",
+	"         | true, false, true, false, true => prim(HASH5 a1 b2 c1 d2 e1)",
+	"         | true, false, true, true, false => prim(HASH5 a1 b2 c1 d1 e2)",
+	"         | true, true, false, false, true => prim(HASH5 a1 b1 c2 d2 e1)",
+	"         | true, true, false, true, false => prim(HASH5 a1 b1 c2 d1 e2)",
+	"         | true, true, true, false, false => prim(HASH5 a1 b1 c1 d2 e2)",
+	"         | true, true, false, false, false => prim(HASH5 a1 b1 c2 d2 e2)",
+	"         | true, false, true, false, false => prim(HASH5 a1 b2 c1 d2 e2)",
+	"         | true, false, false, true, false => prim(HASH5 a1 b2 c2 d1 e2)",
+	"         | true, false, false, false, true => prim(HASH5 a1 b2 c2 d2 e1)",
+	"         | false, true, true, false, false => prim(HASH5 a2 b1 c1 d2 e2)",
+	"         | false, true, false, true, false => prim(HASH5 a2 b1 c2 d1 e2)",
+	"         | false, true, false, false, true => prim(HASH5 a2 b1 c2 d2 e1)",
+	"         | false, false, true, true, false => prim(HASH5 a2 b2 c1 d1 e2)",
+	"         | false, false, true, false, true => prim(HASH5 a2 b2 c1 d2 e1)",
+	"         | false, false, false, true, true => prim(HASH5 a2 b2 c2 d1 e1)",
+	"         | true, false, false, false, false => prim(HASH5 a1 b2 c2 d2 e2)",
+	"         | false, true, false, false, false => prim(HASH5 a2 b1 c2 d2 e2)",
+	"         | false, false, true, false, false => prim(HASH5 a2 b2 c1 d2 e2)",
+	"         | false, false, false, true, false => prim(HASH5 a2 b2 c2 d1 e2)",
+	"         | false, false, false, false, true => prim(HASH5 a2 b2 c2 d2 e1)",
+	"         | false, false, false, false, false => new",
+	"       end",
+	"        | MAC k1 m1, MAC k2 m2 => match value_beq k1 k2, value_beq m1 m2 with",
+	"            | true, true => old",
+	"            | false, true => prim(MAC k2 m1)",
+	"            | true, false => prim(MAC k1 m2)",
+	"            | false, false => new",
+	"          end",
+	"        | HKDF1 salt1 ikm1 info1, HKDF1 salt2 ikm2 info2 =>",
+	"          match value_beq salt1 salt2, value_beq ikm1 ikm2, value_beq info1 info2 with",
+	"           | true, true, true => old",
+	"           | false, true, true => prim(HKDF1 salt2 ikm1 info1)",
+	"           | true, false, true => prim(HKDF1 salt1 ikm2 info1)",
+	"           | true, true, false => prim(HKDF1 salt1 ikm1 info2)",
+	"           | true, false, false => prim(HKDF1 salt1 ikm2 info2)",
+	"           | false, true, false => prim(HKDF1 salt2 ikm1 info1)",
+	"           | false, false, true => prim(HKDF1 salt2 ikm2 info1)",
+	"           | false, false, false => new",
+	"         end",
+	"        | HKDF2 salt1 ikm1 info1, HKDF2 salt2 ikm2 info2 =>",
+	"          match value_beq salt1 salt2, value_beq ikm1 ikm2, value_beq info1 info2 with",
+	"           | true, true, true => old",
+	"           | false, true, true => prim(HKDF2 salt2 ikm1 info1)",
+	"           | true, false, true => prim(HKDF2 salt1 ikm2 info1)",
+	"           | true, true, false => prim(HKDF2 salt1 ikm1 info2)",
+	"           | true, false, false => prim(HKDF2 salt1 ikm2 info2)",
+	"           | false, true, false => prim(HKDF2 salt2 ikm1 info1)",
+	"           | false, false, true => prim(HKDF2 salt2 ikm2 info1)",
+	"           | false, false, false => new",
+	"         end",
+	"        | HKDF3 salt1 ikm1 info1, HKDF3 salt2 ikm2 info2 =>",
+	"          match value_beq salt1 salt2, value_beq ikm1 ikm2, value_beq info1 info2 with",
+	"           | true, true, true => old",
+	"           | false, true, true => prim(HKDF3 salt2 ikm1 info1)",
+	"           | true, false, true => prim(HKDF3 salt1 ikm2 info1)",
+	"           | true, true, false => prim(HKDF3 salt1 ikm1 info2)",
+	"           | true, false, false => prim(HKDF3 salt1 ikm2 info2)",
+	"           | false, true, false => prim(HKDF3 salt2 ikm1 info1)",
+	"           | false, false, true => prim(HKDF3 salt2 ikm2 info1)",
+	"           | false, false, false => new",
+	"         end",
+	"        | HKDF4 salt1 ikm1 info1, HKDF4 salt2 ikm2 info2 =>",
+	"          match value_beq salt1 salt2, value_beq ikm1 ikm2, value_beq info1 info2 with",
+	"           | true, true, true => old",
+	"           | false, true, true => prim(HKDF4 salt2 ikm1 info1)",
+	"           | true, false, true => prim(HKDF4 salt1 ikm2 info1)",
+	"           | true, true, false => prim(HKDF4 salt1 ikm1 info2)",
+	"           | true, false, false => prim(HKDF4 salt1 ikm2 info2)",
+	"           | false, true, false => prim(HKDF4 salt2 ikm1 info1)",
+	"           | false, false, true => prim(HKDF4 salt2 ikm2 info1)",
+	"           | false, false, false => new",
+	"         end",
+	"        | HKDF5 salt1 ikm1 info1, HKDF5 salt2 ikm2 info2 =>",
+	"          match value_beq salt1 salt2, value_beq ikm1 ikm2, value_beq info1 info2 with",
+	"           | true, true, true => old",
+	"           | false, true, true => prim(HKDF5 salt2 ikm1 info1)",
+	"           | true, false, true => prim(HKDF5 salt1 ikm2 info1)",
+	"           | true, true, false => prim(HKDF5 salt1 ikm1 info2)",
+	"           | true, false, false => prim(HKDF5 salt1 ikm2 info2)",
+	"           | false, true, false => prim(HKDF5 salt2 ikm1 info1)",
+	"           | false, false, true => prim(HKDF5 salt2 ikm2 info1)",
+	"           | false, false, false => new",
+	"         end",
+	"      | PW_HASH1 a1, PW_HASH1 a2 => match value_beq a1 a2 with",
+	"          | true => old",
+	"          | false => new",
+	"        end",
+	"      | PW_HASH2 a1 b1, PW_HASH2 a2 b2 => match value_beq a1 a2, value_beq b1 b2 with",
+	"          | true, true => old",
+	"          | false, true => prim(PW_HASH2 a2 b1)",
+	"          | true, false => prim(PW_HASH2 a1 b2)",
+	"          | false, false => new",
+	"        end",
+	"      | PW_HASH3 a1 b1 c1, PW_HASH3 a2 b2 c2 =>",
+	"        match value_beq a1 a2, value_beq b1 b2, value_beq c1 c2 with",
+	"         | true, true, true => old",
+	"         | false, true, true => prim(PW_HASH3 a2 b1 c1)",
+	"         | true, false, true => prim(PW_HASH3 a1 b2 c1)",
+	"         | true, true, false => prim(PW_HASH3 a1 b1 c2)",
+	"         | true, false, false => prim(PW_HASH3 a1 b2 c2)",
+	"         | false, true, false => prim(PW_HASH3 a2 b1 c1)",
+	"         | false, false, true => prim(PW_HASH3 a2 b2 c1)",
+	"         | false, false, false => new",
+	"       end",
+	"      | PW_HASH4 a1 b1 c1 d1, PW_HASH4 a2 b2 c2 d2 =>",
+	"        match value_beq a1 a2, value_beq b1 b2, value_beq c1 c2, value_beq d1 d2 with",
+	"         | true, true, true, true => old",
+	"         | false, true, true, true => prim(PW_HASH4 a2 b1 c1 d1)",
+	"         | true, false, true, true => prim(PW_HASH4 a1 b2 c1 d1)",
+	"         | true, true, false, true => prim(PW_HASH4 a1 b1 c2 d1)",
+	"         | true, true, true, false => prim(PW_HASH4 a1 b1 c1 d2)",
+	"         | false, false, true, true => prim(PW_HASH4 a2 b2 c1 d1)",
+	"         | false, true, false, true => prim(PW_HASH4 a2 b1 c2 d1)",
+	"         | false, true, true, false => prim(PW_HASH4 a2 b1 c1 d2)",
+	"         | true, false, false, true => prim(PW_HASH4 a1 b2 c2 d1)",
+	"         | true, false, true, false => prim(PW_HASH4 a1 b2 c1 d2)",
+	"         | true, true, false, false => prim(PW_HASH4 a1 b1 c2 d2)",
+	"         | true, false, false, false => prim(PW_HASH4 a1 b2 c2 d2)",
+	"         | false, true, false, false => prim(PW_HASH4 a2 b1 c2 d2)",
+	"         | false, false, true, false => prim(PW_HASH4 a2 b2 c1 d2)",
+	"         | false, false, false, true => prim(PW_HASH4 a2 b2 c2 d1)",
+	"         | false, false, false, false => new",
+	"       end",
+	"      | PW_HASH5 a1 b1 c1 d1 e1, PW_HASH5 a2 b2 c2 d2 e2=>",
+	"        match value_beq a1 a2, value_beq b1 b2, value_beq c1 c2, value_beq d1 d2, value_beq e1 e2 with",
+	"         | true, true, true, true, true => old",
+	"         | false, true, true, true, true => prim(PW_HASH5 a2 b1 c1 d1 e1)",
+	"         | true, false, true, true, true => prim(PW_HASH5 a1 b2 c1 d1 e1)",
+	"         | true, true, false, true, true => prim(PW_HASH5 a1 b1 c2 d1 e1)",
+	"         | true, true, true, false, true => prim(PW_HASH5 a1 b1 c1 d2 e1)",
+	"         | true, true, true, true, false => prim(PW_HASH5 a1 b1 c1 d1 e2)",
+	"         | false, false, true, true, true => prim(PW_HASH5 a2 b2 c1 d1 e1)",
+	"         | false, true, false, true, true => prim(PW_HASH5 a2 b1 c2 d1 e1)",
+	"         | false, true, true, false, true => prim(PW_HASH5 a2 b1 c1 d2 e1)",
+	"         | false, true, true, true, false => prim(PW_HASH5 a2 b1 c1 d1 e2)",
+	"         | true, false, false, true, true => prim(PW_HASH5 a1 b2 c2 d1 e1)",
+	"         | true, false, true, false, true => prim(PW_HASH5 a1 b2 c1 d2 e1)",
+	"         | true, false, true, true, false => prim(PW_HASH5 a1 b2 c1 d1 e2)",
+	"         | true, true, false, false, true => prim(PW_HASH5 a1 b1 c2 d2 e1)",
+	"         | true, true, false, true, false => prim(PW_HASH5 a1 b1 c2 d1 e2)",
+	"         | true, true, true, false, false => prim(PW_HASH5 a1 b1 c1 d2 e2)",
+	"         | true, true, false, false, false => prim(PW_HASH5 a1 b1 c2 d2 e2)",
+	"         | true, false, true, false, false => prim(PW_HASH5 a1 b2 c1 d2 e2)",
+	"         | true, false, false, true, false => prim(PW_HASH5 a1 b2 c2 d1 e2)",
+	"         | true, false, false, false, true => prim(PW_HASH5 a1 b2 c2 d2 e1)",
+	"         | false, true, true, false, false => prim(PW_HASH5 a2 b1 c1 d2 e2)",
+	"         | false, true, false, true, false => prim(PW_HASH5 a2 b1 c2 d1 e2)",
+	"         | false, true, false, false, true => prim(PW_HASH5 a2 b1 c2 d2 e1)",
+	"         | false, false, true, true, false => prim(PW_HASH5 a2 b2 c1 d1 e2)",
+	"         | false, false, true, false, true => prim(PW_HASH5 a2 b2 c1 d2 e1)",
+	"         | false, false, false, true, true => prim(PW_HASH5 a2 b2 c2 d1 e1)",
+	"         | true, false, false, false, false => prim(PW_HASH5 a1 b2 c2 d2 e2)",
+	"         | false, true, false, false, false => prim(PW_HASH5 a2 b1 c2 d2 e2)",
+	"         | false, false, true, false, false => prim(PW_HASH5 a2 b2 c1 d2 e2)",
+	"         | false, false, false, true, false => prim(PW_HASH5 a2 b2 c2 d1 e2)",
+	"         | false, false, false, false, true => prim(PW_HASH5 a2 b2 c2 d2 e1)",
+	"         | false, false, false, false, false => new",
+	"       end",
+	"      | SIGN k1 m1, SIGN k2 m2 => match value_beq k1 k2, value_beq m1 m2 with",
+	"          | true, true => old",
+	"          | false, true => prim(SIGN k2 m1)",
+	"          | true, false => prim(SIGN k1 m2)",
+	"          | false, false => new",
+	"        end",
+	"      | SIGNVERIF k1 m1 s1, SIGNVERIF k2 m2 s2 =>",
+	"         match value_beq k1 k2, value_beq m1 m2, value_beq s1 s2 with",
+	"          | true, true, true => old",
+	"          | false, true, true => prim(SIGNVERIF k2 m1 s1)",
+	"          | true, false, true => prim(SIGNVERIF k1 m2 s1)",
+	"          | true, true, false => prim(SIGNVERIF k1 m1 s2)",
+	"          | true, false, false => prim(SIGNVERIF k1 m2 s2)",
+	"          | false, true, false => prim(SIGNVERIF k2 m1 s1)",
+	"          | false, false, true => prim(SIGNVERIF k2 m2 s1)",
+	"          | false, false, false => new",
+	"        end",
+	"      | RINGSIGN ka1 gkb1 gkc1 m1, RINGSIGN ka2 gkb2 gkc2 m2 =>",
+	"        match value_beq ka1 ka2, value_beq gkb1 gkb2, value_beq gkc1 gkc2, value_beq m1 m2 with",
+	"          | true, true, true, true => old",
+	"          | false, true, true, true => prim(RINGSIGN ka2 gkb1 gkc1 m1)",
+	"          | true, false, true, true => prim(RINGSIGN ka1 gkb2 gkc1 m1)",
+	"          | true, true, false, true => prim(RINGSIGN ka1 gkb1 gkc2 m1)",
+	"          | true, true, true, false => prim(RINGSIGN ka1 gkb1 gkc1 m2)",
+	"          | false, false, true, true => prim(RINGSIGN ka2 gkb2 gkc1 m1)",
+	"          | false, true, false, true => prim(RINGSIGN ka2 gkb1 gkc2 m1)",
+	"          | false, true, true, false => prim(RINGSIGN ka2 gkb1 gkc1 m2)",
+	"          | true, false, false, true => prim(RINGSIGN ka1 gkb2 gkc2 m1)",
+	"          | true, false, true, false => prim(RINGSIGN ka1 gkb2 gkc1 m2)",
+	"          | true, true, false, false => prim(RINGSIGN ka1 gkb1 gkc2 m2)",
+	"          | true, false, false, false => prim(RINGSIGN ka1 gkb2 gkc2 m2)",
+	"          | false, true, false, false => prim(RINGSIGN ka2 gkb1 gkc2 m2)",
+	"          | false, false, true, false => prim(RINGSIGN ka2 gkb2 gkc1 m2)",
+	"          | false, false, false, true => prim(RINGSIGN ka2 gkb2 gkc2 m1)",
+	"          | false, false, false, false => new",
+	"        end",
+	"      | RINGSIGNVERIF gka1 gkb1 gkc1 m1 s1, RINGSIGNVERIF gka2 gkb2 gkc2 m2 s2=>",
+	"        match value_beq gka1 gka2, value_beq gkb1 gkb2, value_beq gkc1 gkc2, value_beq m1 m2, value_beq s1 s2 with",
+	"          | true, true, true, true, true => old",
+	"          | false, true, true, true, true => prim(RINGSIGNVERIF gka2 gkb1 gkc1 m1 s1)",
+	"          | true, false, true, true, true => prim(RINGSIGNVERIF gka1 gkb2 gkc1 m1 s1)",
+	"          | true, true, false, true, true => prim(RINGSIGNVERIF gka1 gkb1 gkc2 m1 s1)",
+	"          | true, true, true, false, true => prim(RINGSIGNVERIF gka1 gkb1 gkc1 m2 s1)",
+	"          | true, true, true, true, false => prim(RINGSIGNVERIF gka1 gkb1 gkc1 m1 s2)",
+	"          | false, false, true, true, true => prim(RINGSIGNVERIF gka2 gkb2 gkc1 m1 s1)",
+	"          | false, true, false, true, true => prim(RINGSIGNVERIF gka2 gkb1 gkc2 m1 s1)",
+	"          | false, true, true, false, true => prim(RINGSIGNVERIF gka2 gkb1 gkc1 m2 s1)",
+	"          | false, true, true, true, false => prim(RINGSIGNVERIF gka2 gkb1 gkc1 m1 s2)",
+	"          | true, false, false, true, true => prim(RINGSIGNVERIF gka1 gkb2 gkc2 m1 s1)",
+	"          | true, false, true, false, true => prim(RINGSIGNVERIF gka1 gkb2 gkc1 m2 s1)",
+	"          | true, false, true, true, false => prim(RINGSIGNVERIF gka1 gkb2 gkc1 m1 s2)",
+	"          | true, true, false, false, true => prim(RINGSIGNVERIF gka1 gkb1 gkc2 m2 s1)",
+	"          | true, true, false, true, false => prim(RINGSIGNVERIF gka1 gkb1 gkc2 m1 s2)",
+	"          | true, true, true, false, false => prim(RINGSIGNVERIF gka1 gkb1 gkc1 m2 s2)",
+	"          | true, true, false, false, false => prim(RINGSIGNVERIF gka1 gkb1 gkc2 m2 s2)",
+	"          | true, false, true, false, false => prim(RINGSIGNVERIF gka1 gkb2 gkc1 m2 s2)",
+	"          | true, false, false, true, false => prim(RINGSIGNVERIF gka1 gkb2 gkc2 m1 s2)",
+	"          | true, false, false, false, true => prim(RINGSIGNVERIF gka1 gkb2 gkc2 m2 s1)",
+	"          | false, true, true, false, false => prim(RINGSIGNVERIF gka2 gkb1 gkc1 m2 s2)",
+	"          | false, true, false, true, false => prim(RINGSIGNVERIF gka2 gkb1 gkc2 m1 s2)",
+	"          | false, true, false, false, true => prim(RINGSIGNVERIF gka2 gkb1 gkc2 m2 s1)",
+	"          | false, false, true, true, false => prim(RINGSIGNVERIF gka2 gkb2 gkc1 m1 s2)",
+	"          | false, false, true, false, true => prim(RINGSIGNVERIF gka2 gkb2 gkc1 m2 s1)",
+	"          | false, false, false, true, true => prim(RINGSIGNVERIF gka2 gkb2 gkc2 m1 s1)",
+	"          | true, false, false, false, false => prim(RINGSIGNVERIF gka1 gkb2 gkc2 m2 s2)",
+	"          | false, true, false, false, false => prim(RINGSIGNVERIF gka2 gkb1 gkc2 m2 s2)",
+	"          | false, false, true, false, false => prim(RINGSIGNVERIF gka2 gkb2 gkc1 m2 s2)",
+	"          | false, false, false, true, false => prim(RINGSIGNVERIF gka2 gkb2 gkc2 m1 s2)",
+	"          | false, false, false, false, true => prim(RINGSIGNVERIF gka2 gkb2 gkc2 m2 s1)",
+	"          | false, false, false, false, false => new",
+	"        end",
+	"      | BLIND k1 m1, BLIND k2 m2 => match value_beq k1 k2, value_beq m1 m2 with",
+	"          | true, true => old",
+	"          | false, true => prim(BLIND k2 m1)",
+	"          | true, false => prim(BLIND k1 m2)",
+	"          | false, false => new",
+	"        end",
+	"      | UNBLIND k1 m1 s1, UNBLIND k2 m2 s2 =>",
+	"        match value_beq k1 k2, value_beq m1 m2, value_beq s1 s2 with",
+	"          | true, true, true => old",
+	"          | false, true, true => prim(UNBLIND k2 m1 s1)",
+	"          | true, false, true => prim(UNBLIND k1 m2 s1)",
+	"          | true, true, false => prim(UNBLIND k1 m1 s2)",
+	"          | true, false, false => prim(UNBLIND k1 m2 s2)",
+	"          | false, true, false => prim(UNBLIND k2 m1 s1)",
+	"          | false, false, true => prim(UNBLIND k2 m2 s1)",
+	"          | false, false, false => new",
+	"        end",
+	"      | SHAMIR_SPLIT1 a1, SHAMIR_SPLIT1 a2 => match value_beq a1 a2 with",
+	"          | true => old",
+	"          | false => new",
+	"        end",
+	"      | SHAMIR_SPLIT2 a1, SHAMIR_SPLIT2 a2 => match value_beq a1 a2 with",
+	"          | true => old",
+	"          | false => new",
+	"        end",
+	"      | SHAMIR_SPLIT3 a1, SHAMIR_SPLIT3 a2 => match value_beq a1 a2 with",
+	"          | true => old",
+	"          | false => new",
+	"        end",
+	"      | SHAMIR_JOIN sa1 sb1, SHAMIR_JOIN sa2 sb2 => match value_beq sa1 sa2, value_beq sb1 sb2 with",
+	"          | true, true => old",
+	"          | false, true => prim(SHAMIR_JOIN sa2 sb1)",
+	"          | true, false => prim(SHAMIR_JOIN sa1 sb2)",
+	"          | false, false => new",
+	"        end",
+	"      | CONCAT2 a1 b1, CONCAT2 a2 b2 => match value_beq a1 a2, value_beq b1 b2 with",
+	"          | true, true => old",
+	"          | false, true => prim(CONCAT2 a2 b1)",
+	"          | true, false => prim(CONCAT2 a1 b2)",
+	"          | false, false => new",
+	"        end",
+	"      | CONCAT3 a1 b1 c1, CONCAT3 a2 b2 c2 =>",
+	"        match value_beq a1 a2, value_beq b1 b2, value_beq c1 c2 with",
+	"          | true, true, true => old",
+	"          | false, true, true => prim(CONCAT3 a2 b1 c1)",
+	"          | true, false, true => prim(CONCAT3 a1 b2 c1)",
+	"          | true, true, false => prim(CONCAT3 a1 b1 c2)",
+	"          | true, false, false => prim(CONCAT3 a1 b2 c2)",
+	"          | false, true, false => prim(CONCAT3 a2 b1 c1)",
+	"          | false, false, true => prim(CONCAT3 a2 b2 c1)",
+	"          | false, false, false => new",
+	"        end",
+	"      | CONCAT4 a1 b1 c1 d1, CONCAT4 a2 b2 c2 d2 =>",
+	"        match value_beq a1 a2, value_beq b1 b2, value_beq c1 c2, value_beq d1 d2 with",
+	"          | true, true, true, true => old",
+	"          | false, true, true, true => prim(CONCAT4 a2 b1 c1 d1)",
+	"          | true, false, true, true => prim(CONCAT4 a1 b2 c1 d1)",
+	"          | true, true, false, true => prim(CONCAT4 a1 b1 c2 d1)",
+	"          | true, true, true, false => prim(CONCAT4 a1 b1 c1 d2)",
+	"          | false, false, true, true => prim(CONCAT4 a2 b2 c1 d1)",
+	"          | false, true, false, true => prim(CONCAT4 a2 b1 c2 d1)",
+	"          | false, true, true, false => prim(CONCAT4 a2 b1 c1 d2)",
+	"          | true, false, false, true => prim(CONCAT4 a1 b2 c2 d1)",
+	"          | true, false, true, false => prim(CONCAT4 a1 b2 c1 d2)",
+	"          | true, true, false, false => prim(CONCAT4 a1 b1 c2 d2)",
+	"          | true, false, false, false => prim(CONCAT4 a1 b2 c2 d2)",
+	"          | false, true, false, false => prim(CONCAT4 a2 b1 c2 d2)",
+	"          | false, false, true, false => prim(CONCAT4 a2 b2 c1 d2)",
+	"          | false, false, false, true => prim(CONCAT4 a2 b2 c2 d1)",
+	"          | false, false, false, false => new",
+	"        end",
+	"      | CONCAT5 a1 b1 c1 d1 e1, CONCAT5 a2 b2 c2 d2 e2=>",
+	"        match value_beq a1 a2, value_beq b1 b2, value_beq c1 c2, value_beq d1 d2, value_beq e1 e2 with",
+	"          | true, true, true, true, true => old",
+	"          | false, true, true, true, true => prim(CONCAT5 a2 b1 c1 d1 e1)",
+	"          | true, false, true, true, true => prim(CONCAT5 a1 b2 c1 d1 e1)",
+	"          | true, true, false, true, true => prim(CONCAT5 a1 b1 c2 d1 e1)",
+	"          | true, true, true, false, true => prim(CONCAT5 a1 b1 c1 d2 e1)",
+	"          | true, true, true, true, false => prim(CONCAT5 a1 b1 c1 d1 e2)",
+	"          | false, false, true, true, true => prim(CONCAT5 a2 b2 c1 d1 e1)",
+	"          | false, true, false, true, true => prim(CONCAT5 a2 b1 c2 d1 e1)",
+	"          | false, true, true, false, true => prim(CONCAT5 a2 b1 c1 d2 e1)",
+	"          | false, true, true, true, false => prim(CONCAT5 a2 b1 c1 d1 e2)",
+	"          | true, false, false, true, true => prim(CONCAT5 a1 b2 c2 d1 e1)",
+	"          | true, false, true, false, true => prim(CONCAT5 a1 b2 c1 d2 e1)",
+	"          | true, false, true, true, false => prim(CONCAT5 a1 b2 c1 d1 e2)",
+	"          | true, true, false, false, true => prim(CONCAT5 a1 b1 c2 d2 e1)",
+	"          | true, true, false, true, false => prim(CONCAT5 a1 b1 c2 d1 e2)",
+	"          | true, true, true, false, false => prim(CONCAT5 a1 b1 c1 d2 e2)",
+	"          | true, true, false, false, false => prim(CONCAT5 a1 b1 c2 d2 e2)",
+	"          | true, false, true, false, false => prim(CONCAT5 a1 b2 c1 d2 e2)",
+	"          | true, false, false, true, false => prim(CONCAT5 a1 b2 c2 d1 e2)",
+	"          | true, false, false, false, true => prim(CONCAT5 a1 b2 c2 d2 e1)",
+	"          | false, true, true, false, false => prim(CONCAT5 a2 b1 c1 d2 e2)",
+	"          | false, true, false, true, false => prim(CONCAT5 a2 b1 c2 d1 e2)",
+	"          | false, true, false, false, true => prim(CONCAT5 a2 b1 c2 d2 e1)",
+	"          | false, false, true, true, false => prim(CONCAT5 a2 b2 c1 d1 e2)",
+	"          | false, false, true, false, true => prim(CONCAT5 a2 b2 c1 d2 e1)",
+	"          | false, false, false, true, true => prim(CONCAT5 a2 b2 c2 d1 e1)",
+	"          | true, false, false, false, false => prim(CONCAT5 a1 b2 c2 d2 e2)",
+	"          | false, true, false, false, false => prim(CONCAT5 a2 b1 c2 d2 e2)",
+	"          | false, false, true, false, false => prim(CONCAT5 a2 b2 c1 d2 e2)",
+	"          | false, false, false, true, false => prim(CONCAT5 a2 b2 c2 d1 e2)",
+	"          | false, false, false, false, true => prim(CONCAT5 a2 b2 c2 d2 e1)",
+	"          | false, false, false, false, false => new",
+	"        end",
+	"      | SPLIT1 a1, SPLIT1 a2 => match value_beq a1 a2 with",
+	"          | true => old",
+	"          | false => new",
+	"        end",
+	"      | SPLIT2 a1, SPLIT2 a2 => match value_beq a1 a2 with",
+	"          | true => old",
+	"          | false => new",
+	"        end",
+	"      | SPLIT3 a1, SPLIT3 a2 => match value_beq a1 a2 with",
+	"          | true => old",
+	"          | false => new",
+	"        end",
+	"      | SPLIT4 a1, SPLIT4 a2 => match value_beq a1 a2 with",
+	"          | true => old",
+	"          | false => new",
+	"        end",
+	"      | SPLIT5 a1, SPLIT5 a2 => match value_beq a1 a2 with",
+	"          | true => old",
+	"          | false => new",
+	"        end",
+	"      | _ , _ => new",
+	"    end",
+	"  | eq e1, eq e2 => match e1, e2 with",
+	"      | PUBKEY _ exp1, PUBKEY _ exp2 => match value_beq exp1 exp2 with",
+	"          | true => old",
+	"          | false => new",
+	"        end",
+	"      | DH _ expa1 expb1, DH _ expa2 expb2 => match value_beq expa1 expa2, value_beq expb1 expb2 with",
+	"          | true, true => old",
+	"          | true, false => eq(DH G expa1 expb2)",
+	"          | false, true => eq(DH G expa2 expb1)",
+	"          | false, false => new",
+	"        end",
+	"      | _ , _ => new",
+	"    end   ",
+	"  | _, _ => new  ",
+	"end.",
+	"      ",
+	"",
+	"Fixpoint apply_rewrites (l: list value) (v: value) : value := ",
+	"  match v with",
+	"      | default => default",
+	"      | const c => v",
+	"      | pass a => v",
+	"      | eq e => match e with",
+	"          | PUBKEY _ exp => eq(PUBKEY G (apply_rewrites l exp))",
+	"          | DH _ exp1 exp2 => eq(DH G (apply_rewrites l exp1) (apply_rewrites l exp2))",
+	"        end",
+	"      | prim p => match p with",
+	"          | ENC k m => prim(ENC (apply_rewrites l k) (apply_rewrites l m))",
+	"          | DEC k c => match c with",
+	"              | prim p' => match p' with",
+	"                  | ENC k' m => match value_beq k k' with    ",
+	"                      | true => m",
+	"                      | false => prim(DEC (apply_rewrites l k) (prim(ENC (apply_rewrites l k) m)))",
+	"                  end",
+	"                  | _ => prim(DEC (apply_rewrites l k) (apply_rewrites l c))",
+	"                end",
+	"              | _ => prim(DEC (apply_rewrites l k) (apply_rewrites l c)) ",
+	"            end",
+	"          | AEAD_ENC k m ad => prim(AEAD_ENC (apply_rewrites l k) (apply_rewrites l m) (apply_rewrites l ad))",
+	"          | AEAD_DEC k c ad => match c with",
+	"              | prim p' => match p' with",
+	"                  | AEAD_ENC k' m ad' => match value_beq k k', value_beq ad ad' with",
+	"                      | true, true => m",
+	"                      | true, false => prim(AEAD_DEC k c (apply_rewrites l ad))",
+	"                      | false, true => prim(AEAD_DEC (apply_rewrites l k) (prim (AEAD_ENC (apply_rewrites l k') m ad)) ad)",
+	"                      | false, false => prim(AEAD_DEC (apply_rewrites l k) (prim (AEAD_ENC (apply_rewrites l k') m (apply_rewrites l ad))) (apply_rewrites l ad))",
+	"                    end",
+	"                  | _ => prim(AEAD_DEC (apply_rewrites l k) (apply_rewrites l c) (apply_rewrites l ad))",
+	"                end",
+	"              | _ => prim(AEAD_DEC (apply_rewrites l k) (apply_rewrites l c) (apply_rewrites l ad))",
+	"            end",
+	"          | PKE_ENC gk m => prim(PKE_ENC (apply_rewrites l gk) (apply_rewrites l m))",
+	"          | PKE_DEC k c => match c with",
+	"              | prim p' => match p' with",
+	"                  | PKE_ENC gk m => match gk with",
+	"                      | eq e => match e with",
+	"                          | PUBKEY _ exp => match value_beq exp k with",
+	"                              | true => m",
+	"                              | false => prim(PKE_DEC (apply_rewrites l k) (prim(PKE_ENC (apply_rewrites l exp) m)))",
+	"                            end",
+	"                          | _ => prim(PKE_DEC k (apply_rewrites l c))",
+	"                        end",
+	"                      | _ => prim(PKE_DEC (apply_rewrites l k) (apply_rewrites l c))",
+	"                    end",
+	"                | _ => prim(PKE_DEC (apply_rewrites l k) (apply_rewrites l c))",
+	"                    end",
+	"              | _ => prim(PKE_DEC (apply_rewrites l k) (apply_rewrites l c))",
+	"            end",
+	"          | HASH1 a => prim(HASH1 (apply_rewrites l a))",
+	"          | HASH2 a b => prim(HASH2 (apply_rewrites l a) (apply_rewrites l b))",
+	"          | HASH3 a b c => prim(HASH3 (apply_rewrites l a) (apply_rewrites l b) (apply_rewrites l c))",
+	"          | HASH4 a b c d => prim(HASH4 (apply_rewrites l a) (apply_rewrites l b) (apply_rewrites l c) (apply_rewrites l d))",
+	"          | HASH5 a b c d e => prim(HASH5 (apply_rewrites l a) (apply_rewrites l b) (apply_rewrites l c) (apply_rewrites l d) (apply_rewrites l e))",
+	"          | MAC k m => prim(MAC (apply_rewrites l k) (apply_rewrites l m))",
+	"          | HKDF1 salt ikm info => prim(HKDF1 (apply_rewrites l salt) (apply_rewrites l ikm) (apply_rewrites l info))",
+	"          | HKDF2 salt ikm info => prim(HKDF2 (apply_rewrites l salt) (apply_rewrites l ikm) (apply_rewrites l info))",
+	"          | HKDF3 salt ikm info => prim(HKDF3 (apply_rewrites l salt) (apply_rewrites l ikm) (apply_rewrites l info))",
+	"          | HKDF4 salt ikm info => prim(HKDF4 (apply_rewrites l salt) (apply_rewrites l ikm) (apply_rewrites l info))",
+	"          | HKDF5 salt ikm info => prim(HKDF5 (apply_rewrites l salt) (apply_rewrites l ikm) (apply_rewrites l info))",
+	"          | PW_HASH1 a => prim(PW_HASH1 (apply_rewrites l a))",
+	"          | PW_HASH2 a b => prim(PW_HASH2 (apply_rewrites l a) (apply_rewrites l b))",
+	"          | PW_HASH3 a b c => prim(PW_HASH3 (apply_rewrites l a) (apply_rewrites l b) (apply_rewrites l c))",
+	"          | PW_HASH4 a b c d => prim(PW_HASH4 (apply_rewrites l a) (apply_rewrites l b) (apply_rewrites l c) (apply_rewrites l d))",
+	"          | PW_HASH5 a b c d e => prim(PW_HASH5 (apply_rewrites l a) (apply_rewrites l b) (apply_rewrites l c) (apply_rewrites l d) (apply_rewrites l e))",
+	"          | SIGN k m => prim(SIGN (apply_rewrites l k) (apply_rewrites l m))",
+	"          | SIGNVERIF k m s => match s with",
+	"              | prim p' => match p' with",
+	"                  | SIGN k' m' => match value_beq k k', value_beq m m' with",
+	"                      | true, true => m",
+	"                      | true, false => prim(SIGNVERIF k (apply_rewrites l m) (prim(SIGN k (apply_rewrites l m'))))",
+	"                      | false, true => prim(SIGNVERIF (apply_rewrites l k) m (prim(SIGN (apply_rewrites l k') m')))",
+	"                      | false, false => prim(SIGNVERIF (apply_rewrites l k) (apply_rewrites l m) (prim(SIGN (apply_rewrites l k') (apply_rewrites l m'))))",
+	"                    end",
+	"                  | _ => prim(SIGNVERIF (apply_rewrites l k) (apply_rewrites l m) (apply_rewrites l s))",
+	"                end",
+	"              | _ => prim(SIGNVERIF (apply_rewrites l k) (apply_rewrites l m) (apply_rewrites l s))",
+	"            end",
+	"          | RINGSIGN ka gkb gkc m => prim(RINGSIGN (apply_rewrites l ka) (apply_rewrites l gkb) (apply_rewrites l gkc) (apply_rewrites l m))",
+	"          | RINGSIGNVERIF gka gkb gkc m s => match s with",
+	"              | prim p' => match p' with",
+	"                  | RINGSIGN ka' gkb' gkc' m' => match value_beq m m' with",
+	"                      | false => prim(RINGSIGNVERIF gka gkb gkc (apply_rewrites l m) (prim(RINGSIGN ka' gkb' gkc' (apply_rewrites l m))))",
+	"                      | true => match gka, gkb, gkc with",
+	"                          | eq e1, eq e2, eq e3 => match e1, e2, e3 with",
+	"                              | PUBKEY _ ka, PUBKEY _ kb, PUBKEY _ kc => match (value_beq ka' ka) && (((value_beq gkb' gkb) && (value_beq gkc' gkc)) || ((value_beq gkb' gkc) && (value_beq gkc' gkb))) with",
+	"                                  | true => m",
+	"                                  | false => match (value_beq ka' kb) && (((value_beq gkb' gkc) && (value_beq gkc' gka)) || ((value_beq gkb' gka) && (value_beq gkc' gkc))) with",
+	"                                      | true => m",
+	"                                      | false => match (value_beq ka' kc) && (((value_beq gkb' gkb) && (value_beq gkc' gka)) || ((value_beq gkb' gka) && (value_beq gkc' gkb))) with",
+	"                                          | true => m",
+	"                                          | false => prim(RINGSIGNVERIF (apply_rewrites l gka) (apply_rewrites l gkb) (apply_rewrites l gkc) m (prim(RINGSIGN (apply_rewrites l ka') (apply_rewrites l gkb') (apply_rewrites l gkc') m')))",
+	"                                        end",
+	"                                   end",
+	"                               end",
+	"                              | _, _, _ => prim(RINGSIGNVERIF (apply_rewrites l gka) (apply_rewrites l gkb) (apply_rewrites l gkc) m (prim(RINGSIGN ka' gkb' gkc' m')))",
+	"                          end",
+	"                        | _, _, _ => prim(RINGSIGNVERIF (apply_rewrites l gka) (apply_rewrites l gkb) (apply_rewrites l gkc) m (prim(RINGSIGN ka' gkb' gkc' m')))",
+	"                  end ",
+	"                  end",
+	"                  | _ => prim(RINGSIGNVERIF gka gkb gkc m (apply_rewrites l s))",
+	"                  end",
+	"              | _ => prim(RINGSIGNVERIF gka gkb gkc m (apply_rewrites l s))",
+	"            end",
+	"          | BLIND k m => prim(BLIND (apply_rewrites l k) (apply_rewrites l m))",
+	"          | UNBLIND k m s => match s with",
+	"              | prim p' => match p' with",
+	"                  | SIGN a b => match b with",
+	"                      | prim p'' => match p'' with",
+	"                          | BLIND k' m' => match value_beq k k', value_beq m m' with",
+	"                              | true, true => prim(SIGN a m)",
+	"                              | true, false => prim(UNBLIND k (apply_rewrites l m) (prim(SIGN a (prim(BLIND k' (apply_rewrites l m'))))))",
+	"                              | false, true => prim(UNBLIND (apply_rewrites l k) m (prim(SIGN a (prim(BLIND (apply_rewrites l k') m')))))",
+	"                              | false, false => prim(UNBLIND (apply_rewrites l k) (apply_rewrites l m) (prim(SIGN a (prim(BLIND (apply_rewrites l k') (apply_rewrites l m'))))))",
+	"                            end",
+	"                            | _ => prim(UNBLIND k m (prim(SIGN a (apply_rewrites l b))))",
+	"                            end",
+	"                  | _ => prim(UNBLIND k m (prim(SIGN a (apply_rewrites l b))))",
+	"                  end",
+	"                  | _ => prim(UNBLIND k m (apply_rewrites l s))",
+	"                end",
+	"              | _ => prim(UNBLIND k m (apply_rewrites l s))",
+	"            end",
+	"          | SHAMIR_SPLIT1 k => prim(SHAMIR_SPLIT1 (apply_rewrites l k))",
+	"          | SHAMIR_SPLIT2 k => prim(SHAMIR_SPLIT2 (apply_rewrites l k))",
+	"          | SHAMIR_SPLIT3 k => prim(SHAMIR_SPLIT3 (apply_rewrites l k))",
+	"          | SHAMIR_JOIN psa psb => match psa, psb with",
+	"              | prim sa, prim sb => match sa, sb with",
+	"                  | SHAMIR_SPLIT1 k, SHAMIR_SPLIT2 k' => match value_beq k k' with",
+	"                      | true => k",
+	"                      | false => prim(SHAMIR_JOIN (apply_rewrites l psa) (apply_rewrites l psb))",
+	"                    end",
+	"                  | SHAMIR_SPLIT1 k, SHAMIR_SPLIT3 k' => match value_beq k k' with",
+	"                      | true => k",
+	"                      | false => prim(SHAMIR_JOIN (apply_rewrites l psa) (apply_rewrites l psb))",
+	"                    end",
+	"                  | SHAMIR_SPLIT2 k, SHAMIR_SPLIT1 k' => match value_beq k k' with",
+	"                      | true => k",
+	"                      | false => prim(SHAMIR_JOIN (apply_rewrites l psa) (apply_rewrites l psb))",
+	"                    end",
+	"                  | SHAMIR_SPLIT2 k, SHAMIR_SPLIT3 k' => match value_beq k k' with",
+	"                      | true => k",
+	"                      | false => prim(SHAMIR_JOIN (apply_rewrites l psa) (apply_rewrites l psb))",
+	"                    end",
+	"                  | SHAMIR_SPLIT3 k, SHAMIR_SPLIT1 k' => match value_beq k k' with",
+	"                      | true => k",
+	"                      | false => prim(SHAMIR_JOIN (apply_rewrites l psa) (apply_rewrites l psb))",
+	"                    end",
+	"                  | SHAMIR_SPLIT3 k, SHAMIR_SPLIT2 k' => match value_beq k k' with",
+	"                      | true => k",
+	"                      | false => prim(SHAMIR_JOIN (apply_rewrites l psa) (apply_rewrites l psb))",
+	"                    end",
+	"                  | _, _ => prim(SHAMIR_JOIN (apply_rewrites l psa) (apply_rewrites l psb))",
+	"                end",
+	"                | _, _ => prim(SHAMIR_JOIN (apply_rewrites l psa) (apply_rewrites l psb))",
+	"              end",
+	"          | CONCAT2 a b => prim(CONCAT2 (apply_rewrites l a) (apply_rewrites l b))",
+	"          | CONCAT3 a b c => prim(CONCAT3 (apply_rewrites l a) (apply_rewrites l b) (apply_rewrites l c))",
+	"          | CONCAT4 a b c d => prim(CONCAT4 (apply_rewrites l a) (apply_rewrites l b) (apply_rewrites l c) (apply_rewrites l d))",
+	"          | CONCAT5 a b c d e => prim(CONCAT5 (apply_rewrites l a) (apply_rewrites l b) (apply_rewrites l c) (apply_rewrites l d) (apply_rewrites l e))",
+	"          | SPLIT1 a => prim(SPLIT1 (apply_rewrites l a))",
+	"          | SPLIT2 a => prim(SPLIT2 (apply_rewrites l a))",
+	"          | SPLIT3 a => prim(SPLIT3 (apply_rewrites l a))",
+	"          | SPLIT4 a => prim(SPLIT4 (apply_rewrites l a))",
+	"          | SPLIT5 a => prim(SPLIT5 (apply_rewrites l a))",
+	"        end",
+	" end.",
+	"",
+	"Fixpoint rewrite_list (l: list value) (i n: nat): list value :=",
+	"  match n with",
+	"      | 0 => l",
+	"      | S n' => match ((List.length l) =? i) with",
+	"          | true => l",
+	"          | false => match l with",
+	"              | [] => []",
+	"              | h :: t =>",
+	"              let v := (nth i l default) in",
+	"              let v' := apply_rewrites l v in",
+	"              let diff := rewrite_diff v v' in",
+	"                  match value_beq v diff with",
+	"                  | true => rewrite_list l (i+1) n'",
+	"                  | false => rewrite_list ((remove_value_list l v) ++ [diff]) 0 n'",
+	"                end",
+	"            end",
+	"        end",
+	"    end.",
+	"",
+	"Fixpoint rewrite_principals (l: list (list value)) (n: nat) : list(list value) :=",
+	"  match l with",
+	"    | [] => [[]]",
+	"    | h :: t => [(rewrite_list h 0 n)] ++ (rewrite_principals t n)",
+	"  end.",
+	"",
+	"",
+	"Fixpoint decompose_primitive (l: list value) (p: primitive) (n: nat) : list value :=",
+	"  match n with",
+	"    | 0 => l",
+	"    | S n' => match p with",
+	"          | ENC k m => let l' := (merge_lists l (find l k n')) in",
+	"            match shallow_search l' k with",
+	"              | true => l' ++ [m]",
+	"              | false => l'",
+	"            end",
+	"          | DEC k c => let l' := (merge_lists l (find l k n')) in",
+	"            match shallow_search l' k with",
+	"              | true => l' ++ [c]",
+	"              | false => l'",
+	"            end",
+	"          | AEAD_ENC k m ad => let l' := (merge_lists l (find l k n')) in",
+	"            match shallow_search l' k with",
+	"              | true => l' ++ [m]",
+	"              | false => l'",
+	"            end",
+	"          | AEAD_DEC k c ad => let l' := (merge_lists l (find l k n')) in",
+	"            match shallow_search l' k with",
+	"              | true => l' ++ [c]",
+	"              | false => l'",
+	"            end",
+	"          | PKE_ENC gk m => match gk with",
+	"              | eq e => match e with",
+	"                  | PUBKEY _ exp => let l' := (merge_lists l (find l exp n')) in",
+	"                    match shallow_search l' exp with",
+	"                        | true => l' ++ [m]",
+	"                        | false => l'",
+	"                      end",
+	"                  | _ => l",
+	"                end",
+	"              | _ => l",
+	"            end",
+	"          | PKE_DEC k c => let l' := (merge_lists l (find l k n')) in",
+	"            match shallow_search l' k with",
+	"              | true => l' ++ [c]",
+	"              | false => l'",
+	"            end",
+	"            | BLIND k m => let l' := (merge_lists l (find l k n')) in",
+	"              match shallow_search l' k with",
+	"                | true => l' ++ [m]",
+	"                | false => l'",
+	"              end",
+	"            | _ => l",
+	"          end",
+	"    end",
+	"with reconstruct_primitive (l: list value) (p: primitive) (n: nat) : list value :=",
+	"  match n with",
+	"    | 0 => l",
+	"    | S n' => match p with",
+	"        | ENC k m => let l' := find l k n' in",
+	"          let l'' := find l' m n' in",
+	"            match shallow_search l'' k, shallow_search l'' m with",
+	"              | true, true => l'' ++ [prim p]",
+	"              | _, _ => l''",
+	"            end",
+	"        | DEC k c => let l' := find l k n' in",
+	"          let l'' := find l' c n' in",
+	"            match shallow_search l'' k, shallow_search l'' c with",
+	"              | true, true => l'' ++ [prim p]",
+	"              | _, _ => l''",
+	"            end",
+	"        | AEAD_ENC k m ad => let l' := find l k n' in",
+	"          let l'' := find l' m n' in",
+	"          let l''' := find l'' ad n' in",
+	"          match shallow_search l''' k, shallow_search l''' m, shallow_search l''' ad with",
+	"            | true, true, true => l''' ++ [prim p]",
+	"            | _, _, _ => l'''",
+	"          end",
+	"        | AEAD_DEC k c ad => let l' := find l k n' in",
+	"          let l'' := find l' c n' in",
+	"          let l''' := find l'' ad n' in",
+	"          match shallow_search l''' k, shallow_search l''' c, shallow_search l''' ad with",
+	"            | true, true, true => l''' ++ [prim p]",
+	"            | _, _, _ => l'''",
+	"          end",
+	"        | PKE_ENC gk m => let l' := find l gk n' in",
+	"          let l'' := find l' m n' in",
+	"          match shallow_search l'' gk, shallow_search l'' m with",
+	"            | true, true => l'' ++ [prim p]",
+	"            | _, _ => l''",
+	"          end",
+	"        | PKE_DEC k c => let l' := find l k n' in",
+	"          let l'' := find l' c n' in",
+	"          match shallow_search l'' k, shallow_search l'' c with",
+	"            | true, true => l'' ++ [prim p]",
+	"            | _, _ => l''",
+	"          end",
+	"        | HASH1 a => let l' := find l a n' in",
+	"          match shallow_search l' a with",
+	"            | true => l' ++ [prim p]",
+	"            | false => l'",
+	"          end",
+	"        | HASH2 a b => let l' := find l a n' in",
+	"          let l'' := find l' b n' in",
+	"          match shallow_search l'' a, shallow_search l'' b with",
+	"            | true, true => l'' ++ [prim p]",
+	"            | _, _ => l''",
+	"          end",
+	"        | HASH3 a b c => let l' := find l a n' in",
+	"          let l'' := find l' b n' in",
+	"          let l''' := find l'' c n' in",
+	"          match shallow_search l''' a, shallow_search l''' b, shallow_search l''' c with",
+	"            | true, true, true => l''' ++ [prim p]",
+	"            | _, _, _ => l'''",
+	"          end",
+	"        | HASH4 a b c d => let l' := find l a n' in",
+	"          let l'' := find l' b n' in",
+	"          let l''' := find l'' c n' in",
+	"          let l'''' := find l''' d n' in",
+	"          match shallow_search l'''' a, shallow_search l'''' b, shallow_search l'''' c, shallow_search l'''' d with",
+	"            | true, true, true, true => l'''' ++ [prim p]",
+	"            | _, _, _, _ => l''''",
+	"          end",
+	"        | HASH5 a b c d e => let l' := find l a n' in",
+	"          let l'' := find l' b n' in",
+	"          let l''' := find l'' c n' in",
+	"          let l'''' := find l''' d n' in",
+	"          let l''''' := find l'''' e n' in",
+	"          match shallow_search l''''' a, shallow_search l''''' b, shallow_search l''''' c, shallow_search l''''' d, shallow_search l''''' e with",
+	"            | true, true, true, true, true => l''''' ++ [prim p]",
+	"            | _, _, _, _, _ => l'''''",
+	"          end",
+	"        | MAC k m => let l' := find l k n' in",
+	"          let l'' := find l' m n' in",
+	"            match shallow_search l'' k, shallow_search l'' m with",
+	"              | true, true => l'' ++ [prim p]",
+	"              | _, _ => l''",
+	"            end",
+	"        | HKDF1 salt ikm info => let l' := find l salt n' in",
+	"          let l'' := find l' ikm n' in",
+	"          let l''' := find l'' info n' in",
+	"          match shallow_search l''' salt, shallow_search l''' ikm, shallow_search l''' info with",
+	"              | true, true, true => l''' ++ [prim p]",
+	"              | _, _, _ => l'''",
+	"            end",
+	"        | HKDF2 salt ikm info => let l' := find l salt n' in",
+	"          let l'' := find l' ikm n' in",
+	"          let l''' := find l'' info n' in",
+	"          match shallow_search l''' salt, shallow_search l''' ikm, shallow_search l''' info with",
+	"              | true, true, true => l''' ++ [prim p]",
+	"              | _, _, _ => l'''",
+	"            end",
+	"        | HKDF3 salt ikm info => let l' := find l salt n' in",
+	"          let l'' := find l' ikm n' in",
+	"          let l''' := find l'' info n' in",
+	"          match shallow_search l''' salt, shallow_search l''' ikm, shallow_search l''' info with",
+	"              | true, true, true => l''' ++ [prim p]",
+	"              | _, _, _ => l'''",
+	"            end",
+	"        | HKDF4 salt ikm info => let l' := find l salt n' in",
+	"          let l'' := find l' ikm n' in",
+	"          let l''' := find l'' info n' in",
+	"          match shallow_search l''' salt, shallow_search l''' ikm, shallow_search l''' info with",
+	"              | true, true, true => l''' ++ [prim p]",
+	"              | _, _, _ => l'''",
+	"            end",
+	"        | HKDF5 salt ikm info => let l' := find l salt n' in",
+	"          let l'' := find l' ikm n' in",
+	"          let l''' := find l'' info n' in",
+	"          match shallow_search l''' salt, shallow_search l''' ikm, shallow_search l''' info with",
+	"              | true, true, true => l''' ++ [prim p]",
+	"              | _, _, _ => l'''",
+	"            end",
+	"        | PW_HASH1 a => let l' := find l a n' in",
+	"          match shallow_search l' a with",
+	"            | true => l' ++ [prim p]",
+	"            | false => l'",
+	"          end",
+	"        | PW_HASH2 a b => let l' := find l a n' in",
+	"          let l'' := find l' b n' in",
+	"          match shallow_search l'' a, shallow_search l'' b with",
+	"            | true, true => l'' ++ [prim p]",
+	"            | _, _ => l''",
+	"          end",
+	"        | PW_HASH3 a b c => let l' := find l a n' in",
+	"          let l'' := find l' b n' in",
+	"          let l''' := find l'' c n' in",
+	"          match shallow_search l''' a, shallow_search l''' b, shallow_search l''' c with",
+	"            | true, true, true => l''' ++ [prim p]",
+	"            | _, _, _ => l'''",
+	"          end",
+	"        | PW_HASH4 a b c d => let l' := find l a n' in",
+	"          let l'' := find l' b n' in",
+	"          let l''' := find l'' c n' in",
+	"          let l'''' := find l''' d n' in",
+	"          match shallow_search l'''' a, shallow_search l'''' b, shallow_search l'''' c, shallow_search l'''' d with",
+	"            | true, true, true, true => l'''' ++ [prim p]",
+	"            | _, _, _, _ => l''''",
+	"          end",
+	"        | PW_HASH5 a b c d e => let l' := find l a n' in",
+	"          let l'' := find l' b n' in",
+	"          let l''' := find l'' c n' in",
+	"          let l'''' := find l''' d n' in",
+	"          let l''''' := find l'''' e n' in",
+	"          match shallow_search l''''' a, shallow_search l''''' b, shallow_search l''''' c, shallow_search l''''' d, shallow_search l''''' e with",
+	"            | true, true, true, true, true => l''''' ++ [prim p]",
+	"            | _, _, _, _, _ => l'''''",
+	"          end",
+	"        | SIGN k m => let l' := find l k n' in",
+	"          let l'' := find l' m n' in",
+	"            match shallow_search l'' k, shallow_search l'' m with",
+	"              | true, true => l'' ++ [prim p]",
+	"              | _, _ => l''",
+	"            end",
+	"",
+	"        | SIGNVERIF k m s => let l' := find l k n' in",
+	"            let l'' := find l' m n' in",
+	"            let l''' := find l'' s n' in",
+	"            match shallow_search l''' k, shallow_search l''' m, shallow_search l''' s with",
+	"              | true, true, true => l''' ++ [prim p]",
+	"              | _, _, _ => l'''",
+	"            end",
+	"        | RINGSIGN ka gkb gkc m => let l' := find l ka n' in",
+	"            let l'' := find l' gkb n' in",
+	"            let l''' := find l'' gkc n' in",
+	"            let l'''' := find l''' m n' in",
+	"            match shallow_search l'''' ka, shallow_search l'''' gkb, shallow_search l'''' gkc, shallow_search l'''' m with",
+	"              | true, true, true, true => l'''' ++ [prim p]",
+	"              | _, _, _, _ => l''''",
+	"            end",
+	"          | RINGSIGNVERIF gka gkb gkc m s => let l' := find l gka n' in",
+	"            let l'' := find l' gkb n' in",
+	"            let l''' := find l'' gkc n' in",
+	"            let l'''' := find l''' m n' in",
+	"            let l''''' := find l'''' s n' in",
+	"            match shallow_search l''''' gka, shallow_search l''''' gkb, shallow_search l''''' gkc, shallow_search l''''' m, shallow_search l''''' s with",
+	"              | true, true, true, true, true => l''''' ++ [prim p]",
+	"              | _, _, _, _, _ => l'''''",
+	"            end",
+	"        | BLIND k m => let l' := find l k n' in",
+	"          let l'' := find l' m n' in",
+	"            match shallow_search l'' k, shallow_search l'' m with",
+	"              | true, true => l'' ++ [prim p]",
+	"              | _, _ => l''",
+	"            end",
+	"        | UNBLIND k m b => let l' := find l k n' in",
+	"            let l'' := find l' m n' in",
+	"            let l''' := find l'' b n' in",
+	"            match shallow_search l''' k, shallow_search l''' m, shallow_search l''' b with",
+	"              | true, true, true => l''' ++ [prim p]",
+	"              | _, _, _ => l'''",
+	"            end",
+	"        | SHAMIR_SPLIT1 k => let l' := find l k n' in",
+	"            match shallow_search l' k with",
+	"              | true => l' ++ [prim p]",
+	"              | false => l'",
+	"            end",
+	"        | SHAMIR_SPLIT2 k => let l' := find l k n' in",
+	"            match shallow_search l' k with",
+	"              | true => l' ++ [prim p]",
+	"              | false => l'",
+	"            end",
+	"        | SHAMIR_SPLIT3 k => let l' := find l k n' in",
+	"            match shallow_search l' k with",
+	"              | true => l' ++ [prim p]",
+	"              | false => l'",
+	"            end",
+	"        | SHAMIR_JOIN sa sb => let l' := find l sa n' in",
+	"            let l'' := find l' sb n' in",
+	"            match shallow_search l'' sa, shallow_search l'' sb with",
+	"              | true, true => l'' ++ [prim p]",
+	"              | _, _ => l''",
+	"            end",
+	"        | CONCAT2 a b => let l' := find l a n' in",
+	"            let l'' := find l' b n' in",
+	"            match shallow_search l'' a, shallow_search l'' b with",
+	"              | true, true => l'' ++ [prim p]",
+	"              | _, _ => l''",
+	"            end",
+	"        | CONCAT3 a b c => let l' := find l a n' in",
+	"            let l'' := find l' b n' in",
+	"            let l''' := find l'' c n' in",
+	"            match shallow_search l''' a, shallow_search l''' b, shallow_search l''' c with",
+	"              | true, true, true => l''' ++ [prim p]",
+	"              | _, _, _ => l'''",
+	"            end",
+	"        | CONCAT4 a b c d => let l' := find l a n' in",
+	"            let l'' := find l' b n' in",
+	"            let l''' := find l'' c n' in",
+	"            let l'''' := find l''' d n' in",
+	"            match shallow_search l'''' a, shallow_search l'''' b, shallow_search l'''' c, shallow_search l'''' d with",
+	"              | true, true, true, true => l'''' ++ [prim p]",
+	"              | _, _, _, _ => l''''",
+	"            end",
+	"        | CONCAT5 a b c d e  => let l' := find l a n' in",
+	"            let l'' := find l' b n' in",
+	"            let l''' := find l'' c n' in",
+	"            let l'''' := find l''' d n' in",
+	"            let l''''' := find l'''' e n' in",
+	"            match shallow_search l''''' a, shallow_search l''''' b, shallow_search l''''' c, shallow_search l''''' d, shallow_search l''''' e with",
+	"              | true, true, true, true, true => l''''' ++ [prim p]",
+	"              | _, _, _, _, _ => l'''''",
+	"            end",
+	"        | SPLIT1 a => let l' := find l a n' in",
+	"            match shallow_search l' a with",
+	"              | true => l' ++ [prim p]",
+	"              | false => l'",
+	"            end",
+	"        | SPLIT2 a => let l' := find l a n' in",
+	"            match shallow_search l' a with",
+	"              | true => l' ++ [prim p]",
+	"              | false => l'",
+	"            end",
+	"        | SPLIT3 a => let l' := find l a n' in",
+	"            match shallow_search l' a with",
+	"              | true => l' ++ [prim p]",
+	"              | false => l'",
+	"            end",
+	"        | SPLIT4 a => let l' := find l a n' in",
+	"            match shallow_search l' a with",
+	"              | true => l' ++ [prim p]",
+	"              | false => l'",
+	"            end",
+	"        | SPLIT5 a => let l' := find l a n' in",
+	"            match shallow_search l' a with",
+	"              | true => l' ++ [prim p]",
+	"              | false => l'",
+	"            end",
+	"      end",
+	" end",
+	"with reconstruct_equation (l: list value) (e: equation) (n: nat) : list value :=",
+	"  match n with",
+	"    | 0 => l",
+	"    | S n' => match e with",
+	"        | PUBKEY _ exp => let l' := find l exp n' in",
+	"            match shallow_search l' exp with",
+	"              | true => l' ++ [eq e]",
+	"              | false => l'",
+	"            end",
+	"        | DH _ exp1 exp2 => let l' := find l exp1 n' in",
+	"            match shallow_search l' exp1 with",
+	"              | true => let l'' := find l' exp2 n' in",
+	"                  match shallow_search l'' exp2 with",
+	"                    | true => l'' ++ [eq e]",
+	"                    | false => let gexp2 := (eq (PUBKEY G exp2)) in",
+	"                      let l''' := find l'' gexp2 n' in",
+	"                      match shallow_search l''' gexp2 with",
+	"                        | true => l''' ++ [eq e]",
+	"                        | false => l'''",
+	"                      end",
+	"                 end",
+	"              | false => let gexp1 := (eq (PUBKEY G exp1)) in",
+	"                let l'' := find l' gexp1 n' in",
+	"                match shallow_search l'' gexp1 with",
+	"                  | true => let l''' := find l'' exp2 n' in",
+	"                    match shallow_search l''' exp2 with",
+	"                      | true => l''' ++ [eq e]",
+	"                      | false => l'''",
+	"                   end",
+	"                  | false => l''",
+	"                end",
+	"            end",
+	"      end",
+	"  end",
+	"with find (l: list value) (goal: value) (n: nat) : list value := ",
+	"    match n with",
+	"      | 0 => l",
+	"      | S n' => match shallow_search l goal with",
+	"          | true => l",
+	"          | false => match goal with",
+	"              | const c => l",
+	"              | pass a => l",
+	"              | default => l",
+	"              | eq e => reconstruct_equation l e n'",
+	"              | prim p => let l' := decompose_primitive l p n' in",
+	"                  match shallow_search l' goal with",
+	"                    | true => l'",
+	"                    | false => reconstruct_primitive l' p n'",
+	"                  end ",
+	"            end",
+	"        end",
+	"    end.",
+	"",
+	"Fixpoint analysis_decompose (l: list value) (i n: nat): list value :=",
+	"match n with",
+	"| 0 => l",
+	"| S n' => match ((List.length l) =? i) with",
+	"    | true => l",
+	"    | false => match l with",
+	"        | [] => []",
+	"        | h :: t =>",
+	"        let v := (nth i l default) in",
+	"        match v with",
+	"          | prim p => let l' := decompose_primitive l p n' in",
+	"              match (List.length l =? List.length l') with",
+	"                | true => analysis_decompose l (i+1) n'",
+	"                | false => analysis_decompose l' 0 n'",
+	"                end",
+	"          | _ => analysis_decompose l (i+1) n'",
+	"          end",
+	"      end",
+	"  end",
+	"end.",
+	"",
+	"Fixpoint analysis_concat (l: list value) : list value :=",
+	"  match l with",
+	"    | [] => []",
+	"    | h :: t => match h with",
+	"        | prim p => match p with",
+	"            | CONCAT2 a b =>  [a; b] ++ analysis_concat t",
+	"            | CONCAT3 a b c => [a; b; c] ++ analysis_concat t",
+	"            | CONCAT4 a b c d => [a; b; c; d] ++ analysis_concat t",
+	"            | CONCAT5 a b c d e => [a; b; c; d; e] ++ analysis_concat t",
+	"            | _ => [h] ++ analysis_concat t",
+	"            end",
+	"        | _ => [h] ++ analysis_concat t",
+	"      end",
+	"  end.",
+	"",
+	"",
+	"Inductive query : Type :=",
+	"  | confidentiality: value -> query.",
+	"",
+	"Definition resolve_query (q: query) (l: list value) : bool := ",
+	"  match q with",
+	"    | confidentiality v => shallow_search l v",
+	"  end.",
+	"",
+	"Definition recompose (l: list value) (v: value) : list value :=",
+	"  match ((shallow_search l (prim(SHAMIR_SPLIT1 v)) && shallow_search l (prim(SHAMIR_SPLIT2 v)))",
+	"    || (shallow_search l (prim(SHAMIR_SPLIT1 v)) && shallow_search l (prim(SHAMIR_SPLIT3 v)))",
+	"    || (shallow_search l (prim(SHAMIR_SPLIT2 v)) && shallow_search l (prim(SHAMIR_SPLIT3 v))) ",
+	"    )  with",
+	"    | true => l ++ [v]",
+	"    | false => l",
+	"  end.",
+	"",
+	"Fixpoint recompose_analysis (l: list value) (pl: list (list value)) (n: nat) : list value :=",
+	"match n with",
+	"  | 0 => l",
+	"  | S n' => match pl with",
+	"    | [] => l",
+	"    | h :: t => match h with",
+	"        | [] => merge_lists l (recompose_analysis l t n')",
+	"        | h' :: t' => let l' := recompose l h' in",
+	"            merge_lists l' (recompose_analysis l' ([t']++ t) n')",
+	"          end",
+	"          end",
+	"        end.",
+	"",
+	"Fixpoint reconstruct_analysis (l: list value) (pl: list(list value)) (n: nat) : list value :=",
+	"  match n with",
+	"    | 0 => l",
+	"    | S n' => match pl with",
+	"        | [] => l",
+	"        |  h :: t => match h with",
+	"            | [] => merge_lists l (reconstruct_analysis l t n')",
+	"            | h' :: t' => match h' with",
+	"                | prim p => let l' := reconstruct_primitive l p n' in",
+	"                   merge_lists l' (reconstruct_analysis l' ([t'] ++ t) n')",
+	"                | eq e => let l' := reconstruct_equation l e n' in",
+	"                  merge_lists l' (reconstruct_analysis l' ([t'] ++ t) n')",
+	"                | _ => merge_lists l (reconstruct_analysis l ([t'] ++ t) n')",
+	"              end",
+	"          end",
+	"      end",
+	"  end.",
+	"             ",
+	"",
+	"Fixpoint analysis (q: query) (ak: list value) (p: list (list value)) (n: nat) : bool :=",
+	"  match n with",
+	"    | 0 => true",
+	"    | S n' => match ak with",
+	"        | [] => true",
+	"        | _ => let ak2 := analysis_decompose ak 0 n' in",
+	"            let ak3 := analysis_concat ak2 in",
+	"            let ak4 := recompose_analysis ak3 p n' in",
+	"            let ak5 := reconstruct_analysis ak4 p n'",
+	"          in match resolve_query q ak with",
+	"              | true => false",
+	"              | false => match (List.length ak =? List.length ak5) with",
+	"                  | true => true",
+	"                  | false => analysis q ak5 p n'",
+	"                end",
+	"           end",
+	"       end",
+	"  end.",
+	""},
+	"\n")
diff --git a/cmd/vplogic/libpeg.go b/cmd/vplogic/libpeg.go
new file mode 100644
index 0000000..f004942
--- /dev/null
+++ b/cmd/vplogic/libpeg.go
@@ -0,0 +1,3526 @@
+// Code generated by pigeon; DO NOT EDIT.
+
+/* SPDX-FileCopyrightText: © 2019-2022 Nadim Kobeissi <nadim@symbolic.software>
+ * SPDX-License-Identifier: GPL-3.0-only */
+
+// This file is generated automatically from libpeg.peg.
+// Do not modify.
+
+package vplogic
+
+import (
+	"bytes"
+	"errors"
+	"fmt"
+	"io"
+	"math"
+	"os"
+	"path/filepath"
+	"sort"
+	"strconv"
+	"strings"
+	"sync"
+	"unicode"
+	"unicode/utf8"
+)
+
+var libpegReserved = []string{
+	"attacker", "passive", "active", "principal",
+	"knows", "generates", "leaks",
+	"phase", "public", "private", "password",
+	"confidentiality", "authentication",
+	"freshness", "unlinkability", "equivalence",
+	"precondition", "ringsign", "ringsignverif",
+	"primitive", "pw_hash", "hash", "hkdf",
+	"aead_enc", "aead_dec", "enc", "dec",
+	"mac", "assert", "sign", "signverif",
+	"pke_enc", "pke_dec", "shamir_split",
+	"shamir_join", "concat", "split", "unnamed",
+}
+
+var libpegUnnamedCounter = 0
+
+func libpegCheckIfReserved(s string) error {
+	found := false
+	switch {
+	case strInSlice(s, libpegReserved):
+		found = true
+	case strings.HasPrefix(s, "attacker"):
+		found = true
+	case strings.HasPrefix(s, "unnamed"):
+		found = true
+	}
+	if found {
+		return fmt.Errorf("cannot use reserved keyword in Name: %s", s)
+	}
+	return nil
+}
+
+func libpegParseModel(filePath string, verbose bool) (Model, error) {
+	fileName := filepath.Base(filePath)
+	if len(fileName) > 64 {
+		return Model{}, fmt.Errorf("model file name must be 64 characters or less")
+	}
+	if filepath.Ext(fileName) != ".vp" {
+		return Model{}, fmt.Errorf("model file name must have a '.vp' extension")
+	}
+	if verbose {
+		InfoMessage(fmt.Sprintf(
+			"Parsing model '%s'...", fileName,
+		), "verifpal", false)
+	}
+	parsed, err := ParseFile(filePath)
+	if err != nil {
+		return Model{}, err
+	}
+	m := parsed.(Model)
+	m.FileName = fileName
+	return m, nil
+}
+
+var g = &grammar{
+	rules: []*rule{
+		{
+			name: "Model",
+			pos:  position{line: 79, col: 1, offset: 1779},
+			expr: &actionExpr{
+				pos: position{line: 79, col: 10, offset: 1788},
+				run: (*parser).callonModel1,
+				expr: &seqExpr{
+					pos: position{line: 79, col: 10, offset: 1788},
+					exprs: []any{
+						&ruleRefExpr{
+							pos:  position{line: 79, col: 10, offset: 1788},
+							name: "_",
+						},
+						&zeroOrMoreExpr{
+							pos: position{line: 79, col: 12, offset: 1790},
+							expr: &ruleRefExpr{
+								pos:  position{line: 79, col: 12, offset: 1790},
+								name: "Comment",
+							},
+						},
+						&labeledExpr{
+							pos:   position{line: 79, col: 21, offset: 1799},
+							label: "Attacker",
+							expr: &zeroOrOneExpr{
+								pos: position{line: 79, col: 30, offset: 1808},
+								expr: &ruleRefExpr{
+									pos:  position{line: 79, col: 30, offset: 1808},
+									name: "Attacker",
+								},
+							},
+						},
+						&labeledExpr{
+							pos:   position{line: 79, col: 40, offset: 1818},
+							label: "Blocks",
+							expr: &zeroOrOneExpr{
+								pos: position{line: 79, col: 47, offset: 1825},
+								expr: &oneOrMoreExpr{
+									pos: position{line: 79, col: 48, offset: 1826},
+									expr: &ruleRefExpr{
+										pos:  position{line: 79, col: 48, offset: 1826},
+										name: "Block",
+									},
+								},
+							},
+						},
+						&labeledExpr{
+							pos:   position{line: 79, col: 57, offset: 1835},
+							label: "Queries",
+							expr: &zeroOrOneExpr{
+								pos: position{line: 79, col: 65, offset: 1843},
+								expr: &ruleRefExpr{
+									pos:  position{line: 79, col: 65, offset: 1843},
+									name: "Queries",
+								},
+							},
+						},
+						&zeroOrMoreExpr{
+							pos: position{line: 79, col: 74, offset: 1852},
+							expr: &ruleRefExpr{
+								pos:  position{line: 79, col: 74, offset: 1852},
+								name: "Comment",
+							},
+						},
+						&ruleRefExpr{
+							pos:  position{line: 79, col: 83, offset: 1861},
+							name: "_",
+						},
+						&ruleRefExpr{
+							pos:  position{line: 79, col: 85, offset: 1863},
+							name: "EOF",
+						},
+					},
+				},
+			},
+		},
+		{
+			name: "Attacker",
+			pos:  position{line: 101, col: 1, offset: 2415},
+			expr: &actionExpr{
+				pos: position{line: 101, col: 13, offset: 2427},
+				run: (*parser).callonAttacker1,
+				expr: &seqExpr{
+					pos: position{line: 101, col: 13, offset: 2427},
+					exprs: []any{
+						&litMatcher{
+							pos:        position{line: 101, col: 13, offset: 2427},
+							val:        "attacker",
+							ignoreCase: false,
+							want:       "\"attacker\"",
+						},
+						&ruleRefExpr{
+							pos:  position{line: 101, col: 24, offset: 2438},
+							name: "_",
+						},
+						&litMatcher{
+							pos:        position{line: 101, col: 26, offset: 2440},
+							val:        "[",
+							ignoreCase: false,
+							want:       "\"[\"",
+						},
+						&ruleRefExpr{
+							pos:  position{line: 101, col: 30, offset: 2444},
+							name: "_",
+						},
+						&labeledExpr{
+							pos:   position{line: 101, col: 32, offset: 2446},
+							label: "Type",
+							expr: &zeroOrOneExpr{
+								pos: position{line: 101, col: 37, offset: 2451},
+								expr: &ruleRefExpr{
+									pos:  position{line: 101, col: 37, offset: 2451},
+									name: "AttackerType",
+								},
+							},
+						},
+						&ruleRefExpr{
+							pos:  position{line: 101, col: 51, offset: 2465},
+							name: "_",
+						},
+						&litMatcher{
+							pos:        position{line: 101, col: 53, offset: 2467},
+							val:        "]",
+							ignoreCase: false,
+							want:       "\"]\"",
+						},
+						&ruleRefExpr{
+							pos:  position{line: 101, col: 57, offset: 2471},
+							name: "_",
+						},
+					},
+				},
+			},
+		},
+		{
+			name: "AttackerType",
+			pos:  position{line: 108, col: 1, offset: 2595},
+			expr: &actionExpr{
+				pos: position{line: 108, col: 17, offset: 2611},
+				run: (*parser).callonAttackerType1,
+				expr: &choiceExpr{
+					pos: position{line: 108, col: 18, offset: 2612},
+					alternatives: []any{
+						&litMatcher{
+							pos:        position{line: 108, col: 18, offset: 2612},
+							val:        "active",
+							ignoreCase: false,
+							want:       "\"active\"",
+						},
+						&litMatcher{
+							pos:        position{line: 108, col: 27, offset: 2621},
+							val:        "passive",
+							ignoreCase: false,
+							want:       "\"passive\"",
+						},
+					},
+				},
+			},
+		},
+		{
+			name: "Block",
+			pos:  position{line: 112, col: 1, offset: 2665},
+			expr: &actionExpr{
+				pos: position{line: 112, col: 10, offset: 2674},
+				run: (*parser).callonBlock1,
+				expr: &seqExpr{
+					pos: position{line: 112, col: 10, offset: 2674},
+					exprs: []any{
+						&zeroOrMoreExpr{
+							pos: position{line: 112, col: 10, offset: 2674},
+							expr: &ruleRefExpr{
+								pos:  position{line: 112, col: 10, offset: 2674},
+								name: "Comment",
+							},
+						},
+						&labeledExpr{
+							pos:   position{line: 112, col: 19, offset: 2683},
+							label: "Block",
+							expr: &choiceExpr{
+								pos: position{line: 112, col: 26, offset: 2690},
+								alternatives: []any{
+									&ruleRefExpr{
+										pos:  position{line: 112, col: 26, offset: 2690},
+										name: "Phase",
+									},
+									&ruleRefExpr{
+										pos:  position{line: 112, col: 32, offset: 2696},
+										name: "Principal",
+									},
+									&ruleRefExpr{
+										pos:  position{line: 112, col: 42, offset: 2706},
+										name: "Message",
+									},
+								},
+							},
+						},
+						&ruleRefExpr{
+							pos:  position{line: 112, col: 51, offset: 2715},
+							name: "_",
+						},
+						&zeroOrMoreExpr{
+							pos: position{line: 112, col: 53, offset: 2717},
+							expr: &ruleRefExpr{
+								pos:  position{line: 112, col: 53, offset: 2717},
+								name: "Comment",
+							},
+						},
+					},
+				},
+			},
+		},
+		{
+			name: "Principal",
+			pos:  position{line: 116, col: 1, offset: 2750},
+			expr: &actionExpr{
+				pos: position{line: 116, col: 14, offset: 2763},
+				run: (*parser).callonPrincipal1,
+				expr: &seqExpr{
+					pos: position{line: 116, col: 14, offset: 2763},
+					exprs: []any{
+						&litMatcher{
+							pos:        position{line: 116, col: 14, offset: 2763},
+							val:        "principal",
+							ignoreCase: false,
+							want:       "\"principal\"",
+						},
+						&ruleRefExpr{
+							pos:  position{line: 116, col: 26, offset: 2775},
+							name: "_",
+						},
+						&labeledExpr{
+							pos:   position{line: 116, col: 28, offset: 2777},
+							label: "Name",
+							expr: &ruleRefExpr{
+								pos:  position{line: 116, col: 33, offset: 2782},
+								name: "PrincipalName",
+							},
+						},
+						&ruleRefExpr{
+							pos:  position{line: 116, col: 47, offset: 2796},
+							name: "_",
+						},
+						&litMatcher{
+							pos:        position{line: 116, col: 49, offset: 2798},
+							val:        "[",
+							ignoreCase: false,
+							want:       "\"[\"",
+						},
+						&ruleRefExpr{
+							pos:  position{line: 116, col: 53, offset: 2802},
+							name: "_",
+						},
+						&zeroOrMoreExpr{
+							pos: position{line: 116, col: 55, offset: 2804},
+							expr: &ruleRefExpr{
+								pos:  position{line: 116, col: 55, offset: 2804},
+								name: "Comment",
+							},
+						},
+						&labeledExpr{
+							pos:   position{line: 116, col: 64, offset: 2813},
+							label: "Expressions",
+							expr: &zeroOrMoreExpr{
+								pos: position{line: 116, col: 77, offset: 2826},
+								expr: &ruleRefExpr{
+									pos:  position{line: 116, col: 77, offset: 2826},
+									name: "Expression",
+								},
+							},
+						},
+						&zeroOrMoreExpr{
+							pos: position{line: 116, col: 90, offset: 2839},
+							expr: &ruleRefExpr{
+								pos:  position{line: 116, col: 90, offset: 2839},
+								name: "Comment",
+							},
+						},
+						&ruleRefExpr{
+							pos:  position{line: 116, col: 99, offset: 2848},
+							name: "_",
+						},
+						&litMatcher{
+							pos:        position{line: 116, col: 101, offset: 2850},
+							val:        "]",
+							ignoreCase: false,
+							want:       "\"]\"",
+						},
+						&ruleRefExpr{
+							pos:  position{line: 116, col: 105, offset: 2854},
+							name: "_",
+						},
+					},
+				},
+			},
+		},
+		{
+			name: "PrincipalName",
+			pos:  position{line: 131, col: 1, offset: 3149},
+			expr: &actionExpr{
+				pos: position{line: 131, col: 18, offset: 3166},
+				run: (*parser).callonPrincipalName1,
+				expr: &labeledExpr{
+					pos:   position{line: 131, col: 18, offset: 3166},
+					label: "Name",
+					expr: &ruleRefExpr{
+						pos:  position{line: 131, col: 23, offset: 3171},
+						name: "Identifier",
+					},
+				},
+			},
+		},
+		{
+			name: "Qualifier",
+			pos:  position{line: 136, col: 1, offset: 3274},
+			expr: &actionExpr{
+				pos: position{line: 136, col: 14, offset: 3287},
+				run: (*parser).callonQualifier1,
+				expr: &choiceExpr{
+					pos: position{line: 136, col: 15, offset: 3288},
+					alternatives: []any{
+						&litMatcher{
+							pos:        position{line: 136, col: 15, offset: 3288},
+							val:        "private",
+							ignoreCase: false,
+							want:       "\"private\"",
+						},
+						&litMatcher{
+							pos:        position{line: 136, col: 25, offset: 3298},
+							val:        "public",
+							ignoreCase: false,
+							want:       "\"public\"",
+						},
+						&litMatcher{
+							pos:        position{line: 136, col: 34, offset: 3307},
+							val:        "password",
+							ignoreCase: false,
+							want:       "\"password\"",
+						},
+					},
+				},
+			},
+		},
+		{
+			name: "Message",
+			pos:  position{line: 147, col: 1, offset: 3495},
+			expr: &actionExpr{
+				pos: position{line: 147, col: 12, offset: 3506},
+				run: (*parser).callonMessage1,
+				expr: &seqExpr{
+					pos: position{line: 147, col: 12, offset: 3506},
+					exprs: []any{
+						&labeledExpr{
+							pos:   position{line: 147, col: 12, offset: 3506},
+							label: "Sender",
+							expr: &zeroOrOneExpr{
+								pos: position{line: 147, col: 19, offset: 3513},
+								expr: &ruleRefExpr{
+									pos:  position{line: 147, col: 19, offset: 3513},
+									name: "PrincipalName",
+								},
+							},
+						},
+						&ruleRefExpr{
+							pos:  position{line: 147, col: 34, offset: 3528},
+							name: "_",
+						},
+						&choiceExpr{
+							pos: position{line: 147, col: 37, offset: 3531},
+							alternatives: []any{
+								&litMatcher{
+									pos:        position{line: 147, col: 37, offset: 3531},
+									val:        "->",
+									ignoreCase: false,
+									want:       "\"->\"",
+								},
+								&litMatcher{
+									pos:        position{line: 147, col: 42, offset: 3536},
+									val:        "→",
+									ignoreCase: false,
+									want:       "\"→\"",
+								},
+							},
+						},
+						&ruleRefExpr{
+							pos:  position{line: 147, col: 47, offset: 3543},
+							name: "_",
+						},
+						&labeledExpr{
+							pos:   position{line: 147, col: 49, offset: 3545},
+							label: "Recipient",
+							expr: &zeroOrOneExpr{
+								pos: position{line: 147, col: 59, offset: 3555},
+								expr: &ruleRefExpr{
+									pos:  position{line: 147, col: 59, offset: 3555},
+									name: "PrincipalName",
+								},
+							},
+						},
+						&ruleRefExpr{
+							pos:  position{line: 147, col: 74, offset: 3570},
+							name: "_",
+						},
+						&litMatcher{
+							pos:        position{line: 147, col: 76, offset: 3572},
+							val:        ":",
+							ignoreCase: false,
+							want:       "\":\"",
+						},
+						&ruleRefExpr{
+							pos:  position{line: 147, col: 80, offset: 3576},
+							name: "_",
+						},
+						&labeledExpr{
+							pos:   position{line: 147, col: 82, offset: 3578},
+							label: "Constants",
+							expr: &zeroOrOneExpr{
+								pos: position{line: 147, col: 92, offset: 3588},
+								expr: &ruleRefExpr{
+									pos:  position{line: 147, col: 92, offset: 3588},
+									name: "MessageConstants",
+								},
+							},
+						},
+					},
+				},
+			},
+		},
+		{
+			name: "MessageConstants",
+			pos:  position{line: 168, col: 1, offset: 4142},
+			expr: &actionExpr{
+				pos: position{line: 168, col: 21, offset: 4162},
+				run: (*parser).callonMessageConstants1,
+				expr: &labeledExpr{
+					pos:   position{line: 168, col: 21, offset: 4162},
+					label: "MessageConstants",
+					expr: &oneOrMoreExpr{
+						pos: position{line: 168, col: 38, offset: 4179},
+						expr: &choiceExpr{
+							pos: position{line: 168, col: 39, offset: 4180},
+							alternatives: []any{
+								&ruleRefExpr{
+									pos:  position{line: 168, col: 39, offset: 4180},
+									name: "GuardedConstant",
+								},
+								&ruleRefExpr{
+									pos:  position{line: 168, col: 55, offset: 4196},
+									name: "Constant",
+								},
+							},
+						},
+					},
+				},
+			},
+		},
+		{
+			name: "Expression",
+			pos:  position{line: 178, col: 1, offset: 4370},
+			expr: &actionExpr{
+				pos: position{line: 178, col: 15, offset: 4384},
+				run: (*parser).callonExpression1,
+				expr: &seqExpr{
+					pos: position{line: 178, col: 15, offset: 4384},
+					exprs: []any{
+						&zeroOrMoreExpr{
+							pos: position{line: 178, col: 15, offset: 4384},
+							expr: &ruleRefExpr{
+								pos:  position{line: 178, col: 15, offset: 4384},
+								name: "Comment",
+							},
+						},
+						&labeledExpr{
+							pos:   position{line: 178, col: 24, offset: 4393},
+							label: "Expression",
+							expr: &choiceExpr{
+								pos: position{line: 178, col: 36, offset: 4405},
+								alternatives: []any{
+									&ruleRefExpr{
+										pos:  position{line: 178, col: 36, offset: 4405},
+										name: "Knows",
+									},
+									&ruleRefExpr{
+										pos:  position{line: 178, col: 42, offset: 4411},
+										name: "Generates",
+									},
+									&ruleRefExpr{
+										pos:  position{line: 178, col: 52, offset: 4421},
+										name: "Leaks",
+									},
+									&ruleRefExpr{
+										pos:  position{line: 178, col: 58, offset: 4427},
+										name: "Assignment",
+									},
+								},
+							},
+						},
+						&ruleRefExpr{
+							pos:  position{line: 178, col: 70, offset: 4439},
+							name: "_",
+						},
+						&zeroOrMoreExpr{
+							pos: position{line: 178, col: 72, offset: 4441},
+							expr: &ruleRefExpr{
+								pos:  position{line: 178, col: 72, offset: 4441},
+								name: "Comment",
+							},
+						},
+					},
+				},
+			},
+		},
+		{
+			name: "Knows",
+			pos:  position{line: 182, col: 1, offset: 4479},
+			expr: &actionExpr{
+				pos: position{line: 182, col: 10, offset: 4488},
+				run: (*parser).callonKnows1,
+				expr: &seqExpr{
+					pos: position{line: 182, col: 10, offset: 4488},
+					exprs: []any{
+						&litMatcher{
+							pos:        position{line: 182, col: 10, offset: 4488},
+							val:        "knows",
+							ignoreCase: false,
+							want:       "\"knows\"",
+						},
+						&ruleRefExpr{
+							pos:  position{line: 182, col: 18, offset: 4496},
+							name: "_",
+						},
+						&labeledExpr{
+							pos:   position{line: 182, col: 20, offset: 4498},
+							label: "Qualifier",
+							expr: &zeroOrOneExpr{
+								pos: position{line: 182, col: 30, offset: 4508},
+								expr: &ruleRefExpr{
+									pos:  position{line: 182, col: 30, offset: 4508},
+									name: "Qualifier",
+								},
+							},
+						},
+						&ruleRefExpr{
+							pos:  position{line: 182, col: 41, offset: 4519},
+							name: "_",
+						},
+						&labeledExpr{
+							pos:   position{line: 182, col: 43, offset: 4521},
+							label: "Constants",
+							expr: &zeroOrOneExpr{
+								pos: position{line: 182, col: 53, offset: 4531},
+								expr: &ruleRefExpr{
+									pos:  position{line: 182, col: 53, offset: 4531},
+									name: "Constants",
+								},
+							},
+						},
+					},
+				},
+			},
+		},
+		{
+			name: "Generates",
+			pos:  position{line: 196, col: 1, offset: 4883},
+			expr: &actionExpr{
+				pos: position{line: 196, col: 14, offset: 4896},
+				run: (*parser).callonGenerates1,
+				expr: &seqExpr{
+					pos: position{line: 196, col: 14, offset: 4896},
+					exprs: []any{
+						&litMatcher{
+							pos:        position{line: 196, col: 14, offset: 4896},
+							val:        "generates",
+							ignoreCase: false,
+							want:       "\"generates\"",
+						},
+						&ruleRefExpr{
+							pos:  position{line: 196, col: 26, offset: 4908},
+							name: "_",
+						},
+						&labeledExpr{
+							pos:   position{line: 196, col: 28, offset: 4910},
+							label: "Constants",
+							expr: &zeroOrOneExpr{
+								pos: position{line: 196, col: 38, offset: 4920},
+								expr: &ruleRefExpr{
+									pos:  position{line: 196, col: 38, offset: 4920},
+									name: "Constants",
+								},
+							},
+						},
+					},
+				},
+			},
+		},
+		{
+			name: "Leaks",
+			pos:  position{line: 207, col: 1, offset: 5165},
+			expr: &actionExpr{
+				pos: position{line: 207, col: 10, offset: 5174},
+				run: (*parser).callonLeaks1,
+				expr: &seqExpr{
+					pos: position{line: 207, col: 10, offset: 5174},
+					exprs: []any{
+						&litMatcher{
+							pos:        position{line: 207, col: 10, offset: 5174},
+							val:        "leaks",
+							ignoreCase: false,
+							want:       "\"leaks\"",
+						},
+						&ruleRefExpr{
+							pos:  position{line: 207, col: 18, offset: 5182},
+							name: "_",
+						},
+						&labeledExpr{
+							pos:   position{line: 207, col: 20, offset: 5184},
+							label: "Constants",
+							expr: &zeroOrOneExpr{
+								pos: position{line: 207, col: 30, offset: 5194},
+								expr: &ruleRefExpr{
+									pos:  position{line: 207, col: 30, offset: 5194},
+									name: "Constants",
+								},
+							},
+						},
+					},
+				},
+			},
+		},
+		{
+			name: "Assignment",
+			pos:  position{line: 218, col: 1, offset: 5431},
+			expr: &actionExpr{
+				pos: position{line: 218, col: 15, offset: 5445},
+				run: (*parser).callonAssignment1,
+				expr: &seqExpr{
+					pos: position{line: 218, col: 15, offset: 5445},
+					exprs: []any{
+						&labeledExpr{
+							pos:   position{line: 218, col: 15, offset: 5445},
+							label: "Left",
+							expr: &zeroOrOneExpr{
+								pos: position{line: 218, col: 20, offset: 5450},
+								expr: &ruleRefExpr{
+									pos:  position{line: 218, col: 20, offset: 5450},
+									name: "Constants",
+								},
+							},
+						},
+						&ruleRefExpr{
+							pos:  position{line: 218, col: 31, offset: 5461},
+							name: "_",
+						},
+						&litMatcher{
+							pos:        position{line: 218, col: 33, offset: 5463},
+							val:        "=",
+							ignoreCase: false,
+							want:       "\"=\"",
+						},
+						&ruleRefExpr{
+							pos:  position{line: 218, col: 37, offset: 5467},
+							name: "_",
+						},
+						&labeledExpr{
+							pos:   position{line: 218, col: 39, offset: 5469},
+							label: "Right",
+							expr: &zeroOrOneExpr{
+								pos: position{line: 218, col: 45, offset: 5475},
+								expr: &ruleRefExpr{
+									pos:  position{line: 218, col: 45, offset: 5475},
+									name: "Value",
+								},
+							},
+						},
+					},
+				},
+			},
+		},
+		{
+			name: "Constant",
+			pos:  position{line: 234, col: 1, offset: 5824},
+			expr: &actionExpr{
+				pos: position{line: 234, col: 13, offset: 5836},
+				run: (*parser).callonConstant1,
+				expr: &seqExpr{
+					pos: position{line: 234, col: 13, offset: 5836},
+					exprs: []any{
+						&labeledExpr{
+							pos:   position{line: 234, col: 13, offset: 5836},
+							label: "Const",
+							expr: &ruleRefExpr{
+								pos:  position{line: 234, col: 19, offset: 5842},
+								name: "Identifier",
+							},
+						},
+						&zeroOrOneExpr{
+							pos: position{line: 234, col: 30, offset: 5853},
+							expr: &seqExpr{
+								pos: position{line: 234, col: 31, offset: 5854},
+								exprs: []any{
+									&ruleRefExpr{
+										pos:  position{line: 234, col: 31, offset: 5854},
+										name: "_",
+									},
+									&litMatcher{
+										pos:        position{line: 234, col: 33, offset: 5856},
+										val:        ",",
+										ignoreCase: false,
+										want:       "\",\"",
+									},
+									&ruleRefExpr{
+										pos:  position{line: 234, col: 37, offset: 5860},
+										name: "_",
+									},
+								},
+							},
+						},
+					},
+				},
+			},
+		},
+		{
+			name: "Constants",
+			pos:  position{line: 256, col: 1, offset: 6254},
+			expr: &actionExpr{
+				pos: position{line: 256, col: 14, offset: 6267},
+				run: (*parser).callonConstants1,
+				expr: &labeledExpr{
+					pos:   position{line: 256, col: 14, offset: 6267},
+					label: "Constants",
+					expr: &oneOrMoreExpr{
+						pos: position{line: 256, col: 24, offset: 6277},
+						expr: &ruleRefExpr{
+							pos:  position{line: 256, col: 24, offset: 6277},
+							name: "Constant",
+						},
+					},
+				},
+			},
+		},
+		{
+			name: "Phase",
+			pos:  position{line: 265, col: 1, offset: 6434},
+			expr: &actionExpr{
+				pos: position{line: 265, col: 10, offset: 6443},
+				run: (*parser).callonPhase1,
+				expr: &seqExpr{
+					pos: position{line: 265, col: 10, offset: 6443},
+					exprs: []any{
+						&litMatcher{
+							pos:        position{line: 265, col: 10, offset: 6443},
+							val:        "phase",
+							ignoreCase: false,
+							want:       "\"phase\"",
+						},
+						&ruleRefExpr{
+							pos:  position{line: 265, col: 18, offset: 6451},
+							name: "_",
+						},
+						&litMatcher{
+							pos:        position{line: 265, col: 20, offset: 6453},
+							val:        "[",
+							ignoreCase: false,
+							want:       "\"[\"",
+						},
+						&ruleRefExpr{
+							pos:  position{line: 265, col: 24, offset: 6457},
+							name: "_",
+						},
+						&labeledExpr{
+							pos:   position{line: 265, col: 26, offset: 6459},
+							label: "Number",
+							expr: &oneOrMoreExpr{
+								pos: position{line: 265, col: 33, offset: 6466},
+								expr: &charClassMatcher{
+									pos:        position{line: 265, col: 33, offset: 6466},
+									val:        "[0-9]",
+									ranges:     []rune{'0', '9'},
+									ignoreCase: false,
+									inverted:   false,
+								},
+							},
+						},
+						&ruleRefExpr{
+							pos:  position{line: 265, col: 40, offset: 6473},
+							name: "_",
+						},
+						&litMatcher{
+							pos:        position{line: 265, col: 42, offset: 6475},
+							val:        "]",
+							ignoreCase: false,
+							want:       "\"]\"",
+						},
+						&ruleRefExpr{
+							pos:  position{line: 265, col: 46, offset: 6479},
+							name: "_",
+						},
+					},
+				},
+			},
+		},
+		{
+			name: "GuardedConstant",
+			pos:  position{line: 278, col: 1, offset: 6701},
+			expr: &actionExpr{
+				pos: position{line: 278, col: 20, offset: 6720},
+				run: (*parser).callonGuardedConstant1,
+				expr: &seqExpr{
+					pos: position{line: 278, col: 20, offset: 6720},
+					exprs: []any{
+						&litMatcher{
+							pos:        position{line: 278, col: 20, offset: 6720},
+							val:        "[",
+							ignoreCase: false,
+							want:       "\"[\"",
+						},
+						&labeledExpr{
+							pos:   position{line: 278, col: 24, offset: 6724},
+							label: "Guarded",
+							expr: &ruleRefExpr{
+								pos:  position{line: 278, col: 32, offset: 6732},
+								name: "Constant",
+							},
+						},
+						&litMatcher{
+							pos:        position{line: 278, col: 41, offset: 6741},
+							val:        "]",
+							ignoreCase: false,
+							want:       "\"]\"",
+						},
+						&zeroOrOneExpr{
+							pos: position{line: 278, col: 45, offset: 6745},
+							expr: &seqExpr{
+								pos: position{line: 278, col: 46, offset: 6746},
+								exprs: []any{
+									&ruleRefExpr{
+										pos:  position{line: 278, col: 46, offset: 6746},
+										name: "_",
+									},
+									&litMatcher{
+										pos:        position{line: 278, col: 48, offset: 6748},
+										val:        ",",
+										ignoreCase: false,
+										want:       "\",\"",
+									},
+									&ruleRefExpr{
+										pos:  position{line: 278, col: 52, offset: 6752},
+										name: "_",
+									},
+								},
+							},
+						},
+					},
+				},
+			},
+		},
+		{
+			name: "Primitive",
+			pos:  position{line: 291, col: 1, offset: 6994},
+			expr: &actionExpr{
+				pos: position{line: 291, col: 14, offset: 7007},
+				run: (*parser).callonPrimitive1,
+				expr: &seqExpr{
+					pos: position{line: 291, col: 14, offset: 7007},
+					exprs: []any{
+						&labeledExpr{
+							pos:   position{line: 291, col: 14, offset: 7007},
+							label: "Name",
+							expr: &ruleRefExpr{
+								pos:  position{line: 291, col: 19, offset: 7012},
+								name: "PrimitiveName",
+							},
+						},
+						&litMatcher{
+							pos:        position{line: 291, col: 33, offset: 7026},
+							val:        "(",
+							ignoreCase: false,
+							want:       "\"(\"",
+						},
+						&ruleRefExpr{
+							pos:  position{line: 291, col: 37, offset: 7030},
+							name: "_",
+						},
+						&labeledExpr{
+							pos:   position{line: 291, col: 39, offset: 7032},
+							label: "Arguments",
+							expr: &oneOrMoreExpr{
+								pos: position{line: 291, col: 49, offset: 7042},
+								expr: &ruleRefExpr{
+									pos:  position{line: 291, col: 49, offset: 7042},
+									name: "Value",
+								},
+							},
+						},
+						&ruleRefExpr{
+							pos:  position{line: 291, col: 56, offset: 7049},
+							name: "_",
+						},
+						&litMatcher{
+							pos:        position{line: 291, col: 58, offset: 7051},
+							val:        ")",
+							ignoreCase: false,
+							want:       "\")\"",
+						},
+						&labeledExpr{
+							pos:   position{line: 291, col: 62, offset: 7055},
+							label: "Check",
+							expr: &zeroOrOneExpr{
+								pos: position{line: 291, col: 68, offset: 7061},
+								expr: &litMatcher{
+									pos:        position{line: 291, col: 68, offset: 7061},
+									val:        "?",
+									ignoreCase: false,
+									want:       "\"?\"",
+								},
+							},
+						},
+						&zeroOrOneExpr{
+							pos: position{line: 291, col: 73, offset: 7066},
+							expr: &seqExpr{
+								pos: position{line: 291, col: 74, offset: 7067},
+								exprs: []any{
+									&ruleRefExpr{
+										pos:  position{line: 291, col: 74, offset: 7067},
+										name: "_",
+									},
+									&litMatcher{
+										pos:        position{line: 291, col: 76, offset: 7069},
+										val:        ",",
+										ignoreCase: false,
+										want:       "\",\"",
+									},
+									&ruleRefExpr{
+										pos:  position{line: 291, col: 80, offset: 7073},
+										name: "_",
+									},
+								},
+							},
+						},
+					},
+				},
+			},
+		},
+		{
+			name: "PrimitiveName",
+			pos:  position{line: 308, col: 1, offset: 7388},
+			expr: &actionExpr{
+				pos: position{line: 308, col: 18, offset: 7405},
+				run: (*parser).callonPrimitiveName1,
+				expr: &labeledExpr{
+					pos:   position{line: 308, col: 18, offset: 7405},
+					label: "Name",
+					expr: &ruleRefExpr{
+						pos:  position{line: 308, col: 23, offset: 7410},
+						name: "Identifier",
+					},
+				},
+			},
+		},
+		{
+			name: "Equation",
+			pos:  position{line: 312, col: 1, offset: 7470},
+			expr: &actionExpr{
+				pos: position{line: 312, col: 13, offset: 7482},
+				run: (*parser).callonEquation1,
+				expr: &seqExpr{
+					pos: position{line: 312, col: 13, offset: 7482},
+					exprs: []any{
+						&labeledExpr{
+							pos:   position{line: 312, col: 13, offset: 7482},
+							label: "First",
+							expr: &ruleRefExpr{
+								pos:  position{line: 312, col: 19, offset: 7488},
+								name: "Constant",
+							},
+						},
+						&seqExpr{
+							pos: position{line: 312, col: 29, offset: 7498},
+							exprs: []any{
+								&ruleRefExpr{
+									pos:  position{line: 312, col: 29, offset: 7498},
+									name: "_",
+								},
+								&litMatcher{
+									pos:        position{line: 312, col: 31, offset: 7500},
+									val:        "^",
+									ignoreCase: false,
+									want:       "\"^\"",
+								},
+								&ruleRefExpr{
+									pos:  position{line: 312, col: 35, offset: 7504},
+									name: "_",
+								},
+							},
+						},
+						&labeledExpr{
+							pos:   position{line: 312, col: 38, offset: 7507},
+							label: "Second",
+							expr: &ruleRefExpr{
+								pos:  position{line: 312, col: 45, offset: 7514},
+								name: "Constant",
+							},
+						},
+					},
+				},
+			},
+		},
+		{
+			name: "Value",
+			pos:  position{line: 324, col: 1, offset: 7671},
+			expr: &choiceExpr{
+				pos: position{line: 324, col: 10, offset: 7680},
+				alternatives: []any{
+					&ruleRefExpr{
+						pos:  position{line: 324, col: 10, offset: 7680},
+						name: "Primitive",
+					},
+					&ruleRefExpr{
+						pos:  position{line: 324, col: 20, offset: 7690},
+						name: "Equation",
+					},
+					&ruleRefExpr{
+						pos:  position{line: 324, col: 29, offset: 7699},
+						name: "Constant",
+					},
+				},
+			},
+		},
+		{
+			name: "Queries",
+			pos:  position{line: 326, col: 1, offset: 7709},
+			expr: &actionExpr{
+				pos: position{line: 326, col: 12, offset: 7720},
+				run: (*parser).callonQueries1,
+				expr: &seqExpr{
+					pos: position{line: 326, col: 12, offset: 7720},
+					exprs: []any{
+						&litMatcher{
+							pos:        position{line: 326, col: 12, offset: 7720},
+							val:        "queries",
+							ignoreCase: false,
+							want:       "\"queries\"",
+						},
+						&ruleRefExpr{
+							pos:  position{line: 326, col: 22, offset: 7730},
+							name: "_",
+						},
+						&litMatcher{
+							pos:        position{line: 326, col: 24, offset: 7732},
+							val:        "[",
+							ignoreCase: false,
+							want:       "\"[\"",
+						},
+						&ruleRefExpr{
+							pos:  position{line: 326, col: 28, offset: 7736},
+							name: "_",
+						},
+						&labeledExpr{
+							pos:   position{line: 326, col: 30, offset: 7738},
+							label: "Queries",
+							expr: &zeroOrMoreExpr{
+								pos: position{line: 326, col: 39, offset: 7747},
+								expr: &ruleRefExpr{
+									pos:  position{line: 326, col: 39, offset: 7747},
+									name: "Query",
+								},
+							},
+						},
+						&litMatcher{
+							pos:        position{line: 326, col: 47, offset: 7755},
+							val:        "]",
+							ignoreCase: false,
+							want:       "\"]\"",
+						},
+						&ruleRefExpr{
+							pos:  position{line: 326, col: 51, offset: 7759},
+							name: "_",
+						},
+					},
+				},
+			},
+		},
+		{
+			name: "Query",
+			pos:  position{line: 330, col: 1, offset: 7787},
+			expr: &actionExpr{
+				pos: position{line: 330, col: 10, offset: 7796},
+				run: (*parser).callonQuery1,
+				expr: &seqExpr{
+					pos: position{line: 330, col: 10, offset: 7796},
+					exprs: []any{
+						&zeroOrMoreExpr{
+							pos: position{line: 330, col: 10, offset: 7796},
+							expr: &ruleRefExpr{
+								pos:  position{line: 330, col: 10, offset: 7796},
+								name: "Comment",
+							},
+						},
+						&labeledExpr{
+							pos:   position{line: 330, col: 19, offset: 7805},
+							label: "Query",
+							expr: &choiceExpr{
+								pos: position{line: 330, col: 26, offset: 7812},
+								alternatives: []any{
+									&ruleRefExpr{
+										pos:  position{line: 330, col: 26, offset: 7812},
+										name: "QueryConfidentiality",
+									},
+									&ruleRefExpr{
+										pos:  position{line: 330, col: 47, offset: 7833},
+										name: "QueryAuthentication",
+									},
+									&ruleRefExpr{
+										pos:  position{line: 330, col: 67, offset: 7853},
+										name: "QueryFreshness",
+									},
+									&ruleRefExpr{
+										pos:  position{line: 330, col: 82, offset: 7868},
+										name: "QueryUnlinkability",
+									},
+									&ruleRefExpr{
+										pos:  position{line: 330, col: 101, offset: 7887},
+										name: "QueryEquivalence",
+									},
+								},
+							},
+						},
+						&zeroOrMoreExpr{
+							pos: position{line: 330, col: 119, offset: 7905},
+							expr: &ruleRefExpr{
+								pos:  position{line: 330, col: 119, offset: 7905},
+								name: "Comment",
+							},
+						},
+					},
+				},
+			},
+		},
+		{
+			name: "QueryConfidentiality",
+			pos:  position{line: 334, col: 1, offset: 7938},
+			expr: &actionExpr{
+				pos: position{line: 334, col: 25, offset: 7962},
+				run: (*parser).callonQueryConfidentiality1,
+				expr: &seqExpr{
+					pos: position{line: 334, col: 25, offset: 7962},
+					exprs: []any{
+						&litMatcher{
+							pos:        position{line: 334, col: 25, offset: 7962},
+							val:        "confidentiality?",
+							ignoreCase: false,
+							want:       "\"confidentiality?\"",
+						},
+						&ruleRefExpr{
+							pos:  position{line: 334, col: 44, offset: 7981},
+							name: "_",
+						},
+						&labeledExpr{
+							pos:   position{line: 334, col: 46, offset: 7983},
+							label: "Const",
+							expr: &zeroOrOneExpr{
+								pos: position{line: 334, col: 52, offset: 7989},
+								expr: &ruleRefExpr{
+									pos:  position{line: 334, col: 52, offset: 7989},
+									name: "Constant",
+								},
+							},
+						},
+						&ruleRefExpr{
+							pos:  position{line: 334, col: 62, offset: 7999},
+							name: "_",
+						},
+						&labeledExpr{
+							pos:   position{line: 334, col: 64, offset: 8001},
+							label: "Options",
+							expr: &zeroOrOneExpr{
+								pos: position{line: 334, col: 72, offset: 8009},
+								expr: &ruleRefExpr{
+									pos:  position{line: 334, col: 72, offset: 8009},
+									name: "QueryOptions",
+								},
+							},
+						},
+						&ruleRefExpr{
+							pos:  position{line: 334, col: 86, offset: 8023},
+							name: "_",
+						},
+					},
+				},
+			},
+		},
+		{
+			name: "QueryAuthentication",
+			pos:  position{line: 349, col: 1, offset: 8363},
+			expr: &actionExpr{
+				pos: position{line: 349, col: 24, offset: 8386},
+				run: (*parser).callonQueryAuthentication1,
+				expr: &seqExpr{
+					pos: position{line: 349, col: 24, offset: 8386},
+					exprs: []any{
+						&litMatcher{
+							pos:        position{line: 349, col: 24, offset: 8386},
+							val:        "authentication?",
+							ignoreCase: false,
+							want:       "\"authentication?\"",
+						},
+						&ruleRefExpr{
+							pos:  position{line: 349, col: 42, offset: 8404},
+							name: "_",
+						},
+						&labeledExpr{
+							pos:   position{line: 349, col: 44, offset: 8406},
+							label: "Message",
+							expr: &zeroOrOneExpr{
+								pos: position{line: 349, col: 52, offset: 8414},
+								expr: &ruleRefExpr{
+									pos:  position{line: 349, col: 52, offset: 8414},
+									name: "Message",
+								},
+							},
+						},
+						&ruleRefExpr{
+							pos:  position{line: 349, col: 61, offset: 8423},
+							name: "_",
+						},
+						&labeledExpr{
+							pos:   position{line: 349, col: 63, offset: 8425},
+							label: "Options",
+							expr: &zeroOrOneExpr{
+								pos: position{line: 349, col: 71, offset: 8433},
+								expr: &ruleRefExpr{
+									pos:  position{line: 349, col: 71, offset: 8433},
+									name: "QueryOptions",
+								},
+							},
+						},
+						&ruleRefExpr{
+							pos:  position{line: 349, col: 85, offset: 8447},
+							name: "_",
+						},
+					},
+				},
+			},
+		},
+		{
+			name: "QueryFreshness",
+			pos:  position{line: 364, col: 1, offset: 8771},
+			expr: &actionExpr{
+				pos: position{line: 364, col: 19, offset: 8789},
+				run: (*parser).callonQueryFreshness1,
+				expr: &seqExpr{
+					pos: position{line: 364, col: 19, offset: 8789},
+					exprs: []any{
+						&litMatcher{
+							pos:        position{line: 364, col: 19, offset: 8789},
+							val:        "freshness?",
+							ignoreCase: false,
+							want:       "\"freshness?\"",
+						},
+						&ruleRefExpr{
+							pos:  position{line: 364, col: 32, offset: 8802},
+							name: "_",
+						},
+						&labeledExpr{
+							pos:   position{line: 364, col: 34, offset: 8804},
+							label: "Const",
+							expr: &zeroOrOneExpr{
+								pos: position{line: 364, col: 40, offset: 8810},
+								expr: &ruleRefExpr{
+									pos:  position{line: 364, col: 40, offset: 8810},
+									name: "Constant",
+								},
+							},
+						},
+						&ruleRefExpr{
+							pos:  position{line: 364, col: 50, offset: 8820},
+							name: "_",
+						},
+						&labeledExpr{
+							pos:   position{line: 364, col: 52, offset: 8822},
+							label: "Options",
+							expr: &zeroOrOneExpr{
+								pos: position{line: 364, col: 60, offset: 8830},
+								expr: &ruleRefExpr{
+									pos:  position{line: 364, col: 60, offset: 8830},
+									name: "QueryOptions",
+								},
+							},
+						},
+						&ruleRefExpr{
+							pos:  position{line: 364, col: 74, offset: 8844},
+							name: "_",
+						},
+					},
+				},
+			},
+		},
+		{
+			name: "QueryUnlinkability",
+			pos:  position{line: 379, col: 1, offset: 9172},
+			expr: &actionExpr{
+				pos: position{line: 379, col: 23, offset: 9194},
+				run: (*parser).callonQueryUnlinkability1,
+				expr: &seqExpr{
+					pos: position{line: 379, col: 23, offset: 9194},
+					exprs: []any{
+						&litMatcher{
+							pos:        position{line: 379, col: 23, offset: 9194},
+							val:        "unlinkability?",
+							ignoreCase: false,
+							want:       "\"unlinkability?\"",
+						},
+						&ruleRefExpr{
+							pos:  position{line: 379, col: 40, offset: 9211},
+							name: "_",
+						},
+						&labeledExpr{
+							pos:   position{line: 379, col: 42, offset: 9213},
+							label: "Consts",
+							expr: &zeroOrOneExpr{
+								pos: position{line: 379, col: 49, offset: 9220},
+								expr: &ruleRefExpr{
+									pos:  position{line: 379, col: 49, offset: 9220},
+									name: "Constants",
+								},
+							},
+						},
+						&ruleRefExpr{
+							pos:  position{line: 379, col: 60, offset: 9231},
+							name: "_",
+						},
+						&labeledExpr{
+							pos:   position{line: 379, col: 62, offset: 9233},
+							label: "Options",
+							expr: &zeroOrOneExpr{
+								pos: position{line: 379, col: 70, offset: 9241},
+								expr: &ruleRefExpr{
+									pos:  position{line: 379, col: 70, offset: 9241},
+									name: "QueryOptions",
+								},
+							},
+						},
+						&ruleRefExpr{
+							pos:  position{line: 379, col: 84, offset: 9255},
+							name: "_",
+						},
+					},
+				},
+			},
+		},
+		{
+			name: "QueryEquivalence",
+			pos:  position{line: 394, col: 1, offset: 9569},
+			expr: &actionExpr{
+				pos: position{line: 394, col: 21, offset: 9589},
+				run: (*parser).callonQueryEquivalence1,
+				expr: &seqExpr{
+					pos: position{line: 394, col: 21, offset: 9589},
+					exprs: []any{
+						&litMatcher{
+							pos:        position{line: 394, col: 21, offset: 9589},
+							val:        "equivalence?",
+							ignoreCase: false,
+							want:       "\"equivalence?\"",
+						},
+						&ruleRefExpr{
+							pos:  position{line: 394, col: 36, offset: 9604},
+							name: "_",
+						},
+						&labeledExpr{
+							pos:   position{line: 394, col: 38, offset: 9606},
+							label: "Consts",
+							expr: &zeroOrOneExpr{
+								pos: position{line: 394, col: 45, offset: 9613},
+								expr: &ruleRefExpr{
+									pos:  position{line: 394, col: 45, offset: 9613},
+									name: "Constants",
+								},
+							},
+						},
+						&ruleRefExpr{
+							pos:  position{line: 394, col: 56, offset: 9624},
+							name: "_",
+						},
+						&labeledExpr{
+							pos:   position{line: 394, col: 58, offset: 9626},
+							label: "Options",
+							expr: &zeroOrOneExpr{
+								pos: position{line: 394, col: 66, offset: 9634},
+								expr: &ruleRefExpr{
+									pos:  position{line: 394, col: 66, offset: 9634},
+									name: "QueryOptions",
+								},
+							},
+						},
+						&ruleRefExpr{
+							pos:  position{line: 394, col: 80, offset: 9648},
+							name: "_",
+						},
+					},
+				},
+			},
+		},
+		{
+			name: "QueryOptions",
+			pos:  position{line: 409, col: 1, offset: 9958},
+			expr: &actionExpr{
+				pos: position{line: 409, col: 17, offset: 9974},
+				run: (*parser).callonQueryOptions1,
+				expr: &seqExpr{
+					pos: position{line: 409, col: 17, offset: 9974},
+					exprs: []any{
+						&litMatcher{
+							pos:        position{line: 409, col: 17, offset: 9974},
+							val:        "[",
+							ignoreCase: false,
+							want:       "\"[\"",
+						},
+						&ruleRefExpr{
+							pos:  position{line: 409, col: 21, offset: 9978},
+							name: "_",
+						},
+						&labeledExpr{
+							pos:   position{line: 409, col: 23, offset: 9980},
+							label: "Options",
+							expr: &zeroOrMoreExpr{
+								pos: position{line: 409, col: 32, offset: 9989},
+								expr: &ruleRefExpr{
+									pos:  position{line: 409, col: 32, offset: 9989},
+									name: "QueryOption",
+								},
+							},
+						},
+						&litMatcher{
+							pos:        position{line: 409, col: 46, offset: 10003},
+							val:        "]",
+							ignoreCase: false,
+							want:       "\"]\"",
+						},
+						&ruleRefExpr{
+							pos:  position{line: 409, col: 50, offset: 10007},
+							name: "_",
+						},
+					},
+				},
+			},
+		},
+		{
+			name: "QueryOption",
+			pos:  position{line: 416, col: 1, offset: 10144},
+			expr: &actionExpr{
+				pos: position{line: 416, col: 16, offset: 10159},
+				run: (*parser).callonQueryOption1,
+				expr: &seqExpr{
+					pos: position{line: 416, col: 16, offset: 10159},
+					exprs: []any{
+						&labeledExpr{
+							pos:   position{line: 416, col: 16, offset: 10159},
+							label: "OptionName",
+							expr: &ruleRefExpr{
+								pos:  position{line: 416, col: 27, offset: 10170},
+								name: "Identifier",
+							},
+						},
+						&ruleRefExpr{
+							pos:  position{line: 416, col: 38, offset: 10181},
+							name: "_",
+						},
+						&litMatcher{
+							pos:        position{line: 416, col: 40, offset: 10183},
+							val:        "[",
+							ignoreCase: false,
+							want:       "\"[\"",
+						},
+						&ruleRefExpr{
+							pos:  position{line: 416, col: 44, offset: 10187},
+							name: "_",
+						},
+						&labeledExpr{
+							pos:   position{line: 416, col: 46, offset: 10189},
+							label: "Message",
+							expr: &ruleRefExpr{
+								pos:  position{line: 416, col: 54, offset: 10197},
+								name: "Message",
+							},
+						},
+						&ruleRefExpr{
+							pos:  position{line: 416, col: 62, offset: 10205},
+							name: "_",
+						},
+						&litMatcher{
+							pos:        position{line: 416, col: 64, offset: 10207},
+							val:        "]",
+							ignoreCase: false,
+							want:       "\"]\"",
+						},
+						&ruleRefExpr{
+							pos:  position{line: 416, col: 68, offset: 10211},
+							name: "_",
+						},
+					},
+				},
+			},
+		},
+		{
+			name: "Identifier",
+			pos:  position{line: 428, col: 1, offset: 10429},
+			expr: &actionExpr{
+				pos: position{line: 428, col: 15, offset: 10443},
+				run: (*parser).callonIdentifier1,
+				expr: &labeledExpr{
+					pos:   position{line: 428, col: 15, offset: 10443},
+					label: "Identifier",
+					expr: &oneOrMoreExpr{
+						pos: position{line: 428, col: 26, offset: 10454},
+						expr: &charClassMatcher{
+							pos:        position{line: 428, col: 26, offset: 10454},
+							val:        "[a-zA-Z0-9_]",
+							chars:      []rune{'_'},
+							ranges:     []rune{'a', 'z', 'A', 'Z', '0', '9'},
+							ignoreCase: false,
+							inverted:   false,
+						},
+					},
+				},
+			},
+		},
+		{
+			name: "Comment",
+			pos:  position{line: 433, col: 1, offset: 10544},
+			expr: &seqExpr{
+				pos: position{line: 433, col: 12, offset: 10555},
+				exprs: []any{
+					&ruleRefExpr{
+						pos:  position{line: 433, col: 12, offset: 10555},
+						name: "_",
+					},
+					&litMatcher{
+						pos:        position{line: 433, col: 14, offset: 10557},
+						val:        "//",
+						ignoreCase: false,
+						want:       "\"//\"",
+					},
+					&zeroOrMoreExpr{
+						pos: position{line: 433, col: 19, offset: 10562},
+						expr: &charClassMatcher{
+							pos:        position{line: 433, col: 19, offset: 10562},
+							val:        "[^\\n]",
+							chars:      []rune{'\n'},
+							ignoreCase: false,
+							inverted:   true,
+						},
+					},
+					&ruleRefExpr{
+						pos:  position{line: 433, col: 26, offset: 10569},
+						name: "_",
+					},
+				},
+			},
+		},
+		{
+			name:        "_",
+			displayName: "\"whitespace\"",
+			pos:         position{line: 435, col: 1, offset: 10572},
+			expr: &zeroOrMoreExpr{
+				pos: position{line: 435, col: 19, offset: 10590},
+				expr: &charClassMatcher{
+					pos:        position{line: 435, col: 19, offset: 10590},
+					val:        "[ \\t\\n\\r]",
+					chars:      []rune{' ', '\t', '\n', '\r'},
+					ignoreCase: false,
+					inverted:   false,
+				},
+			},
+		},
+		{
+			name: "EOF",
+			pos:  position{line: 437, col: 1, offset: 10602},
+			expr: &notExpr{
+				pos: position{line: 437, col: 8, offset: 10609},
+				expr: &anyMatcher{
+					line: 437, col: 9, offset: 10610,
+				},
+			},
+		},
+	},
+}
+
+func (c *current) onModel1(Attacker, Blocks, Queries any) (any, error) {
+	switch {
+	case Attacker == nil:
+		return nil, errors.New("no `attacker` block defined")
+	case Blocks == nil:
+		return nil, errors.New("no principal or message blocks defined")
+	case Queries == nil:
+		return nil, errors.New("no `queries` block defined")
+	}
+	b := Blocks.([]interface{})
+	q := Queries.([]interface{})
+	db := make([]Block, len(b))
+	dq := make([]Query, len(q))
+	for i, v := range b {
+		db[i] = v.(Block)
+	}
+	for i, v := range q {
+		dq[i] = v.(Query)
+	}
+	return Model{
+		Attacker: Attacker.(string),
+		Blocks:   db,
+		Queries:  dq,
+	}, nil
+}
+
+func (p *parser) callonModel1() (any, error) {
+	stack := p.vstack[len(p.vstack)-1]
+	_ = stack
+	return p.cur.onModel1(stack["Attacker"], stack["Blocks"], stack["Queries"])
+}
+
+func (c *current) onAttacker1(Type any) (any, error) {
+	if Type == nil {
+		return nil, errors.New("`attacker` is declared with missing attacker type")
+	}
+	return Type, nil
+}
+
+func (p *parser) callonAttacker1() (any, error) {
+	stack := p.vstack[len(p.vstack)-1]
+	_ = stack
+	return p.cur.onAttacker1(stack["Type"])
+}
+
+func (c *current) onAttackerType1() (any, error) {
+	return string(c.text), nil
+}
+
+func (p *parser) callonAttackerType1() (any, error) {
+	stack := p.vstack[len(p.vstack)-1]
+	_ = stack
+	return p.cur.onAttackerType1()
+}
+
+func (c *current) onBlock1(Block any) (any, error) {
+	return Block, nil
+}
+
+func (p *parser) callonBlock1() (any, error) {
+	stack := p.vstack[len(p.vstack)-1]
+	_ = stack
+	return p.cur.onBlock1(stack["Block"])
+}
+
+func (c *current) onPrincipal1(Name, Expressions any) (any, error) {
+	e := Expressions.([]interface{})
+	de := make([]Expression, len(e))
+	for i, v := range e {
+		de[i] = v.(Expression)
+	}
+	id := principalNamesMapAdd(Name.(string))
+	return Block{
+		Kind: "principal",
+		Principal: Principal{
+			Name:        Name.(string),
+			ID:          id,
+			Expressions: de,
+		},
+	}, nil
+}
+
+func (p *parser) callonPrincipal1() (any, error) {
+	stack := p.vstack[len(p.vstack)-1]
+	_ = stack
+	return p.cur.onPrincipal1(stack["Name"], stack["Expressions"])
+}
+
+func (c *current) onPrincipalName1(Name any) (any, error) {
+	err := libpegCheckIfReserved(Name.(string))
+	return strings.Title(Name.(string)), err
+}
+
+func (p *parser) callonPrincipalName1() (any, error) {
+	stack := p.vstack[len(p.vstack)-1]
+	_ = stack
+	return p.cur.onPrincipalName1(stack["Name"])
+}
+
+func (c *current) onQualifier1() (any, error) {
+	switch string(c.text) {
+	default:
+		return typesEnumPrivate, nil
+	case "public":
+		return typesEnumPublic, nil
+	case "password":
+		return typesEnumPassword, nil
+	}
+}
+
+func (p *parser) callonQualifier1() (any, error) {
+	stack := p.vstack[len(p.vstack)-1]
+	_ = stack
+	return p.cur.onQualifier1()
+}
+
+func (c *current) onMessage1(Sender, Recipient, Constants any) (any, error) {
+	switch {
+	case Sender == nil:
+		return nil, errors.New("message sender is not defined")
+	case Recipient == nil:
+		return nil, errors.New("message recipient is not defined")
+	case Constants == nil:
+		return nil, errors.New("message constants are not defined")
+	}
+	senderID := principalNamesMapAdd(Sender.(string))
+	recipientID := principalNamesMapAdd(Recipient.(string))
+	return Block{
+		Kind: "message",
+		Message: Message{
+			Sender:    senderID,
+			Recipient: recipientID,
+			Constants: Constants.([]*Constant),
+		},
+	}, nil
+}
+
+func (p *parser) callonMessage1() (any, error) {
+	stack := p.vstack[len(p.vstack)-1]
+	_ = stack
+	return p.cur.onMessage1(stack["Sender"], stack["Recipient"], stack["Constants"])
+}
+
+func (c *current) onMessageConstants1(MessageConstants any) (any, error) {
+	var da []*Constant
+	a := MessageConstants.([]interface{})
+	for _, v := range a {
+		c := v.(*Value).Data.(*Constant)
+		da = append(da, c)
+	}
+	return da, nil
+}
+
+func (p *parser) callonMessageConstants1() (any, error) {
+	stack := p.vstack[len(p.vstack)-1]
+	_ = stack
+	return p.cur.onMessageConstants1(stack["MessageConstants"])
+}
+
+func (c *current) onExpression1(Expression any) (any, error) {
+	return Expression, nil
+}
+
+func (p *parser) callonExpression1() (any, error) {
+	stack := p.vstack[len(p.vstack)-1]
+	_ = stack
+	return p.cur.onExpression1(stack["Expression"])
+}
+
+func (c *current) onKnows1(Qualifier, Constants any) (any, error) {
+	switch {
+	case Qualifier == nil:
+		return nil, errors.New("`knows` declaration is missing qualifier")
+	case Constants == nil:
+		return nil, errors.New("`knows` declaration is missing constant name(s)")
+	}
+	return Expression{
+		Kind:      typesEnumKnows,
+		Qualifier: Qualifier.(typesEnum),
+		Constants: Constants.([]*Constant),
+	}, nil
+}
+
+func (p *parser) callonKnows1() (any, error) {
+	stack := p.vstack[len(p.vstack)-1]
+	_ = stack
+	return p.cur.onKnows1(stack["Qualifier"], stack["Constants"])
+}
+
+func (c *current) onGenerates1(Constants any) (any, error) {
+	if Constants == nil {
+		return nil, errors.New("`generates` declaration is missing constant name(s)")
+	}
+	return Expression{
+		Kind:      typesEnumGenerates,
+		Qualifier: typesEnumEmpty,
+		Constants: Constants.([]*Constant),
+	}, nil
+}
+
+func (p *parser) callonGenerates1() (any, error) {
+	stack := p.vstack[len(p.vstack)-1]
+	_ = stack
+	return p.cur.onGenerates1(stack["Constants"])
+}
+
+func (c *current) onLeaks1(Constants any) (any, error) {
+	if Constants == nil {
+		return nil, errors.New("`leaks` declaration is missing constant name(s)")
+	}
+	return Expression{
+		Kind:      typesEnumLeaks,
+		Qualifier: typesEnumEmpty,
+		Constants: Constants.([]*Constant),
+	}, nil
+}
+
+func (p *parser) callonLeaks1() (any, error) {
+	stack := p.vstack[len(p.vstack)-1]
+	_ = stack
+	return p.cur.onLeaks1(stack["Constants"])
+}
+
+func (c *current) onAssignment1(Left, Right any) (any, error) {
+	if Left == nil || Right == nil {
+		return nil, errors.New("invalid value assignment")
+	}
+	switch Right.(*Value).Kind {
+	case typesEnumConstant:
+		err := errors.New("cannot assign value to value")
+		return nil, err
+	}
+	return Expression{
+		Kind:      typesEnumAssignment,
+		Constants: Left.([]*Constant),
+		Assigned:  Right.(*Value),
+	}, nil
+}
+
+func (p *parser) callonAssignment1() (any, error) {
+	stack := p.vstack[len(p.vstack)-1]
+	_ = stack
+	return p.cur.onAssignment1(stack["Left"], stack["Right"])
+}
+
+func (c *current) onConstant1(Const any) (any, error) {
+	var err error
+	name := Const.(string)
+	err = libpegCheckIfReserved(name)
+	if err != nil {
+		return &Value{}, err
+	}
+	switch name {
+	case "_":
+		name = fmt.Sprintf("unnamed_%d", libpegUnnamedCounter)
+		libpegUnnamedCounter = libpegUnnamedCounter + 1
+	}
+	id := valueNamesMapAdd(name)
+	return &Value{
+		Kind: typesEnumConstant,
+		Data: &Constant{
+			Name: name,
+			ID:   id,
+		},
+	}, err
+}
+
+func (p *parser) callonConstant1() (any, error) {
+	stack := p.vstack[len(p.vstack)-1]
+	_ = stack
+	return p.cur.onConstant1(stack["Const"])
+}
+
+func (c *current) onConstants1(Constants any) (any, error) {
+	var da []*Constant
+	a := Constants.([]interface{})
+	for _, c := range a {
+		da = append(da, c.(*Value).Data.(*Constant))
+	}
+	return da, nil
+}
+
+func (p *parser) callonConstants1() (any, error) {
+	stack := p.vstack[len(p.vstack)-1]
+	_ = stack
+	return p.cur.onConstants1(stack["Constants"])
+}
+
+func (c *current) onPhase1(Number any) (any, error) {
+	a := Number.([]interface{})
+	da := make([]uint8, len(a))
+	for i, v := range a {
+		da[i] = v.([]uint8)[0]
+	}
+	n, err := strconv.Atoi(b2s(da))
+	return Block{
+		Kind: "phase",
+		Phase: Phase{
+			Number: n,
+		},
+	}, err
+}
+
+func (p *parser) callonPhase1() (any, error) {
+	stack := p.vstack[len(p.vstack)-1]
+	_ = stack
+	return p.cur.onPhase1(stack["Number"])
+}
+
+func (c *current) onGuardedConstant1(Guarded any) (any, error) {
+	g := Guarded.(*Value)
+	err := libpegCheckIfReserved(g.Data.(*Constant).Name)
+	return &Value{
+		Kind: typesEnumConstant,
+		Data: &Constant{
+			Name:  g.Data.(*Constant).Name,
+			ID:    g.Data.(*Constant).ID,
+			Guard: true,
+		},
+	}, err
+}
+
+func (p *parser) callonGuardedConstant1() (any, error) {
+	stack := p.vstack[len(p.vstack)-1]
+	_ = stack
+	return p.cur.onGuardedConstant1(stack["Guarded"])
+}
+
+func (c *current) onPrimitive1(Name, Arguments, Check any) (any, error) {
+	args := []*Value{}
+	for _, a := range Arguments.([]interface{}) {
+		args = append(args, a.(*Value))
+	}
+	primEnum, err := primitiveGetEnum(Name.(string))
+	return &Value{
+		Kind: typesEnumPrimitive,
+		Data: &Primitive{
+			ID:        primEnum,
+			Arguments: args,
+			Output:    0,
+			Check:     Check != nil,
+		},
+	}, err
+}
+
+func (p *parser) callonPrimitive1() (any, error) {
+	stack := p.vstack[len(p.vstack)-1]
+	_ = stack
+	return p.cur.onPrimitive1(stack["Name"], stack["Arguments"], stack["Check"])
+}
+
+func (c *current) onPrimitiveName1(Name any) (any, error) {
+	return strings.ToUpper(Name.(string)), nil
+}
+
+func (p *parser) callonPrimitiveName1() (any, error) {
+	stack := p.vstack[len(p.vstack)-1]
+	_ = stack
+	return p.cur.onPrimitiveName1(stack["Name"])
+}
+
+func (c *current) onEquation1(First, Second any) (any, error) {
+	return &Value{
+		Kind: typesEnumEquation,
+		Data: &Equation{
+			Values: []*Value{
+				First.(*Value),
+				Second.(*Value),
+			},
+		},
+	}, nil
+}
+
+func (p *parser) callonEquation1() (any, error) {
+	stack := p.vstack[len(p.vstack)-1]
+	_ = stack
+	return p.cur.onEquation1(stack["First"], stack["Second"])
+}
+
+func (c *current) onQueries1(Queries any) (any, error) {
+	return Queries, nil
+}
+
+func (p *parser) callonQueries1() (any, error) {
+	stack := p.vstack[len(p.vstack)-1]
+	_ = stack
+	return p.cur.onQueries1(stack["Queries"])
+}
+
+func (c *current) onQuery1(Query any) (any, error) {
+	return Query, nil
+}
+
+func (p *parser) callonQuery1() (any, error) {
+	stack := p.vstack[len(p.vstack)-1]
+	_ = stack
+	return p.cur.onQuery1(stack["Query"])
+}
+
+func (c *current) onQueryConfidentiality1(Const, Options any) (any, error) {
+	switch {
+	case Const == nil:
+		return nil, errors.New("`confidentiality` query is missing constant")
+	case Options == nil:
+		Options = []QueryOption{}
+	}
+	return Query{
+		Kind:      typesEnumConfidentiality,
+		Constants: []*Constant{Const.(*Value).Data.(*Constant)},
+		Message:   Message{},
+		Options:   Options.([]QueryOption),
+	}, nil
+}
+
+func (p *parser) callonQueryConfidentiality1() (any, error) {
+	stack := p.vstack[len(p.vstack)-1]
+	_ = stack
+	return p.cur.onQueryConfidentiality1(stack["Const"], stack["Options"])
+}
+
+func (c *current) onQueryAuthentication1(Message, Options any) (any, error) {
+	switch {
+	case Message == nil:
+		return nil, errors.New("`authentication` query is missing message")
+	case Options == nil:
+		Options = []QueryOption{}
+	}
+	return Query{
+		Kind:      typesEnumAuthentication,
+		Constants: []*Constant{},
+		Message:   (Message.(Block)).Message,
+		Options:   Options.([]QueryOption),
+	}, nil
+}
+
+func (p *parser) callonQueryAuthentication1() (any, error) {
+	stack := p.vstack[len(p.vstack)-1]
+	_ = stack
+	return p.cur.onQueryAuthentication1(stack["Message"], stack["Options"])
+}
+
+func (c *current) onQueryFreshness1(Const, Options any) (any, error) {
+	switch {
+	case Const == nil:
+		return nil, errors.New("`freshness` query is missing constant")
+	case Options == nil:
+		Options = []QueryOption{}
+	}
+	return Query{
+		Kind:      typesEnumFreshness,
+		Constants: []*Constant{Const.(*Value).Data.(*Constant)},
+		Message:   Message{},
+		Options:   Options.([]QueryOption),
+	}, nil
+}
+
+func (p *parser) callonQueryFreshness1() (any, error) {
+	stack := p.vstack[len(p.vstack)-1]
+	_ = stack
+	return p.cur.onQueryFreshness1(stack["Const"], stack["Options"])
+}
+
+func (c *current) onQueryUnlinkability1(Consts, Options any) (any, error) {
+	switch {
+	case Consts == nil:
+		return nil, errors.New("`unlinkability` query is missing constants")
+	case Options == nil:
+		Options = []QueryOption{}
+	}
+	return Query{
+		Kind:      typesEnumUnlinkability,
+		Constants: Consts.([]*Constant),
+		Message:   Message{},
+		Options:   Options.([]QueryOption),
+	}, nil
+}
+
+func (p *parser) callonQueryUnlinkability1() (any, error) {
+	stack := p.vstack[len(p.vstack)-1]
+	_ = stack
+	return p.cur.onQueryUnlinkability1(stack["Consts"], stack["Options"])
+}
+
+func (c *current) onQueryEquivalence1(Consts, Options any) (any, error) {
+	switch {
+	case Consts == nil:
+		return nil, errors.New("`equivalence` query is missing constants")
+	case Options == nil:
+		Options = []QueryOption{}
+	}
+	return Query{
+		Kind:      typesEnumEquivalence,
+		Constants: Consts.([]*Constant),
+		Message:   Message{},
+		Options:   Options.([]QueryOption),
+	}, nil
+}
+
+func (p *parser) callonQueryEquivalence1() (any, error) {
+	stack := p.vstack[len(p.vstack)-1]
+	_ = stack
+	return p.cur.onQueryEquivalence1(stack["Consts"], stack["Options"])
+}
+
+func (c *current) onQueryOptions1(Options any) (any, error) {
+	o := Options.([]interface{})
+	do := make([]QueryOption, len(o))
+	for i, v := range o {
+		do[i] = v.(QueryOption)
+	}
+	return do, nil
+}
+
+func (p *parser) callonQueryOptions1() (any, error) {
+	stack := p.vstack[len(p.vstack)-1]
+	_ = stack
+	return p.cur.onQueryOptions1(stack["Options"])
+}
+
+func (c *current) onQueryOption1(OptionName, Message any) (any, error) {
+	optionEnum := typesEnumEmpty
+	switch OptionName.(string) {
+	case "precondition":
+		optionEnum = typesEnumPrecondition
+	}
+	return QueryOption{
+		Kind:    optionEnum,
+		Message: (Message.(Block)).Message,
+	}, nil
+}
+
+func (p *parser) callonQueryOption1() (any, error) {
+	stack := p.vstack[len(p.vstack)-1]
+	_ = stack
+	return p.cur.onQueryOption1(stack["OptionName"], stack["Message"])
+}
+
+func (c *current) onIdentifier1(Identifier any) (any, error) {
+	identifier := strings.ToLower(string(c.text))
+	return identifier, nil
+}
+
+func (p *parser) callonIdentifier1() (any, error) {
+	stack := p.vstack[len(p.vstack)-1]
+	_ = stack
+	return p.cur.onIdentifier1(stack["Identifier"])
+}
+
+var (
+	// errNoRule is returned when the grammar to parse has no rule.
+	errNoRule = errors.New("grammar has no rule")
+
+	// errInvalidEntrypoint is returned when the specified entrypoint rule
+	// does not exit.
+	errInvalidEntrypoint = errors.New("invalid entrypoint")
+
+	// errInvalidEncoding is returned when the source is not properly
+	// utf8-encoded.
+	errInvalidEncoding = errors.New("invalid encoding")
+
+	// errMaxExprCnt is used to signal that the maximum number of
+	// expressions have been parsed.
+	errMaxExprCnt = errors.New("max number of expresssions parsed")
+)
+
+// Option is a function that can set an option on the parser. It returns
+// the previous setting as an Option.
+type Option func(*parser) Option
+
+// MaxExpressions creates an Option to stop parsing after the provided
+// number of expressions have been parsed, if the value is 0 then the parser will
+// parse for as many steps as needed (possibly an infinite number).
+//
+// The default for maxExprCnt is 0.
+func MaxExpressions(maxExprCnt uint64) Option {
+	return func(p *parser) Option {
+		oldMaxExprCnt := p.maxExprCnt
+		p.maxExprCnt = maxExprCnt
+		return MaxExpressions(oldMaxExprCnt)
+	}
+}
+
+// Entrypoint creates an Option to set the rule name to use as entrypoint.
+// The rule name must have been specified in the -alternate-entrypoints
+// if generating the parser with the -optimize-grammar flag, otherwise
+// it may have been optimized out. Passing an empty string sets the
+// entrypoint to the first rule in the grammar.
+//
+// The default is to start parsing at the first rule in the grammar.
+func Entrypoint(ruleName string) Option {
+	return func(p *parser) Option {
+		oldEntrypoint := p.entrypoint
+		p.entrypoint = ruleName
+		if ruleName == "" {
+			p.entrypoint = g.rules[0].name
+		}
+		return Entrypoint(oldEntrypoint)
+	}
+}
+
+// Statistics adds a user provided Stats struct to the parser to allow
+// the user to process the results after the parsing has finished.
+// Also the key for the "no match" counter is set.
+//
+// Example usage:
+//
+//	input := "input"
+//	stats := Stats{}
+//	_, err := Parse("input-file", []byte(input), Statistics(&stats, "no match"))
+//	if err != nil {
+//	    log.Panicln(err)
+//	}
+//	b, err := json.MarshalIndent(stats.ChoiceAltCnt, "", "  ")
+//	if err != nil {
+//	    log.Panicln(err)
+//	}
+//	fmt.Println(string(b))
+func Statistics(stats *Stats, choiceNoMatch string) Option {
+	return func(p *parser) Option {
+		oldStats := p.Stats
+		p.Stats = stats
+		oldChoiceNoMatch := p.choiceNoMatch
+		p.choiceNoMatch = choiceNoMatch
+		if p.Stats.ChoiceAltCnt == nil {
+			p.Stats.ChoiceAltCnt = make(map[string]map[string]int)
+		}
+		return Statistics(oldStats, oldChoiceNoMatch)
+	}
+}
+
+// Debug creates an Option to set the debug flag to b. When set to true,
+// debugging information is printed to stdout while parsing.
+//
+// The default is false.
+func Debug(b bool) Option {
+	return func(p *parser) Option {
+		old := p.debug
+		p.debug = b
+		return Debug(old)
+	}
+}
+
+// Memoize creates an Option to set the memoize flag to b. When set to true,
+// the parser will cache all results so each expression is evaluated only
+// once. This guarantees linear parsing time even for pathological cases,
+// at the expense of more memory and slower times for typical cases.
+//
+// The default is false.
+func Memoize(b bool) Option {
+	return func(p *parser) Option {
+		old := p.memoize
+		p.memoize = b
+		return Memoize(old)
+	}
+}
+
+// AllowInvalidUTF8 creates an Option to allow invalid UTF-8 bytes.
+// Every invalid UTF-8 byte is treated as a utf8.RuneError (U+FFFD)
+// by character class matchers and is matched by the any matcher.
+// The returned matched value, c.text and c.offset are NOT affected.
+//
+// The default is false.
+func AllowInvalidUTF8(b bool) Option {
+	return func(p *parser) Option {
+		old := p.allowInvalidUTF8
+		p.allowInvalidUTF8 = b
+		return AllowInvalidUTF8(old)
+	}
+}
+
+// Recover creates an Option to set the recover flag to b. When set to
+// true, this causes the parser to recover from panics and convert it
+// to an error. Setting it to false can be useful while debugging to
+// access the full stack trace.
+//
+// The default is true.
+func Recover(b bool) Option {
+	return func(p *parser) Option {
+		old := p.recover
+		p.recover = b
+		return Recover(old)
+	}
+}
+
+// GlobalStore creates an Option to set a key to a certain value in
+// the globalStore.
+func GlobalStore(key string, value any) Option {
+	return func(p *parser) Option {
+		old := p.cur.globalStore[key]
+		p.cur.globalStore[key] = value
+		return GlobalStore(key, old)
+	}
+}
+
+// InitState creates an Option to set a key to a certain value in
+// the global "state" store.
+func InitState(key string, value any) Option {
+	return func(p *parser) Option {
+		old := p.cur.state[key]
+		p.cur.state[key] = value
+		return InitState(key, old)
+	}
+}
+
+// ParseFile parses the file identified by filename.
+func ParseFile(filename string, opts ...Option) (i any, err error) {
+	f, err := os.Open(filename)
+	if err != nil {
+		return nil, err
+	}
+	defer func() {
+		if closeErr := f.Close(); closeErr != nil {
+			err = closeErr
+		}
+	}()
+	return ParseReader(filename, f, opts...)
+}
+
+// ParseReader parses the data from r using filename as information in the
+// error messages.
+func ParseReader(filename string, r io.Reader, opts ...Option) (any, error) {
+	b, err := io.ReadAll(r)
+	if err != nil {
+		return nil, err
+	}
+
+	return Parse(filename, b, opts...)
+}
+
+// Parse parses the data from b using filename as information in the
+// error messages.
+func Parse(filename string, b []byte, opts ...Option) (any, error) {
+	return newParser(filename, b, opts...).parse(g)
+}
+
+// position records a position in the text.
+type position struct {
+	line, col, offset int
+}
+
+func (p position) String() string {
+	return strconv.Itoa(p.line) + ":" + strconv.Itoa(p.col) + " [" + strconv.Itoa(p.offset) + "]"
+}
+
+// savepoint stores all state required to go back to this point in the
+// parser.
+type savepoint struct {
+	position
+	rn rune
+	w  int
+}
+
+type current struct {
+	pos  position // start position of the match
+	text []byte   // raw text of the match
+
+	// state is a store for arbitrary key,value pairs that the user wants to be
+	// tied to the backtracking of the parser.
+	// This is always rolled back if a parsing rule fails.
+	state storeDict
+
+	// globalStore is a general store for the user to store arbitrary key-value
+	// pairs that they need to manage and that they do not want tied to the
+	// backtracking of the parser. This is only modified by the user and never
+	// rolled back by the parser. It is always up to the user to keep this in a
+	// consistent state.
+	globalStore storeDict
+}
+
+type storeDict map[string]any
+
+// the AST types...
+
+type grammar struct {
+	pos   position
+	rules []*rule
+}
+
+type rule struct {
+	pos         position
+	name        string
+	displayName string
+	expr        any
+}
+
+type choiceExpr struct {
+	pos          position
+	alternatives []any
+}
+
+type actionExpr struct {
+	pos  position
+	expr any
+	run  func(*parser) (any, error)
+}
+
+type recoveryExpr struct {
+	pos          position
+	expr         any
+	recoverExpr  any
+	failureLabel []string
+}
+
+type seqExpr struct {
+	pos   position
+	exprs []any
+}
+
+type throwExpr struct {
+	pos   position
+	label string
+}
+
+type labeledExpr struct {
+	pos   position
+	label string
+	expr  any
+}
+
+type expr struct {
+	pos  position
+	expr any
+}
+
+type (
+	andExpr        expr
+	notExpr        expr
+	zeroOrOneExpr  expr
+	zeroOrMoreExpr expr
+	oneOrMoreExpr  expr
+)
+
+type ruleRefExpr struct {
+	pos  position
+	name string
+}
+
+type stateCodeExpr struct {
+	pos position
+	run func(*parser) error
+}
+
+type andCodeExpr struct {
+	pos position
+	run func(*parser) (bool, error)
+}
+
+type notCodeExpr struct {
+	pos position
+	run func(*parser) (bool, error)
+}
+
+type litMatcher struct {
+	pos        position
+	val        string
+	ignoreCase bool
+	want       string
+}
+
+type charClassMatcher struct {
+	pos             position
+	val             string
+	basicLatinChars [128]bool
+	chars           []rune
+	ranges          []rune
+	classes         []*unicode.RangeTable
+	ignoreCase      bool
+	inverted        bool
+}
+
+type anyMatcher position
+
+// errList cumulates the errors found by the parser.
+type errList []error
+
+func (e *errList) add(err error) {
+	*e = append(*e, err)
+}
+
+func (e errList) err() error {
+	if len(e) == 0 {
+		return nil
+	}
+	e.dedupe()
+	return e
+}
+
+func (e *errList) dedupe() {
+	var cleaned []error
+	set := make(map[string]bool)
+	for _, err := range *e {
+		if msg := err.Error(); !set[msg] {
+			set[msg] = true
+			cleaned = append(cleaned, err)
+		}
+	}
+	*e = cleaned
+}
+
+func (e errList) Error() string {
+	switch len(e) {
+	case 0:
+		return ""
+	case 1:
+		return e[0].Error()
+	default:
+		var buf bytes.Buffer
+
+		for i, err := range e {
+			if i > 0 {
+				buf.WriteRune('\n')
+			}
+			buf.WriteString(err.Error())
+		}
+		return buf.String()
+	}
+}
+
+// parserError wraps an error with a prefix indicating the rule in which
+// the error occurred. The original error is stored in the Inner field.
+type parserError struct {
+	Inner    error
+	pos      position
+	prefix   string
+	expected []string
+}
+
+// Error returns the error message.
+func (p *parserError) Error() string {
+	return p.prefix + ": " + p.Inner.Error()
+}
+
+// newParser creates a parser with the specified input source and options.
+func newParser(filename string, b []byte, opts ...Option) *parser {
+	stats := Stats{
+		ChoiceAltCnt: make(map[string]map[string]int),
+	}
+
+	p := &parser{
+		filename: filename,
+		errs:     new(errList),
+		data:     b,
+		pt:       savepoint{position: position{line: 1}},
+		recover:  true,
+		cur: current{
+			state:       make(storeDict),
+			globalStore: make(storeDict),
+		},
+		maxFailPos:      position{col: 1, line: 1},
+		maxFailExpected: make([]string, 0, 20),
+		Stats:           &stats,
+		// start rule is rule [0] unless an alternate entrypoint is specified
+		entrypoint: g.rules[0].name,
+	}
+	p.setOptions(opts)
+
+	if p.maxExprCnt == 0 {
+		p.maxExprCnt = math.MaxUint64
+	}
+
+	return p
+}
+
+// setOptions applies the options to the parser.
+func (p *parser) setOptions(opts []Option) {
+	for _, opt := range opts {
+		opt(p)
+	}
+}
+
+type resultTuple struct {
+	v   any
+	b   bool
+	end savepoint
+}
+
+const choiceNoMatch = -1
+
+// Stats stores some statistics, gathered during parsing
+type Stats struct {
+	// ExprCnt counts the number of expressions processed during parsing
+	// This value is compared to the maximum number of expressions allowed
+	// (set by the MaxExpressions option).
+	ExprCnt uint64
+
+	// ChoiceAltCnt is used to count for each ordered choice expression,
+	// which alternative is used how may times.
+	// These numbers allow to optimize the order of the ordered choice expression
+	// to increase the performance of the parser
+	//
+	// The outer key of ChoiceAltCnt is composed of the name of the rule as well
+	// as the line and the column of the ordered choice.
+	// The inner key of ChoiceAltCnt is the number (one-based) of the matching alternative.
+	// For each alternative the number of matches are counted. If an ordered choice does not
+	// match, a special counter is incremented. The name of this counter is set with
+	// the parser option Statistics.
+	// For an alternative to be included in ChoiceAltCnt, it has to match at least once.
+	ChoiceAltCnt map[string]map[string]int
+}
+
+type parser struct {
+	filename string
+	pt       savepoint
+	cur      current
+
+	data []byte
+	errs *errList
+
+	depth   int
+	recover bool
+	debug   bool
+
+	memoize bool
+	// memoization table for the packrat algorithm:
+	// map[offset in source] map[expression or rule] {value, match}
+	memo map[int]map[any]resultTuple
+
+	// rules table, maps the rule identifier to the rule node
+	rules map[string]*rule
+	// variables stack, map of label to value
+	vstack []map[string]any
+	// rule stack, allows identification of the current rule in errors
+	rstack []*rule
+
+	// parse fail
+	maxFailPos            position
+	maxFailExpected       []string
+	maxFailInvertExpected bool
+
+	// max number of expressions to be parsed
+	maxExprCnt uint64
+	// entrypoint for the parser
+	entrypoint string
+
+	allowInvalidUTF8 bool
+
+	*Stats
+
+	choiceNoMatch string
+	// recovery expression stack, keeps track of the currently available recovery expression, these are traversed in reverse
+	recoveryStack []map[string]any
+}
+
+// push a variable set on the vstack.
+func (p *parser) pushV() {
+	if cap(p.vstack) == len(p.vstack) {
+		// create new empty slot in the stack
+		p.vstack = append(p.vstack, nil)
+	} else {
+		// slice to 1 more
+		p.vstack = p.vstack[:len(p.vstack)+1]
+	}
+
+	// get the last args set
+	m := p.vstack[len(p.vstack)-1]
+	if m != nil && len(m) == 0 {
+		// empty map, all good
+		return
+	}
+
+	m = make(map[string]any)
+	p.vstack[len(p.vstack)-1] = m
+}
+
+// pop a variable set from the vstack.
+func (p *parser) popV() {
+	// if the map is not empty, clear it
+	m := p.vstack[len(p.vstack)-1]
+	if len(m) > 0 {
+		// GC that map
+		p.vstack[len(p.vstack)-1] = nil
+	}
+	p.vstack = p.vstack[:len(p.vstack)-1]
+}
+
+// push a recovery expression with its labels to the recoveryStack
+func (p *parser) pushRecovery(labels []string, expr any) {
+	if cap(p.recoveryStack) == len(p.recoveryStack) {
+		// create new empty slot in the stack
+		p.recoveryStack = append(p.recoveryStack, nil)
+	} else {
+		// slice to 1 more
+		p.recoveryStack = p.recoveryStack[:len(p.recoveryStack)+1]
+	}
+
+	m := make(map[string]any, len(labels))
+	for _, fl := range labels {
+		m[fl] = expr
+	}
+	p.recoveryStack[len(p.recoveryStack)-1] = m
+}
+
+// pop a recovery expression from the recoveryStack
+func (p *parser) popRecovery() {
+	// GC that map
+	p.recoveryStack[len(p.recoveryStack)-1] = nil
+
+	p.recoveryStack = p.recoveryStack[:len(p.recoveryStack)-1]
+}
+
+func (p *parser) print(prefix, s string) string {
+	if !p.debug {
+		return s
+	}
+
+	fmt.Printf("%s %d:%d:%d: %s [%#U]\n",
+		prefix, p.pt.line, p.pt.col, p.pt.offset, s, p.pt.rn)
+	return s
+}
+
+func (p *parser) printIndent(mark string, s string) string {
+	return p.print(strings.Repeat(" ", p.depth)+mark, s)
+}
+
+func (p *parser) in(s string) string {
+	res := p.printIndent(">", s)
+	p.depth++
+	return res
+}
+
+func (p *parser) out(s string) string {
+	p.depth--
+	return p.printIndent("<", s)
+}
+
+func (p *parser) addErr(err error) {
+	p.addErrAt(err, p.pt.position, []string{})
+}
+
+func (p *parser) addErrAt(err error, pos position, expected []string) {
+	var buf bytes.Buffer
+	if p.filename != "" {
+		buf.WriteString(p.filename)
+	}
+	if buf.Len() > 0 {
+		buf.WriteString(":")
+	}
+	buf.WriteString(fmt.Sprintf("%d:%d (%d)", pos.line, pos.col, pos.offset))
+	if len(p.rstack) > 0 {
+		if buf.Len() > 0 {
+			buf.WriteString(": ")
+		}
+		rule := p.rstack[len(p.rstack)-1]
+		if rule.displayName != "" {
+			buf.WriteString("rule " + rule.displayName)
+		} else {
+			buf.WriteString("rule " + rule.name)
+		}
+	}
+	pe := &parserError{Inner: err, pos: pos, prefix: buf.String(), expected: expected}
+	p.errs.add(pe)
+}
+
+func (p *parser) failAt(fail bool, pos position, want string) {
+	// process fail if parsing fails and not inverted or parsing succeeds and invert is set
+	if fail == p.maxFailInvertExpected {
+		if pos.offset < p.maxFailPos.offset {
+			return
+		}
+
+		if pos.offset > p.maxFailPos.offset {
+			p.maxFailPos = pos
+			p.maxFailExpected = p.maxFailExpected[:0]
+		}
+
+		if p.maxFailInvertExpected {
+			want = "!" + want
+		}
+		p.maxFailExpected = append(p.maxFailExpected, want)
+	}
+}
+
+// read advances the parser to the next rune.
+func (p *parser) read() {
+	p.pt.offset += p.pt.w
+	rn, n := utf8.DecodeRune(p.data[p.pt.offset:])
+	p.pt.rn = rn
+	p.pt.w = n
+	p.pt.col++
+	if rn == '\n' {
+		p.pt.line++
+		p.pt.col = 0
+	}
+
+	if rn == utf8.RuneError && n == 1 { // see utf8.DecodeRune
+		if !p.allowInvalidUTF8 {
+			p.addErr(errInvalidEncoding)
+		}
+	}
+}
+
+// restore parser position to the savepoint pt.
+func (p *parser) restore(pt savepoint) {
+	if p.debug {
+		defer p.out(p.in("restore"))
+	}
+	if pt.offset == p.pt.offset {
+		return
+	}
+	p.pt = pt
+}
+
+// Cloner is implemented by any value that has a Clone method, which returns a
+// copy of the value. This is mainly used for types which are not passed by
+// value (e.g map, slice, chan) or structs that contain such types.
+//
+// This is used in conjunction with the global state feature to create proper
+// copies of the state to allow the parser to properly restore the state in
+// the case of backtracking.
+type Cloner interface {
+	Clone() any
+}
+
+var statePool = &sync.Pool{
+	New: func() any { return make(storeDict) },
+}
+
+func (sd storeDict) Discard() {
+	for k := range sd {
+		delete(sd, k)
+	}
+	statePool.Put(sd)
+}
+
+// clone and return parser current state.
+func (p *parser) cloneState() storeDict {
+	if p.debug {
+		defer p.out(p.in("cloneState"))
+	}
+
+	state := statePool.Get().(storeDict)
+	for k, v := range p.cur.state {
+		if c, ok := v.(Cloner); ok {
+			state[k] = c.Clone()
+		} else {
+			state[k] = v
+		}
+	}
+	return state
+}
+
+// restore parser current state to the state storeDict.
+// every restoreState should applied only one time for every cloned state
+func (p *parser) restoreState(state storeDict) {
+	if p.debug {
+		defer p.out(p.in("restoreState"))
+	}
+	p.cur.state.Discard()
+	p.cur.state = state
+}
+
+// get the slice of bytes from the savepoint start to the current position.
+func (p *parser) sliceFrom(start savepoint) []byte {
+	return p.data[start.position.offset:p.pt.position.offset]
+}
+
+func (p *parser) getMemoized(node any) (resultTuple, bool) {
+	if len(p.memo) == 0 {
+		return resultTuple{}, false
+	}
+	m := p.memo[p.pt.offset]
+	if len(m) == 0 {
+		return resultTuple{}, false
+	}
+	res, ok := m[node]
+	return res, ok
+}
+
+func (p *parser) setMemoized(pt savepoint, node any, tuple resultTuple) {
+	if p.memo == nil {
+		p.memo = make(map[int]map[any]resultTuple)
+	}
+	m := p.memo[pt.offset]
+	if m == nil {
+		m = make(map[any]resultTuple)
+		p.memo[pt.offset] = m
+	}
+	m[node] = tuple
+}
+
+func (p *parser) buildRulesTable(g *grammar) {
+	p.rules = make(map[string]*rule, len(g.rules))
+	for _, r := range g.rules {
+		p.rules[r.name] = r
+	}
+}
+
+func (p *parser) parse(g *grammar) (val any, err error) {
+	if len(g.rules) == 0 {
+		p.addErr(errNoRule)
+		return nil, p.errs.err()
+	}
+
+	// TODO : not super critical but this could be generated
+	p.buildRulesTable(g)
+
+	if p.recover {
+		// panic can be used in action code to stop parsing immediately
+		// and return the panic as an error.
+		defer func() {
+			if e := recover(); e != nil {
+				if p.debug {
+					defer p.out(p.in("panic handler"))
+				}
+				val = nil
+				switch e := e.(type) {
+				case error:
+					p.addErr(e)
+				default:
+					p.addErr(fmt.Errorf("%v", e))
+				}
+				err = p.errs.err()
+			}
+		}()
+	}
+
+	startRule, ok := p.rules[p.entrypoint]
+	if !ok {
+		p.addErr(errInvalidEntrypoint)
+		return nil, p.errs.err()
+	}
+
+	p.read() // advance to first rune
+	val, ok = p.parseRuleWrap(startRule)
+	if !ok {
+		if len(*p.errs) == 0 {
+			// If parsing fails, but no errors have been recorded, the expected values
+			// for the farthest parser position are returned as error.
+			maxFailExpectedMap := make(map[string]struct{}, len(p.maxFailExpected))
+			for _, v := range p.maxFailExpected {
+				maxFailExpectedMap[v] = struct{}{}
+			}
+			expected := make([]string, 0, len(maxFailExpectedMap))
+			eof := false
+			if _, ok := maxFailExpectedMap["!."]; ok {
+				delete(maxFailExpectedMap, "!.")
+				eof = true
+			}
+			for k := range maxFailExpectedMap {
+				expected = append(expected, k)
+			}
+			sort.Strings(expected)
+			if eof {
+				expected = append(expected, "EOF")
+			}
+			p.addErrAt(errors.New("no match found, expected: "+listJoin(expected, ", ", "or")), p.maxFailPos, expected)
+		}
+
+		return nil, p.errs.err()
+	}
+	return val, p.errs.err()
+}
+
+func listJoin(list []string, sep string, lastSep string) string {
+	switch len(list) {
+	case 0:
+		return ""
+	case 1:
+		return list[0]
+	default:
+		return strings.Join(list[:len(list)-1], sep) + " " + lastSep + " " + list[len(list)-1]
+	}
+}
+
+func (p *parser) parseRuleMemoize(rule *rule) (any, bool) {
+	res, ok := p.getMemoized(rule)
+	if ok {
+		p.restore(res.end)
+		return res.v, res.b
+	}
+
+	startMark := p.pt
+	val, ok := p.parseRule(rule)
+	p.setMemoized(startMark, rule, resultTuple{val, ok, p.pt})
+
+	return val, ok
+}
+
+func (p *parser) parseRuleWrap(rule *rule) (any, bool) {
+	if p.debug {
+		defer p.out(p.in("parseRule " + rule.name))
+	}
+	var (
+		val       any
+		ok        bool
+		startMark = p.pt
+	)
+
+	if p.memoize {
+		val, ok = p.parseRuleMemoize(rule)
+	} else {
+		val, ok = p.parseRule(rule)
+	}
+
+	if ok && p.debug {
+		p.printIndent("MATCH", string(p.sliceFrom(startMark)))
+	}
+	return val, ok
+}
+
+func (p *parser) parseRule(rule *rule) (any, bool) {
+	p.rstack = append(p.rstack, rule)
+	p.pushV()
+	val, ok := p.parseExprWrap(rule.expr)
+	p.popV()
+	p.rstack = p.rstack[:len(p.rstack)-1]
+	return val, ok
+}
+
+func (p *parser) parseExprWrap(expr any) (any, bool) {
+	var pt savepoint
+
+	if p.memoize {
+		res, ok := p.getMemoized(expr)
+		if ok {
+			p.restore(res.end)
+			return res.v, res.b
+		}
+		pt = p.pt
+	}
+
+	val, ok := p.parseExpr(expr)
+
+	if p.memoize {
+		p.setMemoized(pt, expr, resultTuple{val, ok, p.pt})
+	}
+	return val, ok
+}
+
+func (p *parser) parseExpr(expr any) (any, bool) {
+	p.ExprCnt++
+	if p.ExprCnt > p.maxExprCnt {
+		panic(errMaxExprCnt)
+	}
+
+	var val any
+	var ok bool
+	switch expr := expr.(type) {
+	case *actionExpr:
+		val, ok = p.parseActionExpr(expr)
+	case *andCodeExpr:
+		val, ok = p.parseAndCodeExpr(expr)
+	case *andExpr:
+		val, ok = p.parseAndExpr(expr)
+	case *anyMatcher:
+		val, ok = p.parseAnyMatcher(expr)
+	case *charClassMatcher:
+		val, ok = p.parseCharClassMatcher(expr)
+	case *choiceExpr:
+		val, ok = p.parseChoiceExpr(expr)
+	case *labeledExpr:
+		val, ok = p.parseLabeledExpr(expr)
+	case *litMatcher:
+		val, ok = p.parseLitMatcher(expr)
+	case *notCodeExpr:
+		val, ok = p.parseNotCodeExpr(expr)
+	case *notExpr:
+		val, ok = p.parseNotExpr(expr)
+	case *oneOrMoreExpr:
+		val, ok = p.parseOneOrMoreExpr(expr)
+	case *recoveryExpr:
+		val, ok = p.parseRecoveryExpr(expr)
+	case *ruleRefExpr:
+		val, ok = p.parseRuleRefExpr(expr)
+	case *seqExpr:
+		val, ok = p.parseSeqExpr(expr)
+	case *stateCodeExpr:
+		val, ok = p.parseStateCodeExpr(expr)
+	case *throwExpr:
+		val, ok = p.parseThrowExpr(expr)
+	case *zeroOrMoreExpr:
+		val, ok = p.parseZeroOrMoreExpr(expr)
+	case *zeroOrOneExpr:
+		val, ok = p.parseZeroOrOneExpr(expr)
+	default:
+		panic(fmt.Sprintf("unknown expression type %T", expr))
+	}
+	return val, ok
+}
+
+func (p *parser) parseActionExpr(act *actionExpr) (any, bool) {
+	if p.debug {
+		defer p.out(p.in("parseActionExpr"))
+	}
+
+	start := p.pt
+	val, ok := p.parseExprWrap(act.expr)
+	if ok {
+		p.cur.pos = start.position
+		p.cur.text = p.sliceFrom(start)
+		state := p.cloneState()
+		actVal, err := act.run(p)
+		if err != nil {
+			p.addErrAt(err, start.position, []string{})
+		}
+		p.restoreState(state)
+
+		val = actVal
+	}
+	if ok && p.debug {
+		p.printIndent("MATCH", string(p.sliceFrom(start)))
+	}
+	return val, ok
+}
+
+func (p *parser) parseAndCodeExpr(and *andCodeExpr) (any, bool) {
+	if p.debug {
+		defer p.out(p.in("parseAndCodeExpr"))
+	}
+
+	state := p.cloneState()
+
+	ok, err := and.run(p)
+	if err != nil {
+		p.addErr(err)
+	}
+	p.restoreState(state)
+
+	return nil, ok
+}
+
+func (p *parser) parseAndExpr(and *andExpr) (any, bool) {
+	if p.debug {
+		defer p.out(p.in("parseAndExpr"))
+	}
+
+	pt := p.pt
+	state := p.cloneState()
+	p.pushV()
+	_, ok := p.parseExprWrap(and.expr)
+	p.popV()
+	p.restoreState(state)
+	p.restore(pt)
+
+	return nil, ok
+}
+
+func (p *parser) parseAnyMatcher(any *anyMatcher) (any, bool) {
+	if p.debug {
+		defer p.out(p.in("parseAnyMatcher"))
+	}
+
+	if p.pt.rn == utf8.RuneError && p.pt.w == 0 {
+		// EOF - see utf8.DecodeRune
+		p.failAt(false, p.pt.position, ".")
+		return nil, false
+	}
+	start := p.pt
+	p.read()
+	p.failAt(true, start.position, ".")
+	return p.sliceFrom(start), true
+}
+
+func (p *parser) parseCharClassMatcher(chr *charClassMatcher) (any, bool) {
+	if p.debug {
+		defer p.out(p.in("parseCharClassMatcher"))
+	}
+
+	cur := p.pt.rn
+	start := p.pt
+
+	// can't match EOF
+	if cur == utf8.RuneError && p.pt.w == 0 { // see utf8.DecodeRune
+		p.failAt(false, start.position, chr.val)
+		return nil, false
+	}
+
+	if chr.ignoreCase {
+		cur = unicode.ToLower(cur)
+	}
+
+	// try to match in the list of available chars
+	for _, rn := range chr.chars {
+		if rn == cur {
+			if chr.inverted {
+				p.failAt(false, start.position, chr.val)
+				return nil, false
+			}
+			p.read()
+			p.failAt(true, start.position, chr.val)
+			return p.sliceFrom(start), true
+		}
+	}
+
+	// try to match in the list of ranges
+	for i := 0; i < len(chr.ranges); i += 2 {
+		if cur >= chr.ranges[i] && cur <= chr.ranges[i+1] {
+			if chr.inverted {
+				p.failAt(false, start.position, chr.val)
+				return nil, false
+			}
+			p.read()
+			p.failAt(true, start.position, chr.val)
+			return p.sliceFrom(start), true
+		}
+	}
+
+	// try to match in the list of Unicode classes
+	for _, cl := range chr.classes {
+		if unicode.Is(cl, cur) {
+			if chr.inverted {
+				p.failAt(false, start.position, chr.val)
+				return nil, false
+			}
+			p.read()
+			p.failAt(true, start.position, chr.val)
+			return p.sliceFrom(start), true
+		}
+	}
+
+	if chr.inverted {
+		p.read()
+		p.failAt(true, start.position, chr.val)
+		return p.sliceFrom(start), true
+	}
+	p.failAt(false, start.position, chr.val)
+	return nil, false
+}
+
+func (p *parser) incChoiceAltCnt(ch *choiceExpr, altI int) {
+	choiceIdent := fmt.Sprintf("%s %d:%d", p.rstack[len(p.rstack)-1].name, ch.pos.line, ch.pos.col)
+	m := p.ChoiceAltCnt[choiceIdent]
+	if m == nil {
+		m = make(map[string]int)
+		p.ChoiceAltCnt[choiceIdent] = m
+	}
+	// We increment altI by 1, so the keys do not start at 0
+	alt := strconv.Itoa(altI + 1)
+	if altI == choiceNoMatch {
+		alt = p.choiceNoMatch
+	}
+	m[alt]++
+}
+
+func (p *parser) parseChoiceExpr(ch *choiceExpr) (any, bool) {
+	if p.debug {
+		defer p.out(p.in("parseChoiceExpr"))
+	}
+
+	for altI, alt := range ch.alternatives {
+		// dummy assignment to prevent compile error if optimized
+		_ = altI
+
+		state := p.cloneState()
+
+		p.pushV()
+		val, ok := p.parseExprWrap(alt)
+		p.popV()
+		if ok {
+			p.incChoiceAltCnt(ch, altI)
+			return val, ok
+		}
+		p.restoreState(state)
+	}
+	p.incChoiceAltCnt(ch, choiceNoMatch)
+	return nil, false
+}
+
+func (p *parser) parseLabeledExpr(lab *labeledExpr) (any, bool) {
+	if p.debug {
+		defer p.out(p.in("parseLabeledExpr"))
+	}
+
+	p.pushV()
+	val, ok := p.parseExprWrap(lab.expr)
+	p.popV()
+	if ok && lab.label != "" {
+		m := p.vstack[len(p.vstack)-1]
+		m[lab.label] = val
+	}
+	return val, ok
+}
+
+func (p *parser) parseLitMatcher(lit *litMatcher) (any, bool) {
+	if p.debug {
+		defer p.out(p.in("parseLitMatcher"))
+	}
+
+	start := p.pt
+	for _, want := range lit.val {
+		cur := p.pt.rn
+		if lit.ignoreCase {
+			cur = unicode.ToLower(cur)
+		}
+		if cur != want {
+			p.failAt(false, start.position, lit.want)
+			p.restore(start)
+			return nil, false
+		}
+		p.read()
+	}
+	p.failAt(true, start.position, lit.want)
+	return p.sliceFrom(start), true
+}
+
+func (p *parser) parseNotCodeExpr(not *notCodeExpr) (any, bool) {
+	if p.debug {
+		defer p.out(p.in("parseNotCodeExpr"))
+	}
+
+	state := p.cloneState()
+
+	ok, err := not.run(p)
+	if err != nil {
+		p.addErr(err)
+	}
+	p.restoreState(state)
+
+	return nil, !ok
+}
+
+func (p *parser) parseNotExpr(not *notExpr) (any, bool) {
+	if p.debug {
+		defer p.out(p.in("parseNotExpr"))
+	}
+
+	pt := p.pt
+	state := p.cloneState()
+	p.pushV()
+	p.maxFailInvertExpected = !p.maxFailInvertExpected
+	_, ok := p.parseExprWrap(not.expr)
+	p.maxFailInvertExpected = !p.maxFailInvertExpected
+	p.popV()
+	p.restoreState(state)
+	p.restore(pt)
+
+	return nil, !ok
+}
+
+func (p *parser) parseOneOrMoreExpr(expr *oneOrMoreExpr) (any, bool) {
+	if p.debug {
+		defer p.out(p.in("parseOneOrMoreExpr"))
+	}
+
+	var vals []any
+
+	for {
+		p.pushV()
+		val, ok := p.parseExprWrap(expr.expr)
+		p.popV()
+		if !ok {
+			if len(vals) == 0 {
+				// did not match once, no match
+				return nil, false
+			}
+			return vals, true
+		}
+		vals = append(vals, val)
+	}
+}
+
+func (p *parser) parseRecoveryExpr(recover *recoveryExpr) (any, bool) {
+	if p.debug {
+		defer p.out(p.in("parseRecoveryExpr (" + strings.Join(recover.failureLabel, ",") + ")"))
+	}
+
+	p.pushRecovery(recover.failureLabel, recover.recoverExpr)
+	val, ok := p.parseExprWrap(recover.expr)
+	p.popRecovery()
+
+	return val, ok
+}
+
+func (p *parser) parseRuleRefExpr(ref *ruleRefExpr) (any, bool) {
+	if p.debug {
+		defer p.out(p.in("parseRuleRefExpr " + ref.name))
+	}
+
+	if ref.name == "" {
+		panic(fmt.Sprintf("%s: invalid rule: missing name", ref.pos))
+	}
+
+	rule := p.rules[ref.name]
+	if rule == nil {
+		p.addErr(fmt.Errorf("undefined rule: %s", ref.name))
+		return nil, false
+	}
+	return p.parseRuleWrap(rule)
+}
+
+func (p *parser) parseSeqExpr(seq *seqExpr) (any, bool) {
+	if p.debug {
+		defer p.out(p.in("parseSeqExpr"))
+	}
+
+	vals := make([]any, 0, len(seq.exprs))
+
+	pt := p.pt
+	state := p.cloneState()
+	for _, expr := range seq.exprs {
+		val, ok := p.parseExprWrap(expr)
+		if !ok {
+			p.restoreState(state)
+			p.restore(pt)
+			return nil, false
+		}
+		vals = append(vals, val)
+	}
+	return vals, true
+}
+
+func (p *parser) parseStateCodeExpr(state *stateCodeExpr) (any, bool) {
+	if p.debug {
+		defer p.out(p.in("parseStateCodeExpr"))
+	}
+
+	err := state.run(p)
+	if err != nil {
+		p.addErr(err)
+	}
+	return nil, true
+}
+
+func (p *parser) parseThrowExpr(expr *throwExpr) (any, bool) {
+	if p.debug {
+		defer p.out(p.in("parseThrowExpr"))
+	}
+
+	for i := len(p.recoveryStack) - 1; i >= 0; i-- {
+		if recoverExpr, ok := p.recoveryStack[i][expr.label]; ok {
+			if val, ok := p.parseExprWrap(recoverExpr); ok {
+				return val, ok
+			}
+		}
+	}
+
+	return nil, false
+}
+
+func (p *parser) parseZeroOrMoreExpr(expr *zeroOrMoreExpr) (any, bool) {
+	if p.debug {
+		defer p.out(p.in("parseZeroOrMoreExpr"))
+	}
+
+	var vals []any
+
+	for {
+		p.pushV()
+		val, ok := p.parseExprWrap(expr.expr)
+		p.popV()
+		if !ok {
+			return vals, true
+		}
+		vals = append(vals, val)
+	}
+}
+
+func (p *parser) parseZeroOrOneExpr(expr *zeroOrOneExpr) (any, bool) {
+	if p.debug {
+		defer p.out(p.in("parseZeroOrOneExpr"))
+	}
+
+	p.pushV()
+	val, _ := p.parseExprWrap(expr.expr)
+	p.popV()
+	// whether it matched or not, consider it a match
+	return val, true
+}