Result: done
Files: crates/nikaia-std/src/num.rs crates/nikaia-std/std.contracts crates/nikaia-std/src/tools/check_walked.nika crates/nikaia-std/src/tools/emit_below.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/check_walked.rs crates/nikaia-std/src/tools/lowered/emit_below.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 crates/nikaia/src/check/mod.rs crates/nikaia/src/prove.rs docs/specification/10-nikaia-light.md tests/compiler/tests/scalar_from_a_proved_code_point.nika tests/compiler/tests/scalar_from_a_proved_code_point.stdout tests/compiler/tests/scalar_from_an_unproved_code_point_is_refused.nika tests/compiler/tests/scalar_from_an_unproved_code_point_is_refused.stderr tests/compiler/tests/scalar_from_through_a_helper_is_proved_at_its_caller.nika tests/compiler/tests/scalar_from_through_a_helper_is_proved_at_its_caller.stdout
Commit: scalar::from(n) with a precondition std publishes, held as a claim of the program at each call
Body: scalar::from(n) (Rust num::scalar_from, emitter maps the path; scalar needs no use) states n >= 0 && n <= 0x10FFFF && (n < 0xD800 || n > 0xDFFF) as a requires in std.contracts, the first one there. The prover reads std’s ledger for a callee the program’s ledger does not name (kept out of the foreign-contract cache), and the precondition at such a call is a claim of the program, as an assert standing there would be (ADR-269 D5/D15, ADR-380 D1): proved there; carried back to the caller’s entry where it reads only parameters, so it becomes that function’s precondition, proved at its callers; NK1207 where it is false; otherwise refused with NK1300 (a warning and the run-time check of scalar_from under unproved-claims = “warn”), and listed by --asserts as scalar::from: <condition>. The walk publishes these claims (ProverWalk.std_claims), and the checker adds them to its claims, so check_claims and the listing treat them as asserts. Part I 2.2 says how an integer becomes a scalar by name.
Part: #1003
Changelog: scalar::from(n) turns an integer into a scalar under a precondition the compiler proves at each call or refuses (NK1300); std’s preconditions are claims of the program like an assert, listed by --asserts.
Pushed: rejected
