Escape from the tarpit (Cops) This is a cops-and-robbers challenge based around defining languages and proving they are Turing complete.
This is the cops' thread. The robbers' thread is here.
Cops
As a cop, you will prepare two things:

A formal specification of a programming language, or other computational system. (Computational systems are defined below.)

A proof that your system is Turing complete, according to the somewhat strict definition below.


You will post your specification of your language, and the robbers will try to &quot;crack&quot; it by proving its Turing completeness. If your submission is not cracked within one week you can mark it as safe and post your proof. (Your answer can be invalidated if someone finds a flaw in your proof, unless you can fix it.)
This is a popularity-contest, so the winner will be the answer that has the most votes, and which is not cracked or invalidated. The challenge is open-ended - I won't be accepting an answer.
For the sake of this challenge, a computational system will be defined as four things:

A &quot;program set&quot; P. This will be a countably infinite set, e.g. strings, integers, binary trees, configurations of pixels on a grid, etc. (But see the technical restriction below.)

An &quot;input set&quot; I, which will also be a countably infinite set, and need not be the same set as P (although it can be).

An &quot;output set&quot; O, which similarly will be a countably infinite set, and may or may not be the same as P or I

A deterministic, mechanistic procedure for producing an output o from program p and input i, where p, i and o are members of P, I and O respectively. This procedure should be such that it could, in principle, be implemented on a Turing machine or other abstract model of computation. The procedure may, of course, fail to halt, depending on the program and its input.


The sets P, I and O must be such that you can express them as strings in a computable manner. (For most sensible choices this will not matter; this rule exists to prevent you from choosing strange sets, such as the set of Turing machines that don't halt.)
Turing completeness will be defined as the following:

For any computable partial function f from I to O, there exists a program p in P such that given p and input i, the output is f(i) if f(i) has a value. (Otherwise the program doesn't halt.)

The word &quot;computable&quot; in the above definition means &quot;can be computed using a Turing machine&quot;.
Note that neither rule 110 nor bitwise cyclic tag are Turing-complete by this definition, because they don't have the required input-output structure. Lambda calculus is Turing complete, as long as we define I and O to be the Church numerals. (It is not Turing-complete if we take I and O to be lambda expressions in general.)
Note that you don't have to provide an implementation of your language, but you are welcome to include one in your answer if you like. However, you shouldn't rely on the implementation to define the language in any way - the spec should be complete in itself, and if there is a contradiction between the spec and the implementation this should be treated as a bug in the implementation.
Blindfolded Arithmetic

Possibly a fairly easy language to start off with, relatively
speaking.  (There are limits on how difficult a language I can make
because I have to prove it Turing-complete myself!)

For this language, the program set is the set of Blindfolded
Arithmetic programs as given in the section "program" below, the input
set is the set of positive integers, and the output set is the set of
integers (the entire set, not just the positive integers).

This language is fairly interesting – maybe even practically useful –
because it has a more or less total lack of control flow, being
entirely based on computations on numbers you can't see.  That makes
it potentially useful as a language for implementing programs inside
homomorphic encryption
systems.

Specification

Blindfolded Arithmetic is an esoteric programming language with the
following specifications:

Data storage

A state of a running Blindfolded Arithmetic program consists of six
variables, each of which can store an integer.  (There are no limits
on how large or small these integers can get; in particular, they can
go negative.)  The variables are called a, b, c, d, e, and
i.

At the start of the program, a to e inclusive are each initialised
to 0, and i is initialised to a positive integer taken from user
input.  (If no input is available, i is initialised to 1.)

If the program ceases execution (this can only occur due to division
by zero), the value of i immediately before the division was
attempted is used as the program's output.

Program

A Blindfolded Arithmetic program is a list of commands, each of which
has one of the following forms (where v can be replaced by any
variable name, potentially a different name each time it's used):


v = v + v
v = v - v
v = v * v
v = v / v


Note that each operand of the commands must be a variable; this
language does not allow the use of literal integers.

Execution of the program is performed by running each of the commands
in sequence, and then looping back to the start and continuing to run
the commands in sequence again, ad infinitum (or until there's an
attempt to divide by zero, which ends the program).

Each command has the same semantics as you'd expect from the notation,
which is no different from that used by most practical programming
languages: the values of the second and third variables metioned in
the command are taken, an arithmetic operation
(add/subtract/multiply/divide respectively for the four forms of
command) is applied to them, and the resulting value stored into the
first variable.  Division here is integer division, rounding
towards 0.

There is no control flow of any kind, other than program exit; the
commands always cycle in sequence, up until a division by zero (if
any) occurs and ends the program.  In particular, there's no way to
directly read variables, only to use them as a source of calculations
whose results impact the values assigned to other variables.