Skip to content

OCaml version robustness and more refined exception traps #357

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
jargh wants to merge 3 commits into
base: main
Choose a base branch
from
Open

OCaml version robustness and more refined exception traps #357

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
39ddf2a
Improve OCaml version robustness and exception safety in proof code
jrh13 Feb 25, 2026
198fa8c
Merge branch 'awslabs:main' into caml
jargh Feb 25, 2026
64bd800
Merge branch 'awslabs:main' into caml
jargh Mar 24, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 8 additions & 8 deletions arm/proofs/arm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -355,7 +355,7 @@ let ARM_THM =
with Failure _ ->
failwith ("ARM_THM: Cannot decompose PC expression: " ^ (string_of_term (concl pc_th))) in
let _ = if !arm_print_log then
let opt = Option.get execth2.(pc_ofs) in
let opt = option_get execth2.(pc_ofs) in
(* opt: |- forall ... aligned_bytes_loaded ..
==> arm_decode .. (arm_INST ..) *)
let t = snd (strip_forall (concl (opt))) in
Expand All @@ -364,7 +364,7 @@ let ARM_THM =
Printf.printf "Instruction at `pc + %d (%#x)`: `%s`\n" pc_ofs pc_ofs
(string_of_term term)
in
MATCH_MP th (MATCH_MP (Option.get execth2.(pc_ofs)) loaded_mc_th);;
MATCH_MP th (MATCH_MP (option_get execth2.(pc_ofs)) loaded_mc_th);;

let ARM_ENSURES_SUBLEMMA_TAC =
ENSURES_SUBLEMMA_TAC o MATCH_MP aligned_bytes_loaded_update o CONJUNCT1;;
Expand Down Expand Up @@ -397,13 +397,13 @@ let ARM_CONV (decode_ths:thm option array) (ths:thm list) tm =
(fun th -> (* do not use term_match because it is slow. *)
let c = concl th in
is_eq c && is_read_pc (fst (dest_eq c)))
ths with _ -> failwith "ARM_CONV: can't find `read PC .. = ..` from ths" in
ths with Failure _ -> failwith "ARM_CONV: can't find `read PC .. = ..` from ths" in

(* Find `aligned_bytes_loaded ..`. *)
let aligned_bytes_loaded_mc_ths:thm list =
(* Pick the _mc const from decode_ths, if decode_ths[0] != None, which is
likely to be true. *)
let the_mc:term option = Option.bind decode_ths.(0)
let the_mc:term option = option_bind decode_ths.(0)
(fun th ->
(* th is `forall .., bytes_loaded ... _mc ==> arm_decode ..`. *)
let t = concl th in
Expand All @@ -417,11 +417,11 @@ let ARM_CONV (decode_ths:thm option array) (ths:thm list) tm =
let cc = concl th in is_comb cc && (
let c,args = strip_comb (concl th) in
c = aligned_bytes_loaded_tm &&
(the_mc = None || last args = Option.get the_mc)))
(the_mc = None || last args = option_get the_mc)))
ths in
if res = [] then failwith
("ARM_CONV: can't find `aligned_bytes_loaded .. .. " ^
(if the_mc <> None then string_of_term (Option.get the_mc) else "..")
(if the_mc <> None then string_of_term (option_get the_mc) else "..")
^ "` from ths")
else res in

Expand Down Expand Up @@ -821,7 +821,7 @@ let ARM_SUBROUTINE_SIM_TAC ?(is_safety_thm=false) =
and svar0 = mk_var("s",`:armstate`) in
let ilist = map (vsubst[svar,svar0]) ilist0 in
let subth_specl =
try SPECL ilist subth with _ -> begin
try SPECL ilist subth with Failure _ -> begin
(if (!arm_print_log) then
(Printf.printf "ilist and subth's forall vars do not match\n";
Printf.printf "ilist: [%s]\n" (end_itlist
Expand Down Expand Up @@ -1019,7 +1019,7 @@ let check_forallvars_tac:tactic =
let find_and_check (lhs_pat:term) (t:term) (quants:term list) =
let read_eq = try Some (find_term (fun t ->
is_eq t && can (term_match [] lhs_pat) (lhs t)) t)
with _ -> None in
with Failure _ -> None in
match read_eq with
| Some read_eq ->
let the_var = rhs read_eq in
Expand Down
50 changes: 25 additions & 25 deletions arm/proofs/bignum_emontredc_8n_cdiff.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1332,20 +1332,20 @@ let precalc_sign_template =

let precalc_diffs =
let full_expr = mk_list
(List.concat_map (fun (i0, i1) ->
(flat (map (fun (i0, i1) ->
let absdiff, isneg = cdiff_from_bignum `n:num` `i_div_4:num` i0 i1 in
[absdiff; subst [isneg, mk_var("__isnonneg__",`:bool`)] precalc_sign_template])
[(1,0);(2,0);(3,0);(2,1);(3,1);(3,2)],
[(1,0);(2,0);(3,0);(2,1);(3,1);(3,2)]),
`:(64)word`) in
new_definition (subst [full_expr,`__full_expr__:((64)word)list`]
`precalc_diffs (n:num) (i_div_4:num) = (__full_expr__:((64)word)list)`);;

let precalc_diffs_rev =
let full_expr = mk_list
(List.concat_map (fun (i0, i1) ->
(flat (map (fun (i0, i1) ->
let absdiff, isneg = cdiff_from_bignum `n:num` `i_div_4:num` i0 i1 in
[absdiff; subst [isneg, mk_var("__isnonneg__",`:bool`)] precalc_sign_template])
[(0,1);(0,2);(0,3);(1,2);(1,3);(2,3)],
[(0,1);(0,2);(0,3);(1,2);(1,3);(2,3)]),
`:(64)word`) in
new_definition (subst [full_expr,`__full_expr__:((64)word)list`]
`precalc_diffs_rev (n:num) (i_div_4:num) = (__full_expr__:((64)word)list)`);;
Expand Down Expand Up @@ -3119,24 +3119,24 @@ let extend_first_equiv_for_seq_composition equiv_th1 equiv_th2
let ts = find_terms (fun t ->
is_comb t && name_of (fst (dest_comb t)) = "mk_equiv_regs")
body in
let equiv_regs = List.concat_map (fun t -> let regs = snd (dest_comb t) in
dest_list regs) ts in
let equiv_regs = flat (map (fun t -> let regs = snd (dest_comb t) in
dest_list regs) ts) in
(* mk_equiv_regs2 can specify equivalent regs too. *)
let ts' = find_terms (fun t ->
is_comb t && let t = fst (dest_comb t) in
is_comb t && name_of (fst (dest_comb t)) = "mk_equiv_regs2")
body in
let equiv_regs2 = List.concat_map (fun t ->
let equiv_regs2 = flat (map (fun t ->
let _,(ls1::ls2::[]) = strip_comb t in
let regs1,regs2 = dest_list ls1,dest_list ls2 in
let pairs = zip regs1 regs2 in
map fst (filter (fun (t1,t2) -> t1 = t2) pairs)) ts' in
map fst (filter (fun (t1,t2) -> t1 = t2) pairs)) ts') in

(* some registers that are read. *)
let ts2 = find_terms (fun t ->
is_comb t && name_of (fst (dest_comb t)) = "read")
body in
let specified_regs = List.filter_map (fun t ->
let specified_regs = filter_map (fun t ->
let r = snd (dest_comb t) in if is_const r then Some r else None)
ts2 in
(equiv_regs @ equiv_regs2,specified_regs) in
Expand Down Expand Up @@ -4370,8 +4370,8 @@ let regs_no_abbrev_left =
let addr_regs = (pcend,`X27`)::addr_regs in (* loop counter *)
let res = tl (backward_taint_analysis (snd OUTERLOOP_STEP3_EXEC)
[pcbeg,pcend] (map (fun (x,y) -> x,[y]) addr_regs)) in
List.map (fun pcdiv4 ->
try assoc (pcdiv4 * 4) res with _ -> [])
map (fun pcdiv4 ->
try assoc (pcdiv4 * 4) res with Failure _ -> [])
((pcbeg / 4) -- (pcend / 4));;

let regs_no_abbrev_right =
Expand All @@ -4383,8 +4383,8 @@ let regs_no_abbrev_right =
let addr_regs = (pcend,`X27`)::addr_regs in (* loop counter *)
let res = tl (backward_taint_analysis (snd BIGNUM_EMONTREDC_8N_CDIFF_EXEC)
[pcbeg,pcend] (map (fun (x,y) -> x,[y]) addr_regs)) in
List.map (fun pcdiv4 ->
try assoc (pcdiv4 * 4) res with _ -> [])
map (fun pcdiv4 ->
try assoc (pcdiv4 * 4) res with Failure _ -> [])
((pcbeg / 4) -- (pcend / 4));;


Expand Down Expand Up @@ -4668,8 +4668,8 @@ let step3_outerloop_out_regs_left,step3_outerloop_out_regs_right =
(Array.of_list inst_map)
step3_outerloop_out_regs_right in
let lr = zip m step3_outerloop_out_regs_right in
let lr = List.filter_map (fun x,y ->
if x = None then None else Some (snd (Option.get x),y)) lr in
let lr = filter_map (fun x,y ->
if x = None then None else Some (snd (option_get x),y)) lr in
unzip lr;;

let step3_outerloop_eqout_regs = build_equiv_regs2
Expand Down Expand Up @@ -4729,7 +4729,7 @@ let regs_no_abbrev_left =
let addr_regs = (pcend,[`X27`;`X0`;`X1`;`X2`;`SP`;`X30`])::addr_regs in
let res = tl (backward_taint_analysis (snd OUTERLOOP_STEP3_EXEC)
[pcbeg,pcend] addr_regs) in
List.map (fun pcdiv4 -> try assoc (pcdiv4 * 4) res with _ -> [])
map (fun pcdiv4 -> try assoc (pcdiv4 * 4) res with Failure _ -> [])
((pcbeg / 4) -- (pcend / 4));;

let regs_no_abbrev_right =
Expand All @@ -4745,7 +4745,7 @@ let regs_no_abbrev_right =
addr_regs in
let res = tl (backward_taint_analysis (snd BIGNUM_EMONTREDC_8N_CDIFF_EXEC)
[pcbeg,pcend] addr_regs) in
List.map (fun pcdiv4 -> try assoc (pcdiv4 * 4) res with _ -> [])
map (fun pcdiv4 -> try assoc (pcdiv4 * 4) res with Failure _ -> [])
((pcbeg / 4) -- (pcend / 4));;


Expand Down Expand Up @@ -4935,8 +4935,8 @@ let step3_inner_loop_postamble_out_regs_left,
(Array.of_list inst_map)
step3_inner_loop_postamble_out_regs_right in
let lr = zip m step3_inner_loop_postamble_out_regs_right in
let lr = List.filter_map (fun x,y ->
if x = None then None else Some (snd (Option.get x),y)) lr in
let lr = filter_map (fun x,y ->
if x = None then None else Some (snd (option_get x),y)) lr in
unzip lr;;

let step3_inner_loop_postamble_eqout_regs = build_equiv_regs2
Expand Down Expand Up @@ -5001,7 +5001,7 @@ let regs_no_abbrev_left =
let addr_regs = update_key_list pcend [`X0`;`X1`;`X2`;`SP`;`X30`;`X26`] addr_regs in
let res = tl (backward_taint_analysis (snd OUTERLOOP_STEP3_EXEC)
[pcbeg,pcend] addr_regs) in
List.map (fun pcdiv4 -> try assoc (pcdiv4 * 4) res with _ -> [])
map (fun pcdiv4 -> try assoc (pcdiv4 * 4) res with Failure _ -> [])
((pcbeg / 4) -- (pcend / 4));;

let regs_no_abbrev_right =
Expand All @@ -5015,7 +5015,7 @@ let regs_no_abbrev_right =
let addr_regs = update_key_list pcend [`X0`;`X1`;`X2`;`SP`;`X30`;`X26`] addr_regs in
let res = tl (backward_taint_analysis (snd BIGNUM_EMONTREDC_8N_CDIFF_EXEC)
[pcbeg,pcend] addr_regs) in
List.map (fun pcdiv4 -> try assoc (pcdiv4 * 4) res with _ -> [])
map (fun pcdiv4 -> try assoc (pcdiv4 * 4) res with Failure _ -> [])
((pcbeg / 4) -- (pcend / 4));;


Expand Down Expand Up @@ -5567,7 +5567,7 @@ let regs_no_abbrev_left =
[`X27`;`X0`;`X1`;`X2`;`SP`;`X30`] addr_regs in
let res = tl (backward_taint_analysis (snd OUTERLOOP_STEP1_EXEC)
[pcbeg,pcend] addr_regs) in
List.map (fun pcdiv4 -> try assoc (pcdiv4 * 4) res with _ -> [])
map (fun pcdiv4 -> try assoc (pcdiv4 * 4) res with Failure _ -> [])
((pcbeg / 4) -- (pcend / 4));;

let regs_no_abbrev_right =
Expand All @@ -5582,7 +5582,7 @@ let regs_no_abbrev_right =
[`X27`;`X0`;`X1`;`X2`;`SP`;`X30`] addr_regs in
let res = tl (backward_taint_analysis (snd MADDLOOP_STEP2_X30_EXEC)
[pcbeg,pcend] addr_regs) in
List.map (fun pcdiv4 -> try assoc (pcdiv4 * 4) res with _ -> [])
map (fun pcdiv4 -> try assoc (pcdiv4 * 4) res with Failure _ -> [])
((pcbeg / 4) -- (pcend / 4));;


Expand Down Expand Up @@ -5994,7 +5994,7 @@ let regs_no_abbrev =
let addr_regs = (pcend,[`X27`;`X0`;`X1`;`X2`;`SP`;`X30`])::addr_regs in
let res = tl (backward_taint_analysis (snd OUTERLOOP_STEP1_EXEC)
[pcbeg,pcend] addr_regs) in
List.map (fun pcdiv4 -> try assoc (pcdiv4 * 4) res with _ -> [])
map (fun pcdiv4 -> try assoc (pcdiv4 * 4) res with Failure _ -> [])
((pcbeg / 4) -- (pcend / 4));;


Expand Down Expand Up @@ -6215,7 +6215,7 @@ let regs_no_abbrev =
let addr_regs = update_key_list pcend [`X0`;`X1`;`X2`;`SP`;`X30`;`X26`] addr_regs in
let res = tl (backward_taint_analysis (snd OUTERLOOP_STEP1_EXEC)
[pcbeg,pcend] addr_regs) in
List.map (fun pcdiv4 -> try assoc (pcdiv4 * 4) res with _ -> [])
map (fun pcdiv4 -> try assoc (pcdiv4 * 4) res with Failure _ -> [])
((pcbeg / 4) -- (pcend / 4));;

(* (state number, (equation, fresh var)) *)
Expand Down
11 changes: 6 additions & 5 deletions arm/proofs/decode.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1267,7 +1267,7 @@ let ALIAS_CONV =
let th' = INST_TYPE (map (fun ty' -> ty,ty')
(type_vars_in_term (concl th))) th in
try f (CONV_RULE (CHANGED_CONV (REWRITE_CONV [SYM xth])) th')
with _ -> I in
with Failure _ -> I in
g `:64` XZR_ZR o g `:32` WZR_ZR o f th in
let f th =
if can (find_term
Expand Down Expand Up @@ -1303,8 +1303,9 @@ let ALIAS_CONV =
self := ONCE_DEPTH_CONV (REWRITES_CONV net);
OPERAND_ALIAS_CONV THENC ALIAS_CONV;;

open Compute;;

let PURE_DECODE_CONV =
let open Compute in

let custom_word_red_conv_list =
(* No WORD_IWORD_CONV *)
Expand Down Expand Up @@ -1379,12 +1380,12 @@ let PURE_DECODE_CONV =
let c = concl th in (* c should be: `decode .. = SOME ...` *)
let r,_ = dest_comb (rhs c) in
if is_const r && name_of r = "SOME" then th else failwith ""
with _ -> failwith ("PURE_DECODE_CONV: " ^ (string_of_term t));;
with Failure _ -> failwith ("PURE_DECODE_CONV: " ^ (string_of_term t));;

let DECODE_CONV tm =
let th = PURE_DECODE_CONV tm in
try CONV_RULE (RAND_CONV (RAND_CONV ALIAS_CONV)) th
with _ -> th;;
with Failure _ -> th;;

(* ------------------------------------------------------------------------- *)
(* Testing and preparation. *)
Expand Down Expand Up @@ -1792,7 +1793,7 @@ let term_of_relocs_arm, assert_relocs =
assert false)
in
pc+4, next_insns
with _ -> failwith ("could not check opcode " ^ (string_of_term reloc_opcode)) in
with Failure _ -> failwith ("could not check opcode " ^ (string_of_term reloc_opcode)) in

(* opcode_fn is the large OCaml function printed by print_literal_relocs_from_elf *)
fun (args,tm) opcode_fn ->
Expand Down
2 changes: 1 addition & 1 deletion arm/proofs/edwards25519_epadd.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3151,7 +3151,7 @@ let EDWARDS25519_EPADD_CORRECT = time prove
MAP_EVERY X_GEN_TAC [`x1:int`; `y1:int`; `x2:int`; `y2:int`] THEN
STRIP_TAC THEN EVERY_ASSUM(fun th ->
try STRIP_ASSUME_TAC(MATCH_MP EDWARDS25519_EXPROJECTIVE_BOUND th)
with _ -> ALL_TAC) THEN
with Failure _ -> ALL_TAC) THEN
DISCARD_STATE_TAC "s39" THEN
DISCARD_MATCHING_ASSUMPTIONS
[`aligned a b`; `nonoverlapping_modulo a b c`] THEN
Expand Down
2 changes: 1 addition & 1 deletion arm/proofs/edwards25519_epadd_alt.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1790,7 +1790,7 @@ let EDWARDS25519_EPADD_ALT_CORRECT = time prove
MAP_EVERY X_GEN_TAC [`x1:int`; `y1:int`; `x2:int`; `y2:int`] THEN
STRIP_TAC THEN EVERY_ASSUM(fun th ->
try STRIP_ASSUME_TAC(MATCH_MP EDWARDS25519_EXPROJECTIVE_BOUND th)
with _ -> ALL_TAC) THEN
with Failure _ -> ALL_TAC) THEN
DISCARD_STATE_TAC "s39" THEN
DISCARD_MATCHING_ASSUMPTIONS
[`aligned a b`; `nonoverlapping_modulo a b c`] THEN
Expand Down
Loading
Loading