Repository navigation
Refusals of an element loop through an index and of a lane's let mut offset give the loop to write, and cairn rules CODE leads with that code's rule - #184
Conversation
…offset give the loop to write, and cairn rules CODE leads with that code's rule
… protocol corpus is regenerated from the cards
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 42246b0f5a
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| lent = c.p.lends.get(ty.name) if not is_view(ty) else None | ||
| count, one = f"len({whole})", f"{whole}[i]" | ||
| if lent and lent[1] == "0": # a Vec: v.len elements of v.data | ||
| count, one = f"{whole}.{lent[2]}", f"{whole}.{lent[0]}[i]" | ||
| return f"{whole} is reached through an index, and {only}: write for i in 0..{count} {{ let {s.name} = {one}; }}." |
There was a problem hiding this comment.
When the indexed expression is not itself iterable, this fallback presents an invalid rewrite. For example, for x in a[k] {} with a: ro<u64>[n] now recommends for i in 0..len(a[k]) { let x = a[k][i]; }, but that rewrite is rejected with E-LEN because a[k] is a scalar. Use the type obtained above to emit the direct index loop only for supported iterable types; otherwise retain a value/type-specific diagnostic.
Useful? React with 👍 / 👎.
| for lane, size in (block.args, block.args[::-1]): | ||
| if lane.tag == "name" and lane.val == binder and size.tag in {"name", "int"}: |
There was a problem hiding this comment.
This condition treats every named stride as the constant S required by the lane rule. If S is a function parameter in out[b * S + j], the diagnostic recommends either binding j immutably or using for j in 0..S, but both rewrites remain E-PARALLEL-RACE because the checker cannot establish a constant stride. Only append this guidance after confirming that size resolves to a compile-time constant.
Useful? React with 👍 / 👎.
Summary
Three refusals that sent an agent the wrong way now give the change to make.
for x in slots.data[k].bufis refused with the index loop to write, where it said to bind the array to a name, which would move an owner out of its place. A lane's block write through alet mutoffset is refused with the reason its bound is unknown and a rewrite that is accepted.cairn rules CODEputs the card's sentences that name the code first.Motivation
The cold probe of main at dda8208 met each of these writing correct programs. In
pool,E-ELEMENT-LOOPnamed a fix that cannot work, andcairn rules E-ELEMENT-LOOPprinted 1.3k of the base card with no sentence about the code: one wasted round and a card read for nothing. Insieve,while j < S { comp[b * S + j] = 1; j += p; }was refused withE-PARALLEL-RACEthree times over, the message restating the rule the write already followed, until a 30-line experiment showed that only aforbinder or an immutableletcarries a bound: four rounds. Part of #124.Changes
unnamedwrites theE-ELEMENT-LOOPmessage for what is neither a name nor a field path: the index loop for a place reached through an index (v.lenandv.data[i]for aVec,len(p)andp[i]otherwise) or for a part, and aletfor any other value (src/cairn/compiler/check/statements.py).unboundedadds toE-PARALLEL-RACE, for an indexb * S + jwithjalet mutlocal, that a bound is known only of aforbinder or an immutablelet, and the rewritelet at = j; if at < S { out[b * S + at] = ...; }(src/cairn/compiler/check/concurrency.py).rulesof a code leads its card with the sentences that name the code and keeps every other sentence where it stood (led); the base card namesE-ELEMENT-LOOPwhere it statesfor i, x in xs, as(copyable; E-ELEMENT-LOOP)in place of(copyable elements), and the parallel card says that the block's offset is aforbinder or an immutablelet(src/cairn/agent/teaching.py).make editors, tools/corpus/curriculum.py and tools/corpus/protocol_curriculum.py regenerate what quotes the cards.cairn rules); evidence/v1_2/loop gains the sizes below.let mut(tests/soundness/test_blocks.py);cairn rulesleading with the code's sentences while keeping each sentence once, and a card asked by name unchanged (tests/tooling/test_rules.py).Behaviour and compatibility
Only messages and the order of a card's sentences change. Every program is accepted or refused as before, with the same code at the same place.
cairn rules CARDand every card a host sends keep their order;cairn rules CODEreturns the same sentences led by the code's, and a code its card never names, 86 of 215, reads as before. The base card's wording was chosen to stay inside the context budgettests/tooling/test_tools.py::test_measure_contextholds the cards to: 23 packets now carry 130,295 bytes of current cards against 130,366 with the 0.5 cards, where a longer clause had crossed it.Testing
The 6 failures are GCC 11's thread sanitizer failing its own CHECK on this aarch64 host, known here and passing in CI. After #182 was merged in, the refusal, rules, block, element-loop, incremental, docs-example and tool tests ran again: 544 passed. The full run first showed
test_measure_contextfailing, because the base card's first wording (xs a name or a field path: E-ELEMENT-LOOP) put the current cards 757 bytes over the 0.5 cards across its 23 packets; the shorter clause above leaves them 71 bytes under.Evidence and claims
No claim changes. evidence/v1_2/loop gains the sizes below; no model ran.
Performance
Bytes an agent reads, piped, on the programs of the new tests:
for x in slots.data[k].buflet mutoffsetcairn rules E-ELEMENT-LOOPcairn rules E-PARALLEL-RACEcairn rules E-EFFECT-ORDEREach refusal grows by the rewrite it now writes out, 110 to 200 bytes; for the probe each one replaced one round or more of a whole request. Checking time is unchanged: the new text is built only when the refusal is.
Checklist
make editors,make docs)