fact: Definition GuardSpec : ADT GuardSig := Eval simpl in Def ADT { rep := QueryStructure GuardDataSchema, Def Constructor0 "Init" : rep := empty,, Def Method1 "ProcessPacket" (db : rep) (bs : bytes) : rep * bool := Ifopt ipv4_decode bs as hdr Then let src_addr := ipv4ToString hdr.(SourceAddress) in let dst_addr := ipv4ToString hdr.(DestAddress) in Ifopt tcp_decode hdr bs as pkt Then let src_port := port_to_nat (pkt.(SourcePort)) in let dst_port := port_to_nat (pkt.(DestPort)) in count <- Count (For (conn in db!"connections") Where (conn!"src_addr" = src_addr) Where (conn!"dst_addr" = dst_addr) Return ()); If is_conn_end pkt Then ( `(db, _) <- Delete conn from db!"connections" where (conn!"src_addr" = src_addr /\ conn!"dst_addr" = dst_addr /\ conn!"src_port" = src_port /\ conn!"dst_port" = dst_port); ret (db, ACCEPT) ) Else If count <? MAX_OPEN_CONNECTIONS Then ( If is_conn_start pkt Then ( `(db, _) <- Insert <"src_addr" :: src_addr, "src_port" :: src_port, "dst_addr" :: dst_addr, "dst_port" :: dst_port> into db!"connections"; ret (db, ACCEPT) ) Else ret (db, ACCEPT) ) Else ret (db, REJECT) Else ret (db, REJECT) Else ret (db, REJECT) }%methDefParsing.
imports: Fiat.QueryStructure.Automation.MasterPlan Fiat.Narcissus.Examples.NetworkStack.IPv4Header Fiat.Narcissus.Examples.NetworkStack.TCP_Packet Fiat.Narcissus.Formats.ByteBuffer Bedrock.Word Fiat.Narcissus.BinLib.Core