Revision 7f5fe7453912332a9be00d1efc0f880d80f47a7c authored by François Dupressoir on 14 March 2022, 17:21:04 UTC, committed by François Dupressoir on 14 March 2022, 17:21:15 UTC
Some more work needs done to present a clean theory of prime order groups, and use it properly. We should also ensure that we can eventually support DH over cyclic groups of composite order (operating over prime order subgroups)
1 parent 87ff7f8
ecEnv.mli
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2021 - Inria
* Copyright (c) - 2012--2021 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-C-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
open EcPath
open EcSymbols
open EcTypes
open EcMemory
open EcDecl
open EcCoreFol
open EcModules
open EcTheory
(* -------------------------------------------------------------------- *)
type 'a suspension = {
sp_target : 'a;
sp_params : int * (EcIdent.t * module_type) list;
}
(* -------------------------------------------------------------------- *)
type varbind = {
vb_type : EcTypes.ty;
vb_kind : [ `Proj of int | `Var of EcTypes.pvar_kind ];
}
(* -------------------------------------------------------------------- *)
type env
val initial : EcGState.gstate -> env
val root : env -> EcPath.path
val mroot : env -> EcPath.mpath
val xroot : env -> EcPath.xpath option
val astop : env -> env
(* -------------------------------------------------------------------- *)
val gstate : env -> EcGState.gstate
val copy : env -> env
(* -------------------------------------------------------------------- *)
val notify :
?immediate:bool -> env -> EcGState.loglevel
-> ('a, Format.formatter, unit, unit) format4 -> 'a
(* -------------------------------------------------------------------- *)
type lookup_error = [
| `XPath of xpath
| `MPath of mpath
| `Path of path
| `QSymbol of qsymbol
| `AbsStmt of EcIdent.t
]
exception LookupFailure of lookup_error
exception DuplicatedBinding of symbol
(* -------------------------------------------------------------------- *)
exception NotReducible
(* -------------------------------------------------------------------- *)
type meerror =
| UnknownMemory of [`Symbol of symbol | `Memory of memory]
exception MEError of meerror
module Memory : sig
val all : env -> memenv list
val set_active : memory -> env -> env
val get_active : env -> memory option
val byid : memory -> env -> memenv option
val lookup : symbol -> env -> memenv option
val current : env -> memenv option
val push : memenv -> env -> env
val push_all : memenv list -> env -> env
val push_active : memenv -> env -> env
end
(* -------------------------------------------------------------------- *)
module Fun : sig
type t = function_
val by_xpath : xpath -> env -> t
val by_xpath_opt: xpath -> env -> t option
val lookup : qsymbol -> env -> xpath * t
val lookup_opt : qsymbol -> env -> (xpath * t) option
val lookup_path : qsymbol -> env -> xpath
val sp_lookup : qsymbol -> env -> xpath * t suspension
val sp_lookup_opt : qsymbol -> env -> (xpath * t suspension) option
val enter : symbol -> env -> env
val add : xpath -> env -> env
(* ------------------------------------------------------------------ *)
(* FIXME: what are these functions for? *)
val prF_memenv : EcMemory.memory -> xpath -> env -> memenv
val prF : xpath -> env -> env
val hoareF_memenv : xpath -> env -> memenv * memenv
val hoareF : xpath -> env -> env * env
val hoareS : xpath -> env -> memenv * (funsig * function_def) * env
val actmem_post : memory -> xpath -> function_ -> memenv
val inv_memory : [`Left|`Right] -> env -> memenv
val inv_memenv : env -> env
val equivF_memenv : xpath -> xpath -> env ->
(memenv * memenv) * (memenv * memenv)
val equivF : xpath -> xpath -> env -> env * env
val equivS : xpath -> xpath -> env ->
memenv * (funsig * function_def) * memenv * (funsig * function_def) * env
end
(* -------------------------------------------------------------------- *)
module Var : sig
type t = varbind
val by_xpath : xpath -> env -> t
val by_xpath_opt : xpath -> env -> t option
(* Lookup restricted to given kind of variables *)
val lookup_locals : symbol -> env -> (EcIdent.t * EcTypes.ty) list
val lookup_local : symbol -> env -> (EcIdent.t * EcTypes.ty)
val lookup_local_opt : symbol -> env -> (EcIdent.t * EcTypes.ty) option
val lookup_progvar : ?side:memory -> qsymbol -> env ->
([`Proj of EcTypes.prog_var * EcTypes.ty * (int*int) | `Var of EcTypes.prog_var ] *
EcTypes.ty)
val lookup_progvar_opt : ?side:memory -> qsymbol -> env ->
([`Proj of EcTypes.prog_var * EcTypes.ty * (int*int) | `Var of EcTypes.prog_var ] *
EcTypes.ty) option
(* Locals binding *)
val bind_local : EcIdent.t -> EcTypes.ty -> env -> env
val bind_locals : (EcIdent.t * EcTypes.ty) list -> env -> env
(* Program variables binding *)
val bind : symbol -> pvar_kind -> EcTypes.ty -> env -> env
val bindall : (symbol * EcTypes.ty) list -> pvar_kind -> env -> env
val add : xpath -> env -> env
end
(* -------------------------------------------------------------------- *)
module Ax : sig
type t = axiom
val by_path : path -> env -> t
val by_path_opt : path -> env -> t option
val lookup : qsymbol -> env -> path * t
val lookup_opt : qsymbol -> env -> (path * t) option
val lookup_path : qsymbol -> env -> path
val add : path -> env -> env
val bind : ?import:import -> symbol -> t -> env -> env
val iter : ?name:qsymbol -> (path -> t -> unit) -> env -> unit
val all : ?check:(path -> t -> bool) -> ?name:qsymbol -> env -> (path * t) list
val instanciate : path -> EcTypes.ty list -> env -> form
end
(* -------------------------------------------------------------------- *)
module Mod : sig
type t = top_module_expr
type lkt = module_expr * locality option
type spt = mpath * module_expr suspension * locality option
val by_mpath : mpath -> env -> lkt
val by_mpath_opt: mpath -> env -> lkt option
val lookup : qsymbol -> env -> mpath * lkt
val lookup_opt : qsymbol -> env -> (mpath * lkt) option
val lookup_path : qsymbol -> env -> mpath
val sp_lookup : qsymbol -> env -> spt
val sp_lookup_opt : qsymbol -> env -> spt option
val bind : ?import:import -> symbol -> t -> env -> env
val enter : symbol -> (EcIdent.t * module_type) list -> env -> env
val bind_local : EcIdent.t -> module_type -> mod_restr -> env -> env
val declare_local : EcIdent.t -> module_type -> mod_restr -> env -> env
val is_declared : EcIdent.t -> env -> bool
val import_vars : env -> mpath -> env
(* Only bind module, ie no memory and no local variable *)
val add_mod_binding : bindings -> env -> env
val add : mpath -> env -> env
end
(* -------------------------------------------------------------------- *)
module ModTy : sig
type t = top_module_sig
val by_path : path -> env -> top_module_sig
val by_path_opt : path -> env -> top_module_sig option
val lookup : qsymbol -> env -> path * top_module_sig
val lookup_opt : qsymbol -> env -> (path * top_module_sig) option
val lookup_path : qsymbol -> env -> path
val modtype : path -> env -> module_type
val add : path -> env -> env
val bind : ?import:import -> symbol -> t -> env -> env
val mod_type_equiv : env -> module_type -> module_type -> bool
val has_mod_type : env -> module_type list -> module_type -> bool
val sig_of_mt : env -> module_type -> module_sig
end
(* -------------------------------------------------------------------- *)
type use = {
us_pv : ty EcPath.Mx.t;
us_gl : EcIdent.Sid.t;
}
module NormMp : sig
val norm_mpath : env -> mpath -> mpath
val norm_xfun : env -> xpath -> xpath
val norm_pvar : env -> EcTypes.prog_var -> EcTypes.prog_var
val norm_form : env -> form -> form
val mod_use : env -> mpath -> use
val fun_use : env -> xpath -> use
val norm_restr : env -> mod_restr -> use
val equal_restr : env -> mod_restr -> mod_restr -> bool
val get_restr : env -> mpath -> use
val use_mem_xp : xpath -> use -> bool
val use_mem_gl : mpath -> use -> bool
val norm_glob : env -> EcMemory.memory -> mpath -> form
val norm_tglob : env -> mpath -> EcTypes.ty
val tglob_reducible : env -> mpath -> bool
val is_abstract_fun : xpath -> env -> bool
val x_equal : env -> xpath -> xpath -> bool
val pv_equal : env -> EcTypes.prog_var -> EcTypes.prog_var -> bool
end
(* -------------------------------------------------------------------- *)
module Theory : sig
type t = ctheory
type mode = [`All | thmode]
val by_path : ?mode:mode -> path -> env -> t
val by_path_opt : ?mode:mode -> path -> env -> t option
val lookup : ?mode:mode -> qsymbol -> env -> path * t
val lookup_opt : ?mode:mode -> qsymbol -> env -> (path * t) option
val lookup_path : ?mode:mode -> qsymbol -> env -> path
val add : path -> env -> env
val bind : ?import:import -> symbol -> ctheory -> env -> env
(* FIXME: section ? ctheory -> theory *)
val require : symbol -> ctheory -> env -> env
val import : path -> env -> env
val export : path -> is_local -> env -> env
val enter : symbol -> env -> env
val close :
?clears:(path list)
-> ?pempty:[`Full | `ClearOnly | `No]
-> EcTypes.is_local
-> EcTheory.thmode
-> env -> ctheory option
end
(* -------------------------------------------------------------------- *)
module Op : sig
type t = operator
val by_path : path -> env -> t
val by_path_opt : path -> env -> t option
val lookup : qsymbol -> env -> path * t
val lookup_opt : qsymbol -> env -> (path * t) option
val lookup_path : qsymbol -> env -> path
val add : path -> env -> env
val bind : ?import:import -> symbol -> operator -> env -> env
val reducible : ?force:bool -> env -> path -> bool
val reduce : ?force:bool -> env -> path -> ty list -> form
val is_projection : env -> path -> bool
val is_record_ctor : env -> path -> bool
val is_dtype_ctor : env -> path -> bool
val is_fix_def : env -> path -> bool
val is_abbrev : env -> path -> bool
val is_prind : env -> path -> bool
val scheme_of_prind :
env -> [`Ind | `Case] -> EcPath.path -> (path * int) option
type notation = ty_params * EcDecl.notation
val get_notations : env -> (path * notation) list
val iter : ?name:qsymbol -> (path -> t -> unit) -> env -> unit
val all : ?check:(path -> t -> bool) -> ?name:qsymbol -> env -> (path * t) list
end
(* -------------------------------------------------------------------- *)
module Ty : sig
type t = EcDecl.tydecl
val by_path : path -> env -> t
val by_path_opt : path -> env -> t option
val lookup : qsymbol -> env -> path * t
val lookup_opt : qsymbol -> env -> (path * t) option
val lookup_path : qsymbol -> env -> path
val add : path -> env -> env
val bind : ?import:import -> symbol -> t -> env -> env
val defined : path -> env -> bool
val unfold : path -> EcTypes.ty list -> env -> EcTypes.ty
val hnorm : EcTypes.ty -> env -> EcTypes.ty
val decompose_fun : EcTypes.ty -> env -> EcTypes.dom * EcTypes.ty
val get_top_decl :
EcTypes.ty -> env -> (path * EcDecl.tydecl * EcTypes.ty list) option
val scheme_of_ty :
[`Ind | `Case] -> EcTypes.ty -> env -> (path * EcTypes.ty list) option
val signature : env -> ty -> ty list * ty
val iter : ?name:qsymbol -> (path -> t -> unit) -> env -> unit
val all : ?check:(path -> t -> bool) -> ?name:qsymbol -> env -> (path * t) list
end
val ty_hnorm : ty -> env -> ty
(* -------------------------------------------------------------------- *)
module Algebra : sig
val add_ring : ty -> EcDecl.ring -> is_local -> env -> env
val add_field : ty -> EcDecl.field -> is_local -> env -> env
end
(* -------------------------------------------------------------------- *)
module TypeClass : sig
type t = typeclass
val add : path -> env -> env
val bind : ?import:import -> symbol -> t -> env -> env
val graph : env -> EcTypeClass.graph
val by_path : path -> env -> t
val by_path_opt : path -> env -> t option
val lookup : qsymbol -> env -> path * t
val lookup_opt : qsymbol -> env -> (path * t) option
val lookup_path : qsymbol -> env -> path
val add_instance : ?import:import -> (ty_params * ty) -> tcinstance -> is_local -> env -> env
val get_instances : env -> ((ty_params * ty) * tcinstance) list
end
(* -------------------------------------------------------------------- *)
module BaseRw : sig
val by_path : path -> env -> Sp.t
val lookup : qsymbol -> env -> path * Sp.t
val lookup_opt : qsymbol -> env -> (path * Sp.t) option
val lookup_path : qsymbol -> env -> path
val is_base : qsymbol -> env -> bool
val add : ?import:import -> symbol -> is_local -> env -> env
val addto : ?import:import -> path -> path list -> is_local -> env -> env
end
(* -------------------------------------------------------------------- *)
module Reduction : sig
type rule = EcTheory.rule
type topsym = [ `Path of path | `Tuple ]
val add1 : path * rule_option * rule option -> env -> env
val add : ?import:import -> (path * rule_option * rule option) list -> env -> env
val get : topsym -> env -> rule list
end
(* -------------------------------------------------------------------- *)
module Auto : sig
val dname : symbol
val add1 : ?import:import -> level:int -> ?base:symbol -> path -> is_local -> env -> env
val add : ?import:import -> level:int -> ?base:symbol -> path list -> is_local -> env -> env
val get : ?base:symbol -> env -> path list
val getall : symbol list -> env -> path list
val getx : symbol -> env -> (int * path list) list
end
(* -------------------------------------------------------------------- *)
module AbsStmt : sig
type t = EcModules.abs_uses
val byid : EcIdent.t -> env -> t
end
(* -------------------------------------------------------------------- *)
type ebinding = [
| `Variable of EcTypes.pvar_kind * EcTypes.ty
| `Function of function_
| `Module of module_expr
| `ModType of module_sig
]
val bind1 : symbol * ebinding -> env -> env
val bindall : (symbol * ebinding) list -> env -> env
(* -------------------------------------------------------------------- *)
open EcBaseLogic
module LDecl : sig
type error =
| InvalidKind of EcIdent.t * [`Variable | `Hypothesis]
| CannotClear of EcIdent.t * EcIdent.t
| NameClash of [`Ident of EcIdent.t | `Symbol of symbol]
| LookupError of [`Ident of EcIdent.t | `Symbol of symbol]
exception LdeclError of error
type hyps
val init : env -> ?locals:EcBaseLogic.l_local list -> ty_params -> hyps
val tohyps : hyps -> EcBaseLogic.hyps
val toenv : hyps -> env
val baseenv : hyps -> env
val ld_subst : f_subst -> local_kind -> local_kind
val add_local : EcIdent.t -> local_kind -> hyps -> hyps
val by_name : symbol -> hyps -> l_local
val by_id : EcIdent.t -> hyps -> local_kind
val has_name : symbol -> hyps -> bool
val has_id : EcIdent.t -> hyps -> bool
val as_var : l_local -> EcIdent.t * ty
val as_hyp : l_local -> EcIdent.t * form
val hyp_by_name : symbol -> hyps -> EcIdent.t * form
val hyp_exists : symbol -> hyps -> bool
val hyp_by_id : EcIdent.t -> hyps -> form
val var_by_name : symbol -> hyps -> EcIdent.t * ty
val var_exists : symbol -> hyps -> bool
val var_by_id : EcIdent.t -> hyps -> ty
val local_hyps : EcIdent.t -> hyps -> hyps
val hyp_convert :
EcIdent.t
-> (hyps Lazy.t -> form -> form)
-> hyps
-> hyps option
val can_unfold : EcIdent.t -> hyps -> bool
val unfold : EcIdent.t -> hyps -> form
val fresh_id : hyps -> symbol -> EcIdent.t
val fresh_ids : hyps -> symbol list -> EcIdent.t list
val clear : ?leniant:bool -> EcIdent.Sid.t -> hyps -> hyps
val push_all : memenv list -> hyps -> hyps
val push_active : memenv -> hyps -> hyps
val hoareF : xpath -> hyps -> hyps * hyps
val equivF : xpath -> xpath -> hyps -> hyps * hyps
val inv_memenv : hyps -> hyps
val inv_memenv1 : hyps -> hyps
end
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...