Definition

In the HOL-TestGen microprocessor case study, a uniformity hypothesis is generated for each symbolic test case. Its role is to justify selecting one concrete witness value for the schematic variables of that symbolic test case during test data instantiation. [C1]

Form in generated tests

The evidence shows uniformity hypotheses as THYP subgoals paired with schematic test cases. For a single load-byte test case, the generated pair has the form:

1. SUT σ0(Ilb ??X7 ??X6 ??X5) (...)
2. THYP ((∃ x xa xb. SUT σ0(Ilb xb xa x) (...)) −→
        (∀ x xa xb. SUT σ0(Ilb xb xa x) (...)))

Here, variables such as ??X7, ??X6, and ??X5 are schematic variables representing possible witness values. [C2]

For an instruction-sequence test case, the same pattern appears as a second subgoal:

THYP ((∃ x1 x2 x3 x4 x5 x6 x7 x8 x9.
          σ0 |=(s ← mbind [Isw x1 x2 x3,
                            Ilbu x4 x5 x6,
                            Ilbu x7 x8 x9] execVAMP; (...))) −→
      (∀ x1 x2 x3 x4 x5 x6 x7 x8 x9.
          σ0 |=(s ← mbind [Isw x1 x2 x3,
                            Ilbu x4 x5 x6,
                            Ilbu x7 x8 x9] execVAMP; (...))))

The paper states that the first subgoal is the schematic test case and the second subgoal is the uniformity hypothesis for that case. [C3]

Place in the HOL-TestGen workflow

In the described workflow, HOL-TestGen first performs test case generation by exhaustive case splitting on the instruction datatype and producing symbolic operands. For the load/store unit-test scenario, this produced eight symbolic test cases, one for each load/store operation, and each was associated with a uniformity hypothesis. The final generation state therefore contained eight schematic test cases and eight uniformity hypotheses. Their conjunction is called a test theorem. [C4]

The second phase is test data instantiation using gen_test_data, which instantiates schematic variables with concrete values. For example, a sequence containing schematic operands can be instantiated as:

σ0 |=(s ← mbind [Isw 0 1 8, Ilbu 1 0 -3, Ilbu 3 2 8] execVAMP;
      assertSE (λσ. σ =k SUT σ0[Isw 0 1 8, Ilbu 1 0 -3, Ilbu 3 2 8]))

This corresponds to the assembly sequence:

ISW   0 1  8
LLBU  1 0 -3
LLBU  3 2  8

[C5]

Interpretation

Within the cited case study, the uniformity hypothesis has an existential-to-universal shape: if the test predicate holds for some assignment of the schematic operands, then it is treated as holding uniformly for all assignments in that symbolic case. This is what makes it possible to select one concrete witness for the case rather than testing every operand combination represented by the schematic variables. [C1] [C2] [C3]