Skip to content

Commit 3ee667d

Browse files
rossbergrossberg
committed
[spectec] Fix test expect
1 parent df76f27 commit 3ee667d

File tree

6 files changed

+104
-20
lines changed

6 files changed

+104
-20
lines changed

‎spectec/doc/example/output/NanoWasm.pdf‎

0 Bytes
Binary file not shown.

‎spectec/test-frontend/TEST.md‎

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3193,10 +3193,15 @@ relation Instrtype_sub: `%|-%<:%`(context, instrtype, instrtype)
31933193
;; ../../../../specification/wasm-3.0/2.2-validation.subtyping.spectec
31943194
relation Limits_sub: `%|-%<:%`(context, limits, limits)
31953195
;; ../../../../specification/wasm-3.0/2.2-validation.subtyping.spectec
3196-
rule _{C : context, n_1 : n, m_1 : m, n_2 : n, m_2 : m}:
3197-
`%|-%<:%`(C, `[%..%]`_limits(`%`_u64(n_1), ?(`%`_u64(m_1))), `[%..%]`_limits(`%`_u64(n_2), ?(`%`_u64(m_2))))
3196+
rule max{C : context, n_1 : n, m_1 : m, n_2 : n, `m_2?` : m?}:
3197+
`%|-%<:%`(C, `[%..%]`_limits(`%`_u64(n_1), ?(`%`_u64(m_1))), `[%..%]`_limits(`%`_u64(n_2), `%`_u64(m_2)?{m_2 <- `m_2?`}))
3198+
-- if (n_1 >= n_2)
3199+
-- (if (m_1 <= m_2))?{m_2 <- `m_2?`}
3200+
3201+
;; ../../../../specification/wasm-3.0/2.2-validation.subtyping.spectec
3202+
rule eps{C : context, n_1 : n, n_2 : n}:
3203+
`%|-%<:%`(C, `[%..%]`_limits(`%`_u64(n_1), ?()), `[%..%]`_limits(`%`_u64(n_2), ?()))
31983204
-- if (n_1 >= n_2)
3199-
-- if (m_1 <= m_2)
32003205

32013206
;; ../../../../specification/wasm-3.0/2.2-validation.subtyping.spectec
32023207
relation Tagtype_sub: `%|-%<:%`(context, tagtype, tagtype)

‎spectec/test-latex/TEST.md‎

Lines changed: 16 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5637,14 +5637,27 @@ $$
56375637
\frac{
56385638
n_1 \geq n_2
56395639
\qquad
5640-
m_1 \leq m_2
5640+
(m_1 \leq m_2)^?
56415641
}{
5642-
C \vdash {}[ n_1 .. m_1 ] \leq {}[ n_2 .. m_2 ]
5643-
} \, {[\textsc{\scriptsize S{-}limits}]}
5642+
C \vdash {}[ n_1 .. m_1 ] \leq {}[ n_2 .. {m_2^?} ]
5643+
} \, {[\textsc{\scriptsize S{-}limits{-}max}]}
56445644
\qquad
56455645
\end{array}
56465646
$$
56475647

5648+
$$
5649+
\begin{array}{@{}c@{}}\displaystyle
5650+
\frac{
5651+
n_1 \geq n_2
5652+
}{
5653+
C \vdash {}[ n_1 .. \epsilon ] \leq {}[ n_2 .. \epsilon ]
5654+
} \, {[\textsc{\scriptsize S{-}limits{-}eps}]}
5655+
\qquad
5656+
\end{array}
5657+
$$
5658+
5659+
\vspace{1ex}
5660+
56485661
$$
56495662
\begin{array}{@{}c@{}}\displaystyle
56505663
\frac{

‎spectec/test-middlend/TEST.md‎

Lines changed: 24 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -3183,10 +3183,15 @@ relation Instrtype_sub: `%|-%<:%`(context, instrtype, instrtype)
31833183
;; ../../../../specification/wasm-3.0/2.2-validation.subtyping.spectec
31843184
relation Limits_sub: `%|-%<:%`(context, limits, limits)
31853185
;; ../../../../specification/wasm-3.0/2.2-validation.subtyping.spectec
3186-
rule _{C : context, n_1 : n, m_1 : m, n_2 : n, m_2 : m}:
3187-
`%|-%<:%`(C, `[%..%]`_limits(`%`_u64(n_1), ?(`%`_u64(m_1))), `[%..%]`_limits(`%`_u64(n_2), ?(`%`_u64(m_2))))
3186+
rule max{C : context, n_1 : n, m_1 : m, n_2 : n, `m_2?` : m?}:
3187+
`%|-%<:%`(C, `[%..%]`_limits(`%`_u64(n_1), ?(`%`_u64(m_1))), `[%..%]`_limits(`%`_u64(n_2), `%`_u64(m_2)?{m_2 <- `m_2?`}))
3188+
-- if (n_1 >= n_2)
3189+
-- (if (m_1 <= m_2))?{m_2 <- `m_2?`}
3190+
3191+
;; ../../../../specification/wasm-3.0/2.2-validation.subtyping.spectec
3192+
rule eps{C : context, n_1 : n, n_2 : n}:
3193+
`%|-%<:%`(C, `[%..%]`_limits(`%`_u64(n_1), ?()), `[%..%]`_limits(`%`_u64(n_2), ?()))
31883194
-- if (n_1 >= n_2)
3189-
-- if (m_1 <= m_2)
31903195

31913196
;; ../../../../specification/wasm-3.0/2.2-validation.subtyping.spectec
31923197
relation Tagtype_sub: `%|-%<:%`(context, tagtype, tagtype)
@@ -14513,10 +14518,15 @@ relation Instrtype_sub: `%|-%<:%`(context, instrtype, instrtype)
1451314518
;; ../../../../specification/wasm-3.0/2.2-validation.subtyping.spectec
1451414519
relation Limits_sub: `%|-%<:%`(context, limits, limits)
1451514520
;; ../../../../specification/wasm-3.0/2.2-validation.subtyping.spectec
14516-
rule _{C : context, n_1 : n, m_1 : m, n_2 : n, m_2 : m}:
14517-
`%|-%<:%`(C, `[%..%]`_limits(`%`_u64(n_1), ?(`%`_u64(m_1))), `[%..%]`_limits(`%`_u64(n_2), ?(`%`_u64(m_2))))
14521+
rule max{C : context, n_1 : n, m_1 : m, n_2 : n, `m_2?` : m?}:
14522+
`%|-%<:%`(C, `[%..%]`_limits(`%`_u64(n_1), ?(`%`_u64(m_1))), `[%..%]`_limits(`%`_u64(n_2), `%`_u64(m_2)?{m_2 <- `m_2?`}))
14523+
-- if (n_1 >= n_2)
14524+
-- (if (m_1 <= m_2))?{m_2 <- `m_2?`}
14525+
14526+
;; ../../../../specification/wasm-3.0/2.2-validation.subtyping.spectec
14527+
rule eps{C : context, n_1 : n, n_2 : n}:
14528+
`%|-%<:%`(C, `[%..%]`_limits(`%`_u64(n_1), ?()), `[%..%]`_limits(`%`_u64(n_2), ?()))
1451814529
-- if (n_1 >= n_2)
14519-
-- if (m_1 <= m_2)
1452014530

1452114531
;; ../../../../specification/wasm-3.0/2.2-validation.subtyping.spectec
1452214532
relation Tagtype_sub: `%|-%<:%`(context, tagtype, tagtype)
@@ -25864,10 +25874,15 @@ relation Instrtype_sub: `%|-%<:%`(context, instrtype, instrtype)
2586425874
;; ../../../../specification/wasm-3.0/2.2-validation.subtyping.spectec
2586525875
relation Limits_sub: `%|-%<:%`(context, limits, limits)
2586625876
;; ../../../../specification/wasm-3.0/2.2-validation.subtyping.spectec
25867-
rule _{C : context, n_1 : n, m_1 : m, n_2 : n, m_2 : m}:
25868-
`%|-%<:%`(C, `[%..%]`_limits(`%`_u64(n_1), ?(`%`_u64(m_1))), `[%..%]`_limits(`%`_u64(n_2), ?(`%`_u64(m_2))))
25877+
rule max{C : context, n_1 : n, m_1 : m, n_2 : n, `m_2?` : m?}:
25878+
`%|-%<:%`(C, `[%..%]`_limits(`%`_u64(n_1), ?(`%`_u64(m_1))), `[%..%]`_limits(`%`_u64(n_2), `%`_u64(m_2)?{m_2 <- `m_2?`}))
25879+
-- if (n_1 >= n_2)
25880+
-- (if (m_1 <= m_2))?{m_2 <- `m_2?`}
25881+
25882+
;; ../../../../specification/wasm-3.0/2.2-validation.subtyping.spectec
25883+
rule eps{C : context, n_1 : n, n_2 : n}:
25884+
`%|-%<:%`(C, `[%..%]`_limits(`%`_u64(n_1), ?()), `[%..%]`_limits(`%`_u64(n_2), ?()))
2586925885
-- if (n_1 >= n_2)
25870-
-- if (m_1 <= m_2)
2587125886

2587225887
;; ../../../../specification/wasm-3.0/2.2-validation.subtyping.spectec
2587325888
relation Tagtype_sub: `%|-%<:%`(context, tagtype, tagtype)

‎spectec/test-prose/TEST.md‎

Lines changed: 52 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -14886,12 +14886,44 @@ The instruction type :math:`{t_{11}^\ast}~{\rightarrow}_{{x_1^\ast}}\,{t_{12}^\a
1488614886

1488714887

1488814888

14889-
The limits range :math:`{}[ n_1 .. m_1 ]` :ref:`matches <match>` the limits range :math:`{}[ n_2 .. m_2 ]` if:
14889+
The limits range :math:`{}[ n_1 .. {{\mathit{u{\kern-0.1em\scriptstyle 64}}}_1^?} ]` :ref:`matches <match>` the limits range :math:`{}[ n_2 .. {{\mathit{u{\kern-0.1em\scriptstyle 64}}}_2^?} ]` if:
1489014890

1489114891

1489214892
* :math:`n_1` is greater than or equal to :math:`n_2`.
1489314893

14894-
* :math:`m_1` is less than or equal to :math:`m_2`.
14894+
* Either:
14895+
14896+
* :math:`{{\mathit{u{\kern-0.1em\scriptstyle 64}}}_1^?}` is of the form :math:`m_1`.
14897+
14898+
* If :math:`{\mathit{u{\kern-0.1em\scriptstyle 64}}}_2` is defined, then:
14899+
14900+
* :math:`m_1` is less than or equal to :math:`{\mathit{u{\kern-0.1em\scriptstyle 64}}}_2`.
14901+
14902+
* Or:
14903+
14904+
* :math:`{{\mathit{u{\kern-0.1em\scriptstyle 64}}}_1^?}` is absent.
14905+
14906+
* :math:`{{\mathit{u{\kern-0.1em\scriptstyle 64}}}_2^?}` is absent.
14907+
14908+
14909+
14910+
14911+
The limits range :math:`{}[ n_1 .. m_1 ]` :ref:`matches <match>` the limits range :math:`{}[ n_2 .. {m_2^?} ]` if:
14912+
14913+
14914+
* :math:`n_1` is greater than or equal to :math:`n_2`.
14915+
14916+
* If :math:`m_2` is defined, then:
14917+
14918+
* :math:`m_1` is less than or equal to :math:`m_2`.
14919+
14920+
14921+
14922+
14923+
The limits range :math:`{}[ n_1~.. ]` :ref:`matches <match>` the limits range :math:`{}[ n_2~.. ]` if:
14924+
14925+
14926+
* :math:`n_1` is greater than or equal to :math:`n_2`.
1489514927

1489614928

1489714929

@@ -27319,9 +27351,25 @@ Instrtype_sub
2731927351
- C.LOCALS[x] is (SET t).
2732027352

2732127353
Limits_sub
27322-
- the limits range ([ n_1 .. ?(m_1) ]) matches the limits range ([ n_2 .. ?(m_2) ]) if:
27354+
- the limits range ([ n_1 .. u64_1? ]) matches the limits range ([ n_2 .. u64_2? ]) if:
27355+
- n_1 is greater than or equal to n_2.
27356+
- Either:
27357+
- u64_1? is ?(m_1).
27358+
- If u64_2 is defined, then:
27359+
- m_1 is less than or equal to u64_2.
27360+
- Or:
27361+
- u64_1? is ?().
27362+
- u64_2? is ?().
27363+
27364+
Limits_sub/max
27365+
- the limits range ([ n_1 .. ?(m_1) ]) matches the limits range ([ n_2 .. m_2? ]) if:
27366+
- n_1 is greater than or equal to n_2.
27367+
- If m_2 is defined, then:
27368+
- m_1 is less than or equal to m_2.
27369+
27370+
Limits_sub/eps
27371+
- the limits range ([ n_1 .. ?() ]) matches the limits range ([ n_2 .. ?() ]) if:
2732327372
- n_1 is greater than or equal to n_2.
27324-
- m_1 is less than or equal to m_2.
2732527373

2732627374
Tagtype_sub
2732727375
- the tag type deftype_1 matches the tag type deftype_2 if:

‎spectec/test-splice/TEST.md‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1150,7 +1150,8 @@ warning: rule `Instrs_ok/frame` was spliced more than once
11501150
warning: rule `Instrtype_ok` was never spliced
11511151
warning: rule `Instrtype_sub` was never spliced
11521152
warning: rule `Limits_ok` was never spliced
1153-
warning: rule `Limits_sub` was never spliced
1153+
warning: rule `Limits_sub/max` was never spliced
1154+
warning: rule `Limits_sub/eps` was never spliced
11541155
warning: rule `Local_ok/set` was never spliced
11551156
warning: rule `Local_ok/unset` was never spliced
11561157
warning: rule `Mem_ok` was never spliced
@@ -2121,6 +2122,8 @@ warning: rule prose `Instrtype_ok` was never spliced
21212122
warning: rule prose `Instrtype_sub` was never spliced
21222123
warning: rule prose `Limits_ok` was never spliced
21232124
warning: rule prose `Limits_sub` was never spliced
2125+
warning: rule prose `Limits_sub/eps` was never spliced
2126+
warning: rule prose `Limits_sub/max` was never spliced
21242127
warning: rule prose `Local_ok` was never spliced
21252128
warning: rule prose `Local_ok/set` was never spliced
21262129
warning: rule prose `Local_ok/unset` was never spliced

0 commit comments

Comments
 (0)