NVIDIA의 CuTe 라이브러리 뒤에 있는 레이아웃 대수는 텐서 타일이 스레드와 메모리에 어떻게 매핑되는지를 설명합니다. 레이아웃은 각 항목마다 스트라이드를 가진 형태이며, 따라서 좌표의 주소는 그 인덱스들에 스트라이드를 곱한 값들의 합입니다. Shah와 Cecka에 의해 공식화된 바와 같이, 이의 핵심 연산들(예: 합성(composition), 보수(complement), 나눗셈(division), 곱(product))은 최소 여섯 가지 상호작용하는 적합성 조건(admissibility conditions)에 의해 보호됩니다. 우리는 이러한 복잡성이 도메인의 문제가 아니라 표현적 선택의 인공물임을 보여줍니다. 우리는 모든 레이아웃이 입력과 출력이 존재하는 공간을 명명하는 레이아웃 대수를 제시합니다: 논리적(logical), 물리적(physical), 또는 스레드 값 인덱스입니다. 논리적 또는 스레드 값 공간으로 가는 레이아웃은 그 $N$개의 좌표를 $[0, N)$으로 보내는 전단사 함수(bijection)여야 합니다. 물리적 공간으로 가는 레이아웃은 별칭이 없어야 합니다: 서로 다른 좌표들은 고유한 주소에 위치해야 하며, 브로드캐스트(broadcast)의 경우를 제외하고는 그러합니다. 브로드캐스트에서는 여러 스레드가 의도적으로 하나의 값을 읽으므로, 레이아웃은 그 위치를 표시해야 합니다. 아무것도 물리적 인덱스 밖으로 매핑되지 않습니다. $f$와 $g$를 합성하는 것은 단지 $f$의 범위(range)가 정확히 $g$의 평탄화된 좌표 집합이어야 한다는 것만을 요구합니다. 인덱스 산술은 항상 순진하게(naively) 방출될 수 있습니다: $f$를 계산하고, 그 결과를 나눗셈과 나머지로 $g$의 좌표에 따라 분할한 다음, $g$를 적용합니다. 종종 합성된 결과는 레이아웃으로 단순화됩니다. 우리는 그것이 그렇게 할 때, 다른 모든 형태가 이를 정제하는 가장 거친(coarsest) 그러한 형태가 존재하며, 그 형태를 방출한다고 보여줍니다. 워프(warp) 또는 스레드의 슬라이스는 extit{제한(restriction)}입니다. 제한된 레이아웃은 더 이상 합성 가능하지 않으며, 이는 사용자가 타일의 전체 뷰를 설정한 후에 슬라이스를 취하도록 강제합니다. 우리는 CuTe의 연산들, 예를 들어 합성, 보수, 나눗셈 등을 재현함으로써 이 대수를 검증합니다. 우리는 이를 OCaml로 구현하고, 그 구현을 사용하여 CuTe의 원자 요소(atoms)와 사용 패턴을 재도출합니다. 결정 절차는 Rocq에서 정확함이 증명되었습니다.