From a1d546cc74a72abc4973bf96f72bbd529320d711 Mon Sep 17 00:00:00 2001 From: zinc Date: Wed, 14 Oct 2026 20:46:17 +0330 Subject: wip: prover gaps (inline len bound, cross-array, rt.new depth, fixed new, affine i*n+k); unbuilt and untested --- src/compiler/stmt.zc | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'src/compiler/stmt.zc') diff --git a/src/compiler/stmt.zc b/src/compiler/stmt.zc index 703f2db..007306c 100644 --- a/src/compiler/stmt.zc +++ b/src/compiler/stmt.zc @@ -337,7 +337,7 @@ int kw_for() { // i < n with a variable n: a jump to the loop entry, where hoisted checks get their flags (see hoist_guard) if (fbnd && infn && !dry && tk == T_ID) { peekat(1); if (pk_tk == T_ID) { peek(); if (pk_tk == T_OP && pk_tv == s_lt) { xe = hole(); op(O_JMP); } } } c0 = here; - ft_iv = -1; ft_ck = -1; fs_ok = 0; fortest = 1; + ft_iv = -1; ft_ck = -1; ft_ln = -1; fs_ok = 0; fortest = 1; if (!is_op(s_semi)) { if (tk == T_NUM && tv) { peek(); if (pk_tk == T_OP && pk_tv == s_semi) inf = 1; } c = borrow_condition(); @@ -367,6 +367,8 @@ int kw_for() { } if (cl && ft_bd >= 0 && getlo(ft_iv) >= 0 && getln(ft_bd) >= 0) { if (!ldirty(r, lname[getln(ft_bd)]) && lclean(getln(ft_bd))) lpfact[lsp - 1] = pfact(ft_iv, ft_bd, getln(ft_bd)); + } else if (cl && ft_bd < 0 && ft_ln >= 0 && getlo(ft_iv) >= 0) { // i < len(a) written in the test + if (!ldirty(r, lname[ft_ln]) && lclean(ft_ln)) lpfact[lsp - 1] = pfact(ft_iv, 0 - 3, ft_ln); } else if (cl && ft_ck >= 0 && getlo(ft_iv) >= 0) { // i < constant: proves a fixed array that long lpfact[lsp - 1] = pfact(ft_iv, -1, 0 - ft_ck - 2); } else if (cl && xe >= 0 && ft_bd >= 0 && ltype[ft_iv] == tint && ltype[ft_bd] == tint) { r[52] = 1; r[41] = ft_bd; } // i < n: checks against n can be hoisted -- cgit v1.2.3