In An Axiomatic Basis for Computer Programming C.A.R. Hoare stated:
The axioms A1 to A9 are, of course, true of the traditional infinite set of integers in mathematics. However, they are also true of the finite set of "integers" which are manipulated by computers provided that they are confined to nonnegative numbers.
They are as follows:
A1. x + y = y + x
A2. $x \times y$ = $y \times x$
A3. $(x + y) + z = x + (y + z)$
A4. $(x \times y) \times z = x \times (y \times z)$
A5. $x \times (y + z ) = x \times y + x \times z$
A6. $y \le x ⇒ (x - y) + y = x$
A7. x + 0 = x
A8. $x \times 0 = 0$
A9. $x \times 1 = x$
Why are they true only for nonnegative numbers? Computers are perfectly capable of representing signed numbers with systems such as two's complement.
Link to paper: https://www.cs.cmu.edu/~crary/819-f09/Hoare69.pdf
Indeed all of the axioms you quote are true in rings in general (A6 does not then need its premise).
In particular they're true in the ring of integers modulo $2^w$, which is what fixed-width computer arithmetic actually implements at the hardware level.
The axioms may not hold for fixed-with signed arithmetic when overflow leads to an exception being thrown, though. For example, suppose we can represent numbers between $-128$ and $127$, inclusively. Then $$ (-100 + 100) + 100 = 100 \quad\text{but}\quad -100 + (100+100) \text{ overflows}$$ and rewriting one expression to the other is therefore not guaranteed valid.
(Consider, for example, a C compiler for a specialized DSP. Since the compiler knows that signed integer overflow is undefined behavior in C, it might choose to implement some of it by an ALU mode where overflow clamps to the maximum number rather than roll around -- which may improve instruction-level parallelism in concrete cases -- and then the associative law for signed addition fails!)
Also, note that Hoare wrote in the 1960s, when it was not yet universal that computer arithmetic meant arithmetic modulo $2^w$. Just from what I can google up quickly, as late as 1968 IBM had launched their Model 1450, which worked on base-10 sign-magnitude numbers internally. When there are both $+0$ and $-0$ (and perhaps funky rules for choosing between them), some of these equalities may not be exact even when there's no overflow.