From 973aec43ea54bbf95b64fbcb636403401d1ca60e Mon Sep 17 00:00:00 2001
From: Rutger Broekhoff
Date: Fri, 28 Aug 2026 18:03:05 +0200
Subject: Import from e4b104792206ee7ea64bf39c6b7d2c0c230f9d14
---
.dir-locals.el | 5 +
.envrc | 3 +
.gitignore | 6 +
LICENSE | 661 ++++++++++++++++++++++++++++
flake.lock | 59 +++
flake.nix | 57 +++
links.org | 4 +
server/.gitignore | 7 +
server/CMakeLists.txt | 86 ++++
server/CMakePresets.json | 29 ++
server/README | 16 +
server/ct.sh | 1 +
server/formal/.envrc | 1 +
server/formal/.gitignore | 17 +
server/formal/Makefile | 55 +++
server/formal/_CoqProject | 5 +
server/formal/flake.lock | 61 +++
server/formal/flake.nix | 26 ++
server/formal/period.v | 828 +++++++++++++++++++++++++++++++++++
server/formal/period_seq.v | 834 ++++++++++++++++++++++++++++++++++++
server/formal/util.v | 92 ++++
server/hack/rwgps-get-auth-token.sh | 14 +
server/locale/.gitignore | 1 +
server/locale/README | 9 +
server/locale/dev.sh | 7 +
server/locale/en_US.po | 64 +++
server/locale/nl.po | 64 +++
server/locale/xget.sh | 13 +
server/migrations/1_init_down.sql | 1 +
server/migrations/1_init_up.sql | 7 +
server/migrations/2_kaas_up.sql | 23 +
server/routemon.pot | 58 +++
server/src/api.cpp | 206 +++++++++
server/src/api.cppm | 79 ++++
server/src/config.cpp | 167 ++++++++
server/src/config.cppm | 39 ++
server/src/database.cppm | 37 ++
server/src/datex2.cppm | 296 +++++++++++++
server/src/geo.cppm | 40 ++
server/src/gpx.cpp | 189 ++++++++
server/src/gpx.cppm | 43 ++
server/src/http_client.cppm | 62 +++
server/src/http_common.cppm | 139 ++++++
server/src/http_server.cppm | 661 ++++++++++++++++++++++++++++
server/src/locale.cppm | 245 +++++++++++
server/src/log.cppm | 148 +++++++
server/src/main.cpp | 109 +++++
server/src/problem.cppm | 60 +++
server/src/req_ctx.cppm | 51 +++
server/src/routemon.cppm | 11 +
server/src/rwgps.cppm | 137 ++++++
server/src/sqlite3.cppm | 257 +++++++++++
server/src/srv.cppm | 221 ++++++++++
server/src/time.cppm | 205 +++++++++
server/src/trace.cppm | 79 ++++
server/src/util.cppm | 254 +++++++++++
server/src/xml.cpp | 61 +++
server/src/xml.cppm | 632 +++++++++++++++++++++++++++
web/index.html | 52 +++
web/script.js | 149 +++++++
web/style.css | 62 +++
61 files changed, 7805 insertions(+)
create mode 100644 .dir-locals.el
create mode 100644 .envrc
create mode 100644 .gitignore
create mode 100644 LICENSE
create mode 100644 flake.lock
create mode 100644 flake.nix
create mode 100644 links.org
create mode 100644 server/.gitignore
create mode 100644 server/CMakeLists.txt
create mode 100644 server/CMakePresets.json
create mode 100644 server/README
create mode 100644 server/ct.sh
create mode 100644 server/formal/.envrc
create mode 100644 server/formal/.gitignore
create mode 100644 server/formal/Makefile
create mode 100644 server/formal/_CoqProject
create mode 100644 server/formal/flake.lock
create mode 100644 server/formal/flake.nix
create mode 100644 server/formal/period.v
create mode 100644 server/formal/period_seq.v
create mode 100644 server/formal/util.v
create mode 100755 server/hack/rwgps-get-auth-token.sh
create mode 100644 server/locale/.gitignore
create mode 100644 server/locale/README
create mode 100755 server/locale/dev.sh
create mode 100644 server/locale/en_US.po
create mode 100644 server/locale/nl.po
create mode 100755 server/locale/xget.sh
create mode 100644 server/migrations/1_init_down.sql
create mode 100644 server/migrations/1_init_up.sql
create mode 100644 server/migrations/2_kaas_up.sql
create mode 100644 server/routemon.pot
create mode 100644 server/src/api.cpp
create mode 100644 server/src/api.cppm
create mode 100644 server/src/config.cpp
create mode 100644 server/src/config.cppm
create mode 100644 server/src/database.cppm
create mode 100644 server/src/datex2.cppm
create mode 100644 server/src/geo.cppm
create mode 100644 server/src/gpx.cpp
create mode 100644 server/src/gpx.cppm
create mode 100644 server/src/http_client.cppm
create mode 100644 server/src/http_common.cppm
create mode 100644 server/src/http_server.cppm
create mode 100644 server/src/locale.cppm
create mode 100644 server/src/log.cppm
create mode 100644 server/src/main.cpp
create mode 100644 server/src/problem.cppm
create mode 100644 server/src/req_ctx.cppm
create mode 100644 server/src/routemon.cppm
create mode 100644 server/src/rwgps.cppm
create mode 100644 server/src/sqlite3.cppm
create mode 100644 server/src/srv.cppm
create mode 100644 server/src/time.cppm
create mode 100644 server/src/trace.cppm
create mode 100644 server/src/util.cppm
create mode 100644 server/src/xml.cpp
create mode 100644 server/src/xml.cppm
create mode 100644 web/index.html
create mode 100644 web/script.js
create mode 100644 web/style.css
diff --git a/.dir-locals.el b/.dir-locals.el
new file mode 100644
index 0000000..ca230d6
--- /dev/null
+++ b/.dir-locals.el
@@ -0,0 +1,5 @@
+((c++-mode . ((indent-tabs-mode . nil)))
+ (css-mode . ((indent-tabs-mode . nil)))
+ (js-mode . ((indent-tabs-mode . nil)))
+ (js-json-mode . ((indent-tabs-mode . nil)))
+ (sh-mode . ((indent-tabs-mode . nil))))
diff --git a/.envrc b/.envrc
new file mode 100644
index 0000000..d031487
--- /dev/null
+++ b/.envrc
@@ -0,0 +1,3 @@
+export CC=/usr/bin/clang
+export CXX=/usr/bin/clang++
+export CMAKE_BUILD_PARALLEL_LEVEL=17
diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..f8427b5
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,6 @@
+\#*#
+*~
+.#*
+# Nix
+result
+result-*
diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000..be3f7b2
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,661 @@
+ GNU AFFERO GENERAL PUBLIC LICENSE
+ Version 3, 19 November 2007
+
+ Copyright (C) 2007 Free Software Foundation, Inc.
+ Everyone is permitted to copy and distribute verbatim copies
+ of this license document, but changing it is not allowed.
+
+ Preamble
+
+ The GNU Affero General Public License is a free, copyleft license for
+software and other kinds of works, specifically designed to ensure
+cooperation with the community in the case of network server software.
+
+ The licenses for most software and other practical works are designed
+to take away your freedom to share and change the works. By contrast,
+our General Public Licenses are intended to guarantee your freedom to
+share and change all versions of a program--to make sure it remains free
+software for all its users.
+
+ When we speak of free software, we are referring to freedom, not
+price. Our General Public Licenses are designed to make sure that you
+have the freedom to distribute copies of free software (and charge for
+them if you wish), that you receive source code or can get it if you
+want it, that you can change the software or use pieces of it in new
+free programs, and that you know you can do these things.
+
+ Developers that use our General Public Licenses protect your rights
+with two steps: (1) assert copyright on the software, and (2) offer
+you this License which gives you legal permission to copy, distribute
+and/or modify the software.
+
+ A secondary benefit of defending all users' freedom is that
+improvements made in alternate versions of the program, if they
+receive widespread use, become available for other developers to
+incorporate. Many developers of free software are heartened and
+encouraged by the resulting cooperation. However, in the case of
+software used on network servers, this result may fail to come about.
+The GNU General Public License permits making a modified version and
+letting the public access it on a server without ever releasing its
+source code to the public.
+
+ The GNU Affero General Public License is designed specifically to
+ensure that, in such cases, the modified source code becomes available
+to the community. It requires the operator of a network server to
+provide the source code of the modified version running there to the
+users of that server. Therefore, public use of a modified version, on
+a publicly accessible server, gives the public access to the source
+code of the modified version.
+
+ An older license, called the Affero General Public License and
+published by Affero, was designed to accomplish similar goals. This is
+a different license, not a version of the Affero GPL, but Affero has
+released a new version of the Affero GPL which permits relicensing under
+this license.
+
+ The precise terms and conditions for copying, distribution and
+modification follow.
+
+ TERMS AND CONDITIONS
+
+ 0. Definitions.
+
+ "This License" refers to version 3 of the GNU Affero General Public License.
+
+ "Copyright" also means copyright-like laws that apply to other kinds of
+works, such as semiconductor masks.
+
+ "The Program" refers to any copyrightable work licensed under this
+License. Each licensee is addressed as "you". "Licensees" and
+"recipients" may be individuals or organizations.
+
+ To "modify" a work means to copy from or adapt all or part of the work
+in a fashion requiring copyright permission, other than the making of an
+exact copy. The resulting work is called a "modified version" of the
+earlier work or a work "based on" the earlier work.
+
+ A "covered work" means either the unmodified Program or a work based
+on the Program.
+
+ To "propagate" a work means to do anything with it that, without
+permission, would make you directly or secondarily liable for
+infringement under applicable copyright law, except executing it on a
+computer or modifying a private copy. Propagation includes copying,
+distribution (with or without modification), making available to the
+public, and in some countries other activities as well.
+
+ To "convey" a work means any kind of propagation that enables other
+parties to make or receive copies. Mere interaction with a user through
+a computer network, with no transfer of a copy, is not conveying.
+
+ An interactive user interface displays "Appropriate Legal Notices"
+to the extent that it includes a convenient and prominently visible
+feature that (1) displays an appropriate copyright notice, and (2)
+tells the user that there is no warranty for the work (except to the
+extent that warranties are provided), that licensees may convey the
+work under this License, and how to view a copy of this License. If
+the interface presents a list of user commands or options, such as a
+menu, a prominent item in the list meets this criterion.
+
+ 1. Source Code.
+
+ The "source code" for a work means the preferred form of the work
+for making modifications to it. "Object code" means any non-source
+form of a work.
+
+ A "Standard Interface" means an interface that either is an official
+standard defined by a recognized standards body, or, in the case of
+interfaces specified for a particular programming language, one that
+is widely used among developers working in that language.
+
+ The "System Libraries" of an executable work include anything, other
+than the work as a whole, that (a) is included in the normal form of
+packaging a Major Component, but which is not part of that Major
+Component, and (b) serves only to enable use of the work with that
+Major Component, or to implement a Standard Interface for which an
+implementation is available to the public in source code form. A
+"Major Component", in this context, means a major essential component
+(kernel, window system, and so on) of the specific operating system
+(if any) on which the executable work runs, or a compiler used to
+produce the work, or an object code interpreter used to run it.
+
+ The "Corresponding Source" for a work in object code form means all
+the source code needed to generate, install, and (for an executable
+work) run the object code and to modify the work, including scripts to
+control those activities. However, it does not include the work's
+System Libraries, or general-purpose tools or generally available free
+programs which are used unmodified in performing those activities but
+which are not part of the work. For example, Corresponding Source
+includes interface definition files associated with source files for
+the work, and the source code for shared libraries and dynamically
+linked subprograms that the work is specifically designed to require,
+such as by intimate data communication or control flow between those
+subprograms and other parts of the work.
+
+ The Corresponding Source need not include anything that users
+can regenerate automatically from other parts of the Corresponding
+Source.
+
+ The Corresponding Source for a work in source code form is that
+same work.
+
+ 2. Basic Permissions.
+
+ All rights granted under this License are granted for the term of
+copyright on the Program, and are irrevocable provided the stated
+conditions are met. This License explicitly affirms your unlimited
+permission to run the unmodified Program. The output from running a
+covered work is covered by this License only if the output, given its
+content, constitutes a covered work. This License acknowledges your
+rights of fair use or other equivalent, as provided by copyright law.
+
+ You may make, run and propagate covered works that you do not
+convey, without conditions so long as your license otherwise remains
+in force. You may convey covered works to others for the sole purpose
+of having them make modifications exclusively for you, or provide you
+with facilities for running those works, provided that you comply with
+the terms of this License in conveying all material for which you do
+not control copyright. Those thus making or running the covered works
+for you must do so exclusively on your behalf, under your direction
+and control, on terms that prohibit them from making any copies of
+your copyrighted material outside their relationship with you.
+
+ Conveying under any other circumstances is permitted solely under
+the conditions stated below. Sublicensing is not allowed; section 10
+makes it unnecessary.
+
+ 3. Protecting Users' Legal Rights From Anti-Circumvention Law.
+
+ No covered work shall be deemed part of an effective technological
+measure under any applicable law fulfilling obligations under article
+11 of the WIPO copyright treaty adopted on 20 December 1996, or
+similar laws prohibiting or restricting circumvention of such
+measures.
+
+ When you convey a covered work, you waive any legal power to forbid
+circumvention of technological measures to the extent such circumvention
+is effected by exercising rights under this License with respect to
+the covered work, and you disclaim any intention to limit operation or
+modification of the work as a means of enforcing, against the work's
+users, your or third parties' legal rights to forbid circumvention of
+technological measures.
+
+ 4. Conveying Verbatim Copies.
+
+ You may convey verbatim copies of the Program's source code as you
+receive it, in any medium, provided that you conspicuously and
+appropriately publish on each copy an appropriate copyright notice;
+keep intact all notices stating that this License and any
+non-permissive terms added in accord with section 7 apply to the code;
+keep intact all notices of the absence of any warranty; and give all
+recipients a copy of this License along with the Program.
+
+ You may charge any price or no price for each copy that you convey,
+and you may offer support or warranty protection for a fee.
+
+ 5. Conveying Modified Source Versions.
+
+ You may convey a work based on the Program, or the modifications to
+produce it from the Program, in the form of source code under the
+terms of section 4, provided that you also meet all of these conditions:
+
+ a) The work must carry prominent notices stating that you modified
+ it, and giving a relevant date.
+
+ b) The work must carry prominent notices stating that it is
+ released under this License and any conditions added under section
+ 7. This requirement modifies the requirement in section 4 to
+ "keep intact all notices".
+
+ c) You must license the entire work, as a whole, under this
+ License to anyone who comes into possession of a copy. This
+ License will therefore apply, along with any applicable section 7
+ additional terms, to the whole of the work, and all its parts,
+ regardless of how they are packaged. This License gives no
+ permission to license the work in any other way, but it does not
+ invalidate such permission if you have separately received it.
+
+ d) If the work has interactive user interfaces, each must display
+ Appropriate Legal Notices; however, if the Program has interactive
+ interfaces that do not display Appropriate Legal Notices, your
+ work need not make them do so.
+
+ A compilation of a covered work with other separate and independent
+works, which are not by their nature extensions of the covered work,
+and which are not combined with it such as to form a larger program,
+in or on a volume of a storage or distribution medium, is called an
+"aggregate" if the compilation and its resulting copyright are not
+used to limit the access or legal rights of the compilation's users
+beyond what the individual works permit. Inclusion of a covered work
+in an aggregate does not cause this License to apply to the other
+parts of the aggregate.
+
+ 6. Conveying Non-Source Forms.
+
+ You may convey a covered work in object code form under the terms
+of sections 4 and 5, provided that you also convey the
+machine-readable Corresponding Source under the terms of this License,
+in one of these ways:
+
+ a) Convey the object code in, or embodied in, a physical product
+ (including a physical distribution medium), accompanied by the
+ Corresponding Source fixed on a durable physical medium
+ customarily used for software interchange.
+
+ b) Convey the object code in, or embodied in, a physical product
+ (including a physical distribution medium), accompanied by a
+ written offer, valid for at least three years and valid for as
+ long as you offer spare parts or customer support for that product
+ model, to give anyone who possesses the object code either (1) a
+ copy of the Corresponding Source for all the software in the
+ product that is covered by this License, on a durable physical
+ medium customarily used for software interchange, for a price no
+ more than your reasonable cost of physically performing this
+ conveying of source, or (2) access to copy the
+ Corresponding Source from a network server at no charge.
+
+ c) Convey individual copies of the object code with a copy of the
+ written offer to provide the Corresponding Source. This
+ alternative is allowed only occasionally and noncommercially, and
+ only if you received the object code with such an offer, in accord
+ with subsection 6b.
+
+ d) Convey the object code by offering access from a designated
+ place (gratis or for a charge), and offer equivalent access to the
+ Corresponding Source in the same way through the same place at no
+ further charge. You need not require recipients to copy the
+ Corresponding Source along with the object code. If the place to
+ copy the object code is a network server, the Corresponding Source
+ may be on a different server (operated by you or a third party)
+ that supports equivalent copying facilities, provided you maintain
+ clear directions next to the object code saying where to find the
+ Corresponding Source. Regardless of what server hosts the
+ Corresponding Source, you remain obligated to ensure that it is
+ available for as long as needed to satisfy these requirements.
+
+ e) Convey the object code using peer-to-peer transmission, provided
+ you inform other peers where the object code and Corresponding
+ Source of the work are being offered to the general public at no
+ charge under subsection 6d.
+
+ A separable portion of the object code, whose source code is excluded
+from the Corresponding Source as a System Library, need not be
+included in conveying the object code work.
+
+ A "User Product" is either (1) a "consumer product", which means any
+tangible personal property which is normally used for personal, family,
+or household purposes, or (2) anything designed or sold for incorporation
+into a dwelling. In determining whether a product is a consumer product,
+doubtful cases shall be resolved in favor of coverage. For a particular
+product received by a particular user, "normally used" refers to a
+typical or common use of that class of product, regardless of the status
+of the particular user or of the way in which the particular user
+actually uses, or expects or is expected to use, the product. A product
+is a consumer product regardless of whether the product has substantial
+commercial, industrial or non-consumer uses, unless such uses represent
+the only significant mode of use of the product.
+
+ "Installation Information" for a User Product means any methods,
+procedures, authorization keys, or other information required to install
+and execute modified versions of a covered work in that User Product from
+a modified version of its Corresponding Source. The information must
+suffice to ensure that the continued functioning of the modified object
+code is in no case prevented or interfered with solely because
+modification has been made.
+
+ If you convey an object code work under this section in, or with, or
+specifically for use in, a User Product, and the conveying occurs as
+part of a transaction in which the right of possession and use of the
+User Product is transferred to the recipient in perpetuity or for a
+fixed term (regardless of how the transaction is characterized), the
+Corresponding Source conveyed under this section must be accompanied
+by the Installation Information. But this requirement does not apply
+if neither you nor any third party retains the ability to install
+modified object code on the User Product (for example, the work has
+been installed in ROM).
+
+ The requirement to provide Installation Information does not include a
+requirement to continue to provide support service, warranty, or updates
+for a work that has been modified or installed by the recipient, or for
+the User Product in which it has been modified or installed. Access to a
+network may be denied when the modification itself materially and
+adversely affects the operation of the network or violates the rules and
+protocols for communication across the network.
+
+ Corresponding Source conveyed, and Installation Information provided,
+in accord with this section must be in a format that is publicly
+documented (and with an implementation available to the public in
+source code form), and must require no special password or key for
+unpacking, reading or copying.
+
+ 7. Additional Terms.
+
+ "Additional permissions" are terms that supplement the terms of this
+License by making exceptions from one or more of its conditions.
+Additional permissions that are applicable to the entire Program shall
+be treated as though they were included in this License, to the extent
+that they are valid under applicable law. If additional permissions
+apply only to part of the Program, that part may be used separately
+under those permissions, but the entire Program remains governed by
+this License without regard to the additional permissions.
+
+ When you convey a copy of a covered work, you may at your option
+remove any additional permissions from that copy, or from any part of
+it. (Additional permissions may be written to require their own
+removal in certain cases when you modify the work.) You may place
+additional permissions on material, added by you to a covered work,
+for which you have or can give appropriate copyright permission.
+
+ Notwithstanding any other provision of this License, for material you
+add to a covered work, you may (if authorized by the copyright holders of
+that material) supplement the terms of this License with terms:
+
+ a) Disclaiming warranty or limiting liability differently from the
+ terms of sections 15 and 16 of this License; or
+
+ b) Requiring preservation of specified reasonable legal notices or
+ author attributions in that material or in the Appropriate Legal
+ Notices displayed by works containing it; or
+
+ c) Prohibiting misrepresentation of the origin of that material, or
+ requiring that modified versions of such material be marked in
+ reasonable ways as different from the original version; or
+
+ d) Limiting the use for publicity purposes of names of licensors or
+ authors of the material; or
+
+ e) Declining to grant rights under trademark law for use of some
+ trade names, trademarks, or service marks; or
+
+ f) Requiring indemnification of licensors and authors of that
+ material by anyone who conveys the material (or modified versions of
+ it) with contractual assumptions of liability to the recipient, for
+ any liability that these contractual assumptions directly impose on
+ those licensors and authors.
+
+ All other non-permissive additional terms are considered "further
+restrictions" within the meaning of section 10. If the Program as you
+received it, or any part of it, contains a notice stating that it is
+governed by this License along with a term that is a further
+restriction, you may remove that term. If a license document contains
+a further restriction but permits relicensing or conveying under this
+License, you may add to a covered work material governed by the terms
+of that license document, provided that the further restriction does
+not survive such relicensing or conveying.
+
+ If you add terms to a covered work in accord with this section, you
+must place, in the relevant source files, a statement of the
+additional terms that apply to those files, or a notice indicating
+where to find the applicable terms.
+
+ Additional terms, permissive or non-permissive, may be stated in the
+form of a separately written license, or stated as exceptions;
+the above requirements apply either way.
+
+ 8. Termination.
+
+ You may not propagate or modify a covered work except as expressly
+provided under this License. Any attempt otherwise to propagate or
+modify it is void, and will automatically terminate your rights under
+this License (including any patent licenses granted under the third
+paragraph of section 11).
+
+ However, if you cease all violation of this License, then your
+license from a particular copyright holder is reinstated (a)
+provisionally, unless and until the copyright holder explicitly and
+finally terminates your license, and (b) permanently, if the copyright
+holder fails to notify you of the violation by some reasonable means
+prior to 60 days after the cessation.
+
+ Moreover, your license from a particular copyright holder is
+reinstated permanently if the copyright holder notifies you of the
+violation by some reasonable means, this is the first time you have
+received notice of violation of this License (for any work) from that
+copyright holder, and you cure the violation prior to 30 days after
+your receipt of the notice.
+
+ Termination of your rights under this section does not terminate the
+licenses of parties who have received copies or rights from you under
+this License. If your rights have been terminated and not permanently
+reinstated, you do not qualify to receive new licenses for the same
+material under section 10.
+
+ 9. Acceptance Not Required for Having Copies.
+
+ You are not required to accept this License in order to receive or
+run a copy of the Program. Ancillary propagation of a covered work
+occurring solely as a consequence of using peer-to-peer transmission
+to receive a copy likewise does not require acceptance. However,
+nothing other than this License grants you permission to propagate or
+modify any covered work. These actions infringe copyright if you do
+not accept this License. Therefore, by modifying or propagating a
+covered work, you indicate your acceptance of this License to do so.
+
+ 10. Automatic Licensing of Downstream Recipients.
+
+ Each time you convey a covered work, the recipient automatically
+receives a license from the original licensors, to run, modify and
+propagate that work, subject to this License. You are not responsible
+for enforcing compliance by third parties with this License.
+
+ An "entity transaction" is a transaction transferring control of an
+organization, or substantially all assets of one, or subdividing an
+organization, or merging organizations. If propagation of a covered
+work results from an entity transaction, each party to that
+transaction who receives a copy of the work also receives whatever
+licenses to the work the party's predecessor in interest had or could
+give under the previous paragraph, plus a right to possession of the
+Corresponding Source of the work from the predecessor in interest, if
+the predecessor has it or can get it with reasonable efforts.
+
+ You may not impose any further restrictions on the exercise of the
+rights granted or affirmed under this License. For example, you may
+not impose a license fee, royalty, or other charge for exercise of
+rights granted under this License, and you may not initiate litigation
+(including a cross-claim or counterclaim in a lawsuit) alleging that
+any patent claim is infringed by making, using, selling, offering for
+sale, or importing the Program or any portion of it.
+
+ 11. Patents.
+
+ A "contributor" is a copyright holder who authorizes use under this
+License of the Program or a work on which the Program is based. The
+work thus licensed is called the contributor's "contributor version".
+
+ A contributor's "essential patent claims" are all patent claims
+owned or controlled by the contributor, whether already acquired or
+hereafter acquired, that would be infringed by some manner, permitted
+by this License, of making, using, or selling its contributor version,
+but do not include claims that would be infringed only as a
+consequence of further modification of the contributor version. For
+purposes of this definition, "control" includes the right to grant
+patent sublicenses in a manner consistent with the requirements of
+this License.
+
+ Each contributor grants you a non-exclusive, worldwide, royalty-free
+patent license under the contributor's essential patent claims, to
+make, use, sell, offer for sale, import and otherwise run, modify and
+propagate the contents of its contributor version.
+
+ In the following three paragraphs, a "patent license" is any express
+agreement or commitment, however denominated, not to enforce a patent
+(such as an express permission to practice a patent or covenant not to
+sue for patent infringement). To "grant" such a patent license to a
+party means to make such an agreement or commitment not to enforce a
+patent against the party.
+
+ If you convey a covered work, knowingly relying on a patent license,
+and the Corresponding Source of the work is not available for anyone
+to copy, free of charge and under the terms of this License, through a
+publicly available network server or other readily accessible means,
+then you must either (1) cause the Corresponding Source to be so
+available, or (2) arrange to deprive yourself of the benefit of the
+patent license for this particular work, or (3) arrange, in a manner
+consistent with the requirements of this License, to extend the patent
+license to downstream recipients. "Knowingly relying" means you have
+actual knowledge that, but for the patent license, your conveying the
+covered work in a country, or your recipient's use of the covered work
+in a country, would infringe one or more identifiable patents in that
+country that you have reason to believe are valid.
+
+ If, pursuant to or in connection with a single transaction or
+arrangement, you convey, or propagate by procuring conveyance of, a
+covered work, and grant a patent license to some of the parties
+receiving the covered work authorizing them to use, propagate, modify
+or convey a specific copy of the covered work, then the patent license
+you grant is automatically extended to all recipients of the covered
+work and works based on it.
+
+ A patent license is "discriminatory" if it does not include within
+the scope of its coverage, prohibits the exercise of, or is
+conditioned on the non-exercise of one or more of the rights that are
+specifically granted under this License. You may not convey a covered
+work if you are a party to an arrangement with a third party that is
+in the business of distributing software, under which you make payment
+to the third party based on the extent of your activity of conveying
+the work, and under which the third party grants, to any of the
+parties who would receive the covered work from you, a discriminatory
+patent license (a) in connection with copies of the covered work
+conveyed by you (or copies made from those copies), or (b) primarily
+for and in connection with specific products or compilations that
+contain the covered work, unless you entered into that arrangement,
+or that patent license was granted, prior to 28 March 2007.
+
+ Nothing in this License shall be construed as excluding or limiting
+any implied license or other defenses to infringement that may
+otherwise be available to you under applicable patent law.
+
+ 12. No Surrender of Others' Freedom.
+
+ If conditions are imposed on you (whether by court order, agreement or
+otherwise) that contradict the conditions of this License, they do not
+excuse you from the conditions of this License. If you cannot convey a
+covered work so as to satisfy simultaneously your obligations under this
+License and any other pertinent obligations, then as a consequence you may
+not convey it at all. For example, if you agree to terms that obligate you
+to collect a royalty for further conveying from those to whom you convey
+the Program, the only way you could satisfy both those terms and this
+License would be to refrain entirely from conveying the Program.
+
+ 13. Remote Network Interaction; Use with the GNU General Public License.
+
+ Notwithstanding any other provision of this License, if you modify the
+Program, your modified version must prominently offer all users
+interacting with it remotely through a computer network (if your version
+supports such interaction) an opportunity to receive the Corresponding
+Source of your version by providing access to the Corresponding Source
+from a network server at no charge, through some standard or customary
+means of facilitating copying of software. This Corresponding Source
+shall include the Corresponding Source for any work covered by version 3
+of the GNU General Public License that is incorporated pursuant to the
+following paragraph.
+
+ Notwithstanding any other provision of this License, you have
+permission to link or combine any covered work with a work licensed
+under version 3 of the GNU General Public License into a single
+combined work, and to convey the resulting work. The terms of this
+License will continue to apply to the part which is the covered work,
+but the work with which it is combined will remain governed by version
+3 of the GNU General Public License.
+
+ 14. Revised Versions of this License.
+
+ The Free Software Foundation may publish revised and/or new versions of
+the GNU Affero General Public License from time to time. Such new versions
+will be similar in spirit to the present version, but may differ in detail to
+address new problems or concerns.
+
+ Each version is given a distinguishing version number. If the
+Program specifies that a certain numbered version of the GNU Affero General
+Public License "or any later version" applies to it, you have the
+option of following the terms and conditions either of that numbered
+version or of any later version published by the Free Software
+Foundation. If the Program does not specify a version number of the
+GNU Affero General Public License, you may choose any version ever published
+by the Free Software Foundation.
+
+ If the Program specifies that a proxy can decide which future
+versions of the GNU Affero General Public License can be used, that proxy's
+public statement of acceptance of a version permanently authorizes you
+to choose that version for the Program.
+
+ Later license versions may give you additional or different
+permissions. However, no additional obligations are imposed on any
+author or copyright holder as a result of your choosing to follow a
+later version.
+
+ 15. Disclaimer of Warranty.
+
+ THERE IS NO WARRANTY FOR THE PROGRAM, TO THE EXTENT PERMITTED BY
+APPLICABLE LAW. EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT
+HOLDERS AND/OR OTHER PARTIES PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY
+OF ANY KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO,
+THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
+PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE PROGRAM
+IS WITH YOU. SHOULD THE PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF
+ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
+
+ 16. Limitation of Liability.
+
+ IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING
+WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MODIFIES AND/OR CONVEYS
+THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, INCLUDING ANY
+GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE
+USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED TO LOSS OF
+DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD
+PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER PROGRAMS),
+EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF
+SUCH DAMAGES.
+
+ 17. Interpretation of Sections 15 and 16.
+
+ If the disclaimer of warranty and limitation of liability provided
+above cannot be given local legal effect according to their terms,
+reviewing courts shall apply local law that most closely approximates
+an absolute waiver of all civil liability in connection with the
+Program, unless a warranty or assumption of liability accompanies a
+copy of the Program in return for a fee.
+
+ END OF TERMS AND CONDITIONS
+
+ How to Apply These Terms to Your New Programs
+
+ If you develop a new program, and you want it to be of the greatest
+possible use to the public, the best way to achieve this is to make it
+free software which everyone can redistribute and change under these terms.
+
+ To do so, attach the following notices to the program. It is safest
+to attach them to the start of each source file to most effectively
+state the exclusion of warranty; and each file should have at least
+the "copyright" line and a pointer to where the full notice is found.
+
+
+ Copyright (C)
+
+ This program is free software: you can redistribute it and/or modify
+ it under the terms of the GNU Affero General Public License as published by
+ the Free Software Foundation, either version 3 of the License, or
+ (at your option) any later version.
+
+ This program is distributed in the hope that it will be useful,
+ but WITHOUT ANY WARRANTY; without even the implied warranty of
+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ GNU Affero General Public License for more details.
+
+ You should have received a copy of the GNU Affero General Public License
+ along with this program. If not, see .
+
+Also add information on how to contact you by electronic and paper mail.
+
+ If your software can interact with users remotely through a computer
+network, you should also make sure that it provides a way for users to
+get its source. For example, if your program is a web application, its
+interface could display a "Source" link that leads users to an archive
+of the code. There are many ways you could offer source, and different
+solutions will be better for different programs; see section 13 for the
+specific requirements.
+
+ You should also get your employer (if you work as a programmer) or school,
+if any, to sign a "copyright disclaimer" for the program, if necessary.
+For more information on this, and how to apply and follow the GNU AGPL, see
+.
diff --git a/flake.lock b/flake.lock
new file mode 100644
index 0000000..0e6aceb
--- /dev/null
+++ b/flake.lock
@@ -0,0 +1,59 @@
+{
+ "nodes": {
+ "flake-utils": {
+ "inputs": {
+ "systems": "systems"
+ },
+ "locked": {
+ "lastModified": 1731533236,
+ "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=",
+ "owner": "numtide",
+ "repo": "flake-utils",
+ "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b",
+ "type": "github"
+ },
+ "original": {
+ "owner": "numtide",
+ "repo": "flake-utils",
+ "type": "github"
+ }
+ },
+ "nixpkgs": {
+ "locked": {
+ "lastModified": 1787736819,
+ "narHash": "sha256-IkjmqLoWzeqBAi1VIkdhDLMGjQDJ4suEDp59Zwxpswg=",
+ "rev": "9fbb54b33e91ee4ca368e35a78e0613c720600b3",
+ "type": "tarball",
+ "url": "https://releases.nixos.org/nixos/unstable/nixos-26.11pre1062397.9fbb54b33e91/nixexprs.tar.xz"
+ },
+ "original": {
+ "id": "nixpkgs",
+ "ref": "nixos-unstable",
+ "type": "indirect"
+ }
+ },
+ "root": {
+ "inputs": {
+ "flake-utils": "flake-utils",
+ "nixpkgs": "nixpkgs"
+ }
+ },
+ "systems": {
+ "locked": {
+ "lastModified": 1681028828,
+ "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
+ "owner": "nix-systems",
+ "repo": "default",
+ "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
+ "type": "github"
+ },
+ "original": {
+ "owner": "nix-systems",
+ "repo": "default",
+ "type": "github"
+ }
+ }
+ },
+ "root": "root",
+ "version": 7
+}
diff --git a/flake.nix b/flake.nix
new file mode 100644
index 0000000..6756eed
--- /dev/null
+++ b/flake.nix
@@ -0,0 +1,57 @@
+{
+ inputs = {
+ nixpkgs.url = "nixpkgs/nixos-unstable";
+ flake-utils.url = "github:numtide/flake-utils";
+ };
+
+ outputs = { self, nixpkgs, flake-utils, ... }@inputs:
+ flake-utils.lib.eachDefaultSystem
+ (system:
+ let
+ pkgs = import nixpkgs { inherit system; };
+ boost = pkgs.boost191;
+ llvmVersion = "22";
+ llvmPackages = pkgs."llvmPackages_${llvmVersion}";
+ libstdcxxGcc = pkgs.gcc16.cc;
+ clang = llvmPackages.clang.override {
+ gccForLibs = libstdcxxGcc;
+ };
+ inherit (clang) stdenv;
+
+ routemon = stdenv.mkDerivation {
+ name = "routemon";
+ src = ./server;
+
+ buildInputs = with pkgs; [ boost pugixml expat icu openssl sqlite ];
+ nativeBuildInputs = with pkgs; [ pkgs."llvmPackages_${llvmVersion}".clang-tools pkgs."clang_${llvmVersion}" boost cmake ninja gettext ];
+
+ hardeningDisable = [
+ # Disable here because this breaks C++ modules (I suspect because it sets -D_FORTIFY_SOURCE=3)
+ # We set plenty of hardening options in CMakeLists.txt anyway.
+ "all"
+ ];
+
+ env.NIX_CFLAGS_COMPILE = toString [
+ "-DLOCALEDIR=${builtins.placeholder "out"}/share/locale"
+ "-Wno-reserved-module-identifier"
+ "-isystem ${libstdcxxGcc}/include/c++/${libstdcxxGcc.version}/backward"
+ ];
+
+ cmakeFlags = [
+ "--preset=nix-derivation"
+ "-DCMAKE_CXX_STDLIB_MODULES_JSON=${libstdcxxGcc}/lib/libstdc++.modules.json"
+ ];
+ };
+ in
+ {
+ packages.routemon = routemon;
+
+ devShells.default = pkgs.mkShell.override { inherit stdenv; } {
+ buildInputs = [ pkgs.nix-index pkgs.nix-tree ];
+ inputsFrom = [ routemon ];
+ };
+
+ formatter = pkgs.nixpkgs-fmt;
+ });
+}
+
diff --git a/links.org b/links.org
new file mode 100644
index 0000000..c9194e9
--- /dev/null
+++ b/links.org
@@ -0,0 +1,4 @@
+- https://github.com/DATEX-II-EU/Profiles
+- https://opendata.ndw.nu/
+ - =planningsfeed_wegwerkzaamheden_en_evenementen.xml.gz=
+- https://www.mobilitaetsdaten.nrw/dataset/arbeitsstellen-nrw
diff --git a/server/.gitignore b/server/.gitignore
new file mode 100644
index 0000000..0751de2
--- /dev/null
+++ b/server/.gitignore
@@ -0,0 +1,7 @@
+assets/
+src/*.o
+src/*.d
+build/
+config.json
+*.sqlite3
+vendor/
diff --git a/server/CMakeLists.txt b/server/CMakeLists.txt
new file mode 100644
index 0000000..df4eb90
--- /dev/null
+++ b/server/CMakeLists.txt
@@ -0,0 +1,86 @@
+cmake_minimum_required(VERSION 4.3)
+
+project(routemon LANGUAGES CXX)
+
+# Hardening options from https://best.openssf.org/Compiler-Hardening-Guides/Compiler-Options-Hardening-Guide-for-C-and-C++.html
+add_compile_options(
+ # -O2
+ # -g
+ -fno-omit-frame-pointer
+ -Wall -Wextra -Wformat -Wformat=2 -Wconversion -Wimplicit-fallthrough
+ -Werror=format-security
+ -U_FORTIFY_SOURCE # -D_FORTIFY_SOURCE=3 (unfortunately breaks the std module)
+ -D_GLIBCXX_ASSERTIONS
+ -fstrict-flex-arrays=3
+ -fstack-clash-protection -fstack-protector-strong
+ -fPIE -fcf-protection=full
+ -fno-delete-null-pointer-checks -fno-strict-overflow -fno-strict-aliasing -ftrivial-auto-var-init=zero
+ -DBOOST_ASIO_NO_DEPRECATED
+)
+add_link_options(
+ -pie
+ -Wl,-z,nodlopen -Wl,-z,noexecstack
+ -Wl,-z,relro -Wl,-z,now
+ -Wl,--as-needed -Wl,--no-copy-dt-needed-entries
+)
+
+add_library(routemon_lib)
+target_sources(routemon_lib
+ PUBLIC FILE_SET CXX_MODULES FILES
+ src/api.cppm
+ src/api.cpp
+ src/database.cppm
+ src/config.cppm
+ src/config.cpp
+ src/datex2.cppm
+ src/geo.cppm
+ src/gpx.cppm
+ src/gpx.cpp
+ src/http_client.cppm
+ src/http_common.cppm
+ src/http_server.cppm
+ src/locale.cppm
+ src/log.cppm
+ src/problem.cppm
+ src/req_ctx.cppm
+ src/routemon.cppm
+ src/rwgps.cppm
+ src/sqlite3.cppm
+ src/srv.cppm
+ src/time.cppm
+ src/trace.cppm
+ src/util.cppm
+ src/xml.cppm
+ src/xml.cpp
+)
+
+add_executable(routemon src/main.cpp)
+target_link_libraries(routemon routemon_lib)
+install(TARGETS routemon)
+
+find_package(Boost 1.90 REQUIRED COMPONENTS json locale url)
+target_link_libraries(routemon_lib Boost::headers Boost::json Boost::locale Boost::url)
+
+# Already arranged via Boost::locale but this makes it more explicit, I guess
+find_package(ICU REQUIRED COMPONENTS data i18n uc)
+target_link_libraries(routemon_lib ICU::data ICU::i18n ICU::uc)
+
+find_library(pugixml pugixml REQUIRED)
+target_link_libraries(routemon_lib pugixml)
+
+find_package(OpenSSL REQUIRED)
+target_link_libraries(routemon_lib OpenSSL::SSL)
+
+find_package(SQLite3 REQUIRED)
+target_link_libraries(routemon_lib SQLite3::SQLite3)
+
+find_package(Gettext REQUIRED)
+gettext_create_translations(
+ routemon.pot
+ ALL
+ locale/nl.po
+ locale/en_US.po
+)
+
+find_package(expat REQUIRED)
+target_link_libraries(routemon_lib expat::expat)
diff --git a/server/CMakePresets.json b/server/CMakePresets.json
new file mode 100644
index 0000000..ae7fd67
--- /dev/null
+++ b/server/CMakePresets.json
@@ -0,0 +1,29 @@
+{
+ "version": 4,
+ "configurePresets": [
+ {
+ "name": "arch",
+ "binaryDir": "${sourceDir}/build",
+ "generator": "Ninja",
+ "cacheVariables": {
+ "CMAKE_CXX_STANDARD": "26",
+ "CMAKE_COLOR_DIAGNOSTICS": true,
+ "CMAKE_EXPERIMENTAL_CXX_IMPORT_STD": "f35a9ac6-8463-4d38-8eec-5d6008153e7d",
+ "CMAKE_CXX_EXTENSIONS": false,
+ "CMAKE_CXX_MODULE_STD": true,
+ "CMAKE_EXPORT_COMPILE_COMMANDS": true
+ }
+ },
+ {
+ "name": "nix-derivation",
+ "cacheVariables": {
+ "CMAKE_CXX_STANDARD": "26",
+ "CMAKE_COLOR_DIAGNOSTICS": true,
+ "CMAKE_EXPERIMENTAL_CXX_IMPORT_STD": "451f2fe2-a8a2-47c3-bc32-94786d8fc91b",
+ "CMAKE_CXX_EXTENSIONS": false,
+ "CMAKE_CXX_MODULE_STD": true,
+ "CMAKE_EXPORT_COMPILE_COMMANDS": true
+ }
+ }
+ ]
+}
diff --git a/server/README b/server/README
new file mode 100644
index 0000000..04d5d5a
--- /dev/null
+++ b/server/README
@@ -0,0 +1,16 @@
+# Configure
+
+$ cmake --preset arch # (--fresh if the build folder already exists)
+
+# Build
+
+$ cmake --build build
+
+# Dependencies (and versions known to work)
+
+- CMake 4.3.4
+- clang version 22.1.6
+- Boost 1.91
+- pugixml 1.16
+- OpenSSL
+- ICU
\ No newline at end of file
diff --git a/server/ct.sh b/server/ct.sh
new file mode 100644
index 0000000..29ad28b
--- /dev/null
+++ b/server/ct.sh
@@ -0,0 +1 @@
+clang-tidy -checks='boost-*,bugprone-*,clang-analyzer-*,concurrency-*,cppcoreguidlines-*,misc-*,-misc-include-cleaner,-misc-no-recursion,-misc-use-internal-linkage,modernize-*,performance-*,portability-*,radability-*' -p build '--exclude-header-filter=.*' src/time.cpp
diff --git a/server/formal/.envrc b/server/formal/.envrc
new file mode 100644
index 0000000..3550a30
--- /dev/null
+++ b/server/formal/.envrc
@@ -0,0 +1 @@
+use flake
diff --git a/server/formal/.gitignore b/server/formal/.gitignore
new file mode 100644
index 0000000..9023475
--- /dev/null
+++ b/server/formal/.gitignore
@@ -0,0 +1,17 @@
+*.aux
+*.glob
+*.vio
+*.vo
+*.vok
+*.vos
+.CoqMakefile.d
+.Makefile.coq.d
+.direnv
+.lia.cache
+Makefile.coq
+Makefile.coq.conf
+*#*.v#
+*#*.vok#
+*~
+.#*
+\#*#
\ No newline at end of file
diff --git a/server/formal/Makefile b/server/formal/Makefile
new file mode 100644
index 0000000..ac8dba0
--- /dev/null
+++ b/server/formal/Makefile
@@ -0,0 +1,55 @@
+# Default target
+all: Makefile.coq
+ +@$(MAKE) -f Makefile.coq all
+.PHONY: all
+
+# Permit local customization
+-include Makefile.local
+
+# Forward most targets to Coq makefile (with some trick to make this phony)
+%: Makefile.coq phony
+ @#echo "Forwarding $@"
+ +@$(MAKE) -f Makefile.coq $@
+phony: ;
+.PHONY: phony
+
+clean: Makefile.coq
+ +@$(MAKE) -f Makefile.coq clean
+ @# Make sure not to enter the `_opam` folder.
+ find [a-z]*/ \( -name "*.d" -o -name "*.vo" -o -name "*.vo[sk]" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
+ rm -f Makefile.coq .lia.cache builddep/*
+.PHONY: clean
+
+# Create Coq Makefile.
+Makefile.coq: _CoqProject Makefile
+ "$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq $(EXTRA_COQFILES)
+
+# Install build-dependencies
+OPAMFILES=$(wildcard *.opam)
+BUILDDEPFILES=$(addsuffix -builddep.opam, $(addprefix builddep/,$(basename $(OPAMFILES))))
+
+builddep/%-builddep.opam: %.opam Makefile
+ @echo "# Creating builddep package for $<."
+ @mkdir -p builddep
+ @sed <$< -E 's/^(build|install|remove):.*/\1: []/; s/"(.*)"(.*= *version.*)$$/"\1-builddep"\2/;' >$@
+
+builddep-opamfiles: $(BUILDDEPFILES)
+.PHONY: builddep-opamfiles
+
+builddep: builddep-opamfiles
+ @# We want opam to not just install the build-deps now, but to also keep satisfying these
+ @# constraints. Otherwise, `opam upgrade` may well update some packages to versions
+ @# that are incompatible with our build requirements.
+ @# To achieve this, we create a fake opam package that has our build-dependencies as
+ @# dependencies, but does not actually install anything itself.
+ @echo "# Installing builddep packages."
+ @opam install $(OPAMFLAGS) $(BUILDDEPFILES)
+.PHONY: builddep
+
+# Backwards compatibility target
+build-dep: builddep
+.PHONY: build-dep
+
+# Some files that do *not* need to be forwarded to Makefile.coq.
+# ("::" lets Makefile.local overwrite this.)
+Makefile Makefile.local _CoqProject $(OPAMFILES):: ;
diff --git a/server/formal/_CoqProject b/server/formal/_CoqProject
new file mode 100644
index 0000000..92d635c
--- /dev/null
+++ b/server/formal/_CoqProject
@@ -0,0 +1,5 @@
+-Q . routemon
+
+util.v
+period.v
+period_seq.v
\ No newline at end of file
diff --git a/server/formal/flake.lock b/server/formal/flake.lock
new file mode 100644
index 0000000..f4a7de9
--- /dev/null
+++ b/server/formal/flake.lock
@@ -0,0 +1,61 @@
+{
+ "nodes": {
+ "flake-utils": {
+ "inputs": {
+ "systems": "systems"
+ },
+ "locked": {
+ "lastModified": 1731533236,
+ "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=",
+ "owner": "numtide",
+ "repo": "flake-utils",
+ "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b",
+ "type": "github"
+ },
+ "original": {
+ "owner": "numtide",
+ "repo": "flake-utils",
+ "type": "github"
+ }
+ },
+ "nixpkgs": {
+ "locked": {
+ "lastModified": 1777077449,
+ "narHash": "sha256-AIiMJiqvGrN4HyLEbKAoCSRRYn0rnlW5VbKNIMIYqm4=",
+ "owner": "NixOS",
+ "repo": "nixpkgs",
+ "rev": "a4bf06618f0b5ee50f14ed8f0da77d34ecc19160",
+ "type": "github"
+ },
+ "original": {
+ "owner": "NixOS",
+ "ref": "nixos-25.11",
+ "repo": "nixpkgs",
+ "type": "github"
+ }
+ },
+ "root": {
+ "inputs": {
+ "flake-utils": "flake-utils",
+ "nixpkgs": "nixpkgs"
+ }
+ },
+ "systems": {
+ "locked": {
+ "lastModified": 1681028828,
+ "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
+ "owner": "nix-systems",
+ "repo": "default",
+ "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
+ "type": "github"
+ },
+ "original": {
+ "owner": "nix-systems",
+ "repo": "default",
+ "type": "github"
+ }
+ }
+ },
+ "root": "root",
+ "version": 7
+}
diff --git a/server/formal/flake.nix b/server/formal/flake.nix
new file mode 100644
index 0000000..57efa11
--- /dev/null
+++ b/server/formal/flake.nix
@@ -0,0 +1,26 @@
+{
+ inputs = {
+ nixpkgs.url = "github:NixOS/nixpkgs/nixos-25.11";
+ flake-utils.url = "github:numtide/flake-utils";
+ };
+
+ outputs = { self, nixpkgs, flake-utils, ... }:
+ flake-utils.lib.eachDefaultSystem (system:
+ let
+ pkgs = import nixpkgs { inherit system; };
+
+ # From 22-04-2026
+ stdpp = with pkgs; coqPackages.lib.overrideCoqDerivation {
+ version = "dev";
+ release."dev".sha256 = "hN+sEZcIaFoFF2+4dStTc0TRz5A03US6csEk5q0r/z8=";
+ release."dev".rev = "d3c67aa46ed22b1e593457cd34fc711f1a53b8be";
+ } coqPackages.stdpp;
+ in
+ {
+ devShells.default = with pkgs; mkShell {
+ buildInputs = [ coq stdpp ];
+ };
+
+ formatter = pkgs.nixpkgs-fmt;
+ });
+}
diff --git a/server/formal/period.v b/server/formal/period.v
new file mode 100644
index 0000000..82921db
--- /dev/null
+++ b/server/formal/period.v
@@ -0,0 +1,828 @@
+From stdpp Require Import numbers option sorting ssreflect.
+From stdpp Require Import options.
+From routemon Require Import util.
+
+Definition timestamp := Z.
+Variant limit :=
+ | NegInftyLimit
+ | TsLimit (x : timestamp)
+ | PosInftyLimit.
+Instance limit_eq_dec : EqDecision limit.
+Proof. solve_decision. Qed.
+
+Notation "-∞" := NegInftyLimit.
+Notation "+∞" := PosInftyLimit.
+Coercion TsLimit : timestamp >-> limit.
+
+(* The interval [start, end). Considered empty when start >= end. *)
+Record period :=
+ Period
+ { period_start : limit
+ ; period_end : limit
+ }.
+Notation "'[' s ',' e ')'" := (Period s e).
+
+(* Consider making an inductive variant of these? *)
+Definition limit_le (l1 l2 : limit) :=
+ match l1, l2 with
+ | -∞, _ | _, +∞ => True
+ | TsLimit t1, TsLimit t2 => (t1 ≤ t2)%Z
+ | _, _ => False
+ end.
+Arguments limit_le !_ !_ / : assert.
+Definition limit_lt l1 l2 :=
+ match l1 with
+ | -∞ =>
+ match l2 with
+ | -∞ => False
+ | _ => True
+ end
+ | TsLimit t1 =>
+ match l2 with
+ | -∞ => False
+ | TsLimit t2 => (t1 < t2)%Z
+ | +∞ => True
+ end
+ | +∞ => False
+ end.
+Arguments limit_lt !_ !_ / : assert.
+Instance limit_le_dec : RelDecision limit_le.
+Proof. intros [] []; simpl; solve_decision. Qed.
+Instance limit_lt_dec : RelDecision limit_lt.
+Proof. intros [] []; simpl; solve_decision. Qed.
+Instance limit_lt_pi l1 l2 : ProofIrrel (limit_lt l1 l2).
+Proof. destruct l1, l2; apply _. Qed.
+
+Instance relation_equiv {A} : Equiv (relation A) :=
+ λ R1 R2, ∀ x y, R1 x y ↔ R2 x y.
+
+Lemma strict_limit_le_limit_lt :
+ strict limit_le ≡ limit_lt.
+Proof.
+ split.
+ - intros []. destruct x, y; simpl in *; try done. lia.
+ - intros H. destruct x, y; unfold strict; simpl in *; try done; auto with lia.
+Qed.
+
+Instance : Reflexive limit_le.
+Proof. intros l. by destruct l; simpl. Qed.
+Instance : Transitive limit_le.
+Proof. intros [] [] []; simpl; try done. lia. Qed.
+Instance : PreOrder limit_le.
+Proof. constructor; apply _. Qed.
+Instance : AntiSymm (=) limit_le.
+Proof.
+ intros [] []; simpl; try done.
+ intros H1 H2. f_equal. by apply Z.le_antisymm.
+Qed.
+Instance : PartialOrder limit_le.
+Proof. constructor; apply _. Qed.
+Instance : Trichotomy (strict limit_le).
+Proof with auto with lia.
+ intros [] []; unfold strict; simpl...
+ destruct (Z.lt_trichotomy x x0) as [H|[->|H]]...
+Qed.
+Instance : TotalOrder limit_le.
+Proof. constructor; apply _. Qed.
+
+Instance : StrictOrder (strict limit_le) := _.
+(* TODO: apparently useless??
+Instance rel_equiv_proper {A} (x y : A) : Proper ((≡) ==> (↔)) (λ R, R x y).
+Proof. easy. Qed.
+Search Proper iff eq.
+*)
+Instance complement_equiv {A} : Proper ((≡) ==> (≡)) (@complement A).
+Proof. intros R1 R2 HR12. split; unfold complement; intros Hequiv []%HR12%Hequiv. Qed.
+Instance Reflexive_equiv {A} : Proper ((≡) ==> (↔)) (@Reflexive A).
+Proof.
+ intros R1 R2 Hequiv. unfold Reflexive.
+ split; intros H x; by apply Hequiv.
+Qed.
+Instance Irreflexive_equiv {A} : Proper ((≡) ==> (↔)) (@Irreflexive A).
+Proof. unfold Irreflexive. by intros R1 R2 ->. Qed.
+Instance Transitive_equiv {A} : Proper ((≡) ==> (↔)) (@Transitive A).
+Proof.
+ intros R1 R2 Hequiv. unfold Transitive.
+ by split; intros H x y z Hxy%Hequiv Hyz%Hequiv; eapply Hequiv, H.
+Qed.
+Instance StrictOrder_equiv {A} : Proper ((≡) ==> (↔)) (@StrictOrder A).
+Proof.
+ intros R1 R2 Hequiv. split; intros [Hirr Htrans].
+ - by rewrite ->Hequiv in Hirr, Htrans.
+ - by rewrite <-Hequiv in Hirr, Htrans.
+Qed.
+Instance Trichotomy_equiv {A} : Proper ((≡) ==> (↔)) (@Trichotomy A).
+Proof.
+ intros R1 R2 Hequiv. split; intros.
+ - intros x y. by rewrite -(Hequiv x y) -(Hequiv y x).
+ - intros x y. by rewrite (Hequiv x y) (Hequiv y x).
+Qed.
+
+Instance : StrictOrder limit_lt.
+Proof. rewrite -strict_limit_le_limit_lt. apply _. Qed.
+Instance : Trichotomy limit_lt.
+Proof. rewrite -strict_limit_le_limit_lt. apply _. Qed.
+
+Definition limit_lt_ts' (l : limit) (t2 : timestamp) :=
+ match l with
+ | -∞ => True
+ | TsLimit t1 => (t1 < t2)%Z
+ | +∞ => False
+ end.
+Definition ts_le_limit' (t1 : timestamp) (l : limit) :=
+ match l with
+ | -∞ => False
+ | TsLimit t2 => (t1 ≤ t2)%Z
+ | +∞ => True
+ end.
+Lemma limit_lt_limit_lt_ts' l t2 : limit_lt_ts' l t2 ↔ limit_lt l t2.
+Proof. by destruct l. Qed.
+Lemma ts_le_limit'_limit_le t1 l : ts_le_limit' t1 l ↔ limit_le t1 l.
+Proof. by destruct l. Qed.
+
+Declare Scope limit_scope.
+Delimit Scope limit_scope with lim.
+Notation "l1 < l2" := (limit_lt l1 l2) : limit_scope.
+Notation "l1 ≤ l2" := (limit_le l1 l2) : limit_scope.
+Notation "l1 < l2 < l3" := (l1 < l2 ∧ l2 < l3)%lim : limit_scope.
+Notation "l1 ≤ l2 < l3" := (l1 ≤ l2 ∧ l2 < l3)%lim : limit_scope.
+Notation "l1 < l2 ≤ l3" := (l1 < l2 ∧ l2 ≤ l3)%lim : limit_scope.
+Notation "l1 ≤ l2 ≤ l3" := (l1 ≤ l2 ∧ l2 ≤ l3)%lim : limit_scope.
+Open Scope limit_scope.
+
+Instance period_elem_of : ElemOf timestamp period :=
+ λ t '[s, e), (s ≤ t < e).
+Instance period_elem_of_dec t (p : period) : Decision (t ∈ p).
+Proof. destruct p as [s e]. apply _. Qed.
+
+Lemma limit_le_lt l1 l2 : l1 < l2 ↔ l1 ≤ l2 ∧ l1 ≠ l2.
+Proof. by rewrite -(strict_limit_le_limit_lt l1 l2) strict_spec_alt. Qed.
+
+Lemma limit_le_cases {l1 l2} : l1 ≤ l2 ↔ l1 = l2 ∨ l1 < l2.
+Proof.
+ rewrite -(strict_limit_le_limit_lt l1 l2) strict_spec_alt. split.
+ - intros Hl12. destruct (decide (l1 = l2)) as [<-|Hne]; tauto.
+ - by intros [<-|[Hl12 _]].
+Qed.
+
+Lemma limit_lt_le_lt {l1} l2 {l3} : l1 ≤ l2 < l3 → l1 < l3.
+Proof. by intros [[<-|?]%limit_le_cases ?]; last etrans. Qed.
+
+Definition period_empty '[s, e) := e ≤ s.
+Definition period_empty_alt (p : period) := ∀ t, t ∉ p.
+Lemma period_empty_alt_iff p : period_empty p ↔ period_empty_alt p.
+Proof.
+ destruct p as [s e].
+ rewrite /period_empty /period_empty_alt /=.
+ split; intros H.
+ - intros t [contra []]%limit_lt_le_lt%limit_le_lt.
+ by eapply (anti_symm limit_le).
+ - destruct s as [|s|], e as [|e|]; try done.
+ + exfalso. apply (H (Z.pred e)). rewrite /elem_of /period_elem_of /=. lia.
+ + exfalso. by apply (H 0%Z).
+ + rewrite /elem_of /period_elem_of /= in H.
+ specialize (H s). simpl. lia.
+ + exfalso. apply (H s). rewrite /elem_of /period_elem_of /=. lia.
+Qed.
+Instance period_empty_dec p : Decision (period_empty p).
+Proof. destruct p as [s e]. solve_decision. Qed.
+
+Definition period_nonempty '[s, e) := s < e.
+Instance period_nonempty_dec p : Decision (period_nonempty p).
+Proof. destruct p. apply _. Qed.
+Instance period_nonempty_pi p : ProofIrrel (period_nonempty p).
+Proof. destruct p. apply _. Qed.
+
+Instance period_equiv : Equiv period :=
+ λ p1 p2, ∀ t, t ∈ p1 ↔ t ∈ p2.
+Instance period_equiv_reflexive : Reflexive period_equiv.
+Proof. done. Qed.
+Instance period_equiv_trans : Transitive period_equiv.
+Proof. intros p1 p2 p3 H1 H2 t. by rewrite H1. Qed.
+Instance period_equiv_symm : Symmetric period_equiv.
+Proof. by intros p1 p2 H t. Qed.
+Instance period_equiv_equiv : Equivalence period_equiv.
+Proof. constructor; apply _. Qed.
+
+(* All empty periods are equivalent *)
+Lemma period_empty_equiv p1 p2 : period_empty p1 → period_empty p2 ↔ p1 ≡ p2.
+Proof.
+ intros Hp1%period_empty_alt_iff. split.
+ - intros Hp2%period_empty_alt_iff. intros t.
+ split; [intros []%(Hp1 _) | intros []%(Hp2 _)].
+ - intros Hequiv. apply period_empty_alt_iff.
+ intros t []%Hequiv%(Hp1 _).
+Qed.
+
+Instance empty_period : Empty period := [TsLimit 0%Z, TsLimit 0%Z).
+Definition empty_period_empty : period_empty empty_period.
+Proof. done. Qed.
+
+Definition limit_min (l1 l2 : limit) := if decide (l1 ≤ l2) then l1 else l2.
+Definition limit_max (l1 l2 : limit) := if decide (l1 ≤ l2) then l2 else l1.
+
+Notation "l1 '`min`' l2" := (limit_min l1 l2) : limit_scope.
+Notation "l1 '`max`' l2" := (limit_max l1 l2) : limit_scope.
+
+Definition limit_min_ts (t1 t2 : timestamp) :
+ t1 `min` t2 = TsLimit (t1 `min` t2)%Z.
+Proof.
+ unfold limit_min.
+ destruct (decide (t1 ≤ t2));
+ simpl in *; f_equal; lia.
+Qed.
+
+Definition limit_max_ts (t1 t2 : timestamp) :
+ t1 `max` t2 = TsLimit (t1 `max` t2)%Z.
+Proof.
+ unfold limit_max.
+ destruct (decide (t1 ≤ t2));
+ simpl in *; f_equal; lia.
+Qed.
+
+Instance period_intersection : Intersection period := λ '[s1, e1) '[s2, e2),
+ [ s1 `max` s2, e1 `min` e2 ).
+
+Lemma intersect_and (p1 p2 : period) t :
+ t ∈ (p1 ∩ p2) ↔ t ∈ p1 ∧ t ∈ p2.
+Proof.
+ (* It really should be possible to optimize this proof somehow. *)
+ destruct p1 as [[|s1|] [|e1|]], p2 as [[|s2|] [|e2|]];
+ rewrite /intersection /period_intersection /elem_of /period_elem_of /limit_min /limit_max /limit_le /limit_lt /=;
+ repeat case_decide; tauto || lia.
+Qed.
+
+(* The points in time given by p1 except those given by p2, given as a before/after pair. *)
+Definition except '[s1, e1) '[s2, e2) : period * period :=
+ ( [ s1, e1 `min` s2 ),
+ [ s1 `max` e2, e1 ) ).
+
+Lemma limit_lt_ne l1 l2 : l1 < l2 → l1 ≠ l2.
+Proof. rewrite -(strict_limit_le_limit_lt l1 l2) strict_spec_alt. easy. Qed.
+
+Lemma not_limit_le l1 l2 : ¬ (l1 ≤ l2) ↔ l2 < l1.
+Proof.
+ destruct (trichotomy limit_lt l1 l2) as [Hl12|[<-|Hl21]].
+ - split; intros H.
+ + exfalso. apply H, limit_le_cases. by right.
+ + exfalso. by eapply asymmetry.
+ - split; intros H.
+ + exfalso. apply H, limit_le_cases. by left.
+ + by apply (_ : Irreflexive limit_lt) in H.
+ - split; intros H; first done.
+ intros [<-|Hl12]%limit_le_cases.
+ + by apply (_ : Irreflexive limit_lt) in H.
+ + by eapply asymmetry.
+Qed.
+
+Lemma not_limit_le' : complement limit_le ≡ flip limit_lt.
+Proof. apply: not_limit_le. Qed.
+
+Instance relation_equiv_reflexive {A} : Reflexive (@relation_equiv A).
+Proof. done. Qed.
+Instance relation_equiv_trans {A} : Transitive (@relation_equiv A).
+Proof. intros R1 R2 R3 H12 H23 x y. by rewrite H12 -H23. Qed.
+Instance relation_equiv_symm {A} : Symmetric (@relation_equiv A).
+Proof. by intros R1 R2 H12 x y. Qed.
+Instance relation_equiv_equiv {A} : Equivalence (@relation_equiv A).
+Proof. constructor; apply _. Qed.
+
+Lemma relation_flip_equiv {A} : Proper ((≡@{relation A}) ==> (≡)) flip.
+Proof. intros R1 R2 H12 x y. simpl. by rewrite (H12 y x). Qed.
+
+(* Could also be more generic *)
+Lemma relation_flip_involutive {A} (R : relation A) : flip (flip R) ≡ R.
+Proof. done. Qed.
+
+Lemma complement_involutive {A} `{!RelDecision (R : relation A)} : complement (complement R) ≡ R.
+Proof.
+ intros x y. split; intros Hxy.
+ - by destruct (decide (R x y)).
+ - by apply.
+Qed.
+
+Lemma not_limit_lt' : complement limit_lt ≡ flip limit_le.
+Proof.
+ rewrite -(relation_flip_involutive limit_lt) complement_inverse.
+ trans (flip (complement (complement limit_le))).
+ { apply relation_flip_equiv, complement_equiv, symmetry, not_limit_le'. }
+ apply relation_flip_equiv, complement_involutive.
+Qed.
+
+Lemma not_limit_lt l1 l2 : ¬ (l1 < l2) ↔ l2 ≤ l1.
+Proof. apply not_limit_lt'. Qed.
+
+(* TODO: make conclusion positive? *)
+Lemma period_nonempty_equiv_L_1 (s1 e1 s2 e2 : limit) :
+ period_nonempty [s1, e1) →
+ period_nonempty [s2, e2) →
+ [s1, e1) ≡ [s2, e2) →
+ ¬ s1 < s2.
+Proof.
+ unfold period_nonempty.
+ intros Hne1 Hne2 Hequiv Hs12.
+ destruct s2 as [|s2|]; [by destruct s1|..|by destruct s1].
+ destruct s1 as [|s1|]; last done.
+ * assert (Hs2a : s2 ∈ [s2, e2)).
+ { unfold elem_of, period_elem_of. by destruct e2. }
+ pose proof (proj2 (Hequiv s2) Hs2a) as [_ Hs2b].
+ assert (Hs2c : Z.pred s2 ∈ [-∞, e1)).
+ { unfold elem_of, period_elem_of.
+ by destruct e1 as [|e1|]; [|simpl in *; lia|]. }
+ pose proof (proj1 (Hequiv (Z.pred s2)) Hs2c) as [contra _].
+ simpl in contra. lia.
+ * assert (Hs1 : s1 ∈ [s1, e1)).
+ { unfold elem_of, period_elem_of. by destruct e1. }
+ pose proof (proj1 (Hequiv s1) Hs1) as [[Heq|Heq]%limit_le_cases _].
+ { rewrite Heq in Hs12. by eapply (_ : Irreflexive limit_lt). }
+ by eapply asymmetry.
+Qed.
+
+(* TODO: make conclusion positive? *)
+Lemma period_nonempty_equiv_L_2 (s1 e1 s2 e2 : limit) :
+ period_nonempty [s1, e1) →
+ period_nonempty [s2, e2) →
+ [s1, e1) ≡ [s2, e2) →
+ ¬ e1 < e2.
+Proof.
+ intros Hne1 Hne2 Hequiv He12.
+ destruct e1 as [|e1|]; [by destruct s1|..|done].
+ destruct e2 as [|e2|]; first done.
+ * (* e2 - 1 ∈ [s2, e2) → e2 - 1 ∈ [s1, e1) → s1 ≤ e2 - 1 < e1 → e2 ≤ e1 → e2 = e1 ∨ e2 < e1 *)
+ assert (He2a : Z.pred e2 ∈ [s2, e2)).
+ { unfold elem_of, period_elem_of.
+ by destruct s2 as [|s2|]; [simpl in *; lia..|]. }
+ pose proof (proj2 (Hequiv (Z.pred e2)) He2a) as [_ He2b].
+ simpl in *. lia.
+ * (* We want to plug e1 into the right side to get a
+ contradiction, so we need s2 ≤ e1. It suffices to show that
+ s2 ≤ e1 - 1 *)
+ assert (He1a : Z.pred e1 ∈ [s1, e1)).
+ { unfold elem_of, period_elem_of.
+ by destruct s1 as [|s1|]; [simpl in *; lia..|]. }
+ pose proof (proj1 (Hequiv (Z.pred e1)) He1a) as [He1b _].
+ assert (He1c : e1 ∈ [s2, +∞)).
+ { unfold elem_of, period_elem_of.
+ by destruct s2 as [|s2|]; [|simpl in *; lia|]. }
+ pose proof (proj2 (Hequiv e1) He1c) as [_ []%(_ : Irreflexive limit_lt)].
+Qed.
+
+Lemma period_nonempty_equiv_L p1 p2 :
+ period_nonempty p1 →
+ period_nonempty p2 →
+ p1 ≡ p2 → p1 = p2.
+Proof.
+ destruct p1 as [s1 e1], p2 as [s2 e2].
+ unfold equiv, period_equiv.
+ intros Hne1 Hne2 Hequiv.
+ f_equal.
+ - destruct (decide (s1 < s2)) as [Hs12|[<-|Hs21]%not_limit_lt%limit_le_cases]; [|done|].
+ + exfalso. by apply (period_nonempty_equiv_L_1 s1 e1 s2 e2).
+ + exfalso. by apply (period_nonempty_equiv_L_1 s2 e2 s1 e1).
+ - destruct (decide (e1 < e2)) as [He12|[<-|He21]%not_limit_lt%limit_le_cases]; [|done|].
+ + exfalso. by apply (period_nonempty_equiv_L_2 s1 e1 s2 e2).
+ + exfalso. by apply (period_nonempty_equiv_L_2 s2 e2 s1 e1).
+Qed.
+
+Definition period_empty_not_nonempty p : ¬ period_empty p ↔ period_nonempty p.
+Proof. destruct p. apply not_limit_le. Qed.
+
+Lemma limit_lt_min l1 l2 l3 :
+ l1 < l2 ∧ l1 < l3 ↔ l1 < l2 `min` l3.
+Proof.
+ split.
+ - intros [Hl12 Hl13]. unfold limit_min. by case_decide.
+ - unfold limit_min. intros H. case_decide.
+ + split; first done.
+ apply limit_le_cases in H0 as [<-|H0]; first done.
+ by etrans.
+ + apply not_limit_le in H0.
+ by split; first etrans.
+Qed.
+
+Lemma limit_max_le l1 l2 l3 :
+ l1 ≤ l3 ∧ l2 ≤ l3 ↔ l1 `max` l2 ≤ l3.
+Proof.
+ split.
+ - intros [Hl12 Hl23]. unfold limit_max. by case_decide.
+ - unfold limit_max. intros H. case_decide.
+ + by split; first etrans.
+ + apply not_limit_le in H0. split; first done.
+ apply limit_le_lt in H0 as [H0 _]. by etrans.
+Qed.
+Lemma limit_le_max l1 l2 l3 :
+ l1 ≤ l2 `max` l3 ↔ l1 ≤ l2 ∨ l1 ≤ l3.
+Proof.
+ unfold limit_max.
+ destruct (decide (l2 ≤ l3)) as [Hl23|Hl23%not_limit_le].
+ - split; first tauto. intros [H|H]; last done. by etrans.
+ - split; first tauto. intros [H|H]; first done.
+ by trans l3; last (apply limit_le_cases; right).
+Qed.
+
+Lemma except_lem p1 p2 t :
+ t ∈ p1 ∧ t ∉ p2 ↔
+ t ∈ (except p1 p2).1 ∨ t ∈ (except p1 p2).2.
+Proof.
+ destruct p1 as [s1 e1], p2 as [s2 e2]. split.
+ - intros [Hp1 Hp2].
+ (* on the left if t < s2, on the right if e2 ≤ t *)
+ destruct (decide (t < s2)) as [Hts2|Hts2].
+ + (* t < s2 *)
+ left. simpl. split.
+ * apply Hp1.
+ * apply limit_lt_min. split; last done.
+ rewrite /elem_of /period_elem_of in Hp1. easy.
+ + (* ¬ (t < s2) (↔ s2 ≤ t) *)
+ apply not_limit_lt in Hts2.
+ right. simpl. split.
+ * apply limit_max_le. split.
+ -- apply Hp1.
+ -- apply not_limit_lt. intros contra. by apply Hp2.
+ * apply Hp1.
+ - intros [H|H]; simpl in *.
+ + split.
+ * unfold elem_of, period_elem_of in *. split.
+ -- apply H.
+ -- by destruct H as [_ [H _]%limit_lt_min].
+ * unfold elem_of, period_elem_of in *.
+ destruct H as [H1 [H2 H3]%limit_lt_min].
+ intros [Hc1 Hc2].
+ apply limit_le_cases in Hc1 as [Hc1|Hc1].
+ -- inv Hc1. by apply (_ : Irreflexive limit_lt) in H3.
+ -- eapply asymmetry; [apply H3 | apply Hc1].
+ + unfold elem_of, period_elem_of in H.
+ rewrite -limit_max_le in H. destruct H as [[H1 H2] H3].
+ split; first done.
+ intros [Hc1 Hc2].
+ apply limit_le_cases in H2 as [H2|H2].
+ -- inv H2. by apply (_ : Irreflexive limit_lt) in Hc2.
+ -- eapply asymmetry; [apply H2 | apply Hc2].
+Qed.
+
+Lemma limit_max_lt l1 l2 l3 :
+ l1 `max` l2 < l3 ↔ l1 < l3 ∧ l2 < l3.
+Proof.
+ unfold limit_max.
+ destruct (decide (l1 ≤ l2)) as [Hl12|Hl12%not_limit_le].
+ - split; last easy. intros H. by split; first eapply limit_lt_le_lt.
+ - split; last easy. intros H. by split; last etrans.
+Qed.
+
+Lemma limit_min_lt l1 l2 l3 :
+ l1 `min` l2 < l3 ↔ l1 < l3 ∨ l2 < l3.
+Proof.
+ unfold limit_min.
+ destruct (decide (l1 ≤ l2)%lim) as [Hl12|Hl12%not_limit_le].
+ - split; first tauto. by intros [H|H]; last eapply limit_lt_le_lt.
+ - split; first tauto. by intros [H|H]; first etrans.
+Qed.
+
+Lemma limit_lt_max l1 l2 l3 :
+ l1 < l2 `max` l3 ↔ l1 < l2 ∨ l1 < l3.
+Proof.
+ unfold limit_max.
+ destruct (decide (l2 ≤ l3)) as [Hl23|Hl23%not_limit_le].
+ - split; first tauto. intros [H|H]; last done.
+ by apply limit_le_cases in Hl23 as [<-|Hl23]; last etrans.
+ - split; first tauto. by intros [H|H]; last etrans.
+Qed.
+
+Instance limit_min_comm : Comm (=) limit_min.
+Proof.
+ unfold limit_min.
+ intros [] []; repeat case_decide;
+ try done; simpl in *; f_equal; lia.
+Qed.
+Instance limit_max_comm : Comm (=) limit_max.
+Proof.
+ unfold limit_max.
+ intros [] []; repeat case_decide;
+ try done; simpl in *; f_equal; lia.
+Qed.
+
+Lemma limit_max_eq_l l1 l2 : l1 `max` l2 = l1 ↔ l2 ≤ l1.
+Proof.
+ unfold limit_max. case_decide; split.
+ - by intros ->.
+ - intros H12. by eapply (_ : AntiSymm (=) limit_le).
+ - intros _. apply limit_le_cases. right.
+ by apply not_limit_le.
+ - by intros _.
+Qed.
+Lemma limit_max_eq_r l1 l2 : l1 `max` l2 = l2 ↔ l1 ≤ l2.
+Proof. rewrite [l1 `max` l2]comm. apply limit_max_eq_l. Qed.
+
+Lemma limit_max_l l1 l2 : l2 ≤ l1 → l1 `max` l2 = l1.
+Proof. apply limit_max_eq_l. Qed.
+Lemma limit_max_r l1 l2 : l1 ≤ l2 → l1 `max` l2 = l2.
+Proof. apply limit_max_eq_r. Qed.
+
+Definition ne_period := { p : period | period_nonempty p }.
+
+Instance ne_period_elem_of : ElemOf timestamp ne_period :=
+ λ t p, t ∈ `p.
+Instance ne_period_elem_of_dec t (p : ne_period) : Decision (t ∈ p).
+Proof. apply _. Qed.
+
+(* TODO: rename to ne_period_before *)
+Definition period_before '([s1, e1) ↾ _ : ne_period) '([s2, e2) ↾ _ : ne_period) :=
+ e1 < s2.
+
+Instance period_before_pi p1 p2 : ProofIrrel (period_before p1 p2).
+Proof. destruct p1 as [[s1 e1] Hne1], p2 as [[s2 e2] Hne2]. apply _. Qed.
+
+Instance period_before_trans : Transitive period_before.
+Proof.
+ intros [[s1 e1] Hne1] [[s2 e2] Hne2] [[s3 e3] Hne3] H1 H2.
+ unfold period_before in *. simpl in *.
+ by trans s2; last trans e2.
+Qed.
+
+Instance period_before_irrefl : Irreflexive period_before.
+Proof.
+ intros [[s e] Hne] Hp. simpl in *.
+ eapply (_ : Irreflexive limit_lt). by etrans.
+Qed.
+
+Instance period_before_strict_order : StrictOrder period_before.
+Proof. split; apply _. Qed.
+
+Definition ne_period_rel (R : relation ne_period) : relation period :=
+ λ p1 p2, ∃ H1 H2, R (p1 ↾ H1) (p2 ↾ H2).
+
+Instance ne_period_rel_trans `{!Transitive R} : Transitive (ne_period_rel R).
+Proof.
+ intros p1 p2 p3 (H1 & H2 & HR12) (H2' & H3 & HR23).
+ exists H1, H3. replace H2' with H2 in HR23; last apply proof_irrel.
+ by etrans.
+Qed.
+
+Instance ne_period_rel_irrefl `{!Irreflexive R} : Irreflexive (ne_period_rel R).
+Proof.
+ intros p. intros (H1 & H2 & HR).
+ replace H2 with H1 in HR; last apply proof_irrel.
+ by apply (_ : Irreflexive R) in HR.
+Qed.
+
+Instance ne_period_rel_pi (R : relation ne_period) `{!∀ x y, ProofIrrel (R x y)} x y :
+ ProofIrrel (ne_period_rel R x y).
+Proof. apply _. Qed.
+
+Lemma except_parts_order p1 p2 :
+ period_nonempty p2 →
+ period_nonempty (except p1 p2).1 →
+ period_nonempty (except p1 p2).2 →
+ ne_period_rel period_before (except p1 p2).1 (except p1 p2).2.
+Proof.
+ destruct p1 as [s1 e1], p2 as [s2 e2]. simpl. intros H0 Hne1 Hne2.
+ unfold period_before. split; [done|split; [done|]].
+ apply limit_min_lt. right. apply limit_lt_max. right. apply H0.
+Qed.
+
+Definition period_nonempty_alt (p : period) := ∃ t, t ∈ p.
+
+Lemma period_nonempty_alt_iff p :
+ period_nonempty p ↔ period_nonempty_alt p.
+Proof.
+ unfold period_nonempty, period_nonempty_alt.
+ destruct p as [s e]. split.
+ - intros Hlt. destruct s as [|s|]; last done.
+ + destruct e as [|e|]; first done.
+ * exists (Z.pred e). by split; last (simpl; lia).
+ * exists 0%Z. done.
+ + exists s. done.
+ - intros [t Ht]. by eapply limit_lt_le_lt.
+Qed.
+
+Instance period_eq_dec : EqDecision period.
+Proof. solve_decision. Qed.
+
+Instance period_disjoint : Disjoint period :=
+ λ p1 p2, period_empty (p1 ∩ p2).
+
+Instance period_intersection_comm : Comm (=) period_intersection.
+Proof.
+ intros [s1 e1] [s2 e2].
+ by rewrite /= [s2 `max` s1]comm [e2 `min` e1]comm.
+Qed.
+Instance period_disjoint_symm : Symmetric period_disjoint.
+Proof. intros p1 p2. unfold period_disjoint. by rewrite comm. Qed.
+
+Lemma limit_min_eq_l l1 l2 : l1 `min` l2 = l1 ↔ l1 ≤ l2.
+Proof.
+ unfold limit_min. case_decide; first done. split.
+ - intros ->. exfalso. by apply H.
+ - intros []%H.
+Qed.
+Lemma limit_min_eq_r l1 l2 : l1 `min` l2 = l2 ↔ l2 ≤ l1.
+Proof. rewrite [l1 `min` l2]comm. apply limit_min_eq_l. Qed.
+
+Lemma limit_min_l l1 l2 : l1 ≤ l2 → l1 `min` l2 = l1.
+Proof. apply limit_min_eq_l. Qed.
+Lemma limit_min_r l1 l2 : l2 ≤ l1 → l1 `min` l2 = l2.
+Proof. apply limit_min_eq_r. Qed.
+
+Lemma limit_lt_le_trans {l1} l2 {l3} : l1 < l2 → l2 ≤ l3 → l1 < l3.
+Proof. by intros Hlt12 [->|Hlt23]%limit_le_cases; last etrans. Qed.
+
+Instance period_union : Union period :=
+ λ '[s1, e1) '[s2, e2), [s1 `min` s2, e1 `max` e2).
+
+Lemma limit_min_le l1 l2 l3 :
+ l1 ≤ l3 ∨ l2 ≤ l3 ↔
+ l1 `min` l2 ≤ l3.
+Proof.
+ unfold limit_min. case_decide; split.
+ - by intros [H13|H23]; last trans l2.
+ - intros H13. by left.
+ - apply not_limit_le in H. intros [H13|H23]; last done.
+ trans l1; last done.
+ apply limit_le_cases. by right.
+ - intros H23. by right.
+Qed.
+
+Lemma limit_le_min l1 l2 l3 :
+ l1 ≤ l2 ∧ l1 ≤ l3 ↔
+ l1 ≤ l2 `min` l3.
+Proof.
+ unfold limit_min. case_decide; split.
+ - by intros [H12 _].
+ - intros ?. by split; last trans l2.
+ - by intros [_ H13].
+ - intros ?. split; last done.
+ apply not_limit_le in H.
+ trans l3; first done.
+ apply limit_le_cases. by right.
+Qed.
+
+Lemma period_union_lem_1 t (p1 p2 : period) :
+ t ∈ p1 ∨ t ∈ p2 → t ∈ p1 ∪ p2.
+Proof.
+ destruct p1 as [s1 e1], p2 as [s2 e2].
+ unfold union, period_union.
+ intros [Ht|Ht]; split.
+ - apply limit_min_le. left. apply Ht.
+ - apply limit_lt_max. left. apply Ht.
+ - apply limit_min_le. right. apply Ht.
+ - apply limit_lt_max. right. apply Ht.
+Qed.
+
+Definition unifiable '[s1, e1) '[s2, e2) :=
+ s2 ≤ e1 ∧ s1 ≤ e2.
+
+Instance unifiable_dec : RelDecision unifiable.
+Proof. intros [] []. solve_decision. Qed.
+
+Lemma not_limit_le_lt l1 l2 l3 :
+ ¬ l1 ≤ l2 < l3 ↔ l2 < l1 ∨ l3 ≤ l2.
+Proof.
+ split.
+ - intros H123.
+ destruct (decide (l2 < l1)) as [?|H21%not_limit_lt]; first by left.
+ destruct (decide (l3 ≤ l2)) as [?|H32%not_limit_le]; first by right.
+ exfalso. by apply H123.
+ - intros [H21|H32] contra.
+ + eapply not_limit_le; [apply H21|apply contra].
+ + eapply not_limit_lt; [apply H32|apply contra].
+Qed.
+
+Lemma limit_lt_le l1 l2 : l1 < l2 → l1 ≤ l2.
+Proof. intros Hlt. apply limit_le_cases. by right. Qed.
+
+Lemma period_union_lem_2 t (p1 p2 : period) :
+ unifiable p1 p2 →
+ t ∈ p1 ∪ p2 → t ∈ p1 ∨ t ∈ p2.
+Proof.
+ intros Hunif Hunion.
+ destruct (decide (t ∈ p1)) as [?|Ht1]; first by left.
+ destruct (decide (t ∈ p2)) as [?|Ht2]; first by right.
+ exfalso.
+
+ destruct p1 as [s1 e1], p2 as [s2 e2].
+ unfold elem_of, period_elem_of in *.
+ simpl in *. destruct Hunif as [Hunif1 Hunif2].
+
+ (* If t is not in p1, then it must be in p2 *)
+ apply Ht2. clear Ht2.
+ apply not_limit_le_lt in Ht1.
+ destruct Ht1 as [Ht1|Ht1].
+ - (* t is not in p1 because it is before p1 (where p2 must hence be) *)
+ destruct Hunion as [Hunion1 Hunion2].
+ apply limit_min_le in Hunion1 as [[->|contra]%limit_le_cases | Hunion1].
+ { exfalso. by eapply (_ : Irreflexive limit_lt). }
+ { exfalso. by eapply (asymmetry (R:=limit_lt)). }
+ split; first done. by eapply limit_lt_le_trans.
+ - destruct Hunion as [Hunion1 Hunion2].
+ apply limit_lt_max in Hunion2 as [Hunion2 | Hunion2].
+ + apply limit_le_cases in Ht1 as [->|contra].
+ { exfalso. by eapply (_ : Irreflexive limit_lt). }
+ { exfalso. by eapply (asymmetry (R:=limit_lt)). }
+ + split; last done. by trans e1.
+Qed.
+
+Instance period_union_comm : Comm (=) period_union.
+Proof.
+ unfold period_union. intros [s1 e1] [s2 e2].
+ by rewrite limit_min_comm limit_max_comm.
+Qed.
+
+Instance period_singleton : Singleton timestamp period :=
+ λ t, [t, TsLimit (Z.succ t)).
+Lemma period_singleton_lem_1 t : t ∈ ({[t]} : period).
+Proof. by split; simpl; last lia. Qed.
+Lemma period_singleton_lem_2 t t' : t' ∈ ({[t]} : period) → t' = t.
+Proof.
+ unfold singleton, period_singleton.
+ intros [H11 H12]. destruct t, t'; try done; simpl in *; lia.
+Qed.
+Lemma period_singleton_nonempty t : period_nonempty {[t]}.
+Proof.
+ apply period_nonempty_alt_iff.
+ exists t. apply period_singleton_lem_1.
+Qed.
+
+Lemma unifiable_period_union p1 p2 p3 :
+ unifiable p1 p2 → unifiable p2 p3 →
+ unifiable (p1 ∪ p2) p3.
+Proof.
+ destruct p1 as [s1 e1], p2 as [s2 e2], p3 as [s3 e3].
+ intros [Hunif11 Hunif12] [Hunif21 Hunif22]. simpl. split.
+ + apply limit_le_max. by right.
+ + apply limit_min_le. by right.
+Qed.
+
+Instance unifiable_symm : Symmetric unifiable.
+Proof. by intros [] [] []. Qed.
+
+Definition Σlift {A} {Φ : A → Prop} (R : relation A) : relation {x : A | Φ x} :=
+ λ '(x↾_) '(y↾_), R x y.
+
+Instance Σlift_symm {A Φ} `{!Symmetric R} : Symmetric (@Σlift A Φ R).
+Proof. intros [x Hx] [y Hy] HR. simpl in *. by apply symmetry. Qed.
+
+(* TODO: probably unused? *)
+Instance Σlift_dec {A Φ} `{!RelDecision R} : RelDecision (@Σlift A Φ R).
+Proof. intros [x Hx] [y Hy]. by simpl. Qed.
+
+Definition ne_period_unifiable : relation ne_period := Σlift unifiable.
+
+Lemma period_unifiable_not_before p1 p2 : ne_period_unifiable p1 p2 → ¬ period_before p1 p2.
+Proof.
+ destruct p1 as [[s1 e1] Hne1], p2 as [[s2 e2] Hne2]. simpl in *.
+ intros [Hunif1 Hunif2] Hbefore.
+ apply limit_le_cases in Hunif1 as [->|contra].
+ - by eapply (_ : Irreflexive limit_lt).
+ - by eapply (asymmetry (R:=limit_lt)).
+Qed.
+
+(* TODO: define total relation on Σperiod_nonempty, p1 p2 := unifiable p1 p2 ∨ p1 < p2.
+ (Then have [AntiSymm unifiable (≤@{Σperiod_nonempty})].)
+ Show decidability, perform mergesort.
+ Then make the rest of normalization consist in unification of the periods.
+ *)
+
+Definition ne_period_le p1 p2 := ne_period_unifiable p1 p2 ∨ period_before p1 p2.
+
+Instance ne_period_le_antisymm : AntiSymm ne_period_unifiable ne_period_le.
+Proof.
+ intros p1 p2 [H12|H12] [H21|H21]; [done|done|..].
+ - exfalso. apply symmetry in H21.
+ by eapply period_unifiable_not_before.
+ - exfalso. by eapply asymmetry.
+Qed.
+
+Lemma ne_period_neither_before_unifiable p1 p2 :
+ ¬ period_before p1 p2 → ¬ period_before p2 p1 →
+ ne_period_unifiable p1 p2.
+Proof.
+ destruct p1 as [[s1 e1] Hne1], p2 as [[s2 e2] Hne2].
+ simpl in *. by intros ?%not_limit_lt ?%not_limit_lt.
+Qed.
+
+Instance period_before_dec : RelDecision period_before.
+Proof.
+ intros [[s1 e1] ?] [[s2 e2] ?]. simpl in *.
+ solve_decision.
+Qed.
+
+Lemma ne_period_not_unifiable p1 p2 :
+ ¬ ne_period_unifiable p1 p2 →
+ period_before p1 p2 ∨ period_before p2 p1.
+Proof.
+ intros Hnunif.
+ destruct (decide (period_before p1 p2)) as [?|H12]; first by left.
+ destruct (decide (period_before p2 p1)) as [?|H21]; first by right.
+ exfalso. by apply Hnunif, ne_period_neither_before_unifiable.
+Qed.
+
+Instance ne_period_le_total : Total ne_period_le.
+Proof.
+ intros p1 p2.
+ destruct (decide (ne_period_unifiable p1 p2)) as [Hunif|Hnunif].
+ - (* which one we pick does not matter *)
+ by do 2 left.
+ - apply ne_period_not_unifiable in Hnunif as [H12|H21].
+ + left. by right.
+ + right. by right.
+Qed.
diff --git a/server/formal/period_seq.v b/server/formal/period_seq.v
new file mode 100644
index 0000000..705e505
--- /dev/null
+++ b/server/formal/period_seq.v
@@ -0,0 +1,834 @@
+From stdpp Require Import numbers option sorting ssreflect.
+From stdpp Require Import options.
+From routemon Require Import period util.
+
+(* This setup would require the proof irrelevance stuff
+
+Record period_seq :=
+ PeriodSeq
+ { periods : list period
+ ; Hnonempty : Forall period_nonempty periods
+ ; Hsorted : Sorted period_before periods
+ }.
+*)
+
+Definition period_seq := list ne_period.
+
+Definition period_seq_nf (ps : period_seq) :=
+ Sorted period_before ps.
+
+Instance period_seq_elem_of : ElemOf timestamp period_seq :=
+ λ t, Exists (λ p, t ∈ p).
+Instance period_seq_elem_of_dec t (ps : period_seq) : Decision (t ∈ ps).
+Proof.
+ induction ps as [|p ps].
+ - right. inv 1.
+ - destruct IHps.
+ + left. by apply Exists_cons_tl.
+ + destruct (decide (t ∈ p)).
+ * left. by apply Exists_cons_hd.
+ * right. by inv 1.
+Qed.
+
+Instance period_seq_equiv : Equiv period_seq :=
+ λ ps1 ps2, ∀ t, t ∈ ps1 ↔ t ∈ ps2.
+
+Definition ne_period_intersection (p1 p2 : ne_period) :=
+ let p := `p1 ∩ `p2 in
+ match decide (period_nonempty p) with
+ | left H => Some (p ↾ H)
+ | right _ => None
+ end.
+
+Definition ne_period_start (p : ne_period) :=
+ period_start (`p).
+Definition ne_period_end (p : ne_period) :=
+ period_end (`p).
+
+Definition period_seq_intersection_1 go ps1 ps2 :=
+ match ps1, ps2 with
+ | p1 :: ps1', p2 :: ps2' =>
+ let mp12 := ne_period_intersection p1 p2 in
+ let rest := if decide (ne_period_end p1 < ne_period_end p2)%lim then go ps1' ps2 else go ps1 ps2' in
+ match mp12 with
+ | Some p12 => p12 :: rest
+ | None => rest
+ end
+ | _, _ => []
+ end.
+Fixpoint period_seq_intersection_aux n :=
+ match n with
+ | 0 => const (const [])
+ | S n => period_seq_intersection_1 (period_seq_intersection_aux n)
+ end.
+Instance period_seq_intersection : Intersection period_seq :=
+ λ ps1 ps2, period_seq_intersection_aux (S (length ps1 + length ps2)) ps1 ps2.
+
+Lemma period_seq_intersection_eq ps1 ps2 :
+ period_seq_intersection ps1 ps2 =
+ match ps1, ps2 with
+ | p1 :: ps1', p2 :: ps2' =>
+ let mp12 := ne_period_intersection p1 p2 in
+ let rest := if decide (ne_period_end p1 < ne_period_end p2)%lim
+ then period_seq_intersection ps1' ps2
+ else period_seq_intersection ps1 ps2' in
+ match mp12 with
+ | Some p12 => p12 :: rest
+ | None => rest
+ end
+ | _, _ => []
+ end.
+Proof.
+ destruct ps1 as [|p1 ps1], ps2 as [|p2 ps2]; [done..|].
+ have Hlen1 : S (S (length ps1 + length ps2)) = S (length (p1 :: ps1) + length ps2) by simpl; lia.
+ have Hlen2 : S (S (length ps1 + length ps2)) = S (length ps1 + length (p2 :: ps2)) by simpl; lia.
+ by rewrite
+ /period_seq_intersection /period_seq_intersection_aux
+ !length_cons Nat.add_succ_l Nat.add_succ_r -/period_seq_intersection_aux.
+Qed.
+
+Opaque period_seq_intersection.
+
+Lemma period_seq_nf_cons p ps :
+ period_seq_nf (p :: ps) ↔
+ period_seq_nf ps ∧
+ Forall (λ q, ne_period_end p < ne_period_start q)%lim ps.
+Proof.
+ split.
+ - intros HSort%Sorted_StronglySorted; last apply _.
+ inv HSort. repeat split; try done.
+ + by apply StronglySorted_Sorted.
+ + eapply Forall_impl; first done.
+ intros [[sq eq] Hq] Hbef.
+ by destruct p as [[sp ep] Hp].
+ - intros (Hnf & Hlt).
+ constructor; first done. destruct ps as [|q ps]; constructor.
+ inv Hlt. destruct p as [[sp ep] Hp], q as [[sq eq] Hq]. by simpl in *.
+Qed.
+
+(*
+Lemma list_elem_of_cons_inv `{!EqDecision A} (x y : A) (l : list A) :
+ x ∈ y :: l ↔ x = y ∨ x ≠ y ∧ x ∈ l.
+Proof.
+ split.
+ - destruct (decide (x = y)) as [<-|H].
+ + intros _. by left.
+ + inv 1. by right.
+ - by intros [<-|[_ H]]; constructor.
+Qed.
+*)
+
+Lemma list_elem_of_cons_inv {A} (x y : A) (l : list A) :
+ x ∈ y :: l ↔ x = y ∨ x ∈ l.
+Proof.
+ split.
+ - by inv 1; [left|right].
+ - by intros [<-|H]; constructor.
+Qed.
+
+Lemma Sorted_list_elem_of_R_trans {A} `{!Transitive R} (x y z : A) (l : list A) :
+ Sorted R (y :: l) → z ∈ y :: l → R x y → R x z.
+Proof.
+ intros [HSort Hyl]%Sorted_inv.
+ revert y Hyl.
+ induction HSort as [|y' l' HSort IH Hy'l']; intros y.
+ - intros _. by inv 1; last inv H2.
+ - intros Hyy'%HdRel_inv.
+ intros [->|Hz]%list_elem_of_cons_inv; first done.
+ intros Hxy.
+ have : R x y' by eapply (_ : Transitive R).
+ by apply IH.
+Qed.
+
+Lemma Sorted_list_elem_of_cons_inv {A} `{!Transitive R} (x y : A) (l : list A) :
+ Sorted R (y :: l) →
+ x ∈ y :: l → x = y ∧ Forall (R x) l ∨ R y x ∧ x ∈ l.
+Proof.
+ intros HSort [->|H%list_elem_of_In]%list_elem_of_In%in_inv.
+ - left. by apply Sorted_StronglySorted in HSort as [_ ?]%StronglySorted_inv.
+ - right. inv HSort. inv H3; first inv H.
+ by split; first eapply Sorted_list_elem_of_R_trans.
+Qed.
+
+Lemma period_seq_nf_elem_of_cons_inv (p1 p2 : ne_period) (ps : period_seq) :
+ period_seq_nf (p2 :: ps) →
+ p1 ∈ p2 :: ps → p1 = p2 ∧ Forall (period_before p1) ps ∨
+ period_before p2 p1 ∧ p1 ∈ ps.
+Proof. apply Sorted_list_elem_of_cons_inv. Qed.
+
+Inductive option_Exists {A} (Φ : A → Prop) : option A → Prop :=
+ | Exists_Some (x : A) : Φ x → option_Exists Φ (Some x).
+
+Lemma option_Exists_from_option {A} Φ (mx : option A) :
+ option_Exists Φ mx ↔ from_option Φ False mx.
+Proof. split; by [inv 1 | destruct mx]. Qed.
+
+Lemma period_seq_intersect_lem_aux (p1 p2 : ne_period) (ps1 ps2 : period_seq) :
+ is_Some (ne_period_intersection p1 p2) →
+ period_seq_nf ps1 → period_seq_nf ps2 →
+ p1 ∈ ps1 → p2 ∈ ps2 →
+ option_Exists (.∈ ps1 ∩ ps2) (ne_period_intersection p1 p2).
+Proof.
+ intros Hne. revert ps2.
+ induction ps1 as [|[s1 e1] ps1]; first inv 3.
+ intros ps2 Hnf1 Hnf2 H1 H2. revert ps2 Hnf2 H2.
+ induction ps2 as [|[s2 e2] ps2]; first inv 2.
+ intros Hnf2 H2.
+
+ apply option_Exists_from_option.
+ rewrite /intersection period_seq_intersection_eq /=.
+ apply period_seq_nf_elem_of_cons_inv in H1 as [[-> Hp1]|[Hlt1 H1]]; last done.
+ + apply period_seq_nf_elem_of_cons_inv in H2 as [[-> Hp2]|[Hlt2 H2]]; last done.
+ * unfold ne_period_intersection.
+ case_decide.
+ -- exfalso. simpl in Hne.
+ apply limit_le_cases in H as [contra|contra].
+ ++ rewrite contra in Hne. by eapply (_ : Irreflexive limit_lt).
+ ++ by apply asymmetry in Hne.
+ -- constructor.
+ * case_decide.
+ -- case_decide.
+ ++ (* we need to show that [s1, e1) ## p2 *)
+ exfalso. assert ([s1, e1) ## p2).
+ { unfold disjoint, period_disjoint, period_empty.
+ destruct p2 as [s3 e3]. simpl.
+ destruct Hlt2 as [Hne2 [Hne3 Hlt2]].
+ simpl in Hlt2.
+
+ trans (e1 `min` e2)%lim.
+ { apply limit_le_cases. left.
+ trans e1.
+ - apply limit_min_eq_l, limit_le_cases. right.
+ by trans e2; last trans s3.
+ - apply symmetry, limit_min_eq_l, limit_le_cases. by right. }
+ etrans; first done.
+ apply limit_max_le.
+ split.
+ - apply limit_le_max. by left.
+ - apply limit_le_max. right.
+ apply limit_le_cases. right. by trans e2. }
+ by eapply period_empty_not_nonempty.
+ ++ by apply IHps2; first apply period_seq_nf_cons in Hnf2 as [_ [? _]].
+ -- case_decide.
+ ++ apply not_limit_le in H.
+ (* [s1, e1) ## p2 since e1 < e2 and e2 < p2, but [s1, e1) ∩ p2 ≠ ∅ in hyp *)
+ exfalso. assert ([s1, e1) ## p2).
+ { unfold disjoint, period_disjoint, period_empty.
+ destruct p2 as [s3 e3]. simpl.
+ destruct Hlt2 as [Hne2 [Hne3 Hlt2]].
+ simpl in Hlt2.
+
+ rewrite limit_min_l; last first.
+ { apply limit_le_cases. right.
+ by trans e2; last trans s3. }
+ apply limit_le_max. right.
+ apply limit_le_cases. right.
+ by trans e2. }
+ by eapply period_empty_not_nonempty.
+ ++ constructor. by apply IHps2; first apply period_seq_nf_cons in Hnf2 as (_ & ? & _).
+ + apply period_seq_nf_elem_of_cons_inv in H2 as [[-> Hp2]|[Hlt2 H2]]; last done.
+ * case_decide.
+ -- case_decide.
+ ++ apply IHps1; try done.
+ ** by apply period_seq_nf_cons in Hnf1 as (_ & ? & _).
+ ** by constructor.
+ ++ apply not_limit_lt in H0. exfalso. assert (p1 ## [s2, e2)).
+ { unfold disjoint, period_disjoint, period_empty.
+ destruct p1 as [s3 e3]. simpl.
+ destruct Hlt1 as [Hne1 [Hne3 Hlt1]].
+ simpl in Hlt1.
+
+ trans (e1 `min` e2)%lim.
+ { apply limit_le_cases. left.
+ trans e2.
+ - apply limit_min_eq_r. trans e1; first done.
+ apply limit_le_cases. right. by trans s3.
+ - by apply symmetry, limit_min_eq_r. }
+ etrans; first done.
+ apply limit_max_le.
+ split.
+ - apply limit_le_max. left.
+ apply limit_le_cases. right. by trans e1.
+ - apply limit_le_max. by right. }
+ by eapply period_empty_not_nonempty.
+ -- case_decide.
+ ++ constructor. apply IHps1; try done.
+ ** by apply period_seq_nf_cons in Hnf1 as (_ & ? & _).
+ ** by constructor.
+ ++ apply not_limit_lt in H0. apply not_limit_le in H.
+ exfalso. assert (p1 ## [s2, e2)).
+ { unfold disjoint, period_disjoint, period_empty.
+ destruct p1 as [s3 e3]. simpl.
+ destruct Hlt1 as [Hne1 [Hne3 Hlt1]].
+ simpl in Hlt1.
+
+ rewrite limit_min_r; last first.
+ { trans e1; first done.
+ apply limit_le_cases. right.
+ by trans s3. }
+ trans e1; first done.
+ apply limit_le_max. left.
+ apply limit_le_cases. by right. }
+ by eapply period_empty_not_nonempty.
+ * case_decide.
+ -- case_decide.
+ ++ apply IHps1; try done.
+ ** by apply period_seq_nf_cons in Hnf1 as (_ & ? & _).
+ ** by constructor.
+ ++ by apply IHps2; first apply period_seq_nf_cons in Hnf2 as (_ & ? & _).
+ -- case_decide; constructor.
+ ++ apply IHps1; try done.
+ ** by apply period_seq_nf_cons in Hnf1 as (_ & ? & _).
+ ** by constructor.
+ ++ by apply IHps2; first apply period_seq_nf_cons in Hnf2 as (_ & ? & _).
+Qed.
+
+Lemma period_seq_intersection_inv (p : period) (ps1 ps2 : period_seq) :
+ period_seq_nf ps1 → period_seq_nf ps2 → p ∈ ps1 ∩ ps2 →
+ ∃ p1 p2, p1 ∈ ps1 ∧ p2 ∈ ps2 ∧ p = p1 ∩ p2.
+Proof.
+ intros Hnf1. revert ps2.
+ induction ps1; first inv 2.
+ induction ps2.
+ { intros _ contra.
+ rewrite period_seq_intersection_eq in contra.
+ destruct a. inv contra. }
+ destruct a as [s1 e1], a0 as [s2 e2].
+ intros Hnf2 Hint.
+ rewrite period_seq_intersection_eq in Hint.
+ simpl in Hint. case_decide; case_decide.
+ - apply IHps1 in Hint as (q1 & q2 & Hq1 & Hq2 & ->); last done.
+ + exists q1, q2. by repeat split; first constructor.
+ + by apply period_seq_nf_cons in Hnf1 as (_ & ? & _).
+ - apply IHps2 in Hint as (q1 & q2 & Hq1 & Hq2 & ->).
+ + exists q1, q2. by repeat split; last constructor.
+ + by apply period_seq_nf_cons in Hnf2 as (_ & ? & _).
+ - inv Hint.
+ + exists [s1, e1), [s2, e2). repeat split; constructor.
+ + apply IHps1 in H3 as (q1 & q2 & Hq1 & Hq2 & ->); last done.
+ * exists q1, q2. by repeat split; first constructor.
+ * by apply period_seq_nf_cons in Hnf1 as (_ & ? & _).
+ - inv Hint.
+ + exists [s1, e1), [s2, e2). repeat split; constructor.
+ + apply IHps2 in H3 as (q1 & q2 & Hq1 & Hq2 & ->).
+ * exists q1, q2. by repeat split; last constructor.
+ * by apply period_seq_nf_cons in Hnf2 as (_ & ? & _).
+Qed.
+
+Lemma period_seq_intersection_lem t (ps1 ps2 : period_seq) :
+ period_seq_nf ps1 → period_seq_nf ps2 →
+ t ∈ ps1 ∧ t ∈ ps2 ↔ t ∈ ps1 ∩ ps2.
+Proof.
+ intros Hnf1 Hnf2.
+ split.
+ - intros [H1 H2].
+ unfold elem_of, period_seq_elem_of in H1, H2.
+ apply Exists_exists in H1 as (p1 & Hp1 & Ht1).
+ apply Exists_exists in H2 as (p2 & Hp2 & Ht2).
+ assert (Ht : t ∈ p1 ∩ p2). { by apply intersect_and. }
+ clear Ht1 Ht2.
+ unfold elem_of, period_seq_elem_of.
+ apply Exists_exists. exists (p1 ∩ p2).
+ split; first apply period_seq_intersect_lem_aux; try done.
+ apply period_nonempty_alt_iff. by exists t.
+ - intros (p & Hp & Ht)%Exists_exists.
+ apply period_seq_intersection_inv in Hp as (p1 & p2 & Hp1 & Hp2 & ->); try done.
+ apply intersect_and in Ht as [Ht1 Ht2].
+ split; apply Exists_exists; by eexists.
+Qed.
+
+Definition period_seq_extent (ps : period_seq) : period :=
+ match head ps, last ps with
+ | Some [s, _), Some [_, e) => [s, e)
+ | _, _ => ∅
+ end.
+
+(*
+Lemma period_seq_extent_hd ps :
+ period_seq_nf ps →
+ Forall (period_start (period_seq_extent ps)
+
+Lemma period_seq_extent_spec t ps :
+ period_seq_nf ps → t ∈ ps →
+ t ∈ period_seq_extent ps.
+Proof.
+ Search StronglySorted.
+ induction ps as [|p ps]; first inv 2.
+ intros Hnf. inv 1.
+ -
+
+Qed.
+*)
+
+(*
+Definition period_seq_intersection_extent (ps1 ps2 : period_seq) :
+ period_seq_nf ps1 → period_seq_nf ps2 →
+ period_seq_extent (ps1 ∩ ps2) = period_seq_extent ps1 ∩ period_seq_extent ps2.
+Proof.
+ intros Hnf1 Hnf2.
+ destruct (decide (period_empty (period_seq_extent (ps1 ∩ ps2)))).
+ - admit.
+ - apply period_empty_not_nonempty in n.
+ apply period_nonempty_equiv_L; first done.
+ + admit.
+ + intros t.
+ Search period equiv eq.
+*)
+
+(* The intersection preserves normal forms *)
+Lemma period_seq_intersection_nf (ps1 ps2 : period_seq) :
+ period_seq_nf ps1 → period_seq_nf ps2 → period_seq_nf (ps1 ∩ ps2).
+Proof.
+ intros Hnf1. revert ps2.
+ induction ps1 as [|[s1 e1] ps1]; induction ps2 as [|[s2 e2] ps2]; [done..|].
+ intros Hnf2. rewrite period_seq_intersection_eq /=.
+ case_decide.
+ - case_decide.
+ + by apply IHps1; first apply period_seq_nf_cons in Hnf1 as (_ & ? & _).
+ + apply IHps2. by apply period_seq_nf_cons in Hnf2 as (_ & ? & _).
+ - case_decide.
+ + apply IHps1 in Hnf2 as Hnf2'; last by apply period_seq_nf_cons in Hnf1 as (_ & ? & _).
+ destruct Hnf2' as [Hne HSort]. split.
+ * by constructor; first apply period_empty_not_nonempty.
+ * constructor; first done.
+ rewrite {1}/intersection /period_intersection.
+ apply period_seq_nf_cons in Hnf1 as (Hne1 & Hnf1 & Hlt1).
+ destruct (ps1 ∩ ([s2, e2) :: ps2)) as [|[sq eq] qs] eqn:Hqs; constructor.
+ assert (Hq : [sq, eq) ∈ ps1 ∩ ([s2, e2) :: ps2)).
+ { rewrite Hqs. constructor. }
+ unfold period_before. repeat split.
+ -- by apply period_empty_not_nonempty.
+ -- by eapply Forall_forall; first apply Hne.
+ -- specialize (IHps1 Hnf1).
+ apply period_seq_intersection_inv in Hq as ([sq1 eq1] & [sq2 eq2] & Hq1%list_elem_of_In & Hq2 & Hq); [|done..].
+ apply (proj1 (List.Forall_forall _ _) Hlt1) in Hq1.
+ injection Hq as -> ->.
+ simplify_eq/=.
+ apply limit_min_lt. left.
+ apply limit_lt_max. by left.
+ + apply IHps1 in Hnf2 as Hnf2'; last by apply period_seq_nf_cons in Hnf1 as (_ & ? & _).
+ destruct Hnf2' as [Hne HSort].
+ apply not_limit_lt in H0. split.
+ * constructor.
+ -- by apply period_empty_not_nonempty.
+ -- apply IHps2. by apply period_seq_nf_cons in Hnf2 as (_ & ? & _).
+ * constructor.
+ -- apply IHps2. by apply period_seq_nf_cons in Hnf2 as (_ & ? & _).
+ -- rewrite {1}/intersection /period_intersection.
+ apply period_seq_nf_cons in Hnf1 as Hnf1'.
+ destruct Hnf1' as (Hp1 & Hnf1' & Hne1).
+ apply period_seq_nf_cons in Hnf2 as (Hne2 & Hnf2 & Hlt2).
+ apply IHps2 in Hnf2 as Hnf2'.
+ destruct (([s1, e1) :: ps1) ∩ ps2) as [|[sq eq] qs] eqn:Hqs; constructor.
+ assert (Hq : [sq, eq) ∈ ([s1, e1) :: ps1) ∩ ps2).
+ { rewrite Hqs. constructor. }
+ unfold period_before. repeat split.
+ ++ by apply period_empty_not_nonempty.
+ ++ by eapply Forall_forall; first apply Hnf2'.
+ ++ apply period_seq_intersection_inv in Hq as ([sq1 eq1] & [sq2 eq2] & Hq1 & Hq2%list_elem_of_In & Hq); [|done..].
+ apply (proj1 (List.Forall_forall _ _) Hlt2) in Hq2.
+ injection Hq as -> ->.
+ simplify_eq/=.
+ apply limit_min_lt. right.
+ apply limit_lt_max. by right.
+Qed.
+
+Definition period_seq_intersection_comm_equiv ps1 ps2 :
+ period_seq_nf ps1 → period_seq_nf ps2 →
+ ps1 ∩ ps2 ≡ ps2 ∩ ps1.
+Proof.
+ intros Hnf1 Hnf2 t.
+ split; by intros [H2 H1]%period_seq_intersection_lem;
+ first apply period_seq_intersection_lem.
+Qed.
+
+Lemma period_seq_nf_cons_equiv_inv_start_1 p1 ps1 p2 ps2:
+ period_seq_nf (p1 :: ps1) →
+ period_seq_nf (p2 :: ps2) →
+ p1 :: ps1 ≡ p2 :: ps2 →
+ ¬ (period_start p1 < period_start p2)%lim.
+Proof.
+ intros Hnf1 Hnf2 Hequiv Hp12.
+ apply period_seq_nf_cons in Hnf1 as (Hne1 & Hnf1 & Hlt1), Hnf2 as (Hne2 & Hnf2 & Hlt2).
+ destruct p1 as [s1 e1], p2 as [s2 e2]. simpl in Hp12.
+ destruct s2 as [|s2|]; [by destruct s1| |done].
+ destruct s1 as [|s1|]; last done.
+ - destruct e1 as [|e1|]; first done.
+ + assert (Z.pred (s2 `min` e1) ∈ [-∞, e1) :: ps1).
+ { constructor. by split; [|simpl; lia]. }
+ apply Hequiv in H. inv H.
+ * destruct H1 as [H1 _]. simpl in H1. lia.
+ * apply Exists_exists in H1 as ([sp ep] & Hp & Hs2).
+ rewrite Forall_forall in Hlt2.
+ apply Hlt2 in Hp. simpl in Hp.
+ destruct Hs2 as [Hs21 Hs22].
+ assert (contra : (s2 < s2)%lim).
+ { trans e2; first done.
+ apply (limit_lt_le_trans sp); first done.
+ etrans; first apply Hs21. simpl. lia. }
+ by eapply (_ : Irreflexive limit_lt).
+ + assert (Z.pred s2 ∈ [-∞, +∞) :: ps1).
+ { by constructor. }
+ apply Hequiv in H. inv H.
+ * destruct H1 as [H1 _]. simpl in H1. lia.
+ * apply Exists_exists in H1 as ([sp ep] & Hp & Hs2).
+ rewrite Forall_forall in Hlt2.
+ apply Hlt2 in Hp. simpl in Hp.
+ destruct Hs2 as [Hs21 Hs22].
+ assert (contra : (s2 < s2)%lim).
+ { trans e2; first done.
+ apply (limit_lt_le_trans sp); first done.
+ etrans; first apply Hs21. simpl. lia. }
+ by eapply (_ : Irreflexive limit_lt).
+ - assert (s1 ∈ [s1, e1) :: ps1).
+ { by constructor. }
+ apply Hequiv in H. inv H.
+ + destruct H1 as [[[= ->]|H1]%limit_le_cases _].
+ * by eapply (_ : Irreflexive limit_lt).
+ * by eapply (asymmetry (R:=limit_lt)).
+ + apply Exists_exists in H1 as ([sp ep] & Hp & Hs1).
+ rewrite Forall_forall in Hlt2.
+ apply Hlt2 in Hp. simpl in Hp.
+ assert (contra : (s1 < s1)%lim).
+ { trans s2; first done.
+ trans e2; first done.
+ by apply (limit_lt_le_trans sp); last apply Hs1. }
+ by eapply (_ : Irreflexive limit_lt).
+Qed.
+
+Instance period_seq_equiv_trans : Transitive (≡@{period_seq}).
+Proof.
+ intros ps1 ps2 ps3 Heq12 Heq23 t. split.
+ - by intros Ht%Heq12%Heq23.
+ - by intros Ht%Heq23%Heq12.
+Qed.
+
+Instance period_seq_equiv_symm : Symmetric (≡@{period_seq}).
+Proof. intros ps1 ps2 Heq12 t. split; by intros Ht%Heq12. Qed.
+
+Lemma period_seq_nf_cons_equiv_inv_start p1 ps1 p2 ps2:
+ period_seq_nf (p1 :: ps1) →
+ period_seq_nf (p2 :: ps2) →
+ p1 :: ps1 ≡ p2 :: ps2 →
+ period_start p1 = period_start p2.
+Proof.
+ intros Hnf1 Hnf2 Hequiv.
+ destruct (decide (period_start p1 < period_start p2)%lim) as [Hs12|Hs21].
+ - exfalso. by eapply period_seq_nf_cons_equiv_inv_start_1 in Hs12.
+ - apply not_limit_lt, limit_le_cases in Hs21 as [Hs21|Hs21]; first done.
+ exfalso. by eapply period_seq_nf_cons_equiv_inv_start_1 in Hs21.
+Qed.
+
+Lemma period_seq_nf_cons_equiv_inv_end_1 p1 ps1 p2 ps2:
+ period_seq_nf (p1 :: ps1) →
+ period_seq_nf (p2 :: ps2) →
+ p1 :: ps1 ≡ p2 :: ps2 →
+ ¬ (period_end p1 < period_end p2)%lim.
+Proof.
+ intros Hnf1 Hnf2 Hequiv Hp12.
+ assert (Hs : period_start p1 = period_start p2).
+ { by eapply period_seq_nf_cons_equiv_inv_start. }
+ apply period_seq_nf_cons in Hnf1 as (Hne1 & Hnf1 & Hlt1), Hnf2 as (Hne2 & Hnf2 & Hlt2).
+ destruct p1 as [s1 e1], p2 as [s2 e2]. simpl in Hs, Hp12.
+ rewrite <-Hs in *. rename s1 into s. clear Hs s2.
+ destruct e1 as [|e1|]; [by destruct s| |done].
+ assert (e1 ∈ [s, e2) :: ps2).
+ { constructor. by split; [apply limit_le_cases; right|]. }
+ apply Hequiv in H. inv H.
+ + destruct H1 as [_ H12]. by eapply (_ : Irreflexive limit_lt).
+ + apply Exists_exists in H1 as (p & Hp & He1).
+ rewrite Forall_forall in Hlt1.
+ apply Hlt1 in Hp.
+ destruct p as [sp ep].
+ unfold period_end, period_start in Hp.
+ assert (contra : (e1 < e1)%lim).
+ { by eapply limit_lt_le_trans; last apply He1. }
+ by eapply (_ : Irreflexive limit_lt).
+Qed.
+
+Lemma period_seq_nf_cons_equiv_inv_end p1 ps1 p2 ps2:
+ period_seq_nf (p1 :: ps1) →
+ period_seq_nf (p2 :: ps2) →
+ p1 :: ps1 ≡ p2 :: ps2 →
+ period_end p1 = period_end p2.
+Proof.
+ intros Hnf1 Hnf2 Hequiv.
+ destruct (decide (period_end p1 < period_end p2)%lim) as [He12|He21].
+ - exfalso. by eapply period_seq_nf_cons_equiv_inv_end_1 in He12.
+ - apply not_limit_lt, limit_le_cases in He21 as [He21|He21]; first done.
+ exfalso. by eapply period_seq_nf_cons_equiv_inv_end_1 in He21.
+Qed.
+
+Lemma period_seq_nf_cons_equiv_inv p1 ps1 p2 ps2:
+ period_seq_nf (p1 :: ps1) →
+ period_seq_nf (p2 :: ps2) →
+ p1 :: ps1 ≡ p2 :: ps2 →
+ p1 = p2.
+Proof.
+ intros Hnf1 Hnf2 Hequiv.
+ trans [period_start p1, period_end p1); first by destruct p1.
+ trans [period_start p2, period_end p2); last by destruct p2.
+ erewrite period_seq_nf_cons_equiv_inv_start; try done.
+ by erewrite period_seq_nf_cons_equiv_inv_end.
+Qed.
+
+Lemma period_seq_nf_equiv_L ps1 ps2 :
+ period_seq_nf ps1 →
+ period_seq_nf ps2 →
+ ps1 ≡ ps2 → ps1 = ps2.
+Proof.
+ intros Hnf1. revert ps2.
+ induction ps1 as [|p1 ps1]; intros ps2 Hnf2 Hequiv.
+ - destruct ps2; first done.
+ assert (period_nonempty p) as [t Ht]%period_nonempty_alt_iff.
+ { inv Hnf2. by inv H. }
+ assert (t ∈ p :: ps2) as contra%Hequiv.
+ { by apply Exists_cons_hd. }
+ inv contra.
+ - destruct ps2 as [|p2 ps2].
+ + assert (period_nonempty p1) as [t Ht]%period_nonempty_alt_iff.
+ { inv Hnf1. by inv H. }
+ assert (t ∈ p1 :: ps1) as contra%Hequiv.
+ { by apply Exists_cons_hd. }
+ inv contra.
+ + assert (p1 = p2) as <-.
+ { by eapply period_seq_nf_cons_equiv_inv. }
+ rename p1 into p.
+ apply period_seq_nf_cons in Hnf1 as (Hne1 & Hnf1 & Hlt1), Hnf2 as (Hne2 & Hnf2 & Hlt2).
+ f_equal. apply IHps1; [done..|].
+ intros t. split; intros Ht.
+ * assert (t ∈ p :: ps1) as H%Hequiv.
+ { by apply Exists_cons_tl. }
+ inv H; last done.
+ apply Exists_exists in Ht as ([sq eq] & Hp & Ht).
+ rewrite Forall_forall in Hlt1.
+ apply Hlt1 in Hp.
+ exfalso. destruct p as [s e].
+ simpl in *.
+ assert (contra : (t < t)%lim).
+ { trans e; first apply H1.
+ by eapply limit_lt_le_trans; last apply Ht. }
+ by eapply (_ : Irreflexive limit_lt).
+ * assert (t ∈ p :: ps2) as H%Hequiv.
+ { by apply Exists_cons_tl. }
+ inv H; last done.
+ apply Exists_exists in Ht as ([sq eq] & Hp & Ht).
+ rewrite Forall_forall in Hlt2.
+ apply Hlt2 in Hp.
+ exfalso. destruct p as [s e].
+ simpl in *.
+ assert (contra : (t < t)%lim).
+ { trans e; first apply H1.
+ by eapply limit_lt_le_trans; last apply Ht. }
+ by eapply (_ : Irreflexive limit_lt).
+Qed.
+
+Definition period_seq_intersection_comm ps1 ps2 :
+ period_seq_nf ps1 → period_seq_nf ps2 →
+ ps1 ∩ ps2 = ps2 ∩ ps1.
+Proof.
+ intros Hnf1 Hnf2.
+ apply period_seq_nf_equiv_L.
+ - by apply period_seq_intersection_nf.
+ - by apply period_seq_intersection_nf.
+ - by apply period_seq_intersection_comm_equiv.
+Qed.
+
+Instance period_seq_equiv_refl : Reflexive (≡@{period_seq}).
+Proof. done. Qed.
+
+Instance period_seq_equiv_equivalence : Equivalence (≡@{period_seq}).
+Proof. split; apply _. Qed.
+
+Variant bound :=
+ | LtBound of limit
+ | GeBound of limit.
+
+Definition bound_le b1 b2 :=
+ match b1, b2 with
+ | GeBound l1, GeBound l2 => (l1 ≤ l2)%lim
+ | GeBound _, LtBound _ => True
+ | LtBound l1, LtBound l2 => (l1 ≤ l2)%lim
+ | LtBound _, GeBound _ => False
+ end.
+Instance bound_lt_dec : RelDecision bound_le.
+Proof. intros [l1|l1] [l2|l2]; simpl; solve_decision. Qed.
+
+Instance bound_le_refl : Reflexive bound_le.
+Proof. by intros []; simpl. Qed.
+
+Instance bound_le_trans : Transitive bound_le.
+Proof. intros [] [] [] ? ?; simpl in *; done || by etrans. Qed.
+
+Instance bound_le_preorder : PreOrder bound_le.
+Proof. split; apply _. Qed.
+
+Instance bound_le_antisymm : AntiSymm (=) bound_le.
+Proof. intros [] [] ? ?; simpl in *; done || f_equal; by eapply (_ : AntiSymm (=) limit_le). Qed.
+
+Instance bound_le_partial_order : PartialOrder bound_le.
+Proof. split; apply _. Qed.
+
+Instance bound_le_trichotomy : Trichotomy (strict bound_le).
+Proof.
+ intros [] []; simpl in *.
+ - destruct (trichotomy _ l l0) as [?|[?|?]].
+ + left. split; simpl.
+ * apply limit_le_cases. by right.
+ * by apply not_limit_le.
+ + right. left. by subst.
+ + right. right. split; simpl.
+ * apply limit_le_cases. by right.
+ * by apply not_limit_le.
+ - right. right. split; simpl; [done|by intros ?].
+ - left. split; simpl; [done|by intros ?].
+ - destruct (trichotomy _ l l0) as [?|[?|?]].
+ + left. split; simpl.
+ * apply limit_le_cases. by right.
+ * by apply not_limit_le.
+ + right. left. by subst.
+ + right. right. split; simpl.
+ * apply limit_le_cases. by right.
+ * by apply not_limit_le.
+Qed.
+
+Instance bound_le_total_order : TotalOrder bound_le.
+Proof. split; apply _. Qed.
+
+Definition period_bounds '[s, e) :=
+ if decide (period_nonempty [s, e)) then [GeBound s; LtBound e] else [].
+
+Definition period_seq_bounds (ps : period_seq) :=
+ ps ≫= period_bounds.
+
+Definition period_seq_bounds_sorted (ps : period_seq) :=
+ merge_sort bound_le (period_seq_bounds ps).
+
+Variant window_filter_action :=
+ KickLeft | KickRight | NoAction.
+Fixpoint window_filter_aux {A} (f : A → A → window_filter_action) (x : A) (l : list A) :=
+ match l with
+ | [] => [x]
+ | y :: l' =>
+ match f x y with
+ | KickLeft => window_filter_aux f y l'
+ | KickRight => window_filter_aux f x l'
+ | NoAction => x :: window_filter_aux f y l'
+ end
+ end.
+Definition window_filter {A} (f : A → A → window_filter_action) (l : list A) :=
+ match l with
+ | [] => []
+ | x :: l' => window_filter_aux f x l'
+ end.
+
+Definition period_seq_bounds_clean (ps : period_seq) :=
+ window_filter (λ b1 b2, match b1, b2 with
+ | GeBound _, LtBound _ => NoAction
+ | GeBound _, GeBound _ => KickRight
+ | LtBound _, GeBound _ => NoAction
+ | LtBound _, LtBound _ => KickLeft
+ end)
+ (period_seq_bounds_sorted ps).
+
+Fixpoint period_seq_from_bounds (bs : list bound) : period_seq :=
+ match bs with
+ | GeBound s :: LtBound e :: bs' => [s, e) :: period_seq_from_bounds bs'
+ | _ => []
+ end.
+
+Definition period_seq_normalize (ps : period_seq) :=
+ period_seq_from_bounds (period_seq_bounds_clean ps).
+
+
+Lemma period_seq_normalize_lem_1 (ps : period_seq) :
+ period_seq_normalize ps ≡ ps.
+Proof.
+ Search merge_sort.
+ Search Total Trichotomy.
+
+
+(* TODO: continue here *) Admitted.
+
+Lemma period_seq_normalize_lem_2 (ps : period_seq) :
+ period_seq_nf (period_seq_normalize ps).
+Proof. (* TODO: and here *) Admitted.
+
+Definition period_seq_union (ps1 ps2 : period_seq) :=
+ period_seq_normalize (ps1 ++ ps2).
+Lemma period_seq_union_lem t ps1 ps2 :
+ t ∈ period_seq_union ps1 ps2 ↔ t ∈ ps1 ∨ t ∈ ps2.
+Proof.
+ split.
+ - intros Ht%(period_seq_normalize_lem_1 (ps1 ++ ps2)).
+ apply Exists_app in Ht as [Ht|Ht]; by [left|right].
+ - intros [Ht|Ht]; apply period_seq_normalize_lem_1, Exists_app; by [left|right].
+Qed.
+Lemma period_seq_union_nf ps1 ps2 :
+ period_seq_nf (period_seq_union ps1 ps2).
+Proof. apply period_seq_normalize_lem_2. Qed.
+
+Definition nf_period_seq := sig period_seq_nf.
+
+Instance period_seq_nf_pi ps : ProofIrrel (period_seq_nf ps).
+Proof.
+ unfold period_seq_nf. intros [P11 P12] [P21 P22].
+ f_equal; [apply Forall_pi | apply Sorted_pi]; apply _.
+Qed.
+
+Instance period_seq_empty : Empty period_seq := [].
+Lemma period_seq_empty_nf : period_seq_nf ∅.
+Proof. done. Qed.
+
+Instance period_seq_singleton : Singleton timestamp period_seq :=
+ λ t, [{[t]}].
+Lemma period_seq_singleton_lem_1 t : t ∈ ({[t]} : period_seq).
+Proof.
+ unfold singleton, period_seq_singleton.
+ constructor. apply period_singleton_lem_1.
+Qed.
+Lemma period_seq_singleton_lem_2 t t' : t' ∈ ({[t]} : period_seq) → t' = t.
+Proof.
+ unfold singleton, period_seq_singleton.
+ inv 1; last inv H1.
+ by apply period_singleton_lem_2.
+Qed.
+Lemma period_seq_singleton_nf t : period_seq_nf {[t]}.
+Proof.
+ unfold singleton, period_seq_singleton.
+ split.
+ - constructor; last constructor.
+ apply period_singleton_nonempty.
+ - constructor; constructor.
+Qed.
+
+Instance nf_period_seq_elem_of : ElemOf timestamp nf_period_seq :=
+ λ t ps, t ∈ `ps.
+Instance nf_period_seq_empty : Empty nf_period_seq :=
+ ∅ ↾ period_seq_empty_nf.
+Instance nf_period_seq_union : Union nf_period_seq :=
+ λ '(ps1↾_) '(ps2↾_), period_seq_union ps1 ps2 ↾ (period_seq_union_nf ps1 ps2).
+Instance nf_period_seq_singleton : Singleton timestamp nf_period_seq :=
+ λ t, {[t]} ↾ period_seq_singleton_nf t.
+
+Instance nf_period_seq_semiset : SemiSet timestamp nf_period_seq.
+Proof.
+ split.
+ - intros t Ht. inv Ht.
+ - split.
+ + apply period_seq_singleton_lem_2.
+ + intros <-. apply period_seq_singleton_lem_1.
+ - intros [ps1 Hnf1] [ps2 Hnf2] t.
+ unfold union, nf_period_seq_union, elem_of, nf_period_seq_elem_of.
+ simpl. apply period_seq_union_lem.
+Qed.
+
+Instance nf_period_seq_intersection : Intersection nf_period_seq :=
+ λ '(ps1↾Hnf1) '(ps2↾Hnf2), (ps1 ∩ ps2) ↾ (period_seq_intersection_nf ps1 ps2 Hnf1 Hnf2).
+
+(* TODO: difference!
+
+Instance nf_period_seq_set : Set_ timestamp nf_period_seq.
+Proof. (* TODO *) Qed.
+
+*)
diff --git a/server/formal/util.v b/server/formal/util.v
new file mode 100644
index 0000000..8e16ffc
--- /dev/null
+++ b/server/formal/util.v
@@ -0,0 +1,92 @@
+From stdpp Require Import numbers option sorting ssreflect.
+From stdpp Require Import options.
+
+Definition transportf {X} (P : X → Type) {x x' : X} : x = x' → P x → P x'.
+Proof. by induction 1. Defined.
+
+Instance HdRel_pi {A} (R : relation A) `{!EqDecision A} `{!∀ x y, ProofIrrel (R x y)} a l : ProofIrrel (HdRel R a l).
+Proof.
+ intros HR1 HR2.
+ assert (Hnil : ∀ xs (Hxs : [] = xs) (HR : HdRel R a xs),
+ HR = transportf _ Hxs (HdRel_nil R a)).
+ { intros. destruct HR; last done.
+ by replace Hxs with (eq_refl ([] : list A)); last apply eq_pi, list_eq_dec. }
+ assert (Hcons : ∀ xs x y xs' (Hxs : y :: xs' = xs) (HR : HdRel R x xs) (Hxy : R x y),
+ HR = transportf (HdRel R x) Hxs (HdRel_cons R x y xs' Hxy)).
+ { intros. destruct HR; first done.
+ injection Hxs as <- <-.
+ replace Hxs with (eq_refl (y :: xs')); last apply eq_pi, list_eq_dec.
+ simpl.
+ by replace r with Hxy by apply H. }
+ destruct l.
+ - trans (transportf (HdRel R a) eq_refl (HdRel_nil R a)).
+ + apply Hnil.
+ + symmetry. apply Hnil.
+ - apply HdRel_inv in HR1 as Haa0.
+ trans (transportf (HdRel R a) eq_refl (HdRel_cons R a a0 l Haa0)).
+ + apply Hcons.
+ + symmetry. apply Hcons.
+Qed.
+
+Instance Sorted_pi {A} (R : relation A) `{!EqDecision A} `{!∀ x y, ProofIrrel (R x y)} l : ProofIrrel (Sorted R l).
+Proof.
+ intros HS1 HS2.
+ assert (Hbase : ∀ xs (Hxs : [] = xs) (HS : Sorted R xs), HS = transportf _ Hxs (Sorted_nil R)).
+ { intros. destruct HS; last done.
+ by replace Hxs with (eq_refl ([] : list A)); last apply eq_pi, list_eq_dec. }
+ assert (Hind : ∀ xs x xs'
+ (Hxs : x :: xs' = xs) (HS : Sorted R xs)
+ (Hx : HdRel R x xs') (HS' : Sorted R xs')
+ (IH : ∀ HS1' HS2' : Sorted R xs', HS1' = HS2'),
+ HS = transportf _ Hxs (Sorted_cons HS' Hx)).
+ { intros. destruct HS; first done.
+ injection Hxs as <- <-.
+ replace Hxs with (eq_refl (x :: xs')); last apply eq_pi, list_eq_dec.
+ simpl.
+ replace h with Hx by apply: HdRel_pi.
+ by replace HS with HS' by apply IH. }
+ induction l.
+ - trans (transportf _ eq_refl (Sorted_nil R)).
+ + apply Hbase.
+ + symmetry. apply Hbase.
+ - destruct (Sorted_inv HS1) as [Hl Hal].
+ trans (transportf _ eq_refl (Sorted_cons Hl Hal)).
+ + apply Hind, IHl.
+ + symmetry. apply Hind, IHl.
+Qed.
+
+Instance Forall_pi {A} (P : A → Prop) (l : list A) `{!EqDecision A} `{!∀ a, ProofIrrel (P a)} : ProofIrrel (Forall P l).
+Proof.
+ intros HF1 HF2.
+ assert (Hbase : ∀ xs (Hxs : [] = xs) (HF : Forall P xs), HF = transportf (Forall P) Hxs (ListDef.Forall_nil P)).
+ { intros xs Hxs HF. destruct HF; last done.
+ by replace Hxs with (eq_refl ([] : list A)); last apply eq_pi, list_eq_dec. }
+ assert (Hind : ∀ xs x xs'
+ (Hxs : x :: xs' = xs) (HF : Forall P xs)
+ (Hx : P x) (HF' : Forall P xs')
+ (IH : ∀ HF1' HF2' : Forall P xs', HF1' = HF2'),
+ HF = transportf _ Hxs (ListDef.Forall_cons P x xs' Hx HF')).
+ { intros. destruct HF; first done.
+ injection Hxs as <- <-.
+ replace Hxs with (eq_refl (x :: xs')); last apply eq_pi, list_eq_dec.
+ simpl.
+ replace p with Hx by apply H.
+ by replace HF with HF' by apply IH. }
+ induction l.
+ - trans (transportf _ eq_refl (ListDef.Forall_nil P)).
+ + apply Hbase.
+ + symmetry. apply Hbase.
+ - apply Forall_inv in HF1 as Ha.
+ apply Forall_inv_tail in HF1 as Hl.
+ trans (transportf _ eq_refl (ListDef.Forall_cons P a l Ha Hl)).
+ + apply Hind, IHl.
+ + symmetry. apply Hind, IHl.
+Qed.
+
+Instance ex_pi {A} {B : A → Prop} `{!ProofIrrel A} `{!∀ x, ProofIrrel (B x)} :
+ ProofIrrel (∃ (x : A), B x).
+Proof.
+ intros [x Hx] [y Hy].
+ assert (y = x) by apply proof_irrel. subst.
+ assert (Hx = Hy) by apply proof_irrel. by subst.
+Qed.
diff --git a/server/hack/rwgps-get-auth-token.sh b/server/hack/rwgps-get-auth-token.sh
new file mode 100755
index 0000000..d7a14a5
--- /dev/null
+++ b/server/hack/rwgps-get-auth-token.sh
@@ -0,0 +1,14 @@
+#!/bin/bash
+
+rwgps_api_key="$(jq
+# This file is distributed under the same license as the routemon package.
+# Rutger Broekhoff , 2026.
+#
+msgid ""
+msgstr ""
+"Project-Id-Version: PACKAGE VERSION\n"
+"Report-Msgid-Bugs-To: \n"
+"POT-Creation-Date: 2026-08-28 09:20+0200\n"
+"PO-Revision-Date: 2026-08-28 14:31+0200\n"
+"Last-Translator: Rutger Broekhoff \n"
+"Language-Team: English\n"
+"Language: en_US\n"
+"MIME-Version: 1.0\n"
+"Content-Type: text/plain; charset=UTF-8\n"
+"Content-Transfer-Encoding: 8bit\n"
+"Plural-Forms: nplurals=2; plural=(n != 1);\n"
+
+#: ../src/http_server.cppm:232
+msgid "No body expected for this request"
+msgstr "No body expected for this request"
+
+#: ../src/http_server.cppm:500
+msgid "Bad request"
+msgstr "Bad request"
+
+#: ../src/http_server.cppm:511 ../src/http_server.cppm:562
+msgid "Method not allowed"
+msgstr "Method not allowed"
+
+#: ../src/http_server.cppm:527
+msgid ""
+"Path of normalized (RFC 3986, § 6) origin-form request-target (RFC 9112, § "
+"3.2.1) should be absolute"
+msgstr "Path of normalized (RFC 3986, § 6) origin-form request-target (RFC 9112, § 3.2.1) should be absolute"
+
+#: ../src/http_server.cppm:538
+msgid "Not found"
+msgstr "Not found"
+
+#: ../src/http_server.cppm:549
+msgid "Method not implemented"
+msgstr "Method not implemented"
+
+#: ../src/http_server.cppm:573
+msgid ""
+"Invalid request-target, expected asterisk-form or origin-form (see RFC 9112, "
+"§ 3.2)"
+msgstr "Invalid request-target, expected asterisk-form or origin-form (see RFC 9112, § 3.2)"
+
+#: ../src/srv.cppm:148
+msgid "Failed to parse GPX file"
+msgstr "Failed to parse GPX file"
+
+#: ../src/srv.cppm:160
+msgid "Internal server error"
+msgstr "Internal server error"
+
+#~ msgid "Invalid point in GPX file"
+#~ msgstr "Invalid point in GPX file"
+
+#~ msgid "GPX file has no points in track"
+#~ msgstr "GPX file has no points in track"
diff --git a/server/locale/nl.po b/server/locale/nl.po
new file mode 100644
index 0000000..96b6cd9
--- /dev/null
+++ b/server/locale/nl.po
@@ -0,0 +1,64 @@
+# Translations for the routemon project.
+# Copyright (C) 2026 Rutger Broekhoff
+# This file is distributed under the same license as the routemon package.
+# Rutger Broekhoff , 2026.
+#
+msgid ""
+msgstr ""
+"Project-Id-Version: routemon 0.1.0\n"
+"Report-Msgid-Bugs-To: \n"
+"POT-Creation-Date: 2026-08-28 09:20+0200\n"
+"PO-Revision-Date: 2026-08-28 14:35+0200\n"
+"Last-Translator: Rutger Broekhoff \n"
+"Language-Team: Dutch \n"
+"Language: nl\n"
+"MIME-Version: 1.0\n"
+"Content-Type: text/plain; charset=UTF-8\n"
+"Content-Transfer-Encoding: 8bit\n"
+"Plural-Forms: nplurals=2; plural=(n != 1);\n"
+
+#: ../src/http_server.cppm:232
+msgid "No body expected for this request"
+msgstr "Geen body verwacht voor deze aanvraag"
+
+#: ../src/http_server.cppm:500
+msgid "Bad request"
+msgstr "Ongeldige aanvraag"
+
+#: ../src/http_server.cppm:511 ../src/http_server.cppm:562
+msgid "Method not allowed"
+msgstr "Aanvraagmethode niet toegestaan"
+
+#: ../src/http_server.cppm:527
+msgid ""
+"Path of normalized (RFC 3986, § 6) origin-form request-target (RFC 9112, § "
+"3.2.1) should be absolute"
+msgstr "Pad van genormaliseerde (RFC 3986, § 6) origin-form request-target (RFC 9112, § 3.2.1) behoort absoluut te zijn"
+
+#: ../src/http_server.cppm:538
+msgid "Not found"
+msgstr "Niet gevonden"
+
+#: ../src/http_server.cppm:549
+msgid "Method not implemented"
+msgstr "Aanvraagmethode niet geïmplementeerd"
+
+#: ../src/http_server.cppm:573
+msgid ""
+"Invalid request-target, expected asterisk-form or origin-form (see RFC 9112, "
+"§ 3.2)"
+msgstr "Ongeldige request-target, asterisk-form of origin-form verwacht (zie RFC 9112, § 3.2)"
+
+#: ../src/srv.cppm:148
+msgid "Failed to parse GPX file"
+msgstr "GPX-bestand kon niet geladen worden"
+
+#: ../src/srv.cppm:160
+msgid "Internal server error"
+msgstr "Interne serverfout"
+
+#~ msgid "Invalid point in GPX file"
+#~ msgstr "Ongeldig punt in GPX-bestand"
+
+#~ msgid "GPX file has no points in track"
+#~ msgstr "GPX-bestand mist punten in de track"
diff --git a/server/locale/xget.sh b/server/locale/xget.sh
new file mode 100755
index 0000000..06b5775
--- /dev/null
+++ b/server/locale/xget.sh
@@ -0,0 +1,13 @@
+#!/bin/bash
+
+xgettext --keyword=translate:1,1t --keyword=translate:1c,2,2t \
+ --keyword=translate:1,2,3t --keyword=translate:1c,2,3,4t \
+ --keyword=gettext:1 --keyword=pgettext:1c,2 \
+ --keyword=ngettext:1,2 --keyword=npgettext:1c,2,3 \
+ --from-code=UTF-8 --language=C++ \
+ ../src/*.cpp ../src/*.cppm \
+ -o ../routemon.pot
+
+for po_file in *.po; do
+ msgmerge "$po_file" ../routemon.pot -U
+done
diff --git a/server/migrations/1_init_down.sql b/server/migrations/1_init_down.sql
new file mode 100644
index 0000000..795e617
--- /dev/null
+++ b/server/migrations/1_init_down.sql
@@ -0,0 +1 @@
+DROP TABLE migration;
diff --git a/server/migrations/1_init_up.sql b/server/migrations/1_init_up.sql
new file mode 100644
index 0000000..7edb398
--- /dev/null
+++ b/server/migrations/1_init_up.sql
@@ -0,0 +1,7 @@
+BEGIN;
+
+CREATE TABLE migration (version);
+
+INSERT INTO migration VALUES (1);
+
+COMMIT;
diff --git a/server/migrations/2_kaas_up.sql b/server/migrations/2_kaas_up.sql
new file mode 100644
index 0000000..0c7837a
--- /dev/null
+++ b/server/migrations/2_kaas_up.sql
@@ -0,0 +1,23 @@
+BEGIN;
+
+-- TODO enable strict mode so that primary key is automatically enforced to not be NULL
+CREATE TABLE received_route (
+ id INTEGER PRIMARY KEY,
+
+ received_route_source route_source NOT NULL,
+ recieved_route_strava_id TEXT,
+
+ -- ON DELETE what?
+ FOREIGN KEY (received_route_source_id) REFERENCES received_route_source (id),
+ CHECK (received_route_source IN ('gpx_upload', 'strava', 'rwgps')),
+ CHECK ((received_route_source = 'strava') = (received_route_strava_id IS NULL))
+);
+
+CREATE TABLE received_route_linestring (
+ received_route_id INT NOT NULL,
+ linestring BLOB NOT NULL,
+
+ FOREIGN KEY (received_route_id) REFERENCES received_route (id)
+);
+
+COMMIT;
diff --git a/server/routemon.pot b/server/routemon.pot
new file mode 100644
index 0000000..711df4b
--- /dev/null
+++ b/server/routemon.pot
@@ -0,0 +1,58 @@
+# SOME DESCRIPTIVE TITLE.
+# Copyright (C) YEAR THE PACKAGE'S COPYRIGHT HOLDER
+# This file is distributed under the same license as the PACKAGE package.
+# FIRST AUTHOR , YEAR.
+#
+#, fuzzy
+msgid ""
+msgstr ""
+"Project-Id-Version: PACKAGE VERSION\n"
+"Report-Msgid-Bugs-To: \n"
+"POT-Creation-Date: 2026-08-28 09:20+0200\n"
+"PO-Revision-Date: YEAR-MO-DA HO:MI+ZONE\n"
+"Last-Translator: FULL NAME \n"
+"Language-Team: LANGUAGE \n"
+"Language: \n"
+"MIME-Version: 1.0\n"
+"Content-Type: text/plain; charset=UTF-8\n"
+"Content-Transfer-Encoding: 8bit\n"
+
+#: ../src/http_server.cppm:232
+msgid "No body expected for this request"
+msgstr ""
+
+#: ../src/http_server.cppm:500
+msgid "Bad request"
+msgstr ""
+
+#: ../src/http_server.cppm:511 ../src/http_server.cppm:562
+msgid "Method not allowed"
+msgstr ""
+
+#: ../src/http_server.cppm:527
+msgid ""
+"Path of normalized (RFC 3986, § 6) origin-form request-target (RFC 9112, § "
+"3.2.1) should be absolute"
+msgstr ""
+
+#: ../src/http_server.cppm:538
+msgid "Not found"
+msgstr ""
+
+#: ../src/http_server.cppm:549
+msgid "Method not implemented"
+msgstr ""
+
+#: ../src/http_server.cppm:573
+msgid ""
+"Invalid request-target, expected asterisk-form or origin-form (see RFC 9112, "
+"§ 3.2)"
+msgstr ""
+
+#: ../src/srv.cppm:148
+msgid "Failed to parse GPX file"
+msgstr ""
+
+#: ../src/srv.cppm:160
+msgid "Internal server error"
+msgstr ""
diff --git a/server/src/api.cpp b/server/src/api.cpp
new file mode 100644
index 0000000..b3c8e31
--- /dev/null
+++ b/server/src/api.cpp
@@ -0,0 +1,206 @@
+module;
+
+#include
+#include
+
+module routemon:api$impl;
+
+import std;
+import :api;
+import :datex2;
+import :geo;
+import :gpx;
+import :log;
+import :req_ctx;
+import :time;
+import :trace;
+
+namespace {
+
+ namespace chrono = std::chrono;
+ namespace json = boost::json;
+ namespace views = std::views;
+
+} // namespace
+
+namespace routemon::api {
+
+ auto json_value_from_point(geo::point const& p) -> json::value {
+ return json::array{bgeo::get<1>(p), bgeo::get<0>(p)};
+ }
+ auto json_value_from_linestring(geo::linestring const& ls) -> json::value {
+ json::array a;
+ for (auto const& p : ls)
+ a.push_back(json_value_from_point(p));
+ return a;
+ }
+ auto json_value_from_linestrings(std::vector const& lss) -> json::value {
+ json::array a;
+ for (auto const& ls : lss)
+ a.push_back(json_value_from_linestring(ls));
+ return a;
+ }
+
+ auto tag_invoke(json::value_from_tag, json::value& jv, relevant_road_closure const& clo) -> void {
+ jv = json::object{
+ {"relevant_lss", json_value_from_linestrings(clo.relevant_lss)},
+ };
+ }
+ auto tag_invoke(json::value_from_tag, json::value& jv, relevant_situation const& sit) -> void {
+ jv = json::object{
+ {"id", json::value_from(sit.id)},
+ {"location", sit.location ? json_value_from_point(*sit.location) : nullptr},
+ {"comments", json::value_from(sit.comments)},
+ {"relevant_road_closures", json::value_from(sit.relevant_road_closures)},
+ };
+ }
+ auto tag_invoke(json::value_from_tag, json::value& jv, track_segment const& seg) -> void {
+ jv = json::object{
+ {"points", json_value_from_linestring(seg.points)},
+ };
+ }
+ auto tag_invoke(json::value_from_tag, json::value& jv, track const& track) -> void {
+ jv = json::object{
+ {"segments", json::value_from(track.segments)},
+ };
+ }
+ auto tag_invoke(json::value_from_tag, json::value& jv, process_gpx_result const& res) -> void {
+ jv = json::object{
+ {"tracks", json::value_from(res.tracks)},
+ {"relevant_situations", json::value_from(res.relevant_situations)},
+ };
+ }
+ auto tag_invoke(json::value_from_tag, json::value& jv, sysinfo const& info) -> void {
+ jv = json::object{
+ {"using_publication_of", std::format("{:%FT%TZ}", info.using_publication_of)},
+ };
+ }
+
+ handler::handler(log::logger const& l, datex2::situation_publication pub)
+ : l_{l.sub("handler")}, pub_{std::move(pub)}
+ {
+ l_.info("Building indices");
+ auto const before_build = chrono::steady_clock::now();
+ for (auto const& sit : pub_.situations) {
+ for (auto const& rc : sit->road_closures) {
+ for (auto const& ls : rc->relevant_line_strings) {
+ auto box = geo::box{};
+ bgeo::envelope(*ls, box);
+ lse_index_.insert(std::make_tuple(box, ls, rc));
+ }
+ for (auto p : rc->relevant_points) {
+ p_index_.insert(std::make_pair(p, rc));
+ }
+ }
+ }
+ auto const after_build = chrono::steady_clock::now();
+ auto const dur_build = chrono::duration_cast(after_build - before_build);
+ l_.info("Indices built in {}", dur_build);
+ l_.info("LSE index size: {}", lse_index_.size());
+ l_.info("Point index size: {}", p_index_.size());
+ }
+
+ auto handler::process_gpx(gpx::file&& gpx_file) -> std::optional {
+ auto const now = chrono::utc_clock::now();
+ auto const relevant = std::initializer_list{time::period{now - chrono::days(7), now + chrono::days(7)}};
+ auto const check_periods = time::period_seq{relevant.begin(), relevant.end()};
+
+ auto splits_with_overlap_segments = std::vector{};
+ for (auto const& track : gpx_file.tracks)
+ for (auto const& seg : track.segments)
+ geo::split_linestring_with_overlap_segments(seg.waypoints, 5000 /* meters max total dist until a new split is forced */,
+ splits_with_overlap_segments);
+ auto const before_query = chrono::steady_clock::now();
+
+ l_.debug("Querying for relevant situations");
+ auto relevant_road_closures = std::unordered_set>{};
+ auto ls_checked = 0uz;
+ auto p_checked = 0uz;
+ auto i = 0;
+ for (geo::linestring const& part : splits_with_overlap_segments) {
+ l_.debug("Checking part [{}/{}]", ++i, splits_with_overlap_segments.size());
+
+ auto part_box = geo::box{};
+ bgeo::envelope(part, part_box);
+
+ for (auto it = lse_index_.qbegin(bgeo::index::intersects(part_box)); it != lse_index_.qend(); it++) {
+ // Cannot use structured bindings here, as boost::geometry::get interferes with ADL.
+ // It is a candidate as the namespace boost::geometry is part of the associated namespace set,
+ // which happens because geo::linestring ≡ boost::geometry::model::linestring is part
+ // of the whole tuple type (lse_index_value) that is the value_type of the iterator.
+ std::shared_ptr const& ls = std::get<1>(*it);
+ std::shared_ptr const& rc = std::get<2>(*it);
+ if (rc->validity && rc->validity->intersect(check_periods).periods().empty())
+ continue;
+ if (bgeo::distance(*ls, part, geo::vincenty_strategy{}) < 5.0)
+ relevant_road_closures.emplace(rc);
+ ls_checked++;
+ }
+ for (auto it = p_index_.qbegin(bgeo::index::intersects(part_box)); it != p_index_.qend(); it++) {
+ // Cannot use structured bindings here for the same reason as above.
+ geo::point const& p = std::get<0>(*it);
+ std::shared_ptr const& rc = std::get<1>(*it);
+ if (rc->validity && rc->validity->intersect(check_periods).periods().empty())
+ continue;
+ if (bgeo::distance(p, part, geo::vincenty_strategy{}) < 5.0)
+ relevant_road_closures.emplace(rc);
+ p_checked++;
+ }
+ }
+
+ auto const after_query = chrono::steady_clock::now();
+ l_.debug("Done (checked {} line string(s) and {} point(s)) in {}",
+ ls_checked, p_checked, chrono::duration_cast(after_query - before_query));
+
+ auto relevant_situations = std::unordered_set>{};
+ for (auto const& rc : relevant_road_closures)
+ relevant_situations.emplace(rc->parent);
+
+ l_.debug("Identified {} relevant road closure(s), part of {} unique situation(s)",
+ relevant_road_closures.size(), relevant_situations.size());
+ for (auto const& sit : relevant_situations)
+ l_.debug("Relevant situation: {}", sit->id);
+
+ return process_gpx_result{
+ .tracks = gpx_file.tracks
+ | views::transform([](auto const& trk) -> track {
+ return {
+ .segments = trk.segments
+ | views::transform([](auto const& seg) -> track_segment {
+ return {.points = seg.waypoints};
+ })
+ | std::ranges::to>(),
+ };
+ })
+ | std::ranges::to>(),
+ .relevant_situations = relevant_situations
+ | views::transform([&](std::shared_ptr sit) -> relevant_situation {
+ return {
+ .id = sit->id,
+ .location = sit->location,
+ .comments = sit->comments,
+ .relevant_road_closures = relevant_road_closures
+ | views::filter([&](std::shared_ptr const& rc) -> bool {
+ return std::shared_ptr{rc->parent} == sit;
+ })
+ | views::transform([](std::shared_ptr const& rc) -> relevant_road_closure {
+ return {
+ .relevant_lss = rc->relevant_line_strings
+ | views::transform([](auto const& lsp) -> geo::linestring {
+ return *lsp;
+ })
+ | std::ranges::to>(),
+ };
+ })
+ | std::ranges::to>(),
+ };
+ })
+ | std::ranges::to>(),
+ };
+ }
+
+ auto handler::sysinfo() -> struct sysinfo {
+ return {.using_publication_of = pub_.publication_time};
+ }
+
+} // namespace routemon::api
diff --git a/server/src/api.cppm b/server/src/api.cppm
new file mode 100644
index 0000000..caeb44c
--- /dev/null
+++ b/server/src/api.cppm
@@ -0,0 +1,79 @@
+module;
+
+#include
+#include
+
+export module routemon:api;
+
+import std;
+import :datex2;
+import :geo;
+import :gpx;
+import :log;
+import :time;
+import :trace;
+
+namespace {
+
+ namespace chrono = std::chrono;
+ namespace json = boost::json;
+ namespace views = std::views;
+
+} // namespace
+
+export
+namespace routemon::api {
+
+ struct relevant_road_closure {
+ std::vector relevant_lss;
+ };
+ auto tag_invoke(json::value_from_tag, json::value& jv, relevant_road_closure const& clo) -> void;
+
+ struct relevant_situation {
+ std::string id;
+ std::optional location;
+ std::vector comments;
+ std::vector relevant_road_closures;
+ };
+ auto tag_invoke(json::value_from_tag, json::value& jv, relevant_situation const& sit) -> void;
+
+ struct track_segment {
+ geo::linestring points;
+ };
+ auto tag_invoke(json::value_from_tag, json::value& jv, track_segment const& seg) -> void;
+
+ struct track {
+ std::vector segments;
+ };
+ auto tag_invoke(json::value_from_tag, json::value& jv, track const& track) -> void;
+
+ struct process_gpx_result {
+ std::vector