fstar-protocol-equivalence/TestedSystem.fst at main · cuplv/fstar-protocol-equivalence · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
module TestedSystem

open Adversary

open SymbolicTypes

module Protocol = Protocol

module SeqProps = FStar.Seq.Properties

(**
  Helper for `transitions'_valid`: a single transition step satisfies the
  knowledge constraints of `valid_observable_transition_relation`.
*)
private
let transitions'_valid_aux
      (#term: eqtype)
      (#obs #id #internal_state: Type)
      (adv: adversary term)
      (p: Protocol.protocol term obs id internal_state)
      (s: state term internal_state)
      (l: label term obs id adv)
      (s': state term internal_state)
    : Lemma
      (requires transitions' adv p s l s')
      (ensures valid_knowledge_change s l s') =
  match l with
  | Observable o lbl_id ->
    eliminate exists t.
        p.transition (s2p_state s) (Protocol.Observable o t lbl_id) (s2p_state s') /\
        s'.know == Seq.snoc s.know t
    returns (forall t'. knowledge_mem s.know t' ==> knowledge_mem s'.know t')
    with _. SeqProps.lemma_mem_snoc s.know t
  | _ -> ()

let transitions'_valid
      (#term: eqtype)
      (#obs #id #internal_state: Type)
      (adv: adversary term)
      (p: Protocol.protocol term obs id internal_state)
    : Lemma (valid_observable_transition_relation (transitions' adv p)) =
  FStar.Classical.forall_intro_3
    (FStar.Classical.move_requires_3 (transitions'_valid_aux adv p))