(herald "small test" (algebra diffie-hellman))

(comment "CPSA 3.6.8")
(comment "All input read from tst/test_g.scm")

(defprotocol test1 diffie-hellman
  (defrole init
    (vars (x rndx) (w expt) (k skey))
    (trace (send (enc (exp (gen) x) k)) (recv (exp (gen) (mul x w))))
    (non-orig k)
    (uniq-gen x)))

(defskeleton test1
  (vars (k skey) (x rndx) (w expt))
  (defstrand init 2 (k k) (x x) (w w))
  (non-orig k)
  (uniq-gen x)
  (traces ((send (enc (exp (gen) x) k)) (recv (exp (gen) (mul x w)))))
  (label 0)
  (unrealized (0 1))
  (origs)
  (comment "4 in cohort - 4 not yet seen"))

(defskeleton test1
  (vars (k skey) (x rndx))
  (defstrand init 2 (k k) (x x) (w (rec x)))
  (non-orig k)
  (uniq-gen x)
  (operation nonce-test (contracted (x-0 x) (w (rec x))) (gen) (0 1))
  (traces ((send (enc (exp (gen) x) k)) (recv (gen))))
  (label 1)
  (parent 0)
  (unrealized)
  (shape)
  (maps ((0) ((k k) (x x) (w (rec x)))))
  (origs))

(defskeleton test1
  (vars (k skey) (x rndx))
  (defstrand init 2 (k k) (x x) (w (one)))
  (non-orig k)
  (uniq-gen x)
  (operation nonce-test (displaced 1 0 init 1) (exp (gen) x-0) (0 1))
  (traces ((send (enc (exp (gen) x) k)) (recv (exp (gen) x))))
  (label 2)
  (parent 0)
  (unrealized (0 1))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton test1
  (vars (k k-0 skey) (x x-0 rndx))
  (defstrand init 2 (k k) (x x) (w (mul (rec x) x-0)))
  (defstrand init 1 (k k-0) (x x-0))
  (precedes ((1 0) (0 1)))
  (non-orig k k-0)
  (uniq-gen x x-0)
  (operation nonce-test (added-strand init 1) (exp (gen) x-0) (0 1))
  (traces ((send (enc (exp (gen) x) k)) (recv (exp (gen) x-0)))
    ((send (enc (exp (gen) x-0) k-0))))
  (label 3)
  (parent 0)
  (unrealized (0 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton test1
  (vars (k skey) (x rndx) (w w-0 expt))
  (defstrand init 2 (k k) (x x) (w w))
  (deflistener (cat (exp (gen) (mul x w (rec w-0))) w-0))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig k)
  (uniq-gen x)
  (precur (1 0))
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul x w (rec w-0))) w-0))
    (exp (gen) (mul x w)) (0 1))
  (traces ((send (enc (exp (gen) x) k)) (recv (exp (gen) (mul x w))))
    ((recv (cat (exp (gen) (mul x w (rec w-0))) w-0))
      (send (cat (exp (gen) (mul x w (rec w-0))) w-0))))
  (label 4)
  (parent 0)
  (unrealized (1 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton test1
  (vars (k skey) (x rndx) (w expt))
  (defstrand init 2 (k k) (x x) (w (one)))
  (deflistener (cat (exp (gen) (mul x (rec w))) w))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig k)
  (uniq-gen x)
  (precur (1 0))
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul x (rec w))) w)) (exp (gen) x)
    (0 1) (enc (exp (gen) x) k))
  (traces ((send (enc (exp (gen) x) k)) (recv (exp (gen) x)))
    ((recv (cat (exp (gen) (mul x (rec w))) w))
      (send (cat (exp (gen) (mul x (rec w))) w))))
  (label 5)
  (parent 2)
  (unrealized (1 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton test1
  (vars (k k-0 skey) (x x-0 rndx) (w expt))
  (defstrand init 2 (k k) (x x) (w (mul (rec x) x-0)))
  (defstrand init 1 (k k-0) (x x-0))
  (deflistener (cat (exp (gen) (mul x-0 (rec w))) w))
  (precedes ((1 0) (2 0)) ((2 1) (0 1)))
  (non-orig k k-0)
  (uniq-gen x x-0)
  (precur (2 0))
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul x-0 (rec w))) w))
    (exp (gen) x-0) (0 1) (enc (exp (gen) x-0) k-0))
  (traces ((send (enc (exp (gen) x) k)) (recv (exp (gen) x-0)))
    ((send (enc (exp (gen) x-0) k-0)))
    ((recv (cat (exp (gen) (mul x-0 (rec w))) w))
      (send (cat (exp (gen) (mul x-0 (rec w))) w))))
  (label 6)
  (parent 3)
  (unrealized (2 0))
  (comment "4 in cohort - 4 not yet seen"))

(defskeleton test1
  (vars (k skey) (x rndx) (w expt))
  (defstrand init 2 (k k) (x x) (w (mul (rec x) w)))
  (deflistener (cat (gen) w))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig k)
  (uniq-gen x)
  (precur (1 0))
  (operation nonce-test
    (contracted (x-0 x) (w-0 (mul (rec x) w)) (w-1 w)) (gen) (1 0))
  (traces ((send (enc (exp (gen) x) k)) (recv (exp (gen) w)))
    ((recv (cat (gen) w)) (send (cat (gen) w))))
  (label 7)
  (parent 4)
  (seen 0)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton test1
  (vars (k skey) (w expt) (x rndx))
  (defstrand init 2 (k k) (x x) (w w))
  (deflistener (cat (exp (gen) x) w))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig k)
  (precur (1 0))
  (uniq-gen x)
  (operation nonce-test (displaced 2 0 init 1) (exp (gen) x-0) (1 0))
  (traces ((send (enc (exp (gen) x) k)) (recv (exp (gen) (mul w x))))
    ((recv (cat (exp (gen) x) w)) (send (cat (exp (gen) x) w))))
  (label 8)
  (parent 4)
  (unrealized (1 0))
  (dead)
  (comment "empty cohort"))

(defskeleton test1
  (vars (k k-0 skey) (x rndx) (w expt) (x-0 rndx))
  (defstrand init 2 (k k) (x x) (w (mul (rec x) w x-0)))
  (deflistener (cat (exp (gen) x-0) w))
  (defstrand init 1 (k k-0) (x x-0))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((2 0) (1 0)))
  (non-orig k k-0)
  (precur (1 0))
  (uniq-gen x x-0)
  (operation nonce-test (added-strand init 1) (exp (gen) x-0) (1 0))
  (traces ((send (enc (exp (gen) x) k)) (recv (exp (gen) (mul w x-0))))
    ((recv (cat (exp (gen) x-0) w)) (send (cat (exp (gen) x-0) w)))
    ((send (enc (exp (gen) x-0) k-0))))
  (label 9)
  (parent 4)
  (unrealized (1 0))
  (dead)
  (comment "empty cohort"))

(defskeleton test1
  (vars (k skey) (x rndx))
  (defstrand init 2 (k k) (x x) (w (one)))
  (deflistener (cat (gen) x))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig k)
  (uniq-gen x)
  (precur (1 0))
  (operation nonce-test (contracted (x-0 x) (w x)) (gen) (1 0))
  (traces ((send (enc (exp (gen) x) k)) (recv (exp (gen) x)))
    ((recv (cat (gen) x)) (send (cat (gen) x))))
  (label 10)
  (parent 5)
  (unrealized (1 0))
  (dead)
  (comment "empty cohort"))

(defskeleton test1
  (vars (k skey) (x rndx))
  (defstrand init 2 (k k) (x x) (w (one)))
  (deflistener (cat (exp (gen) x) (one)))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig k)
  (precur (1 0))
  (uniq-gen x)
  (operation nonce-test (displaced 2 0 init 1) (exp (gen) x-0) (1 0))
  (traces ((send (enc (exp (gen) x) k)) (recv (exp (gen) x)))
    ((recv (cat (exp (gen) x) (one))) (send (cat (exp (gen) x) (one)))))
  (label 11)
  (parent 5)
  (unrealized (1 0))
  (dead)
  (comment "empty cohort"))

(defskeleton test1
  (vars (k k-0 skey) (x x-0 rndx))
  (defstrand init 2 (k k) (x x) (w (one)))
  (deflistener (cat (exp (gen) x-0) (mul x (rec x-0))))
  (defstrand init 1 (k k-0) (x x-0))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((2 0) (1 0)))
  (non-orig k k-0)
  (precur (1 0))
  (uniq-gen x x-0)
  (operation nonce-test (added-strand init 1) (exp (gen) x-0) (1 0))
  (traces ((send (enc (exp (gen) x) k)) (recv (exp (gen) x)))
    ((recv (cat (exp (gen) x-0) (mul x (rec x-0))))
      (send (cat (exp (gen) x-0) (mul x (rec x-0)))))
    ((send (enc (exp (gen) x-0) k-0))))
  (label 12)
  (parent 5)
  (unrealized (0 1) (1 0))
  (dead)
  (comment "empty cohort"))

(defskeleton test1
  (vars (k k-0 skey) (x x-0 rndx))
  (defstrand init 2 (k k) (x x) (w (mul (rec x) x-0)))
  (defstrand init 1 (k k-0) (x x-0))
  (deflistener (cat (gen) x-0))
  (precedes ((1 0) (2 0)) ((2 1) (0 1)))
  (non-orig k k-0)
  (uniq-gen x x-0)
  (precur (2 0))
  (operation nonce-test (contracted (x-1 x-0) (w x-0)) (gen) (2 0))
  (traces ((send (enc (exp (gen) x) k)) (recv (exp (gen) x-0)))
    ((send (enc (exp (gen) x-0) k-0)))
    ((recv (cat (gen) x-0)) (send (cat (gen) x-0))))
  (label 13)
  (parent 6)
  (unrealized (2 0))
  (dead)
  (comment "empty cohort"))

(defskeleton test1
  (vars (k k-0 skey) (x x-0 rndx))
  (defstrand init 2 (k k) (x x-0) (w (mul x (rec x-0))))
  (defstrand init 1 (k k-0) (x x))
  (deflistener (cat (exp (gen) x-0) (mul x (rec x-0))))
  (precedes ((0 0) (2 0)) ((1 0) (2 0)) ((2 1) (0 1)))
  (non-orig k k-0)
  (precur (2 0))
  (uniq-gen x x-0)
  (operation nonce-test (displaced 3 0 init 1) (exp (gen) x-1) (2 0))
  (traces ((send (enc (exp (gen) x-0) k)) (recv (exp (gen) x)))
    ((send (enc (exp (gen) x) k-0)))
    ((recv (cat (exp (gen) x-0) (mul x (rec x-0))))
      (send (cat (exp (gen) x-0) (mul x (rec x-0))))))
  (label 14)
  (parent 6)
  (unrealized (0 1) (2 0))
  (dead)
  (comment "empty cohort"))

(defskeleton test1
  (vars (k k-0 skey) (x x-0 rndx))
  (defstrand init 2 (k k) (x x) (w (mul (rec x) x-0)))
  (defstrand init 1 (k k-0) (x x-0))
  (deflistener (cat (exp (gen) x-0) (one)))
  (precedes ((1 0) (2 0)) ((2 1) (0 1)))
  (non-orig k k-0)
  (precur (2 0))
  (uniq-gen x x-0)
  (operation nonce-test (displaced 3 1 init 1) (exp (gen) x-1) (2 0))
  (traces ((send (enc (exp (gen) x) k)) (recv (exp (gen) x-0)))
    ((send (enc (exp (gen) x-0) k-0)))
    ((recv (cat (exp (gen) x-0) (one)))
      (send (cat (exp (gen) x-0) (one)))))
  (label 15)
  (parent 6)
  (unrealized (2 0))
  (dead)
  (comment "empty cohort"))

(defskeleton test1
  (vars (k k-0 k-1 skey) (x x-0 x-1 rndx))
  (defstrand init 2 (k k) (x x) (w (mul (rec x) x-0)))
  (defstrand init 1 (k k-0) (x x-0))
  (deflistener (cat (exp (gen) x-1) (mul x-0 (rec x-1))))
  (defstrand init 1 (k k-1) (x x-1))
  (precedes ((1 0) (2 0)) ((2 1) (0 1)) ((3 0) (2 0)))
  (non-orig k k-0 k-1)
  (precur (2 0))
  (uniq-gen x x-0 x-1)
  (operation nonce-test (added-strand init 1) (exp (gen) x-1) (2 0))
  (traces ((send (enc (exp (gen) x) k)) (recv (exp (gen) x-0)))
    ((send (enc (exp (gen) x-0) k-0)))
    ((recv (cat (exp (gen) x-1) (mul x-0 (rec x-1))))
      (send (cat (exp (gen) x-1) (mul x-0 (rec x-1)))))
    ((send (enc (exp (gen) x-1) k-1))))
  (label 16)
  (parent 6)
  (unrealized (0 1) (2 0))
  (dead)
  (comment "empty cohort"))

(comment "Nothing left to do")