diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..69f6818
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,5 @@
+/proof-allconfigs/
+/build/
+/dest/
+/*.gpr
+/.config
diff --git a/COPYING b/COPYING
new file mode 100644
index 0000000..d159169
--- /dev/null
+++ b/COPYING
@@ -0,0 +1,339 @@
+                    GNU GENERAL PUBLIC LICENSE
+                       Version 2, June 1991
+
+ Copyright (C) 1989, 1991 Free Software Foundation, Inc.,
+ 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA
+ Everyone is permitted to copy and distribute verbatim copies
+ of this license document, but changing it is not allowed.
+
+                            Preamble
+
+  The licenses for most software are designed to take away your
+freedom to share and change it.  By contrast, the GNU General Public
+License is intended to guarantee your freedom to share and change free
+software--to make sure the software is free for all its users.  This
+General Public License applies to most of the Free Software
+Foundation's software and to any other program whose authors commit to
+using it.  (Some other Free Software Foundation software is covered by
+the GNU Lesser General Public License instead.)  You can apply it to
+your programs, too.
+
+  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
+this service 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.
+
+  To protect your rights, we need to make restrictions that forbid
+anyone to deny you these rights or to ask you to surrender the rights.
+These restrictions translate to certain responsibilities for you if you
+distribute copies of the software, or if you modify it.
+
+  For example, if you distribute copies of such a program, whether
+gratis or for a fee, you must give the recipients all the rights that
+you have.  You must make sure that they, too, receive or can get the
+source code.  And you must show them these terms so they know their
+rights.
+
+  We protect your rights with two steps: (1) copyright the software, and
+(2) offer you this license which gives you legal permission to copy,
+distribute and/or modify the software.
+
+  Also, for each author's protection and ours, we want to make certain
+that everyone understands that there is no warranty for this free
+software.  If the software is modified by someone else and passed on, we
+want its recipients to know that what they have is not the original, so
+that any problems introduced by others will not reflect on the original
+authors' reputations.
+
+  Finally, any free program is threatened constantly by software
+patents.  We wish to avoid the danger that redistributors of a free
+program will individually obtain patent licenses, in effect making the
+program proprietary.  To prevent this, we have made it clear that any
+patent must be licensed for everyone's free use or not licensed at all.
+
+  The precise terms and conditions for copying, distribution and
+modification follow.
+
+                    GNU GENERAL PUBLIC LICENSE
+   TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION
+
+  0. This License applies to any program or other work which contains
+a notice placed by the copyright holder saying it may be distributed
+under the terms of this General Public License.  The "Program", below,
+refers to any such program or work, and a "work based on the Program"
+means either the Program or any derivative work under copyright law:
+that is to say, a work containing the Program or a portion of it,
+either verbatim or with modifications and/or translated into another
+language.  (Hereinafter, translation is included without limitation in
+the term "modification".)  Each licensee is addressed as "you".
+
+Activities other than copying, distribution and modification are not
+covered by this License; they are outside its scope.  The act of
+running the Program is not restricted, and the output from the Program
+is covered only if its contents constitute a work based on the
+Program (independent of having been made by running the Program).
+Whether that is true depends on what the Program does.
+
+  1. You may copy and distribute 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 and disclaimer of warranty; keep intact all the
+notices that refer to this License and to the absence of any warranty;
+and give any other recipients of the Program a copy of this License
+along with the Program.
+
+You may charge a fee for the physical act of transferring a copy, and
+you may at your option offer warranty protection in exchange for a fee.
+
+  2. You may modify your copy or copies of the Program or any portion
+of it, thus forming a work based on the Program, and copy and
+distribute such modifications or work under the terms of Section 1
+above, provided that you also meet all of these conditions:
+
+    a) You must cause the modified files to carry prominent notices
+    stating that you changed the files and the date of any change.
+
+    b) You must cause any work that you distribute or publish, that in
+    whole or in part contains or is derived from the Program or any
+    part thereof, to be licensed as a whole at no charge to all third
+    parties under the terms of this License.
+
+    c) If the modified program normally reads commands interactively
+    when run, you must cause it, when started running for such
+    interactive use in the most ordinary way, to print or display an
+    announcement including an appropriate copyright notice and a
+    notice that there is no warranty (or else, saying that you provide
+    a warranty) and that users may redistribute the program under
+    these conditions, and telling the user how to view a copy of this
+    License.  (Exception: if the Program itself is interactive but
+    does not normally print such an announcement, your work based on
+    the Program is not required to print an announcement.)
+
+These requirements apply to the modified work as a whole.  If
+identifiable sections of that work are not derived from the Program,
+and can be reasonably considered independent and separate works in
+themselves, then this License, and its terms, do not apply to those
+sections when you distribute them as separate works.  But when you
+distribute the same sections as part of a whole which is a work based
+on the Program, the distribution of the whole must be on the terms of
+this License, whose permissions for other licensees extend to the
+entire whole, and thus to each and every part regardless of who wrote it.
+
+Thus, it is not the intent of this section to claim rights or contest
+your rights to work written entirely by you; rather, the intent is to
+exercise the right to control the distribution of derivative or
+collective works based on the Program.
+
+In addition, mere aggregation of another work not based on the Program
+with the Program (or with a work based on the Program) on a volume of
+a storage or distribution medium does not bring the other work under
+the scope of this License.
+
+  3. You may copy and distribute the Program (or a work based on it,
+under Section 2) in object code or executable form under the terms of
+Sections 1 and 2 above provided that you also do one of the following:
+
+    a) Accompany it with the complete corresponding machine-readable
+    source code, which must be distributed under the terms of Sections
+    1 and 2 above on a medium customarily used for software interchange; or,
+
+    b) Accompany it with a written offer, valid for at least three
+    years, to give any third party, for a charge no more than your
+    cost of physically performing source distribution, a complete
+    machine-readable copy of the corresponding source code, to be
+    distributed under the terms of Sections 1 and 2 above on a medium
+    customarily used for software interchange; or,
+
+    c) Accompany it with the information you received as to the offer
+    to distribute corresponding source code.  (This alternative is
+    allowed only for noncommercial distribution and only if you
+    received the program in object code or executable form with such
+    an offer, in accord with Subsection b above.)
+
+The source code for a work means the preferred form of the work for
+making modifications to it.  For an executable work, complete source
+code means all the source code for all modules it contains, plus any
+associated interface definition files, plus the scripts used to
+control compilation and installation of the executable.  However, as a
+special exception, the source code distributed need not include
+anything that is normally distributed (in either source or binary
+form) with the major components (compiler, kernel, and so on) of the
+operating system on which the executable runs, unless that component
+itself accompanies the executable.
+
+If distribution of executable or object code is made by offering
+access to copy from a designated place, then offering equivalent
+access to copy the source code from the same place counts as
+distribution of the source code, even though third parties are not
+compelled to copy the source along with the object code.
+
+  4. You may not copy, modify, sublicense, or distribute the Program
+except as expressly provided under this License.  Any attempt
+otherwise to copy, modify, sublicense or distribute the Program is
+void, and will automatically terminate your rights under this License.
+However, parties who have received copies, or rights, from you under
+this License will not have their licenses terminated so long as such
+parties remain in full compliance.
+
+  5. You are not required to accept this License, since you have not
+signed it.  However, nothing else grants you permission to modify or
+distribute the Program or its derivative works.  These actions are
+prohibited by law if you do not accept this License.  Therefore, by
+modifying or distributing the Program (or any work based on the
+Program), you indicate your acceptance of this License to do so, and
+all its terms and conditions for copying, distributing or modifying
+the Program or works based on it.
+
+  6. Each time you redistribute the Program (or any work based on the
+Program), the recipient automatically receives a license from the
+original licensor to copy, distribute or modify the Program subject to
+these terms and conditions.  You may not impose any further
+restrictions on the recipients' exercise of the rights granted herein.
+You are not responsible for enforcing compliance by third parties to
+this License.
+
+  7. If, as a consequence of a court judgment or allegation of patent
+infringement or for any other reason (not limited to patent issues),
+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
+distribute so as to satisfy simultaneously your obligations under this
+License and any other pertinent obligations, then as a consequence you
+may not distribute the Program at all.  For example, if a patent
+license would not permit royalty-free redistribution of the Program by
+all those who receive copies directly or indirectly through you, then
+the only way you could satisfy both it and this License would be to
+refrain entirely from distribution of the Program.
+
+If any portion of this section is held invalid or unenforceable under
+any particular circumstance, the balance of the section is intended to
+apply and the section as a whole is intended to apply in other
+circumstances.
+
+It is not the purpose of this section to induce you to infringe any
+patents or other property right claims or to contest validity of any
+such claims; this section has the sole purpose of protecting the
+integrity of the free software distribution system, which is
+implemented by public license practices.  Many people have made
+generous contributions to the wide range of software distributed
+through that system in reliance on consistent application of that
+system; it is up to the author/donor to decide if he or she is willing
+to distribute software through any other system and a licensee cannot
+impose that choice.
+
+This section is intended to make thoroughly clear what is believed to
+be a consequence of the rest of this License.
+
+  8. If the distribution and/or use of the Program is restricted in
+certain countries either by patents or by copyrighted interfaces, the
+original copyright holder who places the Program under this License
+may add an explicit geographical distribution limitation excluding
+those countries, so that distribution is permitted only in or among
+countries not thus excluded.  In such case, this License incorporates
+the limitation as if written in the body of this License.
+
+  9. The Free Software Foundation may publish revised and/or new versions
+of the 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 a version number of this License which applies to it and "any
+later version", you have the option of following the terms and conditions
+either of that version or of any later version published by the Free
+Software Foundation.  If the Program does not specify a version number of
+this License, you may choose any version ever published by the Free Software
+Foundation.
+
+  10. If you wish to incorporate parts of the Program into other free
+programs whose distribution conditions are different, write to the author
+to ask for permission.  For software which is copyrighted by the Free
+Software Foundation, write to the Free Software Foundation; we sometimes
+make exceptions for this.  Our decision will be guided by the two goals
+of preserving the free status of all derivatives of our free software and
+of promoting the sharing and reuse of software generally.
+
+                            NO WARRANTY
+
+  11. BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE, 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.
+
+  12. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING
+WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY AND/OR
+REDISTRIBUTE 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.
+
+                     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
+convey the exclusion of warranty; and each file should have at least
+the "copyright" line and a pointer to where the full notice is found.
+
+    <one line to give the program's name and a brief idea of what it does.>
+    Copyright (C) <year>  <name of author>
+
+    This program is free software; you can redistribute it and/or modify
+    it under the terms of the GNU General Public License as published by
+    the Free Software Foundation; either version 2 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 General Public License for more details.
+
+    You should have received a copy of the GNU General Public License along
+    with this program; if not, write to the Free Software Foundation, Inc.,
+    51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
+
+Also add information on how to contact you by electronic and paper mail.
+
+If the program is interactive, make it output a short notice like this
+when it starts in an interactive mode:
+
+    Gnomovision version 69, Copyright (C) year name of author
+    Gnomovision comes with ABSOLUTELY NO WARRANTY; for details type `show w'.
+    This is free software, and you are welcome to redistribute it
+    under certain conditions; type `show c' for details.
+
+The hypothetical commands `show w' and `show c' should show the appropriate
+parts of the General Public License.  Of course, the commands you use may
+be called something other than `show w' and `show c'; they could even be
+mouse-clicks or menu items--whatever suits your program.
+
+You should also get your employer (if you work as a programmer) or your
+school, if any, to sign a "copyright disclaimer" for the program, if
+necessary.  Here is a sample; alter the names:
+
+  Yoyodyne, Inc., hereby disclaims all copyright interest in the program
+  `Gnomovision' (which makes passes at compilers) written by James Hacker.
+
+  <signature of Ty Coon>, 1 April 1989
+  Ty Coon, President of Vice
+
+This General Public License does not permit incorporating your program into
+proprietary programs.  If your program is a subroutine library, you may
+consider it more useful to permit linking proprietary applications with the
+library.  If this is what you want to do, use the GNU Lesser General
+Public License instead of this License.
diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..2509b58
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,268 @@
+libhw-dir := $(dir $(lastword $(MAKEFILE_LIST)))
+
+DESTDIR ?= dest
+
+name ?= hw
+hw-install = Makefile Makefile.proof gnat.adc spark.adc
+
+top := $(CURDIR)
+cnf := .config
+obj := build
+
+binary := $(obj)/lib$(name).a
+$(binary):
+
+space :=
+space +=
+comma := ,
+
+$(foreach dep,$($(name)-deplibs), \
+	$(eval -include $($(dep)-dir)/config))
+-include $(cnf)
+
+include $(libhw-dir)/Makefile.proof
+
+CC       = $(CROSS_COMPILE)gcc
+GNATBIND = $(CROSS_COMPILE)gnatbind
+
+ADAFLAGS += -gnatA -gnatec=$(libhw-dir)/gnat.adc
+ADAFLAGS += -gnatg -gnatp
+ADAFLAGS += -Wuninitialized -Wall -Werror
+ADAFLAGS += -pipe -g
+ADAFLAGS += -Wstrict-aliasing -Wshadow
+ADAFLAGS += -fno-common -fomit-frame-pointer
+ADAFLAGS += -ffunction-sections -fdata-sections
+# Ada warning options:
+#
+#  a   Activate most optional warnings.
+# .e   Activate every optional warnings.
+#  e   Treat warnings and style checks as errors.
+#
+#  D   Suppress warnings on implicit dereferences:
+#      As SPARK does not accept access types we have to map the
+#      dynamically chosen register locations to a static SPARK
+#      variable.
+#
+# .H   Suppress warnings on holes/gaps in records:
+#      We are modelling hardware here!
+#
+#  H   Suppress warnings on hiding:
+#      It's too annoying, you run out of ideas for identifiers fast.
+#
+#  T   Suppress warnings for tracking of deleted conditional code:
+#      We use static options to select code paths at compile time.
+#
+#  U   Suppress warnings on unused entities:
+#      Would have lots of warnings for unused register definitions,
+#      `withs` for debugging etc.
+#
+# .U   Deactivate warnings on unordered enumeration types:
+#      As SPARK doesn't support `pragma Ordered` by now, we don't
+#      use that, yet.
+#
+# .W   Suppress warnings on unnecessary Warnings Off pragmas:
+#      Things get really messy when you use different compiler
+#      versions, otherwise.
+# .Y   Disable information messages for why package spec needs body:
+#      Those messages are annoying. But don't forget to enable those,
+#      if you need the information.
+ADAFLAGS += -gnatwa.eeD.HHTU.U.W.Y
+# Disable style checks for now
+ADAFLAGS += -gnatyN
+
+MAKEFLAGS += -rR
+
+# Make is silent per default, but 'make V=1' will show all compiler calls.
+ifneq ($(V),1)
+.SILENT:
+endif
+
+# must come rather early
+.SECONDEXPANSION:
+
+$(binary): $$($(name)-objs)
+	@printf "    AR         $(subst $(obj)/,,$@)\n"
+	ar cr $@ $^
+
+$(foreach dep,$($(name)-deplibs), \
+	$(eval $(name)-extra-objs += $($(dep)-dir)/lib) \
+	$(eval $(name)-extra-incs += $($(dep)-dir)/include))
+
+# Converts one or more source file paths to their corresponding build/ paths.
+# Only .ads and .adb get converted to .o, other files keep their names.
+# $1 file path (list)
+src-to-obj = \
+	$(addprefix $(obj)/,\
+	$(patsubst $(obj)/%,%, \
+	$(patsubst %.ads,%.o,\
+	$(patsubst %.adb,%.o,\
+	$(2)))))
+
+# Converts one or more source file paths to the corresponding build/ paths
+# of their Ada library information (.ali) files.
+# $1 file path (list)
+src-to-ali = \
+	$(addprefix $(obj)/,\
+	$(patsubst $(obj)/%,%, \
+	$(patsubst %.ads,%.ali,\
+	$(patsubst %.adb,%.ali,\
+	$(filter %.ads %.adb,$(2))))))
+
+# Clean -y variables, include Makefile.inc
+# Add paths to files in $(name)-y to $(name)-srcs
+# Add subdirs-y to subdirs
+# $1 dir to read Makefile.inc from
+includemakefile = \
+	$(eval $(name)-y :=) \
+	$(eval $(name)-gen-y :=) \
+	$(eval $(name)-proof-y :=) \
+	$(eval subdirs-y :=) \
+	$(eval include $(1)/Makefile.inc) \
+	$(eval $(name)-srcs += \
+		$(subst $(top)/,, \
+		$(abspath $(addprefix $(1)/,$($(name)-y))))) \
+	$(eval $(name)-gens += \
+		$(subst $(top)/,, \
+		$(abspath $($(name)-gen-y)))) \
+	$(eval $(name)-proof += \
+		$(subst $(top)/,, \
+		$(abspath $(addprefix $(1)/,$($(name)-proof-y))))) \
+	$(eval subdirs += \
+		$(subst $(top)/,, \
+		$(abspath $(addprefix $(1)/,$(subdirs-y))))) \
+
+# For each path in $(subdirs) call includemakefiles
+# Repeat until subdirs is empty
+evaluate_subdirs = \
+	$(eval cursubdirs := $(subdirs)) \
+	$(eval subdirs :=) \
+	$(foreach dir,$(cursubdirs), \
+		$(call includemakefile,$(dir))) \
+	$(if $(subdirs), \
+		$(call evaluate_subdirs))
+
+# collect all object files eligible for building
+subdirs := .
+$(call evaluate_subdirs)
+
+# Eliminate duplicate mentions of source files
+$(name)-srcs := $(sort $($(name)-srcs))
+$(name)-gens := $(sort $($(name)-gens))
+
+# For Ada includes
+$(name)-ada-dirs := $(sort $(dir $(filter %.ads %.adb,$($(name)-srcs) $($(name)-gens))))
+
+# To track dependencies, we need all Ada specification (.ads) files in
+# *-srcs. Extract / filter all specification files that have a matching
+# body (.adb) file here (specifications without a body are valid sources
+# in Ada).
+$(name)-extra-specs := \
+	$(filter \
+		$(addprefix %/,$(patsubst %.adb,%.ads,$(notdir $(filter %.adb,$($(name)-srcs))))), \
+		$(filter %.ads,$($(name)-srcs) $($(name)-gens)))
+$(name)-srcs := $(filter-out $($(name)-extra-specs),$($(name)-srcs))
+$(name)-gens := $(filter-out $($(name)-extra-specs),$($(name)-gens))
+
+$(name)-objs := $(call src-to-obj,,$($(name)-srcs) $($(name)-gens))
+$(name)-alis := $(call src-to-ali,,$($(name)-srcs) $($(name)-gens))
+
+# For gnatprove
+$(name)-proof-dirs := \
+	$(sort	$(dir $($(name)-proof)) \
+		$(filter-out ada/% %/ada/%,$($(name)-ada-dirs)))
+
+# For mkdir
+alldirs := $(abspath $(dir $(sort $($(name)-objs))))
+
+# Reads dependencies from an Ada library information (.ali) file
+# Only basenames (with suffix) are preserved so we have to look the
+# paths up in $($(name)-srcs) $($(name)-gens).
+# $1 ali file
+create_ada_deps = \
+	$(if $(wildcard $(1)),\
+		$(filter \
+			$(addprefix %/,$(shell sed -ne's/^D \([^\t]\+\).*$$/\1/p' $(1) 2>/dev/null)), \
+			$($(name)-srcs) $($(name)-gens) $($(name)-extra-specs)), \
+		$($(name)-gens))
+
+# Adds dependency rules
+# $1 source file
+add_ada_deps = \
+	$(call src-to-obj,,$(1)): $(1) \
+		$(call create_ada_deps,$(call src-to-ali,,$(1)))
+
+# Writes a compilation rule for a source type
+# $1 source type (ads, adb)
+# $2 source files (including the colon)
+# $3 obj path prefix (including the trailing slash)
+define add_ada_rule
+$(2) $(3)%.o: %.$(1)
+	@printf "    COMPILE    $$(subst $(obj)/,,$$@)\n"
+	$(CC) \
+		$(ADAFLAGS) $(addprefix -I,$($(name)-ada-dirs) $($(name)-extra-incs)) \
+		-c -o $$@ $$<
+endef
+
+# For sources
+$(foreach type,ads adb, \
+	$(eval $(call add_ada_rule,$(type),$(call src-to-obj,,$(filter %.$(type),$($(name)-srcs))):,$(obj)/)))
+$(foreach file,$($(name)-srcs) $($(name)-gens), \
+	$(eval $(call add_ada_deps,$(file))))
+
+# For generated sources already in $(obj)/
+$(foreach type,ads adb, \
+	$(eval $(call add_ada_rule,$(type),$(call src-to-obj,,$(filter %.$(type),$($(name)-gens))):,)))
+
+# Ali files are generated along with the object file. They need an empty
+# recipe for correct updating.
+$($(name)-alis): %.ali: %.o ;
+
+# To support complex package initializations, we need to call the
+# emitted code explicitly. gnatbind gathers all the calls for us
+# and exports them as a procedure $(name)_adainit(). Every stage that
+# uses Ada code has to call it!
+$(obj)/b__lib$(name).adb: $($(name)-alis)
+	@printf "    BIND       $(subst $(obj)/,,$@)\n"
+	# We have to give gnatbind a simple filename (without leading
+	# path components) so just cd there.
+	cd $(dir $@) && \
+		$(GNATBIND) $(addprefix -aO,$(abspath $($(name)-extra-objs))) \
+			-a -n -L$(name)_ada -o $(notdir $@) \
+			$(subst $(dir $@),,$^)
+$(eval $(call add_ada_rule,adb,$(obj)/b__lib$(name).o:,))
+$(name)-objs += $(obj)/b__lib$(name).o
+
+$(shell mkdir -p $(alldirs))
+
+$(name)-install-srcs = $(sort \
+	$($(name)-extra-specs) $(filter %.ads,$($(name)-srcs)) \
+	$(foreach adb,$(filter %.adb,$($(name)-srcs)), \
+		$(shell grep -q '^U .*\<BN\>' $(call src-to-ali,,$(adb)) 2>/dev/null && echo $(adb))))
+
+$(name)-install-proof = \
+	$(filter $(addprefix %/,$(notdir $($(name)-install-srcs))),$($(name)-proof)) \
+	$(filter-out $(addprefix %/,$(notdir $($(name)-proof))),$($(name)-install-srcs))
+
+install: $(binary) $($(name)-alis) $(libgpr)
+	install -d $(DESTDIR)/lib $(DESTDIR)/include $(DESTDIR)/proof
+	printf "    INSTALL    $(subst $(obj)/,,$(binary))\n"
+	install $(binary) $(DESTDIR)/lib/
+	$(foreach file,$($(name)-install) $(libgpr), \
+		printf "    INSTALL    $(subst $(obj)/,,$(file))\n"; \
+		install $(file) $(DESTDIR);)
+	printf "    INSTALL    $(cnf)\n"
+	install $(cnf) $(DESTDIR)/config
+	printf "    INSTALL    %s\n" $(subst $(obj)/,,$($(name)-alis))
+	install $($(name)-alis) $(DESTDIR)/lib/
+	printf "    INSTALL    %s\n" $(subst $(obj)/,,$($(name)-install-srcs))
+	install $($(name)-install-srcs) $(DESTDIR)/include/
+	printf "    INSTALL    %s\n" $(subst $(obj)/,,$($(name)-install-proof))
+	install $($(name)-install-proof) $(DESTDIR)/proof/
+
+clean::
+	rm -rf $(obj) $(name).gpr
+
+distclean: clean
+	rm -rf dest
+
+.PHONY: install clean distclean
diff --git a/Makefile.inc b/Makefile.inc
new file mode 100644
index 0000000..d4fac0b
--- /dev/null
+++ b/Makefile.inc
@@ -0,0 +1,2 @@
+subdirs-y += ada common proof
+subdirs-y += debug
diff --git a/Makefile.proof b/Makefile.proof
new file mode 100644
index 0000000..91b98c9
--- /dev/null
+++ b/Makefile.proof
@@ -0,0 +1,97 @@
+PROOF_MODE ?= all
+
+jobs ?= 4
+
+$(foreach dep,$($(name)-deplibs), \
+	$(eval SPARKFLAGS += -aP=$($(dep)-dir)))
+
+SPARKFLAGS += -j$(jobs)
+SPARKFLAGS += -k
+SPARKFLAGS += -m
+SPARKFLAGS += --mode=$(PROOF_MODE)
+SPARKFLAGS += --report=fail
+SPARKFLAGS += --warnings=error
+SPARKFLAGS += --prover=cvc4,z3 --steps=500 --timeout=1	# FIXME: timeout used because steps seems broken
+
+quote-list = $(subst $(space),$(comma),$(patsubst %,"%",$(1)))
+
+$(name)-exclude-srcs = \
+	$(filter-out \
+		$(sort $(notdir $($(name)-proof) $($(name)-srcs) $($(name)-gens) $($(name)-extra-specs))), \
+		$(sort $(notdir \
+			$(wildcard $(addsuffix *.ad[sb],$($(name)-proof-dirs))))))
+
+# Has to reside in the working directory. gnatprove takes paths relative
+# to the directory wher it's placed and reports internal errors if used
+# with absolute paths.
+gpr := $(name).gpr
+gpr-name = $(subst -,_,$(subst .,_,$(basename $(notdir $@))))
+
+# Will be installed for inclusion
+libgpr := $(obj)/lib$(name).gpr
+
+.SECONDEXPANSION:
+
+$(gpr):
+	@printf "    GENERATE   $(subst $(obj)/,,$@)\n"
+	printf '$(if $($(name)-deplibs),with "%s";\n)' $($(name)-deplibs) >$@
+	echo 'library project $(gpr-name) is'			>>$@
+	echo '   for Library_Name use "$(name)";'		>>$@
+	echo '   for Library_Dir use "$(obj)/adalib";'		>>$@
+	echo '   for Source_Dirs use' \
+		'($(call quote-list,$($(name)-proof-dirs)));'	>>$@
+	echo '   for Object_Dir use "$(obj)";'			>>$@
+	echo '   package Builder is'				>>$@
+	echo '      for Global_Configuration_Pragmas use' \
+		'"$(abspath $(libhw-dir)/spark.adc)";'		>>$@
+	echo '   end Builder;'					>>$@
+	echo '   for Excluded_Source_Files use' \
+		'($(call quote-list,$($(name)-exclude-srcs)));' >>$@
+	echo 'end $(gpr-name);'					>>$@
+
+.INTERMEDIATE: $(gpr)
+
+$(libgpr): $$(MAKEFILE_LIST)
+	@printf "    GENERATE   $(subst $(obj)/,,$@)\n"
+	printf '$(if $($(name)-deplibs),with "%s";\n)' $($(name)-deplibs) >$@
+	echo 'library project lib$(name) is'			>>$@
+	echo '   for Library_Name use "$(name)";'		>>$@
+	echo '   for Library_Dir use "lib";'			>>$@
+	echo '   for Library_ALI_Dir use "lib";'		>>$@
+	echo '   for Source_Dirs use ("proof");'		>>$@
+	echo '   for Object_Dir use external ("obj", "build");'	>>$@
+	echo 'end lib$(name);'					>>$@
+
+$(obj)/gnatprove/gnatprove.out: $(gpr) $$($(name)-gens) $(obj)/proofmode
+	gnatprove -P$< $(SPARKFLAGS) -Xobj=$(abspath $(obj))
+
+proof:
+	if [ "$(PROOF_MODE)" != "$$(cat $(obj)/proofmode 2>/dev/null)" ]; then \
+		echo "$(PROOF_MODE)" >$(obj)/proofmode; \
+	fi
+	$(MAKE) $(obj)/gnatprove/gnatprove.out
+
+check: export override PROOF_MODE=check
+check: proof
+
+flow: export override PROOF_MODE=flow
+flow: proof
+
+full: export override PROOF_MODE=all
+full: proof
+
+allconfigs = $(wildcard configs/*)
+allconfigs-targets = $(addprefix allconfigs-,$(notdir $(allconfigs)))
+
+$(allconfigs-targets): allconfigs-%: configs/%
+	rm -rf proof-allconfigs/$* $(name)_$*.gpr
+	mkdir -p proof-allconfigs/$*
+	echo "$(PROOF_MODE)" >proof-allconfigs/$*/proofmode
+	$(MAKE) obj=proof-allconfigs/$* cnf=configs/$* gpr=$(name)_$*.gpr jobs=1 proof-allconfigs/$*/gnatprove/gnatprove.out
+
+proof-allconfigs: $(allconfigs-targets)
+
+clean::
+	rm -rf proof-allconfigs/
+
+.PHONY: proof check flow full $(allconfigs-targets) proof-allconfigs
diff --git a/ada/Makefile.inc b/ada/Makefile.inc
new file mode 100644
index 0000000..e09f1a5
--- /dev/null
+++ b/ada/Makefile.inc
@@ -0,0 +1,3 @@
+hw-$(CONFIG_HWBASE_STATIC_MMIO) += static_mmio/hw-mmio_range.adb
+hw-$(CONFIG_HWBASE_DYNAMIC_MMIO) += dynamic_mmio/hw-mmio_range.adb
+hw-$(CONFIG_HWBASE_TIMER_CLOCK_GETTIME) += clock_gettime/hw-time-timer.adb
diff --git a/ada/clock_gettime/hw-time-timer.adb b/ada/clock_gettime/hw-time-timer.adb
new file mode 100644
index 0000000..914b201
--- /dev/null
+++ b/ada/clock_gettime/hw-time-timer.adb
@@ -0,0 +1,61 @@
+--
+-- Copyright (C) 2016 secunet Security Networks AG
+--
+-- This program is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; version 2 of the License.
+--
+-- 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 General Public License for more details.
+--
+
+with Interfaces.C;
+
+use type Interfaces.C.long;
+
+package body HW.Time.Timer
+with
+   Refined_State => (Timer_State => null,
+                     Abstract_Time => null)
+is
+   CLOCK_MONOTONIC_RAW : constant := 4;
+
+   subtype Clock_ID_T is Interfaces.C.int;
+   subtype Time_T is Interfaces.C.long;
+
+   type Struct_Timespec is record
+      TV_Sec   : aliased Time_T;
+      TV_NSec  : aliased Interfaces.C.long;
+   end record;
+   pragma Convention (C_Pass_By_Copy, Struct_Timespec);
+
+   function Clock_Gettime
+     (Clock_ID :        Clock_ID_T;
+      Timespec : access Struct_Timespec)
+      return Interfaces.C.int;
+   pragma Import (C, Clock_Gettime, "clock_gettime");
+
+   function Raw_Value_Min return T
+   is
+      Ignored : Interfaces.C.int;
+      Timespec : aliased Struct_Timespec;
+   begin
+      Ignored := Clock_Gettime (CLOCK_MONOTONIC_RAW, Timespec'Access);
+      return T (Timespec.TV_Sec * 1_000_000_000 + Timespec.TV_NSec);
+   end Raw_Value_Min;
+
+   function Raw_Value_Max return T
+   is
+   begin
+      return Raw_Value_Min + 1;
+   end Raw_Value_Max;
+
+   function Hz return T
+   is
+   begin
+      return 1_000_000_000; -- clock_gettime(2) is fixed to nanoseconds
+   end Hz;
+
+end HW.Time.Timer;
diff --git a/ada/dynamic_mmio/hw-mmio_range.adb b/ada/dynamic_mmio/hw-mmio_range.adb
new file mode 100644
index 0000000..78cc048
--- /dev/null
+++ b/ada/dynamic_mmio/hw-mmio_range.adb
@@ -0,0 +1,76 @@
+--
+-- Copyright (C) 2015-2016 secunet Security Networks AG
+--
+-- This program is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; version 2 of the License.
+--
+-- 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 General Public License for more details.
+--
+
+with HW.Debug;
+with GNAT.Source_Info;
+with System.Storage_Elements;
+with System.Address_To_Access_Conversions;
+
+package body HW.MMIO_Range
+with
+   Refined_State =>
+     (State => Range_A,       -- the contents accessed
+      Base_Address => null)   -- the address, so actually Range_A too
+is
+   pragma Warnings (Off, "implicit dereference",
+                    Reason => "This is what this package is about.");
+
+   Debug_Reads    : constant Boolean := False;
+   Debug_Writes   : constant Boolean := False;
+
+   type Range_Access is access all Array_T;
+   package Conv_Range is new System.Address_To_Access_Conversions (Array_T);
+
+   Range_A : Range_Access :=
+      Range_Access (Conv_Range.To_Pointer (System'To_Address (Base_Addr)))
+   with Volatile;
+
+   procedure Read (Value : out Element_T; Index : in Index_T)
+   is
+      use type Word32;
+   begin
+      Value := Range_A (Index);
+      pragma Debug (Debug_Reads, Debug.Put
+        (GNAT.Source_Info.Enclosing_Entity & ":  "));
+      pragma Debug (Debug_Reads, Debug.Put_Word32 (Word32 (Value)));
+      pragma Debug (Debug_Reads, Debug.Put (" <- "));
+      pragma Debug (Debug_Reads, Debug.Put_Word32
+        (Word32 (System.Storage_Elements.To_Integer
+           (Conv_Range.To_Address (Conv_Range.Object_Pointer (Range_A)))) +
+         Word32 (Index) * (Element_T'Size / 8)));
+      pragma Debug (Debug_Reads, Debug.New_Line);
+   end Read;
+
+   procedure Write (Index : in Index_T; Value : in Element_T)
+   is
+      use type Word32;
+   begin
+      pragma Debug (Debug_Writes, Debug.Put
+        (GNAT.Source_Info.Enclosing_Entity & ": "));
+      pragma Debug (Debug_Writes, Debug.Put_Word32 (Word32 (Value)));
+      pragma Debug (Debug_Writes, Debug.Put (" -> "));
+      pragma Debug (Debug_Writes, Debug.Put_Word32
+        (Word32 (System.Storage_Elements.To_Integer
+           (Conv_Range.To_Address (Conv_Range.Object_Pointer (Range_A)))) +
+         Word32 (Index) * (Element_T'Size / 8)));
+      pragma Debug (Debug_Writes, Debug.New_Line);
+      Range_A (Index) := Value;
+   end Write;
+
+   procedure Set_Base_Address (Base : Word64) is
+   begin
+      Range_A := Range_Access
+        (Conv_Range.To_Pointer (System'To_Address (Base)));
+   end Set_Base_Address;
+
+end HW.MMIO_Range;
diff --git a/ada/static_mmio/hw-mmio_range.adb b/ada/static_mmio/hw-mmio_range.adb
new file mode 100644
index 0000000..fb72152
--- /dev/null
+++ b/ada/static_mmio/hw-mmio_range.adb
@@ -0,0 +1,35 @@
+--
+-- Copyright (C) 2016 secunet Security Networks AG
+--
+-- This program is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; version 2 of the License.
+--
+-- 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 General Public License for more details.
+--
+
+package body HW.MMIO_Range
+with
+   Refined_State =>
+     (State => MMIO,
+      Base_Address => null)
+is
+
+   MMIO : Array_T with Volatile, Address => System'To_Address (Base_Addr);
+
+   procedure Read (Value : out Element_T; Index : in Index_T) is
+   begin
+      Value := MMIO (Index);
+   end Read;
+
+   procedure Write (Index : in Index_T; Value : in Element_T) is
+   begin
+      MMIO (Index) := Value;
+   end Write;
+
+   procedure Set_Base_Address (Base : Word64) is null;
+
+end HW.MMIO_Range;
diff --git a/common/Makefile.inc b/common/Makefile.inc
new file mode 100644
index 0000000..b8e4f35
--- /dev/null
+++ b/common/Makefile.inc
@@ -0,0 +1,10 @@
+hw-y += hw.ads
+hw-y += hw-mmio_range.ads
+hw-y += hw-mmio_regs.adb
+hw-y += hw-mmio_regs.ads
+hw-y += hw-port_io.adb
+hw-y += hw-port_io.ads
+hw-y += hw-sub_regs.ads
+hw-y += hw-time.ads
+hw-y += hw-time.adb
+hw-y += hw-time-timer.ads
diff --git a/common/hw-mmio_range.ads b/common/hw-mmio_range.ads
new file mode 100644
index 0000000..1b33630
--- /dev/null
+++ b/common/hw-mmio_range.ads
@@ -0,0 +1,35 @@
+--
+-- Copyright (C) 2015-2016 secunet Security Networks AG
+--
+-- This program is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; version 2 of the License.
+--
+-- 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 General Public License for more details.
+--
+
+with System;
+
+generic
+   Base_Addr : Word64;
+   type Element_T is mod <>;
+   type Index_T is range <>;
+   type Array_T is array (Index_T) of Element_T;
+package HW.MMIO_Range
+with
+   Abstract_State =>
+     ((State with External),
+      Base_Address),
+   Initializes => Base_Address
+is
+
+   procedure Read (Value : out Element_T; Index : in Index_T);
+
+   procedure Write (Index : in Index_T; Value : in Element_T);
+
+   procedure Set_Base_Address (Base : Word64);
+
+end HW.MMIO_Range;
diff --git a/common/hw-mmio_regs.adb b/common/hw-mmio_regs.adb
new file mode 100644
index 0000000..5eea563
--- /dev/null
+++ b/common/hw-mmio_regs.adb
@@ -0,0 +1,92 @@
+--
+-- Copyright (C) 2016 secunet Security Networks AG
+--
+-- This program is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; version 2 of the License.
+--
+-- 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 General Public License for more details.
+--
+
+package body HW.MMIO_Regs
+is
+
+   generic
+      type Word_T is mod <>;
+   procedure Read_G (Value : out Word_T; Idx : Subs_P.Index_T);
+
+   procedure Read_G (Value : out Word_T; Idx : Subs_P.Index_T)
+   is
+      Off : constant Range_P.Index_T := Range_P.Index_T
+        ((Byte_Offset + Regs (Idx).Byte_Offset) / (Range_P.Element_T'Size / 8));
+      pragma Warnings
+        (GNAT, Off, """Mask"" is not modified, could be declared constant",
+         Reason => "Ada RM forbids making it constant.");
+      Mask : Word64 := Shift_Left (1, Regs (Idx).MSB + 1 - Regs (Idx).LSB) - 1;
+      pragma Warnings
+        (GNAT, On, """Mask"" is not modified, could be declared constant");
+      Temp : Range_P.Element_T;
+   begin
+      Range_P.Read (Temp, Off);
+      Value := Word_T (Shift_Right (Word64 (Temp), Regs (Idx).LSB) and Mask);
+   end Read_G;
+
+   procedure Read_I is new Read_G (Word8);
+   procedure Read (Value : out Word8; Idx : Subs_P.Index_T) renames Read_I;
+
+   procedure Read_I is new Read_G (Word16);
+   procedure Read (Value : out Word16; Idx : Subs_P.Index_T) renames Read_I;
+
+   procedure Read_I is new Read_G (Word32);
+   procedure Read (Value : out Word32; Idx : Subs_P.Index_T) renames Read_I;
+
+   procedure Read_I is new Read_G (Word64);
+   procedure Read (Value : out Word64; Idx : Subs_P.Index_T) renames Read_I;
+
+   ----------------------------------------------------------------------------
+
+   generic
+      type Word_T is mod <>;
+   procedure Write_G (Idx : Subs_P.Index_T; Value : Word_T);
+
+   procedure Write_G (Idx : Subs_P.Index_T; Value : Word_T)
+   is
+      Off : constant Range_P.Index_T := Range_P.Index_T
+        ((Byte_Offset + Regs (Idx).Byte_Offset) / (Range_P.Element_T'Size / 8));
+      pragma Warnings
+        (GNAT, Off, """Mask"" is not modified, could be declared constant",
+         Reason => "Ada RM forbids making it constant.");
+      Mask : Word64 :=
+         Shift_Left (1, Regs (Idx).MSB + 1) - Shift_Left (1, Regs (Idx).LSB);
+      pragma Warnings
+        (GNAT, On, """Mask"" is not modified, could be declared constant");
+      Temp : Range_P.Element_T;
+   begin
+      if Regs (Idx).MSB - Regs (Idx).LSB + 1 = Range_P.Element_T'Size then
+         Range_P.Write (Off, Range_P.Element_T (Value));
+      else
+         -- read/modify/write
+         Range_P.Read (Temp, Off);
+         Temp := Range_P.Element_T
+           ((Word64 (Temp) and not Mask) or
+            (Shift_Left (Word64 (Value), Regs (Idx).LSB)));
+         Range_P.Write (Off, Temp);
+      end if;
+   end Write_G;
+
+   procedure Write_I is new Write_G (Word8);
+   procedure Write (Idx : Subs_P.Index_T; Value : Word8) renames Write_I;
+
+   procedure Write_I is new Write_G (Word16);
+   procedure Write (Idx : Subs_P.Index_T; Value : Word16) renames Write_I;
+
+   procedure Write_I is new Write_G (Word32);
+   procedure Write (Idx : Subs_P.Index_T; Value : Word32) renames Write_I;
+
+   procedure Write_I is new Write_G (Word64);
+   procedure Write (Idx : Subs_P.Index_T; Value : Word64) renames Write_I;
+
+end HW.MMIO_Regs;
diff --git a/common/hw-mmio_regs.ads b/common/hw-mmio_regs.ads
new file mode 100644
index 0000000..9aafed9
--- /dev/null
+++ b/common/hw-mmio_regs.ads
@@ -0,0 +1,127 @@
+--
+-- Copyright (C) 2016 secunet Security Networks AG
+--
+-- This program is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; version 2 of the License.
+--
+-- 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 General Public License for more details.
+--
+
+with HW.Sub_Regs;
+with HW.MMIO_Range;
+
+use type HW.Word64;
+
+generic
+   with package Range_P is new MMIO_Range (<>);
+   Byte_Offset_O : Natural := 0;
+
+   with package Subs_P is new Sub_Regs (<>);
+   Regs : Subs_P.Array_T;
+
+package HW.MMIO_Regs
+is
+
+   Byte_Offset : Natural := Byte_Offset_O;
+
+   ----------------------------------------------------------------------------
+
+   procedure Read (Value : out Word8; Idx : Subs_P.Index_T)
+   with
+      Pre =>   ((Byte_Offset + Regs (Idx).Byte_Offset) /
+                (Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
+               ((Byte_Offset + Regs (Idx).Byte_Offset) /
+                (Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
+               Range_P.Element_T'Size <= Word64'Size and
+               Regs (Idx).MSB < Range_P.Element_T'Size and
+               Regs (Idx).MSB >= Regs (Idx).LSB and
+               Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Word8'Size;
+
+   procedure Read (Value : out Word16; Idx : Subs_P.Index_T)
+   with
+      Pre =>   ((Byte_Offset + Regs (Idx).Byte_Offset) /
+                (Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
+               ((Byte_Offset + Regs (Idx).Byte_Offset) /
+                (Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
+               Range_P.Element_T'Size <= Word64'Size and
+               Regs (Idx).MSB < Range_P.Element_T'Size and
+               Regs (Idx).MSB >= Regs (Idx).LSB and
+               Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Word16'Size;
+
+   procedure Read (Value : out Word32; Idx : Subs_P.Index_T)
+   with
+      Pre =>   ((Byte_Offset + Regs (Idx).Byte_Offset) /
+                (Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
+               ((Byte_Offset + Regs (Idx).Byte_Offset) /
+                (Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
+               Range_P.Element_T'Size <= Word64'Size and
+               Regs (Idx).MSB < Range_P.Element_T'Size and
+               Regs (Idx).MSB >= Regs (Idx).LSB and
+               Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Word32'Size;
+
+   procedure Read (Value : out Word64; Idx : Subs_P.Index_T)
+   with
+      Pre =>   ((Byte_Offset + Regs (Idx).Byte_Offset) /
+                (Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
+               ((Byte_Offset + Regs (Idx).Byte_Offset) /
+                (Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
+               Range_P.Element_T'Size <= Word64'Size and
+               Regs (Idx).MSB < Range_P.Element_T'Size and
+               Regs (Idx).MSB >= Regs (Idx).LSB and
+               Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Word64'Size;
+
+   ----------------------------------------------------------------------------
+
+   procedure Write (Idx : Subs_P.Index_T; Value : Word8)
+   with
+      Pre =>   ((Byte_Offset + Regs (Idx).Byte_Offset) /
+                (Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
+               ((Byte_Offset + Regs (Idx).Byte_Offset) /
+                (Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
+               Range_P.Element_T'Size <= Word64'Size and
+               Regs (Idx).MSB < Range_P.Element_T'Size and
+               Regs (Idx).MSB >= Regs (Idx).LSB and
+               Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Value'Size and
+               Word64 (Value) < Word64 (2 ** (Regs (Idx).MSB + 1 - Regs (Idx).LSB));
+
+   procedure Write (Idx : Subs_P.Index_T; Value : Word16)
+   with
+      Pre =>   ((Byte_Offset + Regs (Idx).Byte_Offset) /
+                (Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
+               ((Byte_Offset + Regs (Idx).Byte_Offset) /
+                (Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
+               Range_P.Element_T'Size <= Word64'Size and
+               Regs (Idx).MSB < Range_P.Element_T'Size and
+               Regs (Idx).MSB >= Regs (Idx).LSB and
+               Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Value'Size and
+               Word64 (Value) < Word64 (2 ** (Regs (Idx).MSB + 1 - Regs (Idx).LSB));
+
+   procedure Write (Idx : Subs_P.Index_T; Value : Word32)
+   with
+      Pre =>   ((Byte_Offset + Regs (Idx).Byte_Offset) /
+                (Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
+               ((Byte_Offset + Regs (Idx).Byte_Offset) /
+                (Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
+               Range_P.Element_T'Size <= Word64'Size and
+               Regs (Idx).MSB < Range_P.Element_T'Size and
+               Regs (Idx).MSB >= Regs (Idx).LSB and
+               Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Value'Size and
+               Word64 (Value) < Word64 (2 ** (Regs (Idx).MSB + 1 - Regs (Idx).LSB));
+
+   procedure Write (Idx : Subs_P.Index_T; Value : Word64)
+   with
+      Pre =>   ((Byte_Offset + Regs (Idx).Byte_Offset) /
+                (Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
+               ((Byte_Offset + Regs (Idx).Byte_Offset) /
+                (Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
+               Range_P.Element_T'Size <= Word64'Size and
+               Regs (Idx).MSB < Range_P.Element_T'Size and
+               Regs (Idx).MSB >= Regs (Idx).LSB and
+               Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Value'Size and
+               Word64 (Value) < Word64 (2 ** (Regs (Idx).MSB + 1 - Regs (Idx).LSB));
+
+end HW.MMIO_Regs;
diff --git a/common/hw-port_io.adb b/common/hw-port_io.adb
new file mode 100644
index 0000000..e8adfc2
--- /dev/null
+++ b/common/hw-port_io.adb
@@ -0,0 +1,71 @@
+--
+-- Copyright (C) 2015 secunet Security Networks AG
+--
+-- This program is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; version 2 of the License.
+--
+-- 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 General Public License for more details.
+--
+
+with System;
+with System.Machine_Code;
+
+package body HW.Port_IO
+with
+   Refined_State  => (State => null),
+   SPARK_Mode     => Off
+is
+
+   generic
+      type Word is private;
+   procedure Port_In (Value : out Word; Port : Port_Type);
+
+   procedure Port_In (Value : out Word; Port : Port_Type) is
+   begin
+      System.Machine_Code.Asm
+        ("in %1, %0",
+         Inputs   => (Port_Type'Asm_Input ("Nd", Port)),
+         Outputs  => (Word'Asm_Output ("=a", Value)),
+         Volatile => True);
+   end Port_In;
+
+   procedure InB_Body is new Port_In (Word => Word8);
+   procedure InB (Value : out Word8; Port : Port_Type) renames InB_Body;
+
+   procedure InW_Body is new Port_In (Word => Word16);
+   procedure InW (Value : out Word16; Port : Port_Type) renames InW_Body;
+
+   procedure InL_Body is new Port_In (Word => Word32);
+   procedure InL (Value : out Word32; Port : Port_Type) renames InL_Body;
+
+   ----------------------------------------------------------------------------
+
+   generic
+      type Word is private;
+   procedure Port_Out (Port : Port_Type; Value : Word);
+
+   procedure Port_Out (Port : Port_Type; Value : Word) is
+   begin
+      System.Machine_Code.Asm
+        ("out %1, %0",
+         Inputs   => (Port_Type'Asm_Input ("Nd", Port),
+                      Word'Asm_Input ("a", Value)),
+         Volatile => True);
+   end Port_Out;
+
+   procedure OutB_Body is new Port_Out (Word => Word8);
+   procedure OutB (Port : Port_Type; Value : Word8) renames OutB_Body;
+
+   procedure OutW_Body is new Port_Out (Word => Word16);
+   procedure OutW (Port : Port_Type; Value : Word16) renames OutW_Body;
+
+   procedure OutL_Body is new Port_Out (Word => Word32);
+   procedure OutL (Port : Port_Type; Value : Word32) renames OutL_Body;
+
+end HW.Port_IO;
+
+--  vim: set ts=8 sts=3 sw=3 et:
diff --git a/common/hw-port_io.ads b/common/hw-port_io.ads
new file mode 100644
index 0000000..a5d0e9e
--- /dev/null
+++ b/common/hw-port_io.ads
@@ -0,0 +1,61 @@
+--
+-- Copyright (C) 2015 secunet Security Networks AG
+--
+-- This program is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; version 2 of the License.
+--
+-- 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 General Public License for more details.
+--
+
+package HW.Port_IO
+with
+   Abstract_State => (State with External => (Async_Readers, Async_Writers))
+is
+
+   type Port_Type is mod 2**16;
+
+   procedure InB (Value : out Word8; Port : Port_Type)
+   with
+      Global   => (In_Out => State),
+      Depends  => ((Value, State) => (Port, State)),
+      Inline_Always;
+
+   procedure InW (Value : out Word16; Port : Port_Type)
+   with
+      Global   => (In_Out => State),
+      Depends  => ((Value, State) => (Port, State)),
+      Pre      => Port mod 2 = 0,
+      Inline_Always;
+
+   procedure InL (Value : out Word32; Port : Port_Type)
+   with
+      Global   => (In_Out => State),
+      Depends  => ((Value, State) => (Port, State)),
+      Pre      => Port mod 4 = 0,
+      Inline_Always;
+
+   procedure OutB (Port : Port_Type; Value : Word8)
+   with
+      Global   => (In_Out => State),
+      Depends  => (State =>+ (Port, Value)),
+      Inline_Always;
+
+   procedure OutW (Port : Port_Type; Value : Word16)
+   with
+      Global   => (In_Out => State),
+      Depends  => (State =>+ (Port, Value)),
+      Pre      => Port mod 2 = 0,
+      Inline_Always;
+
+   procedure OutL (Port : Port_Type; Value : Word32)
+   with
+      Global   => (In_Out => State),
+      Depends  => (State =>+ (Port, Value)),
+      Pre      => Port mod 4 = 0,
+      Inline_Always;
+
+end HW.Port_IO;
diff --git a/common/hw-sub_regs.ads b/common/hw-sub_regs.ads
new file mode 100644
index 0000000..ca04c1d
--- /dev/null
+++ b/common/hw-sub_regs.ads
@@ -0,0 +1,26 @@
+--
+-- Copyright (C) 2016 secunet Security Networks AG
+--
+-- This program is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; version 2 of the License.
+--
+-- 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 General Public License for more details.
+--
+
+generic
+   type Index_T is (<>);
+package HW.Sub_Regs is
+
+   type T is record
+      Byte_Offset : Natural;
+      MSB    : Natural;
+      LSB   : Natural;
+   end record;
+
+   type Array_T is array (Index_T) of T;
+
+end HW.Sub_Regs;
diff --git a/common/hw-time-timer.ads b/common/hw-time-timer.ads
new file mode 100644
index 0000000..4676815
--- /dev/null
+++ b/common/hw-time-timer.ads
@@ -0,0 +1,41 @@
+--
+-- Copyright (C) 2015-2016 secunet Security Networks AG
+--
+-- This program is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; version 2 of the License.
+--
+-- 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 General Public License for more details.
+--
+
+private package HW.Time.Timer
+   with
+      Abstract_State => ((Timer_State with Part_Of => HW.Time.State),
+                         (Abstract_Time with
+                           Part_Of => HW.Time.State,
+                           External => Async_Writers)),
+      Initializes => (Timer_State)
+is
+
+   -- Returns the highest point in time that has definitely passed.
+   function Raw_Value_Min return T
+   with
+      Volatile_Function,
+      Global => (Input => Abstract_Time),
+      Depends => (Raw_Value_Min'Result => Abstract_Time);
+
+   -- Returns the highest point in time that might have been reached yet.
+   function Raw_Value_Max return T
+   with
+      Volatile_Function,
+      Global => (Input => Abstract_Time),
+      Depends => (Raw_Value_Max'Result => Abstract_Time);
+
+   function Hz return T
+   with
+      Global => (Input => Timer_State);
+
+end HW.Time.Timer;
diff --git a/common/hw-time.adb b/common/hw-time.adb
new file mode 100644
index 0000000..3162de1
--- /dev/null
+++ b/common/hw-time.adb
@@ -0,0 +1,105 @@
+--
+-- Copyright (C) 2015-2016 secunet Security Networks AG
+--
+-- This program is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; version 2 of the License.
+--
+-- 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 General Public License for more details.
+--
+
+with HW;
+with HW.Time.Timer;
+
+use type HW.Word64;
+
+package body HW.Time
+   with Refined_State => (State => (Timer.Timer_State, Timer.Abstract_Time))
+is
+
+   function Now return T
+   with
+      Refined_Global => (Input => Timer.Abstract_Time)
+   is
+      Current : constant T := Timer.Raw_Value_Min;
+   begin
+      return Current;
+   end Now;
+
+   function US_From_Now (US : Natural) return T
+   with
+      Refined_Global => (Input => (Timer.Abstract_Time, Timer.Timer_State))
+   is
+      Current : constant T := Timer.Raw_Value_Max;
+   begin
+      return Current + (T (US) * Timer.Hz + 999_999) / 1_000_000;
+   end US_From_Now;
+
+   function MS_From_Now (MS : Natural) return T
+   with
+      Refined_Global => (Input => (Timer.Abstract_Time, Timer.Timer_State))
+   is
+      Current : constant T := Timer.Raw_Value_Max;
+   begin
+      return Current + (T (MS) * Timer.Hz + 999) / 1_000;
+   end MS_From_Now;
+
+   function Now_US return Int64
+   with
+      Refined_Global => (Input => (Timer.Abstract_Time, Timer.Timer_State))
+   is
+      MHz : constant T := Timer.Hz / 1_000_000;
+      Current : constant T := Timer.Raw_Value_Min;
+   begin
+      return Int64 ((Current and (2 ** 63 - 1)) / (if MHz = 0 then 1 else MHz));
+   end Now_US;
+
+   ----------------------------------------------------------------------------
+
+   procedure Delay_Until (Deadline : T)
+   with
+      Refined_Global => (Input => (Timer.Abstract_Time))
+   is
+      Current: T;
+   begin
+      loop
+         Current := Timer.Raw_Value_Min;
+         exit when Current >= Deadline;
+      end loop;
+   end Delay_Until;
+
+   procedure U_Delay (US : Natural)
+   with
+      Refined_Global => (Input => (Timer.Abstract_Time, Timer.Timer_State))
+   is
+      Deadline : constant T := US_From_Now (US);
+   begin
+      Delay_Until (Deadline);
+   end U_Delay;
+
+   procedure M_Delay (MS : Natural)
+   with
+      Refined_Global => (Input => (Timer.Abstract_Time, Timer.Timer_State))
+   is
+      Deadline : constant T := MS_From_Now (MS);
+   begin
+      Delay_Until (Deadline);
+   end M_Delay;
+
+   ----------------------------------------------------------------------------
+
+   function Timed_Out (Deadline : T) return Boolean
+   with
+      Refined_Global => (Input => (Timer.Abstract_Time))
+   is
+      Current : constant T := Timer.Raw_Value_Min;
+   begin
+      return Current >= Deadline;
+   end Timed_Out;
+
+end HW.Time;
+
+--  vim: set ts=8 sts=3 sw=3 et:
diff --git a/common/hw-time.ads b/common/hw-time.ads
new file mode 100644
index 0000000..743279b
--- /dev/null
+++ b/common/hw-time.ads
@@ -0,0 +1,75 @@
+--
+-- Copyright (C) 2015-2016 secunet Security Networks AG
+--
+-- This program is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; version 2 of the License.
+--
+-- 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 General Public License for more details.
+--
+
+package HW.Time
+   with Abstract_State => (State with External => Async_Writers)
+is
+
+   type T is private;
+
+   function Now return T
+   with
+      Volatile_Function,
+      Global => (Input => State);
+
+   function US_From_Now (US : Natural) return T
+   with
+      Volatile_Function,
+      Global => (Input => State);
+
+   function MS_From_Now (MS : Natural) return T
+   with
+      Volatile_Function,
+      Global => (Input => State);
+
+   function Now_US return Int64
+   with
+      Volatile_Function,
+      Global => (Input => State);
+
+   ----------------------------------------------------------------------------
+
+   pragma Warnings
+     (GNATprove, Off, "subprogram ""*Delay*"" has no effect",
+      Reason => "No effect on dataflow but time always passes.");
+
+   -- Delay execution until Deadline has been reached.
+   procedure Delay_Until (Deadline : T)
+   with
+      Global => (Input => State);
+
+   procedure U_Delay (US : Natural)
+   with
+      Global => (Input => State);
+
+   procedure M_Delay (MS : Natural)
+   with
+      Global => (Input => State);
+
+   pragma Warnings
+     (GNATprove, On, "subprogram ""*Delay*"" has no effect");
+
+   ----------------------------------------------------------------------------
+
+   function Timed_Out (Deadline : T) return Boolean
+   with
+      Volatile_Function,
+      Global => (Input => State);
+
+private
+
+   type T is new Word64;
+
+end HW.Time;
+
+--  vim: set ts=8 sts=3 sw=3 et:
diff --git a/common/hw.ads b/common/hw.ads
new file mode 100644
index 0000000..6bfca91
--- /dev/null
+++ b/common/hw.ads
@@ -0,0 +1,58 @@
+--
+-- Copyright (C) 2015 secunet Security Networks AG
+--
+-- This program is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; version 2 of the License.
+--
+-- 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 General Public License for more details.
+--
+
+with Interfaces;
+
+package HW is
+
+   type Bit is mod 2 ** 1;
+
+   subtype Byte is Interfaces.Unsigned_8;
+   subtype Word8 is Byte;
+   function Shift_Left  (Value : Word8; Amount : Natural) return Word8
+      renames Interfaces.Shift_Left;
+   function Shift_Right (Value : Word8; Amount : Natural) return Word8
+      renames Interfaces.Shift_Right;
+
+   subtype Word16 is Interfaces.Unsigned_16;
+   function Shift_Left  (Value : Word16; Amount : Natural) return Word16
+      renames Interfaces.Shift_Left;
+   function Shift_Right (Value : Word16; Amount : Natural) return Word16
+      renames Interfaces.Shift_Right;
+
+   subtype Word32 is Interfaces.Unsigned_32;
+   function Shift_Left  (Value : Word32; Amount : Natural) return Word32
+      renames Interfaces.Shift_Left;
+   function Shift_Right (Value : Word32; Amount : Natural) return Word32
+      renames Interfaces.Shift_Right;
+
+   subtype Word64 is Interfaces.Unsigned_64;
+   function Shift_Left  (Value : Word64; Amount : Natural) return Word64
+      renames Interfaces.Shift_Left;
+   function Shift_Right (Value : Word64; Amount : Natural) return Word64
+      renames Interfaces.Shift_Right;
+
+   subtype Int8 is Interfaces.Integer_8;
+   subtype Int16 is Interfaces.Integer_16;
+   subtype Int32 is Interfaces.Integer_32;
+   subtype Int64 is Interfaces.Integer_64;
+
+   subtype Pos8 is Interfaces.Integer_8 range 1 .. Interfaces.Integer_8'Last;
+   subtype Pos16 is Interfaces.Integer_16 range 1 .. Interfaces.Integer_16'Last;
+   subtype Pos32 is Interfaces.Integer_32 range 1 .. Interfaces.Integer_32'Last;
+   subtype Pos64 is Interfaces.Integer_64 range 1 .. Interfaces.Integer_64'Last;
+
+   subtype Buffer_Range is Natural range 0 .. Natural'Last - 1;
+   type Buffer is array (Buffer_Range range <>) of Byte;
+
+end HW;
diff --git a/configs/defconfig b/configs/defconfig
new file mode 100644
index 0000000..17bb699
--- /dev/null
+++ b/configs/defconfig
@@ -0,0 +1,5 @@
+CONFIG_HWBASE_DEBUG_NULL		= y
+CONFIG_HWBASE_DEBUG_TEXT_IO		=
+CONFIG_HWBASE_STATIC_MMIO		= y
+CONFIG_HWBASE_DYNAMIC_MMIO		=
+CONFIG_HWBASE_TIMER_CLOCK_GETTIME	= y
diff --git a/debug/Makefile.inc b/debug/Makefile.inc
new file mode 100644
index 0000000..b636a6f
--- /dev/null
+++ b/debug/Makefile.inc
@@ -0,0 +1,4 @@
+hw-y += hw-debug.ads
+hw-y += hw-debug.adb
+hw-$(CONFIG_HWBASE_DEBUG_NULL) += null/hw-debug_sink.ads
+hw-$(CONFIG_HWBASE_DEBUG_TEXT_IO) += text_io/hw-debug_sink.ads
diff --git a/debug/hw-debug.adb b/debug/hw-debug.adb
new file mode 100644
index 0000000..3ffa9b5
--- /dev/null
+++ b/debug/hw-debug.adb
@@ -0,0 +1,284 @@
+--
+-- Copyright (C) 2015 secunet Security Networks AG
+--
+-- This program is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; version 2 of the License.
+--
+-- 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 General Public License for more details.
+--
+
+with HW;
+with HW.Time;
+with HW.Debug_Sink;
+
+use type HW.Word64;
+use type HW.Int64;
+
+package body HW.Debug
+with
+   SPARK_Mode => Off
+is
+
+   Start_Of_Line : Boolean := True;
+   Register_Write_Delay_Nanoseconds : Word64 := 0;
+
+   type Base_Range is new Positive range 2 .. 16;
+   type Width_Range is new Natural range 0 .. 64;
+
+   procedure Put_By_Base
+     (Item        : Word64;
+      Min_Width   : Width_Range;
+      Base        : Base_Range);
+
+   procedure Do_Put_Int64
+     (Item        : Int64);
+
+   ----------------------------------------------------------------------------
+
+   procedure Put_Time
+   is
+      Now_US : Int64;
+   begin
+      if Start_Of_Line then
+         Start_Of_Line := False;
+         Now_US := Time.Now_US;
+         Debug_Sink.Put_Char ('[');
+         Do_Put_Int64 ((Now_US / 1_000_000) mod 1_000_000);
+         Debug_Sink.Put_Char ('.');
+         Put_By_Base (Word64 (Now_US mod 1_000_000), 6, 10);
+         Debug_Sink.Put ("] ");
+      end if;
+   end Put_Time;
+
+   ----------------------------------------------------------------------------
+
+   procedure Put (Item : String) is
+   begin
+      Put_Time;
+      HW.Debug_Sink.Put (Item);
+   end Put;
+
+   procedure Put_Line (Item : String) is
+   begin
+      Put (Item);
+      New_Line;
+   end Put_Line;
+
+   procedure New_Line is
+   begin
+      HW.Debug_Sink.New_Line;
+      Start_Of_Line := True;
+   end New_Line;
+
+   ----------------------------------------------------------------------------
+
+   procedure Put_By_Base
+     (Item        : Word64;
+      Min_Width   : Width_Range;
+      Base        : Base_Range)
+   is
+      Temp : Word64 := Item;
+
+      subtype Chars_Range is Width_Range range 0 .. 63;
+      Index : Width_Range := 0;
+
+      type Chars_Array is array (Chars_Range) of Character;
+      Chars : Chars_Array := (others => '0');
+
+      Digit : Natural;
+   begin
+      while Temp > 0 loop
+         Digit := Natural (Temp rem Word64 (Base));
+         if Digit < 10 then
+            Chars (Index) := Character'Val (Character'Pos ('0') + Digit);
+         else
+            Chars (Index) := Character'Val (Character'Pos ('a') + Digit - 10);
+         end if;
+         Temp := Temp / Word64 (Base);
+         Index := Index + 1;
+      end loop;
+      if Index < Min_Width then
+         Index := Min_Width;
+      end if;
+      for I in reverse Width_Range range 0 .. Index - 1 loop
+         HW.Debug_Sink.Put_Char (Chars (I));
+      end loop;
+   end Put_By_Base;
+
+   ----------------------------------------------------------------------------
+
+   procedure Put_Word
+     (Item        : Word64;
+      Min_Width   : Width_Range;
+      Print_Ox    : Boolean := True) is
+   begin
+      Put_Time;
+      if Print_Ox then
+         Put ("0x");
+      end if;
+      Put_By_Base (Item, Min_Width, 16);
+   end Put_Word;
+
+   procedure Put_Word8 (Item : Word8) is
+   begin
+      Put_Word (Word64 (Item), 2);
+   end Put_Word8;
+
+   procedure Put_Word16 (Item : Word16) is
+   begin
+      Put_Word (Word64 (Item), 4);
+   end Put_Word16;
+
+   procedure Put_Word32 (Item : Word32) is
+   begin
+      Put_Word (Word64 (Item), 8);
+   end Put_Word32;
+
+   procedure Put_Word64 (Item : Word64) is
+   begin
+      Put_Word (Item, 16);
+   end Put_Word64;
+
+   ----------------------------------------------------------------------------
+
+   procedure Do_Put_Int64 (Item : Int64)
+   is
+      Temp : Word64;
+   begin
+      if Item < 0 then
+         Debug_Sink.Put_Char ('-');
+         Temp := Word64 (-Item);
+      else
+         Temp := Word64 (Item);
+      end if;
+      Put_By_Base (Temp, 1, 10);
+   end Do_Put_Int64;
+
+   procedure Put_Int64 (Item : Int64)
+   is
+   begin
+      Put_Time;
+      Do_Put_Int64 (Item);
+   end Put_Int64;
+
+   procedure Put_Int8 (Item : Int8) is
+   begin
+      Put_Int64 (Int64 (Item));
+   end Put_Int8;
+
+   procedure Put_Int16 (Item : Int16) is
+   begin
+      Put_Int64 (Int64 (Item));
+   end Put_Int16;
+
+   procedure Put_Int32 (Item : Int32) is
+   begin
+      Put_Int64 (Int64 (Item));
+   end Put_Int32;
+
+   ----------------------------------------------------------------------------
+
+   procedure Put_Reg8 (Name : String; Item : Word8) is
+   begin
+      Put (Name);
+      Put (": ");
+      Put_Word8 (Item);
+      New_Line;
+   end Put_Reg8;
+
+   procedure Put_Reg16 (Name : String; Item : Word16)
+   is
+   begin
+      Put (Name);
+      Put (": ");
+      Put_Word16 (Item);
+      New_Line;
+   end Put_Reg16;
+
+   procedure Put_Reg32 (Name : String; Item : Word32)
+   is
+   begin
+      Put (Name);
+      Put (": ");
+      Put_Word32 (Item);
+      New_Line;
+   end Put_Reg32;
+
+   procedure Put_Reg64 (Name : String; Item : Word64)
+   is
+   begin
+      Put (Name);
+      Put (": ");
+      Put_Word64 (Item);
+      New_Line;
+   end Put_Reg64;
+
+   ----------------------------------------------------------------------------
+
+   procedure Put_Buffer
+     (Name  : String;
+      Buf   : Buffer;
+      Len   : Buffer_Range)
+   is
+      Line_Start, Left : Natural;
+   begin
+      if Len = 0 then
+         if Name'Length > 0 then
+            Put (Name);
+            Put_Line ("+0x00:");
+         end if;
+      else
+         Line_Start  := 0;
+         Left        := Len - 1;
+         for I in Natural range 1 .. ((Len + 15) / 16) loop
+            if Name'Length > 0 then
+               Put (Name);
+               Debug_Sink.Put_Char ('+');
+               Put_Word16 (Word16 (Line_Start));
+               Put (":  ");
+            end if;
+            for J in Natural range 0 .. Natural'Min (7, Left)
+            loop
+               Put_Word (Word64 (Buf (Line_Start + J)), 2, False);
+               Debug_Sink.Put_Char (' ');
+            end loop;
+
+            Debug_Sink.Put_Char (' ');
+            for J in Natural range 8 .. Natural'Min (15, Left)
+            loop
+               Put_Word (Word64(Buf (Line_Start + J)), 2, False);
+               Debug_Sink.Put_Char (' ');
+            end loop;
+            New_Line;
+
+            Line_Start  := Line_Start + 16;
+            Left        := Left - Natural'Min (Left, 16);
+         end loop;
+      end if;
+   end Put_Buffer;
+
+   ----------------------------------------------------------------------------
+
+   procedure Set_Register_Write_Delay (Value : Word64)
+   is
+   begin
+      Register_Write_Delay_Nanoseconds := Value;
+   end Set_Register_Write_Delay;
+
+   ----------------------------------------------------------------------------
+
+   Procedure Register_Write_Wait
+   is
+   begin
+      if Register_Write_Delay_Nanoseconds > 0 then
+         Time.U_Delay (Natural ((Register_Write_Delay_Nanoseconds + 999) / 1000));
+      end if;
+   end Register_Write_Wait;
+
+end HW.Debug;
+
+--  vim: set ts=8 sts=3 sw=3 et:
diff --git a/debug/hw-debug.ads b/debug/hw-debug.ads
new file mode 100644
index 0000000..fd8ce9c
--- /dev/null
+++ b/debug/hw-debug.ads
@@ -0,0 +1,42 @@
+--
+-- Copyright (C) 2015 secunet Security Networks AG
+--
+-- This program is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; version 2 of the License.
+--
+-- 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 General Public License for more details.
+--
+
+
+package HW.Debug is
+
+   procedure Put (Item : String);
+   procedure Put_Line (Item : String);
+   procedure New_Line;
+
+   procedure Put_Word8 (Item : Word8);
+   procedure Put_Word16 (Item : Word16);
+   procedure Put_Word32 (Item : Word32);
+   procedure Put_Word64 (Item : Word64);
+
+   procedure Put_Int8 (Item : Int8);
+   procedure Put_Int16 (Item : Int16);
+   procedure Put_Int32 (Item : Int32);
+   procedure Put_Int64 (Item : Int64);
+
+   procedure Put_Reg8 (Name : String; Item : Word8);
+   procedure Put_Reg16 (Name : String; Item : Word16);
+   procedure Put_Reg32 (Name : String; Item : Word32);
+   procedure Put_Reg64 (Name : String; Item : Word64);
+
+   procedure Put_Buffer (Name : String; Buf : in Buffer; Len : in Buffer_Range);
+
+   procedure Set_Register_Write_Delay (Value : Word64);
+   Procedure Register_Write_Wait;
+end HW.Debug;
+
+--  vim: set ts=8 sts=3 sw=3 et:
diff --git a/debug/null/hw-debug_sink.ads b/debug/null/hw-debug_sink.ads
new file mode 100644
index 0000000..dcd2dd1
--- /dev/null
+++ b/debug/null/hw-debug_sink.ads
@@ -0,0 +1,22 @@
+--
+-- Copyright (C) 2015 secunet Security Networks AG
+--
+-- This program is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; version 2 of the License.
+--
+-- 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 General Public License for more details.
+--
+
+package HW.Debug_Sink is
+
+   procedure Put (Item : String) is null;
+
+   procedure Put_Char (Item : Character) is null;
+
+   procedure New_Line is null;
+
+end HW.Debug_Sink;
diff --git a/debug/text_io/hw-debug_sink.ads b/debug/text_io/hw-debug_sink.ads
new file mode 100644
index 0000000..2f0b2d2
--- /dev/null
+++ b/debug/text_io/hw-debug_sink.ads
@@ -0,0 +1,23 @@
+--
+-- Copyright (C) 2015 secunet Security Networks AG
+--
+-- This program is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; version 2 of the License.
+--
+-- 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 General Public License for more details.
+--
+
+with Ada.Text_IO;
+
+package HW.Debug_Sink is
+
+   procedure Put (Item : String) renames Ada.Text_IO.Put;
+   procedure Put_Char (Item : Character) renames Ada.Text_IO.Put;
+   procedure New_Line (Spacing : Ada.Text_IO.Positive_Count := 1)
+      renames  Ada.Text_IO.New_Line;
+
+end HW.Debug_Sink;
diff --git a/gnat.adc b/gnat.adc
new file mode 100644
index 0000000..eab8a17
--- /dev/null
+++ b/gnat.adc
@@ -0,0 +1,25 @@
+pragma Restrictions (No_Allocators);
+pragma Restrictions (No_Calendar);
+pragma Restrictions (No_Dispatch);
+pragma Restrictions (No_Exception_Handlers);
+pragma Restrictions (No_Fixed_Point);
+pragma Restrictions (No_Floating_Point);
+pragma Restrictions (No_Implicit_Dynamic_Code);
+pragma Restrictions (No_Implicit_Heap_Allocations);
+pragma Restrictions (No_Implicit_Loops);
+pragma Restrictions (No_Initialize_Scalars);
+pragma Restrictions (No_Local_Allocators);
+pragma Restrictions (No_Recursion);
+pragma Restrictions (No_Secondary_Stack);
+pragma Restrictions (No_Streams);
+pragma Restrictions (No_Tasking);
+pragma Restrictions (No_Unchecked_Access);
+pragma Restrictions (No_Unchecked_Deallocation);
+pragma Restrictions (No_Wide_Characters);
+pragma Restrictions (Static_Storage_Size);
+pragma Assertion_Policy
+  (Statement_Assertions => Disable,
+   Pre                  => Disable,
+   Post                 => Disable);
+pragma Overflow_Mode (General => Strict, Assertions => Eliminated);
+pragma SPARK_Mode (On);
diff --git a/proof/Makefile.inc b/proof/Makefile.inc
new file mode 100644
index 0000000..dae0b0d
--- /dev/null
+++ b/proof/Makefile.inc
@@ -0,0 +1 @@
+hw-proof-y += hw-mmio_range.adb
diff --git a/proof/hw-mmio_range.adb b/proof/hw-mmio_range.adb
new file mode 100644
index 0000000..d96fc4b
--- /dev/null
+++ b/proof/hw-mmio_range.adb
@@ -0,0 +1,44 @@
+--
+-- Copyright (C) 2015 secunet Security Networks AG
+--
+-- This program is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; version 2 of the License.
+--
+-- 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 General Public License for more details.
+--
+
+package body HW.MMIO_Range
+with
+   Refined_State =>
+     (State => Range_A,
+      Base_Address => Address)
+is
+
+   Range_A : Array_T
+   with
+      Volatile,
+      Async_Readers, Async_Writers, Effective_Reads, Effective_Writes,
+      Import;
+
+   Address : Word64 := Base_Addr;
+
+   procedure Read (Value : out Element_T; Index : in Index_T) is
+   begin
+      Value := Range_A (Index);
+   end Read;
+
+   procedure Write (Index : in Index_T; Value: in Element_T) is
+   begin
+      Range_A (Index) := Value;
+   end Write;
+
+   procedure Set_Base_Address (Base : Word64) is
+   begin
+      Address := Base;
+   end Set_Base_Address;
+
+end HW.MMIO_Range;
diff --git a/spark.adc b/spark.adc
new file mode 100644
index 0000000..576a120
--- /dev/null
+++ b/spark.adc
@@ -0,0 +1,23 @@
+pragma Restrictions (No_Allocators);
+pragma Restrictions (No_Calendar);
+pragma Restrictions (No_Dispatch);
+pragma Restrictions (No_Exception_Handlers);
+pragma Restrictions (No_Fixed_Point);
+pragma Restrictions (No_Floating_Point);
+pragma Restrictions (No_Implicit_Dynamic_Code);
+pragma Restrictions (No_Implicit_Heap_Allocations);
+pragma Restrictions (No_Implicit_Loops);
+pragma Restrictions (No_Initialize_Scalars);
+pragma Restrictions (No_Local_Allocators);
+pragma Restrictions (No_Recursion);
+pragma Restrictions (No_Secondary_Stack);
+pragma Restrictions (No_Streams);
+pragma Restrictions (No_Tasking);
+pragma Restrictions (No_Unchecked_Access);
+pragma Restrictions (No_Unchecked_Deallocation);
+pragma Restrictions (No_Wide_Characters);
+pragma Restrictions (Static_Storage_Size);
+pragma Assertion_Policy
+  (Debug                => Disable);
+pragma Overflow_Mode (General => Strict, Assertions => Eliminated);
+pragma SPARK_Mode (On);