Result: done Files: crates/nikaia-std/src/tools/bounds_body.nika crates/nikaia-std/src/tools/prover_passes.nika crates/nikaia-std/src/tools/prover_state.nika crates/nikaia-std/src/tools/prover_walk.nika crates/nikaia-std/src/tools/lowered/bounds_body.rs crates/nikaia-std/src/tools/lowered/prover_passes.rs crates/nikaia-std/src/tools/lowered/prover_state.rs crates/nikaia-std/src/tools/lowered/prover_walk.rs tests/compiler/tests/prove_a_precondition_reads_what_an_if_made_known.nika tests/compiler/tests/prove_a_precondition_reads_what_an_if_made_known.stdout tests/compiler/tests/prove_a_let_mut_handed_to_a_call_stays_read.nika tests/compiler/tests/prove_a_let_mut_handed_to_a_call_stays_read.stdout tests/compiler/tests/prove_a_let_mut_given_to_a_mut_parameter_is_not_read.nika tests/compiler/tests/prove_a_let_mut_given_to_a_mut_parameter_is_not_read.stderr tests/compiler/tests/prove_a_let_mut_of_a_call.nika tests/compiler/tests/prove_a_let_mut_of_a_call.stdout tests/compiler/tests/prove_a_branch_let_of_a_call_reaches_the_join.nika tests/compiler/tests/prove_a_branch_let_of_a_call_reaches_the_join.stdout tests/compiler/tests/prove_a_surrogate_pair_decodes_to_a_scalar.nika tests/compiler/tests/prove_a_surrogate_pair_decodes_to_a_scalar.stdout Commit: prover: a let mut of a call, a whole number handed to a reader, a branch’s own let and a call’s precondition read through the join (#1009) Body: Four defects in one commit, since three share prover_walk.nika. (1) precondition_call asks once more with the history (ADR-361 D9, D2), as an_assert does. (2) untracked_in takes the functions whose parameters are all read-only (state.value_readers: the program’s free functions without a mut parameter, and ledger free functions whose signature has none, so scalar::from too). A whole number handed to one of them, or used as a method’s receiver (no std method on a whole number takes mut self), is no longer counted as changed. Deferred bodies, mut parameters and callees it cannot resolve stay as before. readers/Changes are unchanged. (3) prover_let gives a let mut of a call what the callee ensures; prover_follow_mutables follows it as a mutable, or rebinds it where the block hands it on unseen. (4) prover_side renames a branch’s own names (and other names not alive before the if) apart (name#t|e), where before it dropped every fact that read them. Probed at the edges: else-less if, throw in a branch, both sides binding a call, a wrong bound (still refused), and json's while-true/push/continue loop shape (proved). Fixes: #1009 Part: #1003 Tests: the six new tests pass at both settings; with develop's compiler (before the change) the same probe bodies were refused with NK1300 (precondition, id/to_string, let mut of call, branch let, surrogate pair), and the mut-parameter program was refused there too, as it should be; tests/compiler --both-settings 384 passed; packages/yaml 9 passed; it filters prove unproved_claims bounds plus the guard set 203 passed (sequences guard green, not raised); clippy clean Gate: green Deviation: none Found: a match on a bool whose arm assigns a let mut whole number is not joined the way an if is: the name is dropped (probe: let mut cp = first; match cp > 5 { true => { cp = cp + 1 }, false => {} }; assert(cp >= 0 && cp <= 11) is refused NK1300 'not a whole number the prover reads'). It does not depend on this change. ADR-361 D9 names only if. Needs: none Changelog: The prover reads a let mut bound to a call, a whole number handed to a function that does not change it, what a branch's own let of a call bounds past the if, and a call's precondition through the history of an if, so json's surrogate-pair decoding proves scalar::from. Owner: none Disk freed: 0.02 GB (scratch binary copy); cache target/nikaia-project-tests 5.8G, disk 11G free, new entry over 100 MB: run-bundle/b2db8b4e959f1cfc 341 MB Rs2nika: none Pushed: 3a9ec3fd (pushed by drive.nika)

This site is open source. Improve this page.