How to finde postconditions to spark a rubik's cube?

Help
,
1

I programmed a rubik’s cube as a small exercise. So far I got clockwise turns for each site implemented. To make sure that I actually implemented everything right I wanted to spark my code but I got totally stuck on how a post condition would look like for a rubik’s cube.

The current representation for the cube is an array of faces which is an array of squares.

type Square is range 1..6;  --  One of the six "colors" a square can be

type Face is array (1..9) of Square;  --  A side of the cube made of 9 squares

type Cube_Type is array (1..6) of Face;

Cube : Cube_Type := (
   (others => 1),
   (others => 2),
   (others => 3),
   (others => 4),
   (others => 5),
   (others => 6));

Turing the “Upper” side is implemented as

procedure U is
   tmp1 : Square := Cube (2) (1);
   tmp2 : Square := Cube (2) (2);
   tmp3 : Square := Cube (2) (3);

   tmp4 : Square := Cube (1) (1);
   tmp5 : Square := Cube (1) (2);
begin
   Cube (2) (1) := Cube (5) (1);
   Cube (5) (1) := Cube (4) (1);
   Cube (4) (1) := Cube (3) (1);
   Cube (3) (1) := tmp1;

   Cube (2) (2) := Cube (5) (2);
   Cube (5) (2) := Cube (4) (2);
   Cube (4) (2) := Cube (3) (2);
   Cube (3) (2) := tmp2;

   Cube (2) (3) := Cube (5) (3);
   Cube (5) (3) := Cube (4) (3);
   Cube (4) (3) := Cube (3) (3);
   Cube (3) (3) := tmp3;

   Cube (1) (1) := Cube (1) (3);
   Cube (1) (3) := Cube (1) (9);
   Cube (1) (9) := Cube (1) (7);
   Cube (1) (7) := tmp4;

   Cube (1) (2) := Cube (1) (6);
   Cube (1) (6) := Cube (1) (8);
   Cube (1) (8) := Cube (1) (4);
   Cube (1) (4) := tmp5;
end U;

(I know that it looks a bit messy but I double checked the code and tested it already)

I should also add that I use Ada_2022 for the custom 'Image attribute. Makes debugging easier.

How would/should I define the post condition for spark?
Currently I have that the left side is unmoved with Post => Cube (5) = Cube'old (5).
I also need to add the state of all the other squares. How would I tell something like “each third square of one face maps to each third square to another square” in spark?

If you have some comments or recommendations on the way I represent the rubik’s cube or apply movement, I’d be glad to hear them!