Changeset 18316


Ignore:
Timestamp:
03/01/09 10:36:36 (5 years ago)
Author:
hritcu
Message:

Supporting dependent zero-knowledge proof types (Ticket #84)

Location:
src/typechecker
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/typechecker/alpha.ml

    r18238 r18316  
    8181                String_set.empty else 
    8282                String_set.singleton s 
    83                 (* we need to treat all zeroary function symbols we add to spass  differenlty here*) 
     83                (* we need to treat all zeroary function symbols we add to spass  differently here*) 
    8484        | S_Symbol _ -> String_set.empty 
    8585 
     
    9090                (String_set.union (free_type t1) (String_set.remove x (free_type t2)))            
    9191        | TZKProof(_, _, _, yts, xts, c) | TStm (yts, xts, c) -> 
     92                (* this is not perfect but works (we don't enforce the ordering) *) 
    9293                let free_yts = List.fold_left (fun a (y,t) -> String_set.union a (free_type t)) String_set.empty yts in 
    9394                let free_xts = List.fold_left (fun a (x,t) -> String_set.union a (free_type t)) String_set.empty xts in 
    94                 let free_ts = String_set.union free_yts free_xts in 
     95                let ys = List.map (fun (y,_) -> y) yts in 
     96                let xs = List.map (fun (x,_) -> x) xts in 
     97                let free_ts = String_set.diff (String_set.union free_yts free_xts) (list2set (xs @ ys)) in 
    9598                let xys = String_set.union (list2set (List.map (fun (y,t) -> y) yts)) (list2set (List.map (fun (y,t) -> y) xts)) in (* Alternative: list2set (match List.split yts with ys, _ -> ys) *)   
    9699                let free_c = String_set.diff (free_spass c) xys in  
  • src/typechecker/environment.ml

    r18069 r18316  
    5353        [] -> true 
    5454        | EBind(u, t) :: r ->  
    55                 let free = String_set.elements (free_type t) in 
    5655                let a = well_formed' (EBind(u,t) :: top) r in 
    5756                let b = not (String_set.mem u (dom (top @ r))) in 
    5857                if not b then (Logmanager.log (Printf.sprintf "Duplicate binding %s:\n" u) ~loglevel:3) else (); 
    59                 let c = subset free (String_set.elements (dom (top @ r))) in 
    60                 if not c then (Logmanager.log (Printf.sprintf "Missing binding in %s:$t\n" u) ~types:[t]  ~loglevel:3) else (); 
     58                let c = String_set.subset (free_type t) (dom (top @ r)) in 
     59                if not c then  
     60                        (let unbound = String_set.diff (free_type t) (dom (top @ r)) in 
     61                        let s =  String_set.fold (fun x a -> x ^ ", " ^ a) unbound "" in 
     62                        Logmanager.log (Printf.sprintf "Well-type: ill-formed type $t ... \n ... contains free variables: %s:\n" s) ~types:[t] ~loglevel:1) 
     63                else (); 
    6164                a && b && c 
    6265 
     
    7477                        (let unbound = String_set.diff (free_type t) (dom gamma) in 
    7578                        let s =  String_set.fold (fun x a -> x ^ ", " ^ a) unbound "" in 
    76                         Logmanager.log (Printf.sprintf "Well-type: ill-formed type $t ... \n ... contains free variables: %s:\n" s) ~types:[t] ~loglevel:3; 
     79                        Logmanager.log (Printf.sprintf "Well-type: ill-formed type $t ... \n ... contains free variables: %s:\n" s) ~types:[t] ~loglevel:1; 
    7780                        false)) 
    7881        else  
    79                 (Logmanager.log (Printf.sprintf "Well-type: ill-formed environment\n") ~loglevel:3; 
     82                (Logmanager.log (Printf.sprintf "Well-type: ill-formed environment\n") ~loglevel:1; 
    8083                false) 
  • src/typechecker/parser.mly

    r18235 r18316  
    2727(* Warning: some of these functions are similar to gen_pairs in typeterm.ml *) 
    2828 
    29 (* : ((Syntax.term, Syntax.term) list -> Syntax.term -> Syntax.term) *) 
     29(* : ((Syntax.term, string) list -> Syntax.term -> Syntax.term) *) 
    3030let gen_pairs named_terms oktoken = 
    3131        List.fold_right (fun (t1, x) t -> Pair(t1, Some x, t, None)) named_terms oktoken 
  • src/typechecker/typeprocess.ml

    r18235 r18316  
    5757        | _ -> raise (Invalid_argument "typeprocess.ml(env): unmatched case") 
    5858 
    59 let rec ver_result_type'' yts' xts c' = 
     59(* This is a real mess, should be simplified *)  
     60let rec ver_result_type'' l n_list yts yts' xts c' = 
    6061        let xs = List.map (fun (x,_) -> Spasssyntax.S_Symbol(Spasssyntax.S_Sym_Ident(x))) xts in 
    6162        match yts' with 
    6263                | [] -> TRefine(get_fresh_name_now "dummy", TUn, Spasssyntax.S_Term(Spasssyntax.S_Exists, xs ,c')) 
    63                 | (y,t):: yts'' -> TPair(y, t, ver_result_type'' yts'' xts c') 
    64  
    65 let rec ver_result_type' l yts xts c' = 
    66         match yts, l with 
    67         _, 0 -> ver_result_type'' yts xts c' 
    68         | (y,t)::yts', i -> ver_result_type' (l - 1) yts' xts c' 
     64                | (y,t):: yts'' -> 
     65                        let t' =  List.fold_left2 (fun tt n (y,_) -> replace_type y n tt) t n_list (sub_list yts 0 l) in 
     66                                TPair(y, t', ver_result_type'' l n_list yts yts'' xts c') 
     67 
     68let rec ver_result_type' l l' n_list yts yts' xts c' = 
     69        match yts', l' with 
     70        _, 0 -> ver_result_type'' l n_list yts yts' xts c' 
     71        | (y,t)::yts'', i -> ver_result_type' l (l' - 1) n_list yts yts'' xts c' 
    6972        | _ -> raise (Invalid_argument "ver_result_type': too few matched values compared to declared number") 
    7073 
    7174let ver_result_type l n_list yts xts c =  
    7275        let c' = List.fold_left2 (fun cc n (y,_) -> replace_formula y n cc) c n_list (sub_list yts 0 l) in 
    73         ver_result_type' l yts xts c' 
     76        ver_result_type' l l n_list yts yts xts c' 
    7477 
    7578 
     
    117120        let fresh_name = get_fresh_name x (dom f) in 
    118121        if verify_statement bigs f a b c s yus yts xts strong_c then 
    119                 if List.fold_left2 (fun a b (y,t) -> a && alg_check b t f) true l (sub_list yts 0 c) then 
     122(*      (non-dependent zk type case)    if List.fold_left2 (fun a b (y,t) -> a && alg_check b t f) true l (sub_list yts 0 c) then *) 
     123                if alg_check (gen_full_annot_pair l (sub_list yts 0 c) (Constr(Ok, None))) (gen_pair_type_with_c (sub_list yts 0 c) TUn) f then 
    120124                        type_process (rename_process x fresh_name p1) (EBind(fresh_name, ver_result_type c l yts xts strong_c) :: f) && 
    121125                        (match o with Some p2 -> type_process p2 f | None -> true) 
  • src/typechecker/typeterm.ml

    r18235 r18316  
    2929exception Termtyping of string 
    3030 
     31let get_annot m = match m with 
     32        | Ident(_,ot) -> ot 
     33        | Pair(_,_,_,ot) -> ot 
     34        | Constr(_,ot) -> ot   
     35 
     36let set_annot m t = match m with 
     37        | Ident(x, None) -> Ident(x, Some t) 
     38        | Ident(x, Some t1) -> Ident(x, Some (TAnd(t, t1))) 
     39        | Pair(m1, ox, m2, None) -> Pair(m1, ox, m2, Some t) 
     40        | Pair(m1, ox, m2, Some t1) -> Pair(m1, ox, m2, Some (TAnd(t, t1))) 
     41        | Constr(c, None) -> Constr(c, Some t) 
     42        | Constr(c, Some t1) -> Constr(c, Some (TAnd(t, t1))) 
     43 
     44(* 
     45let rec gen_simple_pair terms = 
     46        match terms with 
     47                | [] -> (Constr(Ok, None)) 
     48                | t1::ts -> Pair(t1, None, gen_simple_pair ts, None) 
     49*) 
     50 
     51(* 
     52let rec gen_annot_pair terms vars oktoken = 
     53        match terms, vars with 
     54                | [], [] -> oktoken 
     55                | t1::ts, v1::vs -> Pair(t1, Some v1, gen_annot_pair ts vs oktoken, None) 
     56*) 
     57 
     58let rec gen_full_annot_pair ms yts oktoken = 
     59        match ms, yts with 
     60                | [], [] -> oktoken 
     61                | m1::ms', (y1,t1)::yts' -> Pair(set_annot m1 t1, Some y1, gen_full_annot_pair ms' yts' oktoken, None) 
     62 
     63let rec gen_pair_type_with_c yts oktype = 
     64        match yts with 
     65                | [] -> oktype 
     66                | (y,t)::yts' -> TPair(y, t, gen_pair_type_with_c yts' oktype)  
     67 
     68 
    3169let name_counter = ref 1 
    3270 
    3371let gen_name base = let x = base ^ (string_of_int !name_counter) in 
    3472        incr name_counter; x 
    35  
    36 (* 
    37 let rec gen_exists' n = match n with 
    38         0 -> [] 
    39         | _ -> Spasssyntax.S_Symbol(Spasssyntax.S_Sym_Ident(get_fresh_name "x" String_set.empty)) :: gen_exists' (n - 1) 
    40  
    41 let gen_exists n = Spasssyntax.S_Term(Spasssyntax.S_Exists, List.rev(gen_exists' n), Spasssyntax.S_Symbol(Spasssyntax.S_True)) 
    42 *) 
    4373 
    4474(* Used for the result type of the public destructor *) 
     
    118148                raise (Termtyping "Environment not well-formed"))) 
    119149 
    120  
    121 and get_annot m = match m with 
    122         | Ident(_,ot) -> ot 
    123         | Pair(_,_,_,ot) -> ot 
    124         | Constr(_,ot) -> ot   
    125150 
    126151and alg_pair m ox n f = 
     
    152177        let m_list = sub_list ml 0 a in 
    153178        let n_list = sub_list ml a b in 
     179(* (non-dependent zk type case) 
    154180        List.iter2 (fun a (_,t) -> let _ = alg_check a t f in ()) m_list; 
    155181        let c'' = List.fold_left2 (fun c'' (x,_) m -> replace_formula x m c'') c' xts m_list in 
     
    157183                (let c''' = try List.fold_left2 (fun c n (y,_) -> replace_formula y n c) c'' n_list yts with Invalid_argument _ -> raise (Invalid_argument "typeterm: alg_zk c''' fold_left2") in 
    158184                add_proof_obligation f (formulas f) c'''; 
    159                 TZKProof(a, b, s, yts, xts, c')) 
    160         else raise (Invalid_argument "alg_zk: alg_check failed for the n's") 
     185*) 
     186        let tr = (TRefine(get_fresh_name_now "anon", TUn, c')) in 
     187        if alg_check (gen_full_annot_pair (n_list @ m_list) (yts @ xts) (Constr(Ok, Some tr))) (gen_pair_type_with_c (yts @ xts) tr) f then              
     188                TZKProof(a, b, s, yts, xts, c') 
     189        else raise (Invalid_argument "alg_zk: alg_check could not typecheck the witnesses") 
    161190                 
    162191         
Note: See TracChangeset for help on using the changeset viewer.