Skip to content

[spec] Slight simplification to Rectype_ok2 judgement #2148

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
rossberg merged 1 commit into from
Apr 22, 2026
Merged

[spec] Slight simplification to Rectype_ok2 judgement #2148

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
31 changes: 15 additions & 16 deletions specification/wasm-3.0/2.1-validation.types.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,18 +85,18 @@ rule Expand_use/typeidx: _IDX typeidx ~~_C comptype -- Expand: C.TYPES[typeidx]
;; Type definitions

syntax oktypeidx hint(show OK#((typeidx))) hint(prose_desc "type index") =
| OK typeidx hint(show OK#(%)) hint(macro "%subtype") hint(prose "%1")
syntax oktypeidxnat hint(show OK#(typeidx,n)) =
| OK typeidx nat hint(show OK#(%,%)) hint(macro "%subtypeext")
| OK typeidx hint(show OK#(%)) hint(macro "%subtype") hint(prose "%1")
syntax oktypenat hint(show OK#(n)) =
| OK nat hint(show OK#(%)) hint(macro "%subtypeext")

relation Packtype_ok: context |- packtype : OK hint(name "K-pack") hint(macro "%packtype")
relation Fieldtype_ok: context |- fieldtype : OK hint(name "K-field") hint(macro "%fieldtype")
relation Storagetype_ok: context |- storagetype : OK hint(name "K-storage") hint(macro "%storagetype")
relation Comptype_ok: context |- comptype : OK hint(name "K-comp") hint(macro "%comptype")
relation Subtype_ok: context |- subtype : oktypeidx hint(name "K-sub") hint(macro "%subtype") hint(prosepp "for")
relation Rectype_ok: context |- rectype : oktypeidx hint(name "K-rect") hint(macro "%rectype") hint(prosepp "for")
relation Subtype_ok2: context |- subtype : oktypeidxnat hint(name "K-sub2") hint(macro "%subtypeext") hint(prosepp "for")
relation Rectype_ok2: context |- rectype : oktypeidxnat hint(name "K-rec2") hint(macro "%rectypeext") hint(prosepp "for")
relation Subtype_ok2: context |- subtype : oktypenat hint(name "K-sub2") hint(macro "%subtypeext") hint(prosepp "for")
relation Rectype_ok2: context |- rectype : oktypenat hint(name "K-rec2") hint(macro "%rectypeext") hint(prosepp "for")
relation Deftype_ok: context |- deftype : OK hint(name "K-def") hint(macro "%deftype")

;; Forward declarations for validation.subtyping
Expand Down Expand Up @@ -156,21 +156,20 @@ rule Subtype_ok:
-- Comptype_ok: C |- comptype : OK
-- (Comptype_sub: C |- comptype <: comptype')*

def $before(typeuse, typeidx, nat) : bool hint(show % << %,%) hint(macro "before")
def $before(deftype, x, i) = true
def $before(_IDX typeidx, x, i) = typeidx < x
def $before(REC j, x, i) = j < i
def $before(typeuse, nat) : bool hint(show % << %) hint(macro "before")
def $before(REC j, i) = j < i
def $before(typeuse, i) = true -- otherwise

def $unrollht(context, heaptype) : subtype hint(show $unroll_(%,%))
def $unrollht(C, deftype) = $unrolldt(deftype)
def $unrollht(C, _IDX typeidx) = $unrolldt(C.TYPES[typeidx])
def $unrollht(C, REC i) = C.RECS[i]

rule Subtype_ok2:
C |- SUB FINAL? typeuse* comptype : OK x i
C |- SUB FINAL? typeuse* comptype : OK(i)
-- if |typeuse*| <= 1
-- (Typeuse_ok: C |- typeuse : OK)*
-- (if $before(typeuse, x, i))*
-- (if $before(typeuse, i))*
-- (if $unrollht(C, typeuse) = SUB typeuse'* comptype')*
----
-- Comptype_ok: C |- comptype : OK
Expand All @@ -187,17 +186,17 @@ rule Rectype_ok/cons:


rule Rectype_ok2/empty:
C |- REC eps : OK x i
C |- REC eps : OK(i)

rule Rectype_ok2/cons:
C |- REC (subtype_1 subtype*) : OK x i
-- Subtype_ok2: C |- subtype_1 : OK x i
-- Rectype_ok2: C |- REC subtype* : OK x $(i+1)
C |- REC (subtype_1 subtype*) : OK(i)
-- Subtype_ok2: C |- subtype_1 : OK(i)
-- Rectype_ok2: C |- REC subtype* : OK($(i+1))


rule Deftype_ok:
C |- _DEF rectype i : OK
-- Rectype_ok2: C, RECS subtype^n |- rectype : OK x 0
-- Rectype_ok2: C, RECS subtype^n |- rectype : OK(0)
-- if rectype = REC subtype^n
-- if i < n

Expand Down
2 changes: 1 addition & 1 deletion specification/wasm-3.0/7.0-soundness.contexts.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ rule Context_ok:
}
-- if C_0 = {TYPES dt^n}
-- (Deftype_ok: {TYPES dt^n[0 : i]} |- dt : OK)^(i<n)
-- (Subtype_ok2: {TYPES dt^n, RECS st^m} |- st : OK n i)^(i<m)
-- (Subtype_ok2: {TYPES dt^n, RECS st^m} |- st : OK(i))^(i<m)
-- (Tagtype_ok: C_0 |- jt : OK)*
-- (Globaltype_ok: C_0 |- gt : OK)*
-- (Memtype_ok: C_0 |- mt : OK)*
Expand Down
31 changes: 15 additions & 16 deletions specification/wasm-latest/2.1-validation.types.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,18 +85,18 @@ rule Expand_use/typeidx: _IDX typeidx ~~_C comptype -- Expand: C.TYPES[typeidx]
;; Type definitions

syntax oktypeidx hint(show OK#((typeidx))) hint(prose_desc "type index") =
| OK typeidx hint(show OK#(%)) hint(macro "%subtype") hint(prose "%1")
syntax oktypeidxnat hint(show OK#(typeidx,n)) =
| OK typeidx nat hint(show OK#(%,%)) hint(macro "%subtypeext")
| OK typeidx hint(show OK#(%)) hint(macro "%subtype") hint(prose "%1")
syntax oktypenat hint(show OK#(n)) =
| OK nat hint(show OK#(%)) hint(macro "%subtypeext")

relation Packtype_ok: context |- packtype : OK hint(name "K-pack") hint(macro "%packtype")
relation Fieldtype_ok: context |- fieldtype : OK hint(name "K-field") hint(macro "%fieldtype")
relation Storagetype_ok: context |- storagetype : OK hint(name "K-storage") hint(macro "%storagetype")
relation Comptype_ok: context |- comptype : OK hint(name "K-comp") hint(macro "%comptype")
relation Subtype_ok: context |- subtype : oktypeidx hint(name "K-sub") hint(macro "%subtype") hint(prosepp "for")
relation Rectype_ok: context |- rectype : oktypeidx hint(name "K-rect") hint(macro "%rectype") hint(prosepp "for")
relation Subtype_ok2: context |- subtype : oktypeidxnat hint(name "K-sub2") hint(macro "%subtypeext") hint(prosepp "for")
relation Rectype_ok2: context |- rectype : oktypeidxnat hint(name "K-rec2") hint(macro "%rectypeext") hint(prosepp "for")
relation Subtype_ok2: context |- subtype : oktypenat hint(name "K-sub2") hint(macro "%subtypeext") hint(prosepp "for")
relation Rectype_ok2: context |- rectype : oktypenat hint(name "K-rec2") hint(macro "%rectypeext") hint(prosepp "for")
relation Deftype_ok: context |- deftype : OK hint(name "K-def") hint(macro "%deftype")

;; Forward declarations for validation.subtyping
Expand Down Expand Up @@ -156,21 +156,20 @@ rule Subtype_ok:
-- Comptype_ok: C |- comptype : OK
-- (Comptype_sub: C |- comptype <: comptype')*

def $before(typeuse, typeidx, nat) : bool hint(show % << %,%) hint(macro "before")
def $before(deftype, x, i) = true
def $before(_IDX typeidx, x, i) = typeidx < x
def $before(REC j, x, i) = j < i
def $before(typeuse, nat) : bool hint(show % << %) hint(macro "before")
def $before(REC j, i) = j < i
def $before(typeuse, i) = true -- otherwise

def $unrollht(context, heaptype) : subtype hint(show $unroll_(%,%))
def $unrollht(C, deftype) = $unrolldt(deftype)
def $unrollht(C, _IDX typeidx) = $unrolldt(C.TYPES[typeidx])
def $unrollht(C, REC i) = C.RECS[i]

rule Subtype_ok2:
C |- SUB FINAL? typeuse* comptype : OK x i
C |- SUB FINAL? typeuse* comptype : OK(i)
-- if |typeuse*| <= 1
-- (Typeuse_ok: C |- typeuse : OK)*
-- (if $before(typeuse, x, i))*
-- (if $before(typeuse, i))*
-- (if $unrollht(C, typeuse) = SUB typeuse'* comptype')*
----
-- Comptype_ok: C |- comptype : OK
Expand All @@ -187,17 +186,17 @@ rule Rectype_ok/cons:


rule Rectype_ok2/empty:
C |- REC eps : OK x i
C |- REC eps : OK(i)

rule Rectype_ok2/cons:
C |- REC (subtype_1 subtype*) : OK x i
-- Subtype_ok2: C |- subtype_1 : OK x i
-- Rectype_ok2: C |- REC subtype* : OK x $(i+1)
C |- REC (subtype_1 subtype*) : OK(i)
-- Subtype_ok2: C |- subtype_1 : OK(i)
-- Rectype_ok2: C |- REC subtype* : OK($(i+1))


rule Deftype_ok:
C |- _DEF rectype i : OK
-- Rectype_ok2: C, RECS subtype^n |- rectype : OK x 0
-- Rectype_ok2: C, RECS subtype^n |- rectype : OK(0)
-- if rectype = REC subtype^n
-- if i < n

Expand Down
2 changes: 1 addition & 1 deletion specification/wasm-latest/7.0-soundness.contexts.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ rule Context_ok:
}
-- if C_0 = {TYPES dt^n}
-- (Deftype_ok: {TYPES dt^n[0 : i]} |- dt : OK)^(i<n)
-- (Subtype_ok2: {TYPES dt^n, RECS st^m} |- st : OK n i)^(i<m)
-- (Subtype_ok2: {TYPES dt^n, RECS st^m} |- st : OK(i))^(i<m)
-- (Tagtype_ok: C_0 |- jt : OK)*
-- (Globaltype_ok: C_0 |- gt : OK)*
-- (Memtype_ok: C_0 |- mt : OK)*
Expand Down
Binary file modified spectec/doc/example/output/NanoWasm.pdf
View file
Open in desktop
Binary file not shown.
53 changes: 26 additions & 27 deletions spectec/test-frontend/TEST.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2722,8 +2722,8 @@ relation Vectype_ok: `%|-%:OK`(context, vectype)
`%|-%:OK`(C, vectype)

;; ../../../../specification/wasm-latest/2.1-validation.types.spectec
syntax oktypeidxnat =
| OK(typeidx : typeidx, nat)
syntax oktypenat =
| OK(nat)

;; ../../../../specification/wasm-latest/2.1-validation.types.spectec
relation Packtype_ok: `%|-%:OK`(context, packtype)
Expand Down Expand Up @@ -2757,13 +2757,12 @@ relation Vectype_sub: `%|-%<:%`(context, vectype, vectype)
`%|-%<:%`(C, vectype, vectype)

;; ../../../../specification/wasm-latest/2.1-validation.types.spectec
def $before(typeuse : typeuse, typeidx : typeidx, nat : nat) : bool
def $before(typeuse : typeuse, nat : nat) : bool
;; ../../../../specification/wasm-latest/2.1-validation.types.spectec
def $before{deftype : deftype, x : idx, i : nat}((deftype : deftype <: typeuse), x, i) = true
def $before{j : n, i : nat}(REC_typeuse(j), i) = (j < i)
;; ../../../../specification/wasm-latest/2.1-validation.types.spectec
def $before{typeidx : typeidx, x : idx, i : nat}(_IDX_typeuse(typeidx), x, i) = (typeidx!`%`_typeidx.0 < x!`%`_idx.0)
;; ../../../../specification/wasm-latest/2.1-validation.types.spectec
def $before{j : n, x : idx, i : nat}(REC_typeuse(j), x, i) = (j < i)
def $before{tu : typeuse, i : nat}(tu, i) = true
-- otherwise

;; ../../../../specification/wasm-latest/2.1-validation.types.spectec
def $unrollht(context : context, heaptype : heaptype) : subtype
Expand Down Expand Up @@ -2882,35 +2881,35 @@ relation Comptype_ok: `%|-%:OK`(context, comptype)
-- Resulttype_ok: `%|-%:OK`(C, `%`_resulttype(t_2*{t_2 <- `t_2*`}))

;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:98.1-98.126
relation Subtype_ok2: `%|-%:%`(context, subtype, oktypeidxnat)
;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:169.1-177.49
rule _{C : context, `typeuse*` : typeuse*, comptype : comptype, x : idx, i : nat, `comptype'*` : comptype*, `typeuse'**` : typeuse**}:
`%|-%:%`(C, SUB_subtype(FINAL_final?{}, typeuse*{typeuse <- `typeuse*`}, comptype), OK_oktypeidxnat(x, i))
relation Subtype_ok2: `%|-%:%`(context, subtype, oktypenat)
;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:168.1-176.49
rule _{C : context, `typeuse*` : typeuse*, comptype : comptype, i : nat, `comptype'*` : comptype*, `typeuse'**` : typeuse**}:
`%|-%:%`(C, SUB_subtype(FINAL_final?{}, typeuse*{typeuse <- `typeuse*`}, comptype), OK_oktypenat(i))
-- if (|typeuse*{typeuse <- `typeuse*`}| <= 1)
-- (Typeuse_ok: `%|-%:OK`(C, typeuse))*{typeuse <- `typeuse*`}
-- (if $before(typeuse, x, i))*{typeuse <- `typeuse*`}
-- (if $before(typeuse, i))*{typeuse <- `typeuse*`}
-- (if ($unrollht(C, (typeuse : typeuse <: heaptype)) = SUB_subtype(?(), typeuse'*{typeuse' <- `typeuse'*`}, comptype')))*{comptype' <- `comptype'*`, typeuse <- `typeuse*`, `typeuse'*` <- `typeuse'**`}
-- Comptype_ok: `%|-%:OK`(C, comptype)
-- (Comptype_sub: `%|-%<:%`(C, comptype, comptype'))*{comptype' <- `comptype'*`}

;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:99.1-99.126
relation Rectype_ok2: `%|-%:%`(context, rectype, oktypeidxnat)
;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:189.1-190.24
rule empty{C : context, x : idx, i : nat}:
`%|-%:%`(C, REC_rectype(`%`_list([])), OK_oktypeidxnat(x, i))
relation Rectype_ok2: `%|-%:%`(context, rectype, oktypenat)
;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:188.1-189.23
rule empty{C : context, i : nat}:
`%|-%:%`(C, REC_rectype(`%`_list([])), OK_oktypenat(i))

;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:192.1-195.50
rule cons{C : context, subtype_1 : subtype, `subtype*` : subtype*, x : idx, i : nat}:
`%|-%:%`(C, REC_rectype(`%`_list([subtype_1] ++ subtype*{subtype <- `subtype*`})), OK_oktypeidxnat(x, i))
-- Subtype_ok2: `%|-%:%`(C, subtype_1, OK_oktypeidxnat(x, i))
-- Rectype_ok2: `%|-%:%`(C, REC_rectype(`%`_list(subtype*{subtype <- `subtype*`})), OK_oktypeidxnat(x, (i + 1)))
;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:191.1-194.49
rule cons{C : context, subtype_1 : subtype, `subtype*` : subtype*, i : nat}:
`%|-%:%`(C, REC_rectype(`%`_list([subtype_1] ++ subtype*{subtype <- `subtype*`})), OK_oktypenat(i))
-- Subtype_ok2: `%|-%:%`(C, subtype_1, OK_oktypenat(i))
-- Rectype_ok2: `%|-%:%`(C, REC_rectype(`%`_list(subtype*{subtype <- `subtype*`})), OK_oktypenat((i + 1)))

;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:100.1-100.102
relation Deftype_ok: `%|-%:OK`(context, deftype)
;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:198.1-202.14
rule _{C : context, rectype : rectype, i : n, n : n, `subtype*` : subtype*, x : idx}:
;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:197.1-201.14
rule _{C : context, rectype : rectype, i : n, n : n, `subtype*` : subtype*}:
`%|-%:OK`(C, _DEF_deftype(rectype, i))
-- Rectype_ok2: `%|-%:%`({TYPES [], RECS subtype^n{subtype <- `subtype*`}, TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS []} +++ C, rectype, OK_oktypeidxnat(x, 0))
-- Rectype_ok2: `%|-%:%`({TYPES [], RECS subtype^n{subtype <- `subtype*`}, TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS []} +++ C, rectype, OK_oktypenat(0))
-- if (rectype = REC_rectype(`%`_list(subtype^n{subtype <- `subtype*`})))
-- if (i < n)

Expand Down Expand Up @@ -3151,11 +3150,11 @@ rec {

;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:97.1-97.126
relation Rectype_ok: `%|-%:%`(context, rectype, oktypeidx)
;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:180.1-181.23
;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:179.1-180.23
rule empty{C : context, x : idx}:
`%|-%:%`(C, REC_rectype(`%`_list([])), OK_oktypeidx(x))

;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:183.1-186.48
;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:182.1-185.48
rule cons{C : context, subtype_1 : subtype, `subtype*` : subtype*, x : idx}:
`%|-%:%`(C, REC_rectype(`%`_list([subtype_1] ++ subtype*{subtype <- `subtype*`})), OK_oktypeidx(x))
-- Subtype_ok: `%|-%:%`(C, subtype_1, OK_oktypeidx(x))
Expand Down Expand Up @@ -7665,7 +7664,7 @@ relation Context_ok: `|-%:OK`(context)
-- if (C = {TYPES dt^n{dt <- `dt*`}, RECS st^m{st <- `st*`}, TAGS jt*{jt <- `jt*`}, GLOBALS gt*{gt <- `gt*`}, MEMS mt*{mt <- `mt*`}, TABLES tt*{tt <- `tt*`}, FUNCS dt_F*{dt_F <- `dt_F*`}, DATAS ok*{ok <- `ok*`}, ELEMS et*{et <- `et*`}, LOCALS lct*{lct <- `lct*`}, LABELS [`%`_resulttype((rt : reftype <: valtype)*{rt <- `rt*`})], RETURN ?(`%`_resulttype(lift((rt' : reftype <: valtype)?{rt' <- `rt'?`}))), REFS x*{x <- `x*`}})
-- if (C_0 = {TYPES dt^n{dt <- `dt*`}, RECS [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS []})
-- (Deftype_ok: `%|-%:OK`({TYPES dt^n{dt <- `dt*`}[0 : i], RECS [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS []}, dt))^(i<n){dt <- `dt*`}
-- (Subtype_ok2: `%|-%:%`({TYPES dt^n{dt <- `dt*`}, RECS st^m{st <- `st*`}, TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS []}, st, OK_oktypeidxnat(`%`_typeidx(n), i)))^(i<m){st <- `st*`}
-- (Subtype_ok2: `%|-%:%`({TYPES dt^n{dt <- `dt*`}, RECS st^m{st <- `st*`}, TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS []}, st, OK_oktypenat(i)))^(i<m){st <- `st*`}
-- (Tagtype_ok: `%|-%:OK`(C_0, jt))*{jt <- `jt*`}
-- (Globaltype_ok: `%|-%:OK`(C_0, gt))*{gt <- `gt*`}
-- (Memtype_ok: `%|-%:OK`(C_0, mt))*{mt <- `mt*`}
Expand Down
27 changes: 13 additions & 14 deletions spectec/test-latex/TEST.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4769,7 +4769,7 @@ $$
$$
\begin{array}[t]{@{}lrrl@{}l@{}}
& {\mathsf{ok}}{({\mathit{typeidx}})} & ::= & {\mathsf{ok}}{{\mathit{typeidx}}} \\
& {\mathsf{ok}}{({\mathit{typeidx}}, n)} & ::= & {\mathsf{ok}}{({\mathit{typeidx}}, \mathbb{N})} \\
& {\mathsf{ok}}{n} & ::= & {\mathsf{ok}}{\mathbb{N}} \\
\end{array}
$$

Expand All @@ -4785,9 +4785,9 @@ $\boxed{{\mathit{context}} \vdash {\mathit{subtype}} : {\mathsf{ok}}{({\mathit{t

$\boxed{{\mathit{context}} \vdash {\mathit{rectype}} : {\mathsf{ok}}{({\mathit{typeidx}})}}$

$\boxed{{\mathit{context}} \vdash {\mathit{subtype}} : {\mathsf{ok}}{({\mathit{typeidx}}, n)}}$
$\boxed{{\mathit{context}} \vdash {\mathit{subtype}} : {\mathsf{ok}}{n}}$

$\boxed{{\mathit{context}} \vdash {\mathit{rectype}} : {\mathsf{ok}}{({\mathit{typeidx}}, n)}}$
$\boxed{{\mathit{context}} \vdash {\mathit{rectype}} : {\mathsf{ok}}{n}}$

$\boxed{{\mathit{context}} \vdash {\mathit{deftype}} : \mathsf{ok}}$

Expand Down Expand Up @@ -4937,9 +4937,8 @@ $$

$$
\begin{array}[t]{@{}lcl@{}l@{}}
{\mathit{deftype}} \prec x, i & = & \mathsf{true} \\
{\mathit{typeidx}} \prec x, i & = & {\mathit{typeidx}} < x \\
\mathsf{rec} {.} j \prec x, i & = & j < i \\
\mathsf{rec} {.} j \prec i & = & j < i \\
{\mathit{typeuse}} \prec i & = & \mathsf{true} & \quad \mbox{otherwise} \\
\end{array}
$$

Expand All @@ -4959,7 +4958,7 @@ $$
\qquad
(C \vdash {\mathit{typeuse}} : \mathsf{ok})^\ast
\qquad
({\mathit{typeuse}} \prec x, i)^\ast
({\mathit{typeuse}} \prec i)^\ast
\qquad
({{\mathrm{unroll}}}_{C}({\mathit{typeuse}}) = \mathsf{sub}~{{\mathit{typeuse}'}^\ast}~{\mathit{comptype}'})^\ast
\\
Expand All @@ -4968,7 +4967,7 @@ C \vdash {\mathit{comptype}} : \mathsf{ok}
(C \vdash {\mathit{comptype}} \leq {\mathit{comptype}'})^\ast
\end{array}
}{
C \vdash \mathsf{sub}~{\mathsf{final}^?}~{{\mathit{typeuse}}^\ast}~{\mathit{comptype}} : {\mathsf{ok}}{(x, i)}
C \vdash \mathsf{sub}~{\mathsf{final}^?}~{{\mathit{typeuse}}^\ast}~{\mathit{comptype}} : {\mathsf{ok}}{(i)}
} \, {[\textsc{\scriptsize K{-}sub2}]}
\qquad
\end{array}
Expand Down Expand Up @@ -5005,7 +5004,7 @@ $$
\begin{array}{@{}c@{}}\displaystyle
\frac{
}{
C \vdash \mathsf{rec}~\epsilon : {\mathsf{ok}}{(x, i)}
C \vdash \mathsf{rec}~\epsilon : {\mathsf{ok}}{(i)}
} \, {[\textsc{\scriptsize K{-}rec2{-}empty}]}
\qquad
\end{array}
Expand All @@ -5014,11 +5013,11 @@ $$
$$
\begin{array}{@{}c@{}}\displaystyle
\frac{
C \vdash {\mathit{subtype}}_1 : {\mathsf{ok}}{(x, i)}
C \vdash {\mathit{subtype}}_1 : {\mathsf{ok}}{(i)}
\qquad
C \vdash \mathsf{rec}~{{\mathit{subtype}}^\ast} : {\mathsf{ok}}{(x, i + 1)}
C \vdash \mathsf{rec}~{{\mathit{subtype}}^\ast} : {\mathsf{ok}}{(i + 1)}
}{
C \vdash \mathsf{rec}~({\mathit{subtype}}_1~{{\mathit{subtype}}^\ast}) : {\mathsf{ok}}{(x, i)}
C \vdash \mathsf{rec}~({\mathit{subtype}}_1~{{\mathit{subtype}}^\ast}) : {\mathsf{ok}}{(i)}
} \, {[\textsc{\scriptsize K{-}rec2{-}cons}]}
\qquad
\end{array}
Expand All @@ -5029,7 +5028,7 @@ $$
$$
\begin{array}{@{}c@{}}\displaystyle
\frac{
C, \mathsf{recs}~{{\mathit{subtype}}^{n}} \vdash {\mathit{rectype}} : {\mathsf{ok}}{(x, 0)}
C, \mathsf{recs}~{{\mathit{subtype}}^{n}} \vdash {\mathit{rectype}} : {\mathsf{ok}}{(0)}
\qquad
{\mathit{rectype}} = \mathsf{rec}~{{\mathit{subtype}}^{n}}
\qquad
Expand Down Expand Up @@ -14045,7 +14044,7 @@ C_0 = \{ \mathsf{types}~{{\mathit{dt}}^{n}} \}
\qquad
(\{ \mathsf{types}~{{\mathit{dt}}^{n}}{}[0 : i] \} \vdash {\mathit{dt}} : \mathsf{ok})^{i<n}
\qquad
(\{ \mathsf{types}~{{\mathit{dt}}^{n}},\;\allowbreak \mathsf{recs}~{{\mathit{st}}^{m}} \} \vdash {\mathit{st}} : {\mathsf{ok}}{(n, i)})^{i<m}
(\{ \mathsf{types}~{{\mathit{dt}}^{n}},\;\allowbreak \mathsf{recs}~{{\mathit{st}}^{m}} \} \vdash {\mathit{st}} : {\mathsf{ok}}{(i)})^{i<m}
\qquad
(C_0 \vdash {\mathit{jt}} : \mathsf{ok})^\ast
\qquad
Expand Down
Loading
Loading