Theory Restrictive_Comp

theory Restrictive_Comp
  imports CryptHOL.CryptHOL
begin

section ‹Restrictive Computations›

text ‹We formalize the notion of restrictive computational models. 
These are models in which the adversary is restricted, in the sense that 
its output follows certain rules that can be enforced by constraints composed 
of the input to and the output of the adversary.

We formalize this notion in 3 components: 
1. the Select record -- purpose: select relevant elements from the input
2. the Constrain record -- purpose: constrain output elements to the list 
of relevant (selected) seen elements.
3. Restrictive\_Comp locale -- purpose: select relevant elements from the input and enforce constraints
on the output.

This model is an abstraction over computational models like the Algebraic Group Model (AGM), 
the Algebraic Group Action Model (AGAM), the Algebraic Isogeny Model (AIM), and variants thereof.

We implement generalizations for model-type specific implementations to standard type constructors 
in Isabelle, including (e.g. group) lists, trees, multisets, finite sets, products, and finite maps. 
E.g. a model specific implementation of a group type can be generalized to a group list 
implementation.
Additionally, we provide default implementations noSelect and noConstrain, which select no element
and define no constraints on all inputs.
›

subsection ‹Select›

text ‹A record to select the relevant elements from a type (data structure).
The naming-convention to support automation is \emph{your\_type}S, e.g. for int: intS›
record ('a,'b) Select = select::"'a ⇒'b list" (‹¤ı›)

text ‹We provide a few generalized type constructor implementations.›

context
  fixes r :: "('a,'b) Select"
begin

definition listS::
  "('a list, 'b) Select"
  where "listS ≡ ⦇select = (λxs. concat (map (λx. ¤⇘r⇙x) xs))⦈"

definition treeS :: 
  "('a tree, 'b) Select"
  where "treeS ≡ ⦇select = (λx. ¤⇘listS⇙(inorder x))⦈"

end

context
  fixes r :: "('a::linorder,'b) Select"
begin

definition multisetS :: 
  "('a multiset, 'b) Select"
  where "multisetS ≡ ⦇select = (λx. ¤⇘listS r⇙ (sorted_list_of_multiset x))⦈"


definition fsetS :: 
  "('a fset, 'b) Select"
  where "fsetS ≡ ⦇select = (λx. ¤⇘listS r⇙ (sorted_list_of_fset x))⦈" 

end

context
  fixes ra :: "('a,'c) Select"
  and rb :: "('b,'c) Select"
begin

definition prodS::
  "(('a × 'b), 'c) Select" where
  "prodS ≡ ⦇select = (λ(a,b). ¤⇘ra⇙a @ ¤⇘rb⇙b)⦈"

end

context
  fixes ra :: "('a::linorder,'c) Select"
  and rb :: "('b,'c) Select"
begin

definition fmapS::
  "(('a, 'b) fmap, 'c) Select" where
  "fmapS ≡ ⦇select = (λfm. ¤⇘listS (prodS ra rb)⇙ (sorted_list_of_fmap fm))⦈"

end

definition noSelect :: "('a, 'b) Select"
  where "noSelect ≡ ⦇select = (λx. [])⦈"

lemma noSelectEmpty[simp]: "⋀x. ¤⇘noSelect⇙x = []"
  by (simp add: noSelect_def)

subsection ‹Constrain›

text ‹A record to constrain an (output) element given a list of (input) values. 
constrain returns a Boolean value that states whether the constraint holds.
The naming-convention to support automation is \emph{your\_type}C, e.g. for int: intC›
record ('b,'c) Constrain = constrain::"'b list ⇒ 'c ⇒ bool"(infixl ‹⩥ı› 70)

text ‹We provide a few generalized (data) structures that extend any definition for a 
‹Constrain›.›

context
  fixes r :: "('b,'c) Constrain"
begin

definition listC::
  "('b, 'c list) Constrain"
  where "listC ≡ ⦇constrain = (λip op. list_all (λx. ip ⩥⇘r⇙ x) op)⦈"

definition treeC :: 
  "('b, 'c tree) Constrain"
  where "treeC ≡ ⦇constrain = (λip op. ip ⩥⇘listC⇙(inorder op))⦈"

end

context
  fixes r :: "('b,'c::linorder) Constrain"
begin

definition multisetC :: 
  "('b, 'c multiset) Constrain"
  where "multisetC ≡ ⦇constrain = (λip op. ip ⩥⇘listC r⇙ (sorted_list_of_multiset op))⦈"


definition fsetC :: 
  "('b, 'c fset) Constrain"
  where "fsetC ≡ ⦇constrain = (λip op. ip ⩥⇘listC r⇙ (sorted_list_of_fset op))⦈" 

end

context
  fixes ra :: "('b,'c) Constrain"
  and rb :: "('b,'d) Constrain"
begin

definition prodC::
  "('b, 'c × 'd) Constrain" where
  "prodC ≡ ⦇constrain = (λip (opa,opb). ip ⩥⇘ra⇙ opa ∧ ip ⩥⇘rb⇙ opb)⦈"

end

context
  fixes ra :: "('b,'c::linorder) Constrain"
  and rb :: "('b,'d) Constrain"
begin

definition fmapC::
  "('b, ('c,'d) fmap) Constrain" where
  "fmapC ≡ ⦇constrain = (λip op. ip ⩥⇘listC (prodC ra rb)⇙ (sorted_list_of_fmap op))⦈"

end

definition noConstrain :: "('b,'c) Constrain"
  where "noConstrain ≡  ⦇constrain = (λip op. True)⦈"

lemma noConstrainTrue[simp]: "⋀ip op. ip ⩥⇘noConstrain⇙ op = True"
  by (simp add: noConstrain_def)

subsection ‹restrict›

locale Restrictive_Comp = 
  fixes sel :: "('a,'b) Select"
  and con :: "('b,'c) Constrain"
begin

text ‹Applied to an adversary, ‹restrict› itself becomes a \emph{restricted} adversary that returns
the given adversary's output if and only if it meets the constraints, otherwise it fails.
The constraints are primarily characterized by the constrain function in con (select in sel is 
essentially pre-processing).›
definition restrict :: "('a ⇒ 'c spmf) ⇒ 'a ⇒ 'c spmf" where 
  "restrict 𝒜 arg ≡ do {
  res ← 𝒜 arg;
  _::unit ← assert_spmf ((¤⇘sel⇙ arg) ⩥⇘con⇙ res);
  return_spmf res
  }"

end


subsection ‹Examples›

locale examples 
begin 

text ‹examples for select›

definition intS :: "(int,int) Select"
  where "intS ≡ ⦇select = (λx. [x])⦈"

lemma "¤⇘intS⇙ (1::int) = [1::int]"
  unfolding intS_def
  by simp

lemma "¤⇘listS intS⇙ [1] = [1]"
  by(simp add: listS_def intS_def)

lemma "¤⇘listS (listS intS)⇙ [[1]] = [1]"
  unfolding listS_def intS_def
  by fastforce

lemma "¤⇘prodS (listS intS) intS⇙ ([1],0) = [1,0]"
  unfolding prodS_def listS_def intS_def
  by fastforce

text ‹examples for constrain›

definition intC :: "(int, int) Constrain"
  where "intC ≡ ⦇constrain = (λip op. sum_list ip = op)⦈"

lemma "[0,1,2] ⩥⇘intC⇙ 3"
  by (simp add: intC_def)

lemma "[0,1,2] ⩥⇘listC intC⇙ [3,3,3]"
  unfolding listC_def intC_def
  by simp

lemma "[0,1,2] ⩥⇘prodC (listC intC) intC⇙ ([3,3,3],3)"
  unfolding listC_def intC_def prodC_def
  by fastforce

end

end