Check a single constant chosen by Lean NAME (the `--constant` path). Resolve name → constant address via the env's `named` metadata, map to its ingress block's work item, and ship its closure sub-env. By default the check-list is the ENTIRE closure (full-closure typecheck); with `--skip-deps` it is just the subject (deps trusted). Honors `--dump-input` (write stdin for ziskemu), `--execute` (cycle
( client: &EmbeddedClient, plan: &InputPlan, name: &str, args: &Args, )
| 808 | builder = builder.assembly(); |
| 809 | } |
| 810 | if gpu { |
| 811 | builder = builder.gpu(); |
| 812 | } |
| 813 | Ok(builder.build()?) |
| 814 | } |
| 815 | |
| 816 | /// Check a single constant chosen by Lean NAME (one iteration of `--consts`). |
| 817 | /// Resolve name → constant address via the env's `named` metadata, map to its |
| 818 | /// ingress block's work item, and ship its closure sub-env. By default the |
| 819 | /// check-list is the ENTIRE closure (full-closure typecheck); with |
| 820 | /// `--skip-deps` it is just the subject (deps trusted). Honors `--dump-input` |
| 821 | /// (write stdin for ziskemu), `--execute` (cycles), and plain prove (single |
| 822 | /// leaf, subject-bound + verified). No aggregation — it's one leaf. |
| 823 | async fn run_constant( |
| 824 | client: &EmbeddedClient, |
| 825 | plan: &InputPlan, |
| 826 | name: &str, |
| 827 | args: &Args, |
| 828 | ) -> Result<()> { |
| 829 | use ix_common::address::Address; |
| 830 | |
| 831 | // Resolve the Lean name → constant address via the full env's metadata |
| 832 | // (`get_anon` discards `named`, so load the full env just for the lookup). |
| 833 | let full = |
| 834 | IxonEnv::get(&mut &plan.env_bytes[..]).expect("invalid Ixon environment"); |
| 835 | // `«»`-insensitive match (Lean-escaped vs bare renderings; see |
| 836 | // `ix_common::env::normalize_displayed_name`). |
| 837 | let want = ix_common::env::normalize_displayed_name(name); |
| 838 | let target: Address = full |
| 839 | .named |
| 840 | .iter() |
| 841 | .find(|e| { |
| 842 | ix_common::env::normalize_displayed_name(&e.key().to_string()) == want |
| 843 | }) |
| 844 | .map(|e| e.value().addr.clone()) |
| 845 | .ok_or_else(|| { |
| 846 | anyhow::anyhow!("no constant named {name:?} in {}", plan.label) |
| 847 | })?; |
| 848 | |
| 849 | // The name's work item is the one whose ingress block owns it — works for a |
| 850 | // standalone const (block == itself) and a member of a Muts block (block == |
| 851 | // the mutual container, checked atomically). |
| 852 | let env = IxonEnv::get_anon(&mut &plan.env_bytes[..]) |
| 853 | .expect("invalid Ixon environment"); |
| 854 | let work = build_anon_work(&env).expect("build_anon_work"); |
| 855 | let block = block_of_addr(&env, &target); |
| 856 | let item = work |
| 857 | .iter() |
| 858 | .find(|w| work_block_addr(&env, w) == block) |
| 859 | .ok_or_else(|| { |
| 860 | anyhow::anyhow!( |
| 861 | "{name:?} resolved to block {}… but no work item covers it", |
| 862 | &block.hex()[..16] |
| 863 | ) |
| 864 | })?; |
| 865 | |
| 866 | // Closure sub-env (the named constant's transitive deps), faulted in lazily |
| 867 | // by the guest. |
no test coverage detected