(* standard prefix *) open HolKernel boolLib Parse infix THEN THENL THENC |-> ## open bossLib simpLib boolSimps val SPECIFICATION = pred_setTheory.SPECIFICATION val GSPECIFICATION = pred_setTheory.GSPECIFICATION val PRED_SET_ss = pred_setSimps.PRED_SET_ss local open TNet_typesTheory containerTheory in end; (* containerTheory provides the LIST_TO_SET constant *) val _ = new_theory "TNet_oks"; (* interpret netmasks as the number of one bits *) (* netmask_ok is probably unnecessary as NETMASK 33+ is equivalent in masking behaviour to NETMASK 32 *) val netmask_ok_def = Define `netmask_ok (NETMASK n) = n <= 32`; val num_of_mask_def = Define `num_of_mask (NETMASK n) = ((2 EXP 32 - 1) DIV (2 EXP (32 - n))) * 2 EXP (32 - n)`; val mask_def = Define `mask (NETMASK m) (ip n) = ip ((n DIV (2 EXP (32 - m))) * 2 EXP (32 - m))`; val LOOPBACK_def = Define `LOOPBACK = { i | mask (NETMASK 8) i = mask (NETMASK 8) (ip (127 * 2 EXP 24)) }`; val MULTICAST_def = Define `MULTICAST = { i | mask (NETMASK 4) i = mask (NETMASK 4) (ip (224 * 2 EXP 24)) }`; val BADCLASS_def = Define `BADCLASS = { i | mask (NETMASK 4) i = mask (NETMASK 4) (ip (240 * 2 EXP 24)) }`; val ZERONET_def = Define `ZERONET = { i | mask (NETMASK 8) i = mask (NETMASK 8) (ip 0) }`; val MARTIAN_def = Define `MARTIAN = MULTICAST UNION BADCLASS UNION ZERONET`; val div_fact = prove( ``!x y z. 0 < y ==> ((x * y = z) = (z MOD y = 0) /\ (z DIV y = x))``, REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ MATCH_MP_TAC arithmeticTheory.MOD_UNIQUE THEN PROVE_TAC [arithmeticTheory.ADD_CLAUSES], MATCH_MP_TAC arithmeticTheory.DIV_UNIQUE THEN PROVE_TAC [arithmeticTheory.ADD_CLAUSES], IMP_RES_THEN (ASSUME_TAC o SPEC ``z:num``) arithmeticTheory.DIVISION THEN REPEAT (FIRST_X_ASSUM (SUBST_ALL_TAC o SYM o assert (is_var o rhs o concl))) THEN FIRST_X_ASSUM (SUBST_ALL_TAC o assert (not o is_var o lhs o concl)) THEN PROVE_TAC [arithmeticTheory.ADD_CLAUSES] ]); val LOOPBACK_MARTIAN_DISJOINT = store_thm( "LOOPBACK_MARTIAN_DISJOINT", ``DISJOINT LOOPBACK MARTIAN``, SRW_TAC [PRED_SET_ss][ LOOPBACK_def, MARTIAN_def, pred_setTheory.IN_DISJOINT, GSPECIFICATION, MULTICAST_def, BADCLASS_def, ZERONET_def] THEN Cases_on `x` THEN SRW_TAC [][mask_def] THEN SIMP_TAC std_ss [div_fact] THEN REWRITE_TAC [GSYM IMP_DISJ_THM] THEN DISCH_THEN (ASSUME_TAC o SYM) THEN ASM_SIMP_TAC std_ss [] THEN SUBST_ALL_TAC (SIMP_PROVE std_ss [] ``268435456n = 16777216 * 16``) THEN SIMP_TAC bool_ss [DECIDE ``0 < 16n /\ 0n < 16777216``, GSYM arithmeticTheory.DIV_DIV_DIV_MULT] THEN ASM_SIMP_TAC std_ss []); val body_ips_def = Define `(body_ips (UDP _) = {}) /\ (body_ips (ICMP_HOST_UNREACH(i1,ps1,i2,ps2)) = {i1; i2}) /\ (body_ips (ICMP_PORT_UNREACH(i1,ps1,i2,ps2)) = {i1; i2})`; val martian_def = Define `martian m = ~DISJOINT ({m.src; m.dest} UNION body_ips m.body) MARTIAN`; val loopback_def = Define `loopback m = ~DISJOINT ({m.src; m.dest} UNION body_ips m.body) LOOPBACK`; val localhost_def = Define `localhost = ip (127 * 2 EXP 24 + 1)`; val localhost_IN_LOOPBACK = store_thm( "localhost_IN_LOOPBACK", ``localhost IN LOOPBACK``, RW_TAC arith_ss [localhost_def, LOOPBACK_def, pred_setTheory.GSPECIFICATION, mask_def]); val ifd_set_ok_def = Define `ifd_set_ok ifdset = (* UDP calculus 2.3.24 *) FINITE ifdset /\ (!x y. x IN ifdset /\ y IN ifdset /\ (x.ifid = y.ifid) ==> (x = y)) /\ (!x. x IN ifdset ==> x.primary IN x.ipset) /\ (!x. x IN ifdset ==> !i j. i IN x.ipset /\ j IN x.ipset ==> (mask x.netmask i = mask x.netmask j)) /\ (!x y. x IN ifdset /\ y IN ifdset /\ (x <> y) ==> DISJOINT x.ipset y.ipset) /\ (?!x. x IN ifdset /\ (x.ipset = LOOPBACK) /\ (x.primary = localhost) /\ (x.netmask = NETMASK 24)) /\ (?x. x IN ifdset /\ DISJOINT x.ipset LOOPBACK) /\ (!x. x IN ifdset ==> DISJOINT x.ipset MARTIAN)`; val in_ifds_def = Define `in_ifds i ifds = ?x. x IN ifds /\ i IN x.ipset`; val _ = overload_on("IN", ``in_ifds``); val not_in_ifds_def = Define `not_in_ifds i ifds = ~(in_ifds i ifds)`; val _ = overload_on("NOTIN", ``not_in_ifds``); val UDPpayloadMax_def = Define`UDPpayloadMax = 65507n`; (* n suffix on number forces natural number type *) val msg_ok_def = Define `msg_ok m = case m.body of UDP(ps1, ps2, data) -> string_size data <= UDPpayloadMax || x -> T`; val msg_oq_ok_def = Define `(* UDP Calculus 2.1.1, p8 *) msg_oq_ok m = msg_ok m /\ m.src NOTIN MARTIAN /\ (!i3 ps1 i4 ps2. (m.body = ICMP_PORT_UNREACH(i3, ps1, i4, ps2)) ==> DISJOINT {i3; i4} MARTIAN) /\ (!i3 ps1 i4 ps2. m.body <> ICMP_HOST_UNREACH(i3, ps1, i4, ps2))`; val socket_srcdest_ok_def = Define` (* UDP Calculus 2.1.4 *) socket_srcdest_ok (ifds : ifd -> bool) (is1 : ip option, ps1 : port option, is2 : ip option, ps2 : port option) = ((is1 = NONE) /\ (ps1 = NONE) /\ (is2 = NONE) /\ (ps2 = NONE)) \/ (?p1. (is1 = NONE) /\ (ps1 = SOME p1) /\ (is2 = NONE) /\ (ps2 = NONE)) \/ (?i1 p1. (is1 = SOME i1) /\ i1 IN ifds /\ (ps1 = SOME p1) /\ (is2 = NONE) /\ (ps2 = NONE)) \/ (?i1 p1 i2. (* merge two cases of the text's *) (is1 = SOME i1) /\ i1 IN ifds /\ (ps1 = SOME p1) /\ (is2 = SOME i2))`; val socket_ok_def = Define` (* UDP Calculus 2.1.4 *) socket_ok ifds (s:socket) = socket_srcdest_ok ifds (s.is1, s.ps1, s.is2, s.ps2) /\ (!m ifid. MEM (m,ifid) s.mq ==> msg_ok m /\ ~martian m) /\ ((s.is1 = NONE) /\ (s.ps1 = NONE) /\ (s.is2 = NONE) /\ (s.ps2 = NONE) ==> (s.mq = []) /\ (s.es = NONE))`; val sockfds_def = Define`sockfds sl = { f | MEM f (MAP socket_fd sl)}` val sockfds_thm = store_thm( "sockfds_thm", ``(sockfds [] = {}) /\ (!s ss. sockfds (s::ss) = s.fd INSERT sockfds ss) /\ (!ss1 ss2. sockfds (APPEND ss1 ss2) = sockfds ss1 UNION sockfds ss2)``, SRW_TAC [] [sockfds_def, pred_setTheory.EXTENSION, pred_setTheory.GSPECIFICATION, pred_setTheory.NOT_IN_EMPTY, pred_setTheory.IN_INSERT, pred_setTheory.IN_UNION ]); val sock_with_fd_def = Define` sock_with_fd fd (s::ss) = if s.fd = fd then s else sock_with_fd fd ss`; (* value of function underdetermined if socket doesn't exist with given fd *) val host_ok_def = Define` (* UDP Calculus 2.1.2, p10 *) host_ok (h : host) = ifd_set_ok h.ifds /\ (!v tid d. FDOM h.ts tid /\ (FAPPLY h.ts tid = Timed(Ret v,d)) ==> ?ty. tlang_typing v (TLty_err ty)) /\ (* *** above is new to the HOL formalisation *** *) EVERY (socket_ok h.ifds) h.s /\ (!oq d. (h.oq = Timed(oq,d)) ==> (EVERY msg_oq_ok oq /\ ((oq = []) ==> (h.oqf = F)))) /\ (!fd tid d ips is1 ps1 is2 ps2 data. FDOM h.ts tid /\ (FAPPLY h.ts tid = Timed(Sendto2(fd, ips, is1, ps1, is2, ps2, data),d)) ==> fd IN (sockfds h.s) /\ ((sock_with_fd fd h.s).ps1 <> NONE) /\ (ps1 <> NONE) /\ socket_srcdest_ok h.ifds (is1,ps1,is2,ps2) /\ ((ips <> NONE) \/ (is2 <> NONE))) /\ (!fd tid d. FDOM h.ts tid /\ (FAPPLY h.ts tid = Timed(Recvfrom2 fd,d)) ==> fd IN (sockfds h.s) /\ ((sock_with_fd fd h.s).ps1 <> NONE)) /\ (!tid rseq wseq d. FDOM h.ts tid /\ (FAPPLY h.ts tid = Timed(Select2(rseq, wseq),d)) ==> (LIST_TO_SET (APPEND rseq wseq)) SUBSET (sockfds h.s) /\ (time_zero <= d)) (* this constraint really should be lifted out now - we should have that all timers are within the appropriate range *) /\ (CARD (sockfds h.s) = LENGTH (MAP socket_fd h.s))` handle e => Raise e; (* last condition perhaps not the best way of expressing unique-ness *) (* of socket fds, but prefer it to way in text, which requires *) (* quantification over four variables. CARD well-defined as sockfds *) (* always finite *) open simpLib pred_setTheory (* next two lemmas should be in standard distribution *) val GSPEC_OR = prove( ``!P Q. {f x | P x \/ Q x} = {f x | P x} UNION {f x | Q x}``, RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_UNION] THEN PROVE_TAC []); val GSPEC_SING = prove( ``!y. ({ f x | x = y } = {f y}) /\ ({ f x | y = x} = {f y})``, RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_INSERT, NOT_IN_EMPTY] THEN PROVE_TAC []); val sockfds_FINITE = store_thm( "sockfds_FINITE", ``!sl. FINITE (sockfds sl)``, Induct THENL [ RW_TAC list_ss [FINITE_WEAK_ENUMERATE, sockfds_def, GSPECIFICATION] THEN intLib.COOPER_TAC, FULL_SIMP_TAC list_ss [sockfds_def, GSPEC_OR, FINITE_UNION, GSPEC_SING, FINITE_SING] ]); val _ = export_theory();