Merged
Conversation
- Delete all 34 Pulse.Soundness.* files - Make tot_typing, ghost_typing, universe_of, typing = unit - Remove typing token fields from st_typing, comp_typing, st_comp_typing, bind_comp, st_equiv constructors - Remove effect_annot_typing body (= unit) - Remove post_typing RT field from post_hint_t - Simplify post_hint_typing to return unit values - Move stt_env and check_top_level_environment to Pulse.Typing.Env - Update Pulse.Main.fst to remove soundness_lemma, replace elab_st_typing with RU.magic() - Remove Pulse.Soundness.Common import from Pulse.Typing.FV Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
All typing types (st_typing, comp_typing, st_comp_typing, bind_comp, st_equiv, st_sub, slprop_equiv, lift_comp, br_typing, brs_typing, pats_complete, non_informative) are now defined as unit. Replace all removed constructor calls with () including: - T_WithLocal, T_WithLocalUninit, T_WithLocalArray, T_WithLocalArrayUninit - T_Admit, T_Return, T_If, T_While, T_Abs, T_Match, T_Frame - T_IntroPure, T_IntroExists, T_ElimExists, T_Rewrite, T_Goto - T_ST, T_STGhost, T_Equiv, T_Sub, T_Lift, T_ForwardJumpLabel - T_Unreachable - STC, CT_ST, CT_STGhost, CT_STAtomic - VE_Refl, VE_Ext, VE_Trans, VE_Sym, VE_Comm, VE_Unit, VE_Ctxt - VE_Fa, VE_Assoc - PC_Elab, TBRS_0, TBRS_1, TBR - ST_TotEquiv, ST_SLPropEquiv - STS_Refl, STS_AtomicInvs, STS_GhostInvs - Lift_Observability, Lift_Neutral_Ghost Update comp_for_post_hint calls with explicit g and pre args. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
All remaining inductive typing types (st_typing, comp_typing, st_comp_typing, bind_comp, st_equiv, st_sub, slprop_equiv, lift_comp, non_informative, pats_complete, brs_typing, br_typing) are now unit type aliases. Implicit arguments that were previously inferred from these typing tokens (e.g., #g, #t, #c in functions taking st_typing g t c) are now explicit, since F* can no longer infer them from unit-typed parameters. Key changes: - Pulse.Typing.fst: All remaining inductive types changed to unit - Function signatures updated in Metatheory, Combinators, Checker.Base, FV - All call sites updated to pass explicit arguments - Constructor calls replaced with () - Pattern matches on constructors replaced with admit() or () - br_typing_vis in Checker.Match made into unit alias Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
When typing tokens were replaced with unit, the st_terms that were
implicitly determined by typing constructors were lost in several
files. This commit fixes:
- Abs.fst: Return wtag None (Tm_Abs {...}) instead of body_closed
- Admit.fst: Return wtag (Tm_Admit {...}) instead of t0 (user term)
- Prover.fst: Use Tm_IntroPure instead of Tm_ST placeholder
- Prover.fst: Use Tm_IntroExists instead of Tm_ST placeholder
- Prover.fst: Use Tm_Unreachable instead of Tm_ST placeholder
- Prover.fst: Fix k_unreach to use Tm_Unreachable with correct ctag
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Since all typing token types (tot_typing, slprop_equiv, st_typing, comp_typing, universe_of, etc.) are now unit, the RU.magic() calls used to construct them are unnecessary. Replace ~120 occurrences with (). Remaining RU.magic() calls are for non-unit types (erased vars, RT.tot_typing, prop_validity, R.term) and are left unchanged. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Drop st_typing, tot_typing, universe_of, slprop_equiv, comp_typing, and other unit-typed proof components from return types and destructuring patterns across the checker codebase. Key changes: - st_typing_in_ctxt: 3-tuple → 2-tuple (drop st_typing) - checker_result_t: simplify type_info from (universe & typ & universe_of) to (universe & typ), and ctxt from (slprop & tot_typing) to slprop - match_comp_res_with_post_hint: return comp_st directly - comp_for_post_hint: return comp_st directly - add_frame/apply_frame/mk_bind: return 2-tuples - check_universe: return universe directly - compute_tot_term_type: return (term & typ) instead of 3-tuple - compute_term_type_and_u: flatten universe out of nested tuple - normalize_slprop: return slprop directly - non_informative_t: simplify to just term - st_typing_correctness_ctot: return Ghost.erased universe directly - purify_and_check_spec: return slprop directly - check_abs/check_abs_core: return 2-tuple Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Simplify function signatures and return types by removing unit-typed typing tokens (tot_typing, typing, universe_of, br_typing_vis, brs_typing, pats_complete, effect_annot_typing) from dependent tuples. Key changes: - check_term/check_tot_term now return term directly - compute_term_type returns 3-tuple (was 4-tuple) - compute_term_type_and_u returns 4-tuple (was 5-tuple) - core_compute_term_type returns 2-tuple (was 3-tuple) - core_check_term/core_check_term' return unit - core_check_term_at_type returns tot_or_ghost directly - check_slprop_with_core returns unit - try_get/get_non_informative_witness: removed t_typing param - try_check/check_prop_validity: removed tot_typing param - Match.fst: removed br_typing_vis/brs_typing/pats_complete from tuples - Return.fst: simplified return_type to (ty & u) from (ty & u & universe_of) - WithLocal/WithLocalArray: simplified init tuples - JoinComp: join_effect_annot returns effect_annot directly Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
All functions in these modules returned unit (or tuples of unit) since all typing token types are now unit. Inline the trivial returns at call sites and delete all 4 Metatheory files (384 lines). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
These fields existed to document that post has a free de Bruijn variable for the result. Now that all typing tokens are unit, they served no purpose. Added a comment on the post field instead. Also removed the now-unnecessary post_hint_typing_t type and post_hint_typing function. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Resolved conflicts in Pulse.Typing.fst (keep typing types as unit, discard re-added inductive constructors from upstream) and Pulse.Checker.While.fst (incorporate dec_formula/multi-measure support from upstream while keeping unit-typed tokens). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Remove all 17 type definitions that were previously simplified to unit aliases (tot_typing, st_typing, comp_typing, slprop_equiv, universe_of, st_equiv, st_sub, lift_comp, st_comp_typing, bind_comp, non_informative, pats_complete, brs_typing, br_typing, effect_annot_typing, typing, ghost_typing) from Pulse.Typing.fst. Replace all uses across 54 files with 'unit'. Where implicit arguments were previously inferred from typing token parameters, make them explicit. Remove helper functions that only constructed unit values (star_typing*, emp_typing, etc.). Remove effect_annot_typing and ty_typing fields from post_hint_t record. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Remove 147 let-bindings of the form 'let x : unit = () in' across 19 files, replacing their use sites with (). These bindings were remnants of the typing token removal and served no purpose. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Remove the (pre_typing:unit) parameter from all checker check functions and their call sites, and (ctxt_typing:unit) from Return.check. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Remove unit-typed parameters (pre_typing, ctxt_typing, d, typing, etc.) from function signatures in LN, FV, Elaborate.Core, Combinators, Base, Prover, SLPropEquiv, While, JoinComp, Comp, WithLocal, WithLocalArray, Abs, Exists, Match, Normalize, Pure, and their callers. Also clean up remaining let-bindings of unit values. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Delete the entirely unused Pulse.Typing.LN module (1074 lines). Remove unused GTot/unit-returning functions from: - Pulse.Checker.SLPropEquiv (11 functions) - Pulse.Checker.Base (10 internal functions + 3 exported vals) - Pulse.Typing.Combinators (t_equiv, slprop_equiv_typing, st_equiv_trans) Remove dead FV.st_typing_freevars calls from Abs.fst and Exists.fst. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Remove functions without SMTPat triggers that are never called externally: tot_typing_freevars, comp_typing_freevars, st_typing_freevars, st_typing_freevars_inv, freevars_open_term_both, and 15 internal helpers (tot_or_ghost_typing_freevars, bind_comp_freevars, slprop_equiv_freevars, st_equiv_freevars, prop_validity_fv, st_sub_freevars, st_comp_typing_freevars, freevars_tm_arrow, freevars_mk_*, freevars_ref, freevars_array, etc.) Keep only the SMTPat-triggered lemmas needed by downstream modules. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- Simplify join_comps return type from (comp_st & unit & unit) to comp_st - Simplify invert_forall_typing return from (unit & unit) to unit - Remove unit params: infer_post' (t_typ, post_typing), peel_binders (t_typ), check_fndefn (_pre_typing), non_informative_class_typing (ty_typing) - Remove unused unit functions: slprop_as_list_typing, with_local_pre_typing, with_local_array_pre_typing, body_typing_subst_true, body_typing_ex, unit_typing, equiv_preserves_typing, st_comp_typing_with_post_hint, apply_conversion, tm_inames_subset_typing - Remove stray let-bindings: u_of_1_g', v_equiv_v', eq_v_v', t'_typing, tok', pre_typing' Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.