(* A HOL98 Kananaskis-0 rendering of the UDP calculus *) (* standard prefix *) open HolKernel boolLib Parse infix THEN THENC |-> ## open bossLib local open arithmeticTheory stringTheory pred_setTheory integerTheory finite_mapTheory realTheory in end; val _ = new_theory "TNet_types"; (* -------------------------------------------------- *) (* UDP/IP *) (* -------------------------------------------------- *) val _ = Hol_datatype `port = Port of num`; (* really 16 bits *) val _ = Hol_datatype `ip = ip of num`; (* really 32 bits *) val _ = Hol_datatype `ipBody = UDP of (port option # port option # string) | ICMP_HOST_UNREACH of (ip # port option # ip # port option) | ICMP_PORT_UNREACH of (ip # port option # ip # port option)`; val _ = Hol_datatype `msg = <| src : ip; dest : ip; body : ipBody |>`; val IP_def = Define ` IP (src,dest,body) = <| src := src; dest := dest; body := body |>`; val _ = Hol_datatype `ifid = LO | ETH of num`; val _ = Hol_datatype `netmask = NETMASK of num`; val _ = Hol_datatype `ifd = <| ifid : ifid ; ipset : ip -> bool ; primary : ip ; netmask : netmask |>`; val _ = Hol_datatype `fd = FD of int`; (* -------------------------------------------------- *) (* SOCKETS *) (* -------------------------------------------------- *) val _ = Hol_datatype `error = EACCES | EADDRINUSE | EADDRNOTAVAIL | EAGAIN | EBADF | ECONNREFUSED | EHOSTUNREACH | EINTR | EINVAL | EMFILE | EMSGSIZE | ENFILE | ENOBUFS | ENOMEM | ENOTCONN | ENOTSOCK`; val _ = Hol_datatype `err = OK of 'a | FAIL of error`; val _ = Hol_datatype `sockopt = SO_BSDCOMPAT | SO_REUSEADDR`; val _ = Hol_datatype `flags = <| bsdcompat : bool ; reuseaddr : bool |>`; val Flags_def = xDefine "Flags" ` Flags(bsdcompat,reuseaddr) = <| bsdcompat := bsdcompat; reuseaddr := reuseaddr |>`; val _ = Hol_datatype `socket = <| fd : fd ; is1 : ip option ; ps1 : port option; is2 : ip option ; ps2 : port option; es : error option; f : flags; mq : (msg # ifid) list |>`; val Sock_def = xDefine "Sock" ` Sock(fd,is1,ps1,is2,ps2,es,f,mq) = <| fd := fd; is1 := is1; ps1 := ps1; is2 := is2; ps2 := ps2; es := es; f := f; mq := mq |>`; val _ = Hol_datatype `exn = EX_udp of error | EX_match_failure of (string # num # num)`; val _ = Hol_datatype `except = EOK of 'a | EEX of exn`; (* -------------------------------------------------- *) (* LANGUAGE TYPES *) (* -------------------------------------------------- *) (* thread ids *) val _ = Hol_datatype `tid = TID of num`; (* or do we want names? *) val _ = Hol_datatype `TLang_type = TLty_int | TLty_bool | TLty_string | TLty_one | TLty_pair of (TLang_type # TLang_type) | TLty_list of TLang_type | TLty_lift of TLang_type | TLty_err of TLang_type | TLty_fd | TLty_ip | TLty_port | TLty_error | TLty_netmask | TLty_ifid | TLty_sockopt | TLty_tid | TLty_void | TLty_ref of TLang_type | TLty_exn | TLty_except of TLang_type`; val _ = Hol_datatype `location = Loc of TLang_type # num `; val _ = Hol_datatype `TLang = TL_int of int | TL_bool of bool | TL_string of string | TL_one of one | TL_pair of TLang # TLang | TL_list of TLang list | TL_option of TLang option | TL_err of TLang err | TL_fd of fd | TL_ip of ip | TL_port of port | TL_error of error | TL_netmask of netmask | TL_ifid of ifid | TL_sockopt of sockopt | TL_tid of tid | TL_ref of location | TL_exn of exn | TL_except of TLang except`; (* why do we have TLty_lift but TL_option ? *) val (TLang_typing_rules,TLang_typing_ind,TLang_typing_cases) = IndDefLib.Hol_reln` (!i. tlang_typing (TL_int i) TLty_int) /\ (!b. tlang_typing (TL_bool b) TLty_bool) /\ (!s. tlang_typing (TL_string s) TLty_string) /\ tlang_typing (TL_one one) TLty_one /\ (!p1 p2 ty1 ty2. tlang_typing p1 ty1 /\ tlang_typing p2 ty2 ==> tlang_typing (TL_pair(p1,p2)) (TLty_pair(ty1,ty2))) /\ (!tl ty. (!e. MEM e tl ==> tlang_typing e ty) ==> tlang_typing (TL_list tl) (TLty_list ty)) /\ (!p ty. tlang_typing p ty ==> tlang_typing (TL_option (SOME p)) (TLty_lift ty)) /\ (!ty. tlang_typing (TL_option NONE) (TLty_lift ty)) /\ (!e ty. tlang_typing (TL_err (FAIL e)) (TLty_err ty)) /\ (!p ty. tlang_typing p ty ==> tlang_typing (TL_err (OK p)) (TLty_err ty)) /\ (!fd. tlang_typing (TL_fd fd) TLty_fd) /\ (!i. tlang_typing (TL_ip i) TLty_ip) /\ (!p. tlang_typing (TL_port p) TLty_port) /\ (!e. tlang_typing (TL_error e) TLty_error) /\ (!nm. tlang_typing (TL_netmask nm) TLty_netmask) /\ (!ifid. tlang_typing (TL_ifid ifid) TLty_ifid) /\ (!s. tlang_typing (TL_sockopt s) TLty_sockopt) /\ (!tid. tlang_typing (TL_tid tid) TLty_tid) /\ (!l ty. tlang_typing (TL_ref (Loc (ty,l))) (TLty_ref ty)) /\ (!ex. tlang_typing (TL_exn ex) TLty_exn ) /\ (!p ty. tlang_typing p ty ==> tlang_typing (TL_except (EOK p)) (TLty_except ty)) /\ (!ex ty. tlang_typing (TL_exn ex) TLty_exn ==> tlang_typing (TL_except (EEX ex)) (TLty_except ty))`; val TLang_typing_thm = let open simpLib fun app_letter ty ctxt = let open Lexis val tyopname = #1 (dest_type ty) handle HOL_ERR _ => (* if a vartype *) dest_vartype ty val letter = gen_variant tmvar_vary ctxt (String.substring(tyopname, 0, 1)) in (letter::ctxt, mk_var(letter, ty)) end fun gen_case constr = let val cty = type_of constr val (argtys, _) = strip_fun cty val (_ (* varnames used *), args) = stmonad.mmap app_letter argtys [] val tm = list_mk_comb(constr, args) in GEN_ALL (CONV_RULE (SIMP_CONV (BasicProvers.get_srw_ss()) []) (SPEC tm TLang_typing_cases)) end in save_thm("TLang_typing_thm", LIST_CONJ (map gen_case (TypeBase.constructors_of "TLang"))) end (* -------------------------------------------------- *) (* OK AND FAIL *) (* -------------------------------------------------- *) val OK'_def = xDefine "OK'" `OK' v = TL_err (OK v)`; val FAIL'_def = xDefine "FAIL'" `FAIL' e = TL_err (FAIL e)`; val _ = overload_on("FAIL", ``FAIL'``); val OK'_int_def = Define `OK'_int v = OK' (TL_int v)`; val OK'_bool_def = Define `OK'_bool v = OK' (TL_bool v)`; val OK'_string_def = Define `OK'_string v = OK' (TL_string v)`; val OK'_one_def = Define `OK'_one v = OK' (TL_one v)`; val OK'_pair_def = Define `OK'_pair v = OK' (TL_pair v)`; val OK'_list_def = Define `OK'_list v = OK' (TL_list v)`; val OK'_option_def = Define `OK'_option v = OK' (TL_option v)`; val OK'_err_def = Define `OK'_err v = OK' (TL_err v)`; val OK'_fd_def = Define `OK'_fd v = OK' (TL_fd v)`; val OK'_ip_def = Define `OK'_ip v = OK' (TL_ip v)`; val OK'_port_def = Define `OK'_port v = OK' (TL_port v)`; val OK'_error_def = Define `OK'_error v = OK' (TL_error v)`; val OK'_netmask_def = Define `OK'_netmask v = OK' (TL_netmask v)`; val OK'_ifid_def = Define `OK'_ifid v = OK' (TL_ifid v)`; val OK'_sockopt_def = Define `OK'_sockopt v = OK' (TL_sockopt v)`; val OK'_tid_def = Define `OK'_tid v = OK' (TL_tid v)`; val OK'_ipportlift_def = Define `OK'_ipportlift (is1,ps1) = OK'_pair (TL_option (OPTION_MAP TL_ip is1), TL_option (OPTION_MAP TL_port ps1))`; val OK'_errorlift_def = Define `OK'_errorlift e = OK'_option (OPTION_MAP TL_error e)`; val OK'_msglift_def = Define `OK'_msglift (i1,ps1,data) = TL_err (OK(TL_pair(TL_ip i1, TL_pair(TL_option (OPTION_MAP TL_port ps1), TL_string data))))`; val OK'_fdlistpair_def = Define`OK'_fdlistpair (fdl1, fdl2) = TL_err (OK(TL_pair(TL_list (MAP TL_fd fdl1), TL_list (MAP TL_fd fdl2))))`; val OK'_getifaddrs_ret_def = Define` OK'_getifaddrs_ret retlist = TL_err (OK(TL_list (MAP (\ (ifid, i, ipl, nm). TL_pair(TL_ifid ifid, TL_pair(TL_ip i, TL_pair(TL_list (MAP TL_ip ipl), TL_netmask nm)))) retlist)))`; val _ = overload_on("OK", ``OK'_int``); val _ = overload_on("OK", ``OK'_bool``); val _ = overload_on("OK", ``OK'_string``); val _ = overload_on("OK", ``OK'_one``); val _ = overload_on("OK", ``OK'_pair``); val _ = overload_on("OK", ``OK'_list``); val _ = overload_on("OK", ``OK'_option``); val _ = overload_on("OK", ``OK'_err``); val _ = overload_on("OK", ``OK'_fd``); val _ = overload_on("OK", ``OK'_ip``); val _ = overload_on("OK", ``OK'_port``); val _ = overload_on("OK", ``OK'_error``); val _ = overload_on("OK", ``OK'_netmask``); val _ = overload_on("OK", ``OK'_ifid``); val _ = overload_on("OK", ``OK'_sockopt``); val _ = overload_on("OK", ``OK'_tid``); val _ = overload_on("OK", ``OK'_ipportlift``); val _ = overload_on("OK", ``OK'_errorlift``); val _ = overload_on("OK", ``OK'_msglift``); val _ = overload_on("OK", ``OK'_fdlistpair``); val _ = overload_on("OK", ``OK'_getifaddrs_ret``); (* -------------------------------------------------- *) (* TIME *) (* -------------------------------------------------- *) (* time and duration are defined essentially as type synonyms; these aren't built into HOL so we have to use an ML definition and antiquotation. time = NONE means infinite; otherwise it must be non-negative. duration is always positive and finite. *) val time_ty = ``:real option``; val time_aty = ty_antiq time_ty; val _ = adjoin_to_theory { sig_ps = SOME (fn pps => PP.add_string pps "val time_ty : Type.hol_type\n"), struct_ps = SOME (fn pps => PP.add_string pps "val time_ty = Parse.Type`:real option`\n") } val _ = adjoin_to_theory { sig_ps = SOME (fn pps => PP.add_string pps "val time_aty : Term.term\n"), struct_ps = SOME (fn pps => PP.add_string pps "val time_aty = HolKernel.ty_antiq time_ty\n") } val duration_ty = ``:real``; val duration_aty = ty_antiq duration_ty; val _ = adjoin_to_theory { sig_ps = SOME (fn pps => PP.add_string pps "val duration_ty : Type.hol_type\n"), struct_ps = SOME (fn pps => PP.add_string pps "val duration_ty = Parse.Type`:real`\n") } val _ = adjoin_to_theory { sig_ps = SOME (fn pps => PP.add_string pps "val duration_aty : Term.term\n"), struct_ps = SOME (fn pps => PP.add_string pps "val duration_aty = HolKernel.ty_antiq duration_ty\n") } val time_lt_def = Define `((time_lt:^time_aty -> ^time_aty -> bool) (SOME x) (SOME y) = x < y) /\ (time_lt NONE ys = F) /\ (time_lt xs NONE = T)`; val time_lte_def = Define `time_lte xs ys = ((xs = ys) \/ (time_lt xs ys))`; val time_gt_def = Define `time_gt xs ys = ( (time_lt ys xs))`; val time_gte_def = Define `time_gte xs ys = ((xs = ys) \/ (time_lt ys xs))`; val _ = overload_on("<" , ``time_lt`` ); val _ = overload_on("<=", ``time_lte``); val _ = overload_on(">" , ``time_gt`` ); val _ = overload_on(">=", ``time_gte``); (* adding a duration to a time *) val time_plus_dur_def = Define` ((time_plus_dur:^time_aty -> ^duration_aty -> ^time_aty) (SOME x) y = SOME (x+y)) /\ (time_plus_dur NONE y = NONE)`; val _ = overload_on("+", ``time_plus_dur``) handle e => Raise e; (* subtracting a duration from a time *) val time_minus_dur_def = Define` ((time_minus_dur:^time_aty -> ^duration_aty -> ^time_aty) (SOME x) y = SOME (x-y)) /\ (time_minus_dur NONE y = NONE)`; val _ = overload_on("-", ``time_minus_dur``); val time_def = Define `(time : real -> ^time_aty) x = SOME x`; val time_infty_def = Define `(time_infty : ^time_aty) = NONE `; val time_zero_def = Define `(time_zero : ^time_aty) = SOME 0`; val _ = Hol_datatype `timed = Timed of 'a # ^time_ty`; (* -------------------------------------------------- *) (* HOST THREADS *) (* -------------------------------------------------- *) val _ = Hol_datatype `hostThreadState = Run | Exit | Zombie | Ret of TLang | Sendto2 of (fd # (ip # port) option # ip option # port option # ip option # port option # string) | Recvfrom2 of fd | Select2 of (fd list # fd list) | Delay2 | Print2 of string`; (* -------------------------------------------------- *) (* HOST *) (* -------------------------------------------------- *) val _ = Hol_datatype `host = <| ifds : ifd -> bool ; ts : tid |-> hostThreadState timed ; s : socket list; oq : msg list timed ; oqf : bool |>`; (* -------------------------------------------------- *) val _ = add_infix ("<>", 100, NONASSOC); val neq_def = xDefine "neq" `(x <> y) = ~(x = y)`; val _ = add_infix ("NOTIN", 450, RIGHT); val notin_def = Define `(x NOTIN s) = ~(x IN s)`; val _ = export_theory(); (* -------------------------------------------------- *)