Explain blow up, give examples (encode/decode functions for mappings, C backend), possible solutions Case tree data structure (Agda) Ulf Norell Phd
Steven:
I suggest that you implement the manual derivation of EqDec like for RISC-V PMP and skip the NoConfusionHom. In your case you can derive EqDec automatically without NoConfusionHom, but that does not work for e.g. MinimalCaps. I have also adapted the MinimalCaps code to add the manual derivation of EqDec without NoConfusionHom: https://github.com/katamaran-project/katamaran/commit/fa11745030f3fd9ab5d4b050989c45b08b1d0a47
(* Denotation of muSail types, TypeDecl.v *)
Fixpoint Val (σ : Ty) : Set :=
match σ with
| int => Z
| bool => Datatypes.bool
| string => String.string
| list σ' => Datatypes.list (Val σ')
| prod σ1 σ2 => Val σ1 * Val σ2
| sum σ1 σ2 => Val σ1 + Val σ2
| unit => Datatypes.unit
| enum E => enumt E
| bvec n => bv n
| tuple σs => EnvRec Val σs
| union U => uniont U
| record R => recordt R
end%type.
(* Bitvector value, BitvectorBase.v *)
Record bv (n : nat) : Set :=
mk { bin : N; _ : Is_true (is_wf n bin) }.
(* Bitvector operations *)
Notation "e1 +ᵇ e2" := (exp_binop bop.bvadd e1 e2) : exp_scope.
Notation "e1 -ᵇ e2" := (exp_binop bop.bvsub e1 e2) : exp_scope.
Notation "e1 *ᵇ e2" := (exp_binop bop.bvmul e1 e2) : exp_scope.
Notation "[ 'bits' x ]" := (of_bitstring x%bits)
(format "[ 'bits' x ]") : bv_scope.
Notation "[ 'bits' ]" := (@of_bitstring 0 bitstring.bN)
(format "[ 'bits' ]") : bv_scope.
Notation "[ 'bits' [ n ] x ]" := (@of_bitstring n x%bits)
(only parsing) : bv_scope.
Notation "[ 'bits' [ 0 ] ]" := (@of_bitstring 0 bitstring.bN)
(only parsing) : bv_scope.
Notation "[ 'bv' x ]" := (mk x%xN I) (format "[ 'bv' x ]") : bv_scope.
Notation "[ 'bv' [ n ] x ]" := (@mk n x%xN I) (only parsing) : bv_scope.
| shiftr {m n} : BinOp (bvec m) (bvec n) (bvec m)
| shiftl {m n} : BinOp (bvec m) (bvec n) (bvec m)
| bvadd {n} : BinOp (bvec n) (bvec n) (bvec n)
| bvsub {n} : BinOp (bvec n) (bvec n) (bvec n)
| bvmul {n} : BinOp (bvec n) (bvec n) (bvec n)
| bvand {n} : BinOp (bvec n) (bvec n) (bvec n)
| bvor {n} : BinOp (bvec n) (bvec n) (bvec n)
| bvxor {n} : BinOp (bvec n) (bvec n) (bvec n)
| bvapp {m n} : BinOp (bvec m) (bvec n) (bvec (m + n))
(* works *)
stm_exp (exp_val (ty.bvec 8) ([bv 0]))Definition record_fold (R : recordi) : NamedEnv Val (record_field_type R) -> recordt R :=
match R with
| capability =>
fun fields =>
MkCap
fields.[??"cap_permission"]
fields.[??"cap_begin"]
fields.[??"cap_end"]
fields.[??"cap_cursor"]
end%exp.record_fold =
fun R : recordi =>
match R as R0 return (forall _ : NamedEnv Val (record_field_type R0), recordt R0) with
| capability =>
fun fields : NamedEnv Val (record_field_type capability) =>
{|
cap_permission := env.lookup fields {| ctx.in_at := 3; ctx.in_valid := eq_refl |};
cap_begin := env.lookup fields {| ctx.in_at := 2; ctx.in_valid := eq_refl |};
cap_end := env.lookup fields {| ctx.in_at := 1; ctx.in_valid := eq_refl |};
cap_cursor := env.lookup fields {| ctx.in_at := 0; ctx.in_valid := eq_refl |}
|}
endDefinition record_unfold (R : recordi) : recordt R -> NamedEnv Val (record_field_type R) :=
match R with
| capability =>
fun c=>
env.nil
► ("cap_permission" ∷ ty.perm ↦ cap_permission c)
► ("cap_begin" ∷ ty.addr ↦ cap_begin c)
► ("cap_end" ∷ ty.addr ↦ cap_end c)
► ("cap_cursor" ∷ ty.addr ↦ cap_cursor c)
end%env.record_unfold =
λ R : recordi,
match R as R0 return (recordt R0 → NamedEnv Val (record_field_type R0)) with
| capability =>
λ c : recordt capability, [env].["cap_permission"∷ty.perm ↦ cap_permission c]
.["cap_begin"∷ty.addr ↦ cap_begin c].["cap_end"∷ty.addr ↦ cap_end c].["cap_cursor"∷ty.addr ↦
cap_cursor c]
end
: ∀ R : recordi, recordt R → NamedEnv Val (record_field_type R)union clause ast = JALR_CAP : (dst, src)
union c lause ast = CJALR : (dst, src, imm)
union clause ast = CJAL : (dst, imm_ext)
union clause ast = BNE : (src, src, imm)
union clause ast = LD : (dst, src, imm)
union clause ast = SD : (src, src, imm)
union clause ast = ADDI : (dst, src, imm)
union clause ast = ADD : (dst, src, src)
union clause ast = SUB : (dst, src, src)
union clause ast = SLT : (dst, src, src)
union clause ast = SLTI : (dst, src, imm)
union clause ast = SLTIU : (dst, src, imm)
union clause ast = SLTU : (dst, src, src)
union clause ast = CMOVE : (dst, src)
union clause ast = CINCOFFSET : (dst, src, src)
union clause ast = CANDPERM : (dst, src, src)
union clause ast = CSETBOUNDS : (dst, src, src)
union clause ast = CSETBOUNDSIMM : (dst, src, imm)
union clause ast = CGETTAG : (dst, src)
union clause ast = CGETPERM : (dst, src)
union clause ast = CGETBASE : (dst, src)
union clause ast = CGETLEN : (dst, src)
union clause ast = CGETADDR : (dst, src)
union clause ast = FAIL : unit
union clause ast = RET : unit
function clause execute(JALR_CAP(cd, cs)) =
execute(CJALR(cd, cs, sail_zeros(imm_size)))
function clause execute(CJALR(cd, cs, imm)) = {
let npc = nextPC();
writeReg(cd) = Cap(npc);
let c = readRegCap(cs);
if not(canIncrCursor(c, imm))
then throw(CapabilityCursorCannotBeModified())
else {
let imm = sail_zero_extend(imm, integer_size); // TODO Why sail_zero_extend and not sail_sign_extend?
let c' = updatePCPerm({c with cap_cursor = c.cap_cursor + imm}); // TODO shouldn't cursor[0] should be set to 0?
PC = c';
true
}
}
function clause execute(CJAL(cd, imm)) = {
let npc = nextPC();
writeReg(cd) = Cap(npc);
addPC(sail_shiftleft(sail_zero_extend(imm, integer_size), 1));
true
}
Definition fun_exec_instr : Stm [i :: ty.instr] ty.bool :=
stm_match_union_alt
instruction (exp_var i)
(fun K =>
match K with
| kjalr_cap => MkAlt (pat_pair "cd" "cs")
(call exec_jalr_cap (exp_var "cd") (exp_var "cs"))%exp
| kcjalr => MkAlt (pat_tuple ("cd" , "cs" , "imm"))
(call exec_cjalr (exp_var "cd") (exp_var "cs") (exp_var "imm"))%exp
| kcjal => MkAlt (pat_pair "cd" "imm")
(call exec_cjal (exp_var "cd") (exp_var "imm"))%exp
| kbne => MkAlt (pat_tuple ("rs1" , "rs2" , "imm"))
(call exec_bne (exp_var "rs1") (exp_var "rs2") (exp_var "imm"))%exp
| kcmove => MkAlt (pat_pair "cd" "cs")
(call exec_cmove (exp_var "cd") (exp_var "cs"))%exp
| kld => MkAlt (pat_tuple ("cd" , "cs" , "imm"))
(call exec_ld (exp_var "cd") (exp_var "cs") (exp_var "imm"))%exp
| ksd => MkAlt (pat_tuple ("rs1" , "rs2" , "imm"))
(call exec_sd (exp_var "rs1") (exp_var "rs2") (exp_var "imm"))%exp
| kcincoffset => MkAlt (pat_tuple ("cd" , "cs" , "rs"))
(call exec_cincoffset (exp_var "cd") (exp_var "cs") (exp_var "rs"))%exp
| kcandperm => MkAlt (pat_tuple ("cd" , "cs" , "rs"))
(call exec_candperm (exp_var "cd") (exp_var "cs") (exp_var "rs"))%exp
| kcsetbounds => MkAlt (pat_tuple ("cd" , "cs" , "rs"))
(call exec_csetbounds (exp_var "cd") (exp_var "cs") (exp_var "rs"))%exp
| kcsetboundsimm => MkAlt (pat_tuple ("cd" , "cs" , "imm"))
(call exec_csetboundsimm (exp_var "cd") (exp_var "cs") (exp_var "imm"))%exp
| kaddi => MkAlt (pat_tuple ("rd" , "rs" , "imm"))
(call exec_addi (exp_var "rd") (exp_var "rs") (exp_var "imm"))%exp
| kadd => MkAlt (pat_tuple ("rd" , "rs1" , "rs2"))
(call exec_add (exp_var "rd") (exp_var "rs1") (exp_var "rs2"))%exp
| ksub => MkAlt (pat_tuple ("rd" , "rs1" , "rs2"))
(call exec_sub (exp_var "rd") (exp_var "rs1") (exp_var "rs2"))%exp
| kslt => MkAlt (pat_tuple ("rd" , "rs1" , "rs2"))
(call exec_slt (exp_var "rd") (exp_var "rs1") (exp_var "rs2"))%exp
| kslti => MkAlt (pat_tuple ("rd" , "rs" , "imm"))
(call exec_slti (exp_var "rd") (exp_var "rs") (exp_var "imm"))%exp
| ksltu => MkAlt (pat_tuple ("rd" , "rs1" , "rs2"))
(call exec_sltu (exp_var "rd") (exp_var "rs1") (exp_var "rs2"))%exp
| ksltiu => MkAlt (pat_tuple ("rd" , "rs" , "imm"))
(call exec_sltiu (exp_var "rd") (exp_var "rs") (exp_var "imm"))%exp
| kcgettag => MkAlt (pat_pair "rd" "cs")
(call exec_cgettag (exp_var "rd") (exp_var "cs"))%exp
| kcgetperm => MkAlt (pat_pair "rd" "cs")
(call exec_cgetperm (exp_var "rd") (exp_var "cs"))%exp
| kcgetbase => MkAlt (pat_pair "rd" "cs")
(call exec_cgetbase (exp_var "rd") (exp_var "cs"))%exp
| kcgetlen => MkAlt (pat_pair "rd" "cs")
(call exec_cgetlen (exp_var "rd") (exp_var "cs"))%exp
| kcgetaddr => MkAlt (pat_pair "rd" "cs")
(call exec_cgetaddr (exp_var "rd") (exp_var "cs"))%exp
| kfail => MkAlt pat_unit
(call exec_fail)%exp
| kret => MkAlt pat_unit
(call exec_ret)%exp
end).For the pattern matching on unions I suggest using https://github.com/katamaran-project/katamaran/blob/6b50d42d5fa4027be887fbd39ccadd3acd57b688/theories/Syntax/Statements.v#L181-L188 For a union type U and scrutinee s it takes a list of alternatives altsand a well-formedness (exhaustiveness) proof alts_wf.
(* Statements.v *)
Definition stm_match_union_alt_list {Γ τ} U (s : Stm Γ (ty.union U))
(alts : UnionAlts U Γ τ) (alts_wf : UnionAltsWf alts) : Stm Γ τ :=
stm_match_union_alt U s
(fun K =>
match findUnionAlt K alts as o return findUnionAlt K alts = o -> _ with
| Some alt => fun _ => alt
| None => fun Heq => False_rect _ (union_alts_wf' alts alts_wf Heq)
end eq_refl).https://github.com/katamaran-project/katamaran|katamaran-project/katamarankatamaran-project/katamaran | Added by GitHub 1:42 For the well-formedness you should just pass Logic.I , i.e. the constructor of True which forces Coq’s typechecker to decide well-formedness. See the notation as a reference https://github.com/katamaran-project/katamaran/blob/6b50d42d5fa4027be887fbd39ccadd3acd57b688/theories/Syntax/Statements.v#L562-L564
(* Statements.v *)
Notation "'match:' e 'in' 'union' U 'with' | x | y | .. | z 'end'" :=
(stm_match_union_alt_list U e (cons x%alt (cons y%alt .. (cons z%alt nil) ..)) Logic.I)
(format "'[hv' 'match:' e 'in' 'union' U 'with' '/' | x '/' | y '/' | .. '/' | z '/' 'end' ']'") : exp_scope.Notation "'match:' e 'in' 'union' U 'with' | x | y | .. | z 'end'" :=
(stm_match_union_alt_list U e (cons x%alt (cons y%alt .. (cons z%alt nil) ..)) Logic.I)
(format "'[hv' 'match:' e 'in' 'union' U 'with' '/' | x '/' | y '/' | .. '/' | z '/' 'end' ']'") : exp_scope.
Notation "'>' K pat => rhs" := (existT K (MkAlt pat rhs%exp))
(K global, at level 200, pat at level 9, format "> K pat => rhs") : alt_scope.
match: acc in union access_type with
|> KRead pat_unit => stm_exp (Some E_Load_Access_Fault)
|> KWrite pat_unit => stm_exp (Some E_SAMO_Access_Fault)
|> KReadWrite pat_unit => stm_exp (Some E_SAMO_Access_Fault)
|> KExecute pat_unit => stm_exp (Some E_Fetch_Access_Fault)
end
Definition fun_foo : Stm [ "u" ∷ ty.union Umyunion ] (ty.int) :=
stm_let
"жmatched1"
(ty.union Umyunion)
(stm_exp (exp_var "u"))
(stm_match_union_alt_list
Umyunion
(stm_exp (exp_var "жmatched1"))
[ existT Kpush (MkAlt pat_unit (stm_exp (exp_int 1%Z))) ]
Logic.I).
Notation "'Read'" := (exp_union access_type KRead (exp_val ty.unit tt)) : exp_scope.
Notation "'Write'" := (exp_union access_type KWrite (exp_val ty.unit tt)) : exp_scope.
Notation "'ReadWrite'" := (exp_union access_type KReadWrite (exp_val ty.unit tt)) : exp_scope.
Notation "'Execute'" := (exp_union access_type KExecute (exp_val ty.unit tt)) : exp_scope.
Notation "'E_Fetch_Access_Fault'" := (exp_union exception_type KE_Fetch_Access_Fault (exp_val ty.unit tt)) : exp_scope.
Notation "'E_Load_Access_Fault'" := (exp_union exception_type KE_Load_Access_Fault (exp_val ty.unit tt)) : exp_scope.
Notation "'E_SAMO_Access_Fault'" := (exp_union exception_type KE_SAMO_Access_Fault (exp_val ty.unit tt)) : exp_scope.
Notation "'E_U_EnvCall'" := (exp_union exception_type KE_U_EnvCall (exp_val ty.unit tt)) : exp_scope.
Notation "'E_M_EnvCall'" := (exp_union exception_type KE_M_EnvCall (exp_val ty.unit tt)) : exp_scope.
Notation "'E_Illegal_Instr'" := (exp_union exception_type KE_Illegal_Instr (exp_val ty.unit tt)) : exp_scope.
Notation "'None'" := (exp_inr (exp_val ty.unit tt)) : exp_scope.
Notation "'Some' va" := (exp_inl va) (at level 10, va at next level) : exp_scope.
Notation "'MemValue' bs memv" := (exp_union (memory_op_result bs) KMemValue memv) (at level 10, memv at next level) : exp_scope.
Notation "'MemException' bs meme" := (exp_union (memory_op_result bs) KMemException meme) (at level 10, meme at next level) : exp_scope.
Notation "'F_Base' memv" := (exp_union fetch_result KF_Base memv) (at level 10, memv at next level) : exp_scope.
Notation "'F_Error' meme memv" := (exp_union fetch_result KF_Error (exp_binop bop.pair meme memv)) (at level 10, meme at next level, memv at next level) : exp_scope.
Notation "'CTL_TRAP' exc" := (exp_union ctl_result KCTL_TRAP exc) (at level 10, exc at next level) : exp_scope.
Notation "'CTL_MRET'" := (exp_union ctl_result KCTL_MRET (exp_val ty.unit tt)) : exp_scope.
stm_exp (exp_union Uinstruction Kpop (exp_tuple [(exp_int 2%Z); (exp_int 4%Z); (exp_int 8%Z)])).
Notation "e .[?? x ]" := (@lookup _ _ _ e (x∷_) _)
(at level 2, x at level 200, only parsing).enum Permission = O | R | RW | E
struct Capability = {
cap_permission: Permission,
cap_begin: address,
cap_end: address,
cap_cursor: address,
}
union word = {
Cap : Capability,
Num : integer
}
+ From Coq Require Import
+ Classes.EquivDec
+ Strings.String.
+ From stdpp Require
+ finite.
+ From Equations Require Import
+ Equations.
+ Require Import Katamaran.Base.
+
+ (*** TYPES ***)
+
+ Inductive RegName : Set :=
+ R0 | R1 | R2 | R3.
+
+ Definition Dst : Set := RegName.
+ Definition Src : Set := RegName.
+ Definition Imm : Set := Z.
+
+ Inductive Instruction : Set :=
+ | jalr_cap (cd : Dst) (cs : Src)
+ | cjalr (cd : Dst) (cs : Src) (imm : Imm)
+ | cjal (cd : Dst) (imm : Imm)
+ | bne (rs1 : Src) (rs2 : Src) (imm : Imm)
+ | ld (cd : Dst) (cs : Src) (imm : Imm)
+ | sd (rs1 : Src) (rs2 : Src) (imm : Imm)
+ | addi (rd : Dst) (rs : Src) (imm : Imm)
+ | add (rd : Dst) (rs1 : Src) (rs2 : Src)
+ | sub (rd : Dst) (rs1 : Src) (rs2 : Src)
+ | slt (rd : Dst) (rs1 : Src) (rs2 : Src)
+ | slti (rd : Dst) (rs : Src) (imm : Imm)
+ | sltu (rd : Dst) (rs1 : Src) (rs2 : Src)
+ | sltiu (rd : Dst) (rs : Src) (imm : Imm)
+ | cmove (cd : Dst) (cs : Src)
+ | cincoffset (cd : Dst) (cs : Src) (rs : Src)
+ | candperm (cd : Dst) (cs : Src) (rs : Src)
+ | csetbounds (cd : Dst) (cs : Src) (rs : Src)
+ | csetboundsimm (cd : Dst) (cs : Src) (imm : Imm)
+ | cgettag (rd : Dst) (cd : Src)
+ | cgetperm (rd : Dst) (cs : Src)
+ | cgetbase (rd : Dst) (cs : Src)
+ | cgetlen (rd : Dst) (cs : Src)
+ | cgetaddr (rd : Dst) (cs : Src)
+ | fail
+ | ret.
+
+ Inductive InstructionConstructor : Set :=
+ | kjalr_cap
+ | kcjalr
+ | kcjal
+ | kbne
+ | kcmove
+ | kld
+ | ksd
+ | kaddi
+ | kadd
+ | ksub
+ | kslt
+ | kslti
+ | ksltu
+ | ksltiu
+ | kcincoffset
+ | kcandperm
+ | kcsetbounds
+ | kcsetboundsimm
+ | kcgettag
+ | kcgetperm
+ | kcgetbase
+ | kcgetlen
+ | kcgetaddr
+ | kfail
+ | kret.
+
+ Inductive Permission : Set :=
+ O | R | RW | E.
+
+ Definition Addr : Set := Z.
+
+ Record Capability : Set :=
+ MkCap
+ { cap_permission : Permission;
+ cap_begin : Addr;
+ cap_end : Addr;
+ cap_cursor : Addr;
+ }.
+
+ (** Enums **)
+ Inductive Enums : Set :=
+ | permission
+ | regname.
+
+ (** Unions **)
+ Inductive Unions : Set :=
+ | instruction.
+
+ (** Records **)
+ Inductive Records : Set :=
+ | capability.
+
+ Section TransparentObligations.
+ Local Set Transparent Obligations.
+
+ Derive NoConfusion for Capability.
+ Derive NoConfusion for Permission.
+ Derive NoConfusion for RegName.
+ Derive NoConfusion for Enums.
- Derive NoConfusion for Unions.
- Derive NoConfusion for Records.
- Derive NoConfusion for Instruction.
- Derive NoConfusion for InstructionConstructor.
+
+ End TransparentObligations.
+ Derive EqDec for Permission.
- Definition is_perm := @equiv_decb _ _ _ Permission_eqdec.
- Lemma is_perm_iff : forall p p',
- is_perm p p' = true <-> p = p'.
- Proof.
- unfold is_perm.
- intros; split.
- - destruct p, p'; cbn; intros ?; auto; try discriminate.
- - intros; subst; destruct p'; auto.
- Qed.
-
+ Derive EqDec for Capability.
+ Derive EqDec for RegName.
+
+ Derive EqDec for Enums.
+ Derive EqDec for Unions.
+ Derive EqDec for Records.
+ Derive EqDec for Instruction.
+ Derive EqDec for InstructionConstructor.
+
+ Section Finite.
+
+ Import stdpp.finite.
+
+ Local Obligation Tactic :=
+ finite_from_eqdec.
+
+ #[export,program] Instance Permission_finite : Finite Permission :=
+ {| enum := [O;R;RW;E] |}.
+
+ #[export,program] Instance RegName_finite : Finite RegName :=
+ {| enum := [R0;R1;R2;R3] |}.
+
+ #[export,program] Instance InstructionConstructor_finite :
+ Finite InstructionConstructor :=
+ {| enum := [kjalr_cap;kcjalr;kcjal;kbne;kcmove;kld;ksd;kcincoffset;kcandperm;kcsetbounds;kcsetboundsimm;kcgettag;kaddi;kadd;ksub;kslt;kslti;ksltu;ksltiu;kcgetperm;kcgetbase;kcgetlen;kcgetaddr;kfail;kret] |}.
+
+ End Finite.
+
+ Module Export MinCapsBase <: Base.
+ Import ctx.notations.
+ Import ctx.resolution.
+ Import env.notations.
+ Import stdpp.finite.
+
+ Local Open Scope string_scope.
+
+ #[export] Instance typedeclkit : TypeDeclKit :=
+ {| enumi := Enums;
+ unioni := Unions;
+ recordi := Records;
+ |}.
+
- Notation "ty.dst" := (ty.enum regname).
- Notation "ty.src" := (ty.enum regname).
- Notation "ty.cap" := (ty.record capability).
- Notation "ty.word" := (ty.sum ty.int ty.cap).
- Notation "ty.memval" := (ty.word).
- Notation "ty.addr" := (ty.int).
- Notation "ty.perm" := (ty.enum permission).
- Notation "ty.instr" := (ty.union instruction).
-
+ Definition enum_denote (e : Enums) : Set :=
+ match e with
+ | permission => Permission
+ | regname => RegName
+ end.
+
+ Definition union_denote (U : Unions) : Set :=
+ match U with
+ | instruction => Instruction
+ end.
+
+ Definition record_denote (R : Records) : Set :=
+ match R with
+ | capability => Capability
+ end.
+
+ #[export] Instance typedenotekit : TypeDenoteKit typedeclkit :=
+ {| enumt := enum_denote;
+ uniont := union_denote;
+ recordt := record_denote;
+ |}.
+
+ Definition union_constructor (U : Unions) : Set :=
+ match U with
+ | instruction => InstructionConstructor
+ end.
+
+ Definition union_constructor_type (U : Unions) : union_constructor U -> Ty :=
+ match U with
+ | instruction => fun K =>
+ match K with
+ | kjalr_cap => ty.prod ty.dst ty.src
+ | kcjalr => ty.tuple [ty.dst; ty.src; ty.int]
+ | kcjal => ty.prod ty.dst ty.int
+ | kbne => ty.tuple [ty.src; ty.src; ty.int]
+ | kld => ty.tuple [ty.dst; ty.src; ty.int]
+ | ksd => ty.tuple [ty.src; ty.src; ty.int]
+ | kaddi => ty.tuple [ty.dst; ty.src; ty.int]
+ | kadd => ty.tuple [ty.dst; ty.src; ty.src]
+ | ksub => ty.tuple [ty.dst; ty.src; ty.src]
+ | kslt => ty.tuple [ty.dst; ty.src; ty.src]
+ | kslti => ty.tuple [ty.dst; ty.src; ty.int]
+ | ksltu => ty.tuple [ty.dst; ty.src; ty.src]
+ | ksltiu => ty.tuple [ty.dst; ty.src; ty.int]
+ | kcmove => ty.prod ty.dst ty.src
+ | kcincoffset => ty.tuple [ty.dst; ty.src; ty.src]
+ | kcandperm => ty.tuple [ty.dst; ty.src; ty.src]
+ | kcsetbounds => ty.tuple [ty.dst; ty.src; ty.src]
+ | kcsetboundsimm => ty.tuple [ty.dst; ty.src; ty.int]
+ | kcgetperm => ty.prod ty.dst ty.src
+ | kcgetbase => ty.prod ty.dst ty.src
+ | kcgetlen => ty.prod ty.dst ty.src
+ | kcgetaddr => ty.prod ty.dst ty.src
+ | kfail => ty.unit
+ | kret => ty.unit
+ | kcgettag => ty.prod ty.dst ty.src
+ end
+ end.
-
- #[export] Instance eqdec_enum_denote E : EqDec (enum_denote E) :=
- ltac:(destruct E; auto with typeclass_instances).
- #[export] Instance finite_enum_denote E : finite.Finite (enum_denote E) :=
- ltac:(destruct E; auto with typeclass_instances).
- #[export] Instance eqdec_union_denote U : EqDec (union_denote U) :=
- ltac:(destruct U; cbn; auto with typeclass_instances).
- #[export] Instance eqdec_union_constructor U : EqDec (union_constructor U) :=
- ltac:(destruct U; cbn; auto with typeclass_instances).
- #[export] Instance finite_union_constructor U : finite.Finite (union_constructor U) :=
- ltac:(destruct U; cbn; auto with typeclass_instances).
- #[export] Instance eqdec_record_denote R : EqDec (record_denote R) :=
- ltac:(destruct R; auto with typeclass_instances).
-
- Definition union_fold (U : unioni) : { K & Val (union_constructor_type U K) } -> uniont U :=
- match U with
- | instruction => fun Kv =>
- match Kv with
- | existT kjalr_cap (cd , cs) => jalr_cap cd cs
- | existT kcjalr (tt , cd , cs , imm) => cjalr cd cs imm
- | existT kcjal (cd , imm) => cjal cd imm
- | existT kbne (tt , rs1 , rs2 , imm) => bne rs1 rs2 imm
- | existT kld (tt , cd , cs , imm) => ld cd cs imm
- | existT ksd (tt , rs1 , rs2, imm) => sd rs1 rs2 imm
- | existT kaddi (tt , rd , rs , imm) => addi rd rs imm
- | existT kadd (tt , rd , rs1 , rs2) => add rd rs1 rs2
- | existT ksub (tt , rd , rs1 , rs2) => sub rd rs1 rs2
- | existT kslt (tt , rd , rs1 , rs2) => slt rd rs1 rs2
- | existT kslti (tt , rd , rs , imm) => slti rd rs imm
- | existT ksltu (tt , rd , rs1 , rs2) => sltu rd rs1 rs2
- | existT ksltiu (tt , rd , rs , imm) => sltiu rd rs imm
- | existT kcmove (cd , cs) => cmove cd cs
- | existT kcincoffset (tt , cd , cs , rs) => cincoffset cd cs rs
- | existT kcandperm (tt , cd , cs , rs) => candperm cd cs rs
- | existT kcsetbounds (tt , cd , cs , rs) => csetbounds cd cs rs
- | existT kcsetboundsimm (tt , cd , cs , imm) => csetboundsimm cd cs imm
- | existT kcgettag (rd , cs) => cgettag rd cs
- | existT kcgetperm (rd , cs) => cgetperm rd cs
- | existT kcgetbase (rd , cs) => cgetbase rd cs
- | existT kcgetlen (rd , cs) => cgetlen rd cs
- | existT kcgetaddr (rd , cs) => cgetaddr rd cs
- | existT kfail tt => fail
- | existT kret tt => ret
- end
- end.
-
- Definition union_unfold (U : unioni) : uniont U -> { K & Val (union_constructor_type U K) } :=
- match U with
- | instruction => fun Kv =>
- match Kv with
- | jalr_cap cd cs => existT kjalr_cap (cd , cs)
- | cjalr cd cs imm => existT kcjalr (tt , cd , cs , imm)
- | cjal cd imm => existT kcjal (cd , imm)
- | bne rs1 rs2 imm => existT kbne (tt , rs1 , rs2 , imm)
- | ld cd cs imm => existT kld (tt , cd , cs , imm)
- | sd rs1 rs2 imm => existT ksd (tt , rs1 , rs2 , imm)
- | addi rd rs imm => existT kaddi (tt , rd , rs , imm)
- | add rd rs1 rs2 => existT kadd (tt , rd , rs1 , rs2)
- | sub rd rs1 rs2 => existT ksub (tt , rd , rs1 , rs2)
- | slt rd rs1 rs2 => existT kslt (tt , rd , rs1 , rs2)
- | slti rd rs imm => existT kslti (tt , rd , rs , imm)
- | sltu rd rs1 rs2 => existT ksltu (tt , rd , rs1 , rs2)
- | sltiu rd rs imm => existT ksltiu (tt , rd , rs , imm)
- | cmove cd cs => existT kcmove (cd , cs)
- | cincoffset cd cs rs => existT kcincoffset (tt , cd , cs , rs)
- | candperm cd cs rs => existT kcandperm (tt , cd , cs , rs)
- | csetbounds cd cs rs => existT kcsetbounds (tt, cd , cs , rs)
- | csetboundsimm cd cs imm => existT kcsetboundsimm (tt, cd , cs , imm)
- | cgettag rd cs => existT kcgettag (rd , cs)
- | cgetperm rd cs => existT kcgetperm (rd , cs)
- | cgetbase rd cs => existT kcgetbase (rd , cs)
- | cgetlen rd cs => existT kcgetlen (rd , cs)
- | cgetaddr rd cs => existT kcgetaddr (rd , cs)
- | fail => existT kfail tt
- | ret => existT kret tt
- end
- end.
-
- Definition record_field_type (R : recordi) : NCtx string Ty :=
- match R with
- | capability => [ "cap_permission" ∷ ty.perm;
- "cap_begin" ∷ ty.addr;
- "cap_end" ∷ ty.addr;
- "cap_cursor" ∷ ty.addr
- ]
- end.
-
- Definition record_fold (R : recordi) : NamedEnv Val (record_field_type R) -> recordt R :=
- match R with
- | capability =>
- fun fields =>
- MkCap
- fields.[??"cap_permission"]
- fields.[??"cap_begin"]
- fields.[??"cap_end"]
- fields.[??"cap_cursor"]
- end%exp.
-
- Definition record_unfold (R : recordi) : recordt R -> NamedEnv Val (record_field_type R) :=
- match R with
- | capability =>
- fun c=>
- env.nil
- ► ("cap_permission" ∷ ty.perm ↦ cap_permission c)
- ► ("cap_begin" ∷ ty.addr ↦ cap_begin c)
- ► ("cap_end" ∷ ty.addr ↦ cap_end c)
- ► ("cap_cursor" ∷ ty.addr ↦ cap_cursor c)
- end%env.
-
- #[export,refine] Instance typedefkit : TypeDefKit typedenotekit :=
- {| unionk := union_constructor;
- unionk_ty := union_constructor_type;
- recordf := string;
- recordf_ty := record_field_type;
- unionv_fold := union_fold;
- unionv_unfold := union_unfold;
- recordv_fold := record_fold;
- recordv_unfold := record_unfold;
- |}.
- Proof.
- - abstract (now intros [] []).
- - abstract (intros [] [[] x]; cbn in x;
- repeat
- match goal with
- | x: unit |- _ => destruct x
- | x: prod _ _ |- _ => destruct x
- end; auto).
- - abstract (now intros [] []).
- - abstract (intros []; now apply env.Forall_forall).
- Defined.
-
- Canonical typedeclkit.
- Canonical typedenotekit.
- Canonical typedefkit.
-
- #[export] Instance varkit : VarKit := DefaultVarKit.
-
+ Section RegDeclKit.
+
+ Inductive Reg : Ty -> Set :=
+ | pc : Reg ty.cap
+ | reg1 : Reg ty.word
+ | reg2 : Reg ty.word
+ | reg3 : Reg ty.word.
+
+ Section TransparentObligations.
+ Local Set Transparent Obligations.
+ Derive Signature NoConfusion NoConfusionHom EqDec for Reg.
+ End TransparentObligations.
+
+ Definition 𝑹𝑬𝑮 : Ty -> Set := Reg.
+ #[export] Instance 𝑹𝑬𝑮_eq_dec : EqDec (sigT Reg) :=
+ sigma_eqdec _ _.
+
+ Local Obligation Tactic :=
+ finite_from_eqdec.
+
+ #[export,program] Instance 𝑹𝑬𝑮_finite : Finite (sigT Reg) :=
+ {| enum := [ existT _ pc; existT _ reg1; existT _ reg2; existT _ reg3 ] |}.
+
+ End RegDeclKit.
-
- Section MemoryModel.
- Definition Memory := Addr -> (Z + Capability).
- End MemoryModel.
-
- Include BaseMixin.
-
- End MinCapsBase.+ From Coq Require Import
+ Strings.String
+ ZArith.ZArith.
+ From Equations Require Import
+ Equations.
+ From Katamaran Require Import
+ Program
+ Semantics.Registers
+ Syntax.BinOps.
+ From Katamaran Require Export
+ MinimalCaps.Base.
+
+ From stdpp Require Import finite decidable.
+
+ Set Implicit Arguments.
+ Import ctx.notations.
+ Import ctx.resolution.
+ Import env.notations.
+ Open Scope string_scope.
+
+ (*** Program ***)
+
+ Import MinCapsBase.
+ Module Export MinCapsProgram <: Program MinCapsBase.
+
+ Section FunDeclKit.
+ Inductive Fun : PCtx -> Ty -> Set :=
+ | read_reg : Fun ["rs" :: ty.enum regname] ty.word
+ | read_reg_cap : Fun ["cs" :: ty.enum regname] ty.cap
+ | read_reg_num : Fun ["rs" :: ty.enum regname] ty.int
+ | write_reg : Fun ["rd" :: ty.enum regname; "w" :: ty.word] ty.unit
+ | next_pc : Fun [] ty.cap
+ | update_pc : Fun [] ty.unit
+ | update_pc_perm : Fun ["c" :: ty.cap] ty.cap
+ | is_correct_pc : Fun ["c" :: ty.cap] ty.bool
+ | is_perm : Fun ["p" :: ty.perm; "p'" :: ty.perm] ty.bool
+ | add_pc : Fun ["offset" :: ty.int] ty.unit
+ | read_mem : Fun ["c" :: ty.cap] ty.memval
+ | write_mem : Fun ["c" :: ty.cap; "v" :: ty.memval] ty.unit
+ | read_allowed : Fun ["p" :: ty.perm] ty.bool
+ | write_allowed : Fun ["p" :: ty.perm] ty.bool
+ | within_bounds : Fun ["c" :: ty.cap] ty.bool
+ | perm_to_bits : Fun ["p" :: ty.perm] ty.int
+ | perm_from_bits : Fun ["i" :: ty.int] ty.perm
+ | and_perm : Fun ["p1" :: ty.perm; "p2" :: ty.perm] ty.perm
+ | is_sub_perm : Fun ["p" :: ty.perm; "p'" :: ty.perm] ty.bool
+ | is_within_range : Fun ["b'" :: ty.addr; "e'" :: ty.addr; "b" :: ty.addr; "e" :: ty.addr] ty.bool
+ | abs : Fun ["i" :: ty.int] ty.int
+ | is_not_zero : Fun ["i" :: ty.int] ty.bool
+ | can_incr_cursor : Fun ["c" :: ty.cap; "imm" :: ty.int] ty.bool
+ | exec_jalr_cap : Fun ["cd" :: ty.dst; "cs" :: ty.src] ty.bool
+ | exec_cjalr : Fun ["cd" :: ty.dst; "cs" :: ty.src; "imm" :: ty.int] ty.bool
+ | exec_cjal : Fun ["cd" :: ty.dst; "imm" :: ty.int] ty.bool
+ | exec_bne : Fun ["rs1" :: ty.src; "rs2" :: ty.src; "imm" :: ty.int] ty.bool
+ | exec_ld : Fun ["cd" :: ty.dst; "cs" :: ty.src; "imm" :: ty.int] ty.bool
+ | exec_sd : Fun ["rs1" :: ty.src; "rs2" :: ty.src; "imm" :: ty.int] ty.bool
+ | exec_addi : Fun ["rd" :: ty.dst; "rs" :: ty.src; "imm" :: ty.int] ty.bool
+ | exec_add : Fun ["rd" :: ty.dst; "rs1" :: ty.src; "rs2" :: ty.src] ty.bool
+ | exec_sub : Fun ["rd" :: ty.dst; "rs1" :: ty.src; "rs2" :: ty.src] ty.bool
+ | exec_slt : Fun ["rd" :: ty.dst; "rs1" :: ty.src; "rs2" :: ty.src] ty.bool
+ | exec_slti : Fun ["rd" :: ty.dst; "rs" :: ty.src; "imm" :: ty.int] ty.bool
+ | exec_sltu : Fun ["rd" :: ty.dst; "rs1" :: ty.src; "rs2" :: ty.src] ty.bool
+ | exec_sltiu : Fun ["rd" :: ty.dst; "rs" :: ty.src; "imm" :: ty.int] ty.bool
+ | exec_cmove : Fun ["cd" :: ty.dst; "cs" :: ty.src ] ty.bool
+ | exec_cincoffset : Fun ["cd" :: ty.dst; "cs" :: ty.src; "rs" :: ty.src] ty.bool
+ | exec_candperm : Fun ["cd" :: ty.dst; "cs" :: ty.src; "rs" :: ty.src] ty.bool
+ | exec_csetbounds : Fun ["cd" :: ty.dst; "cs" :: ty.src; "rs" :: ty.src] ty.bool
+ | exec_csetboundsimm : Fun ["cd" :: ty.dst; "cs" :: ty.src; "imm" :: ty.int] ty.bool
+ | exec_cgettag : Fun ["rd" :: ty.dst; "cs" :: ty.src] ty.bool
+ | exec_cgetperm : Fun ["rd" :: ty.dst; "cs" :: ty.src] ty.bool
+ | exec_cgetbase : Fun ["rd" :: ty.dst; "cs" :: ty.src] ty.bool
+ | exec_cgetlen : Fun ["rd" :: ty.dst; "cs" :: ty.src] ty.bool
+ | exec_cgetaddr : Fun ["rd" :: ty.dst; "cs" :: ty.src] ty.bool
+ | exec_fail : Fun [] ty.bool
+ | exec_ret : Fun [] ty.bool
+ | exec_instr : Fun ["i" :: ty.instr] ty.bool
+ | exec : Fun [] ty.bool
+ | step : Fun [] ty.unit
+ | loop : Fun [] ty.unit
+ .
+
- Inductive FunX : PCtx -> Ty -> Set :=
- (* read memory *)
- | rM : FunX ["address" :: ty.int] ty.memval
- (* write memory *)
- | wM : FunX ["address" :: ty.int; "new_value" :: ty.memval] ty.unit
- | dI : FunX ["code" :: ty.int] ty.instr
- .
-
- Inductive Lem : PCtx -> Set :=
- | open_gprs : Lem []
- | close_gprs : Lem []
- | safe_move_cursor : Lem ["c'" :: ty.cap; "c" :: ty.cap]
- | safe_sub_perm : Lem ["c'" :: ty.cap; "c" :: ty.cap]
- | safe_within_range : Lem ["c'" :: ty.cap; "c" :: ty.cap]
- | int_safe : Lem ["i" :: ty.int]
- | correctPC_subperm_R : Lem ["c" :: ty.cap]
- | subperm_not_E : Lem ["p" :: ty.perm; "p'" :: ty.perm]
- | safe_to_execute : Lem ["c" :: ty.cap]
- .
-
- Definition 𝑭 : PCtx -> Ty -> Set := Fun.
- Definition 𝑭𝑿 : PCtx -> Ty -> Set := FunX.
- Definition 𝑳 : PCtx -> Set := Lem.
-
+ End FunDeclKit.
-
- Include FunDeclMixin MinCapsBase.
-
+ Section FunDefKit.
+
+ Local Coercion stm_exp : Exp >-> Stm.
+
- Local Notation "'a'" := (@exp_var _ "a" _ _) : exp_scope.
- Local Notation "'c'" := (@exp_var _ "c" _ _) : exp_scope.
- Local Notation "'e'" := (@exp_var _ "e" _ _) : exp_scope.
- Local Notation "'i'" := (@exp_var _ "i" _ _) : exp_scope.
- Local Notation "'n'" := (@exp_var _ "n" _ _) : exp_scope.
- Local Notation "'p'" := (@exp_var _ "p" _ _) : exp_scope.
- Local Notation "'p1'" := (@exp_var _ "p1" _ _) : exp_scope.
- Local Notation "'p2'" := (@exp_var _ "p2" _ _) : exp_scope.
- Local Notation "'q'" := (@exp_var _ "q" _ _) : exp_scope.
- Local Notation "'r'" := (@exp_var _ "r" _ _) : exp_scope.
- Local Notation "'w'" := (@exp_var _ "w" _ _) : exp_scope.
- Local Notation "'x'" := (@exp_var _ "x" _ _) : exp_scope.
- Local Notation "'immediate'" := (@exp_var _ "immediate" _ _) : exp_scope.
- Local Notation "'offset'" := (@exp_var _ "offset" _ _) : exp_scope.
-
- Local Notation "'c'" := "c" : string_scope.
- Local Notation "'e'" := "e" : string_scope.
- Local Notation "'hv'" := "hv" : string_scope.
- Local Notation "'rv'" := "rv" : string_scope.
- Local Notation "'i'" := "i" : string_scope.
- Local Notation "'n'" := "n" : string_scope.
- Local Notation "'p'" := "p" : string_scope.
- Local Notation "'q'" := "q" : string_scope.
- Local Notation "'r'" := "r" : string_scope.
- Local Notation "'w'" := "w" : string_scope.
- Local Notation "'immediate'" := "immediate" : string_scope.
- Local Notation "'offset'" := "offset" : string_scope.
-
- Notation "'use' 'lemma' f args" := (stm_lemma f args%env) (at level 10, f at next level) : exp_scope.
- Notation "'use' 'lemma' f" := (stm_lemma f env.nil) (at level 10, f at next level) : exp_scope.
-
- (* NOTE: need to wrap s around parentheses when using this notation (not a real let binding!) *)
- Notation "'let*:' '[' perm ',' beg ',' en ',' cur ']' ':=' cap 'in' s" :=
- (stm_match_record capability cap
- (recordpat_snoc (recordpat_snoc (recordpat_snoc (recordpat_snoc recordpat_nil
- "cap_permission" perm)
- "cap_begin" beg)
- "cap_end" en)
- "cap_cursor" cur)
- s) (at level 10) : exp_scope.
-
- Definition lemma_correctPC_not_E {Γ} (cap : Stm Γ ty.cap) : Stm Γ ty.unit :=
- let: "c" := cap in
- use lemma correctPC_subperm_R [exp_var "c"] ;;
- let*: ["perm" , "beg" , "end" , "cur"] := (exp_var "c") in
- (let: "tmp" := exp_val ty.perm R in
- use lemma subperm_not_E [exp_var "tmp"; exp_var "perm"]).
-
+ Definition fun_read_reg : Stm ["rs" :: ty.enum regname] ty.word :=
- use lemma open_gprs ;;
+ let: "x" := match: exp_var "rs" in regname with
+ | R0 =>
+ use lemma int_safe [exp_val ty.int 0%Z] ;;
+ exp_inl (exp_val ty.int 0%Z)
+ | R1 => stm_read_register reg1
+ | R2 => stm_read_register reg2
+ | R3 => stm_read_register reg3
+ end in
- use lemma close_gprs ;;
+ stm_exp x.
-
- Definition fun_read_reg_cap : Stm ["cs" :: ty.enum regname] ty.cap :=
+ let: w := call read_reg (exp_var "cs") in
+ match: w with
+ | inl i => fail "Err [read_reg_cap]: expect register to hold a capability"
+ | inr c =>
- let*: ["p", "b", "e", "a"] := exp_var "c" in (* force record *)
+ (exp_var "c")
+ end.
-
- Definition fun_read_reg_num : Stm ["rs" :: ty.enum regname ] ty.int :=
+ let: w := call read_reg (exp_var "rs") in
+ match: w with
+ | inl i => stm_exp i
+ | inr c => fail "Err [read_reg_num]: expect register to hold a number"
+ end.
-
- Definition fun_write_reg : Stm ["rd" :: ty.enum regname; "w" :: ty.word] ty.unit :=
- use lemma open_gprs ;;
+ match: exp_var "rd" in regname with
+ | R0 => stm_val ty.unit tt
+ | R1 => stm_write_register reg1 (exp_var "w") ;; stm_val ty.unit tt
+ | R2 => stm_write_register reg2 (exp_var "w") ;; stm_val ty.unit tt
+ | R3 => stm_write_register reg3 (exp_var "w") ;; stm_val ty.unit tt
+ end ;;
- use lemma close_gprs.
-
+ Definition fun_next_pc : Stm [] ty.cap :=
+ let: "c" := stm_read_register pc in
+ let*: ["perm" , "beg" , "end" , "cur"] := (exp_var "c") in
+ (exp_record capability
+ [ exp_var "perm";
+ exp_var "beg";
+ exp_var "end";
+ exp_var "cur" + exp_int 1 ]).
-
+ Definition fun_update_pc : Stm [] ty.unit :=
+ let: "opc" := stm_read_register pc in
+ let: "npc" := call next_pc in
- lemma_correctPC_not_E (exp_var "opc") ;;
- use lemma safe_move_cursor [exp_var "npc"; exp_var "opc"] ;;
+ stm_write_register pc (exp_var "npc") ;;
+ stm_val ty.unit tt.
-
+ Definition fun_update_pc_perm : Stm ["c" :: ty.cap] ty.cap :=
- let*: ["p" , "b" , "e" , "a"] := (exp_var "c") in
+ (match: exp_var "p" in permission with
+ | E => let: "p" := exp_val ty.perm R in
- use lemma safe_to_execute [exp_var "c"] ;;
+ exp_record capability
+ [ exp_var "p" ;
+ exp_var "b" ;
+ exp_var "e" ;
+ exp_var "a" ]
+ | _ => exp_var "c"
+ end).
-
+ Definition fun_is_correct_pc : Stm ["c" :: ty.cap] ty.bool :=
- let*: ["perm" , "beg" , "end" , "cur"] := (exp_var "c") in
+ (let: "tmp1" := call is_perm (exp_var "perm") (exp_val ty.perm R) in
+ let: "tmp2" := call is_perm (exp_var "perm") (exp_val ty.perm RW) in
+ if: (exp_var "beg" <= exp_var "cur") && (exp_var "cur" < exp_var "end")
+ && (exp_var "tmp1" || exp_var "tmp2")
+ then stm_val ty.bool true
+ else stm_val ty.bool false).
+
+ Definition fun_is_perm : Stm ["p" :: ty.perm; "p'" :: ty.perm] ty.bool :=
- stm_match_enum permission (exp_var "p") (fun _ => stm_val ty.unit tt) ;;
- stm_match_enum permission (exp_var "p'") (fun _ => stm_val ty.unit tt) ;;
+ exp_var "p" = exp_var "p'".
-
+ Definition fun_add_pc : Stm ["offset" :: ty.int] ty.unit :=
+ let: "opc" := stm_read_register pc in
+ let*: ["perm", "beg", "end", "cur"] := (exp_var "opc") in
+ (let: "npc" := (exp_record capability
+ [ exp_var "perm";
+ exp_var "beg";
+ exp_var "end";
+ exp_var "cur" + exp_var "offset" ]) in
- lemma_correctPC_not_E (exp_var "opc") ;;
- use lemma safe_move_cursor [exp_var "npc"; exp_var "opc"] ;;
+ stm_write_register pc (exp_var "npc") ;;
+ stm_val ty.unit tt).
-
+ Definition fun_read_allowed : Stm ["p" :: ty.perm] ty.bool :=
+ call is_sub_perm (exp_val (ty.enum permission) R) (exp_var "p").
+
+ Definition fun_write_allowed : Stm ["p" :: ty.perm] ty.bool :=
+ call is_sub_perm (exp_val (ty.enum permission) RW) (exp_var "p").
+
+ Definition fun_within_bounds : Stm ["c" :: ty.cap] ty.bool :=
- let*: ["p", "b", "e", "a"] := (exp_var "c") in
+ ((exp_var "b" <= exp_var "a") && (exp_var "a" <= exp_var "e")).
-
- Section ExecStore.
-
- Local Notation "'perm'" := "cap_permission" : string_scope.
- Local Notation "'cursor'" := "cap_cursor" : string_scope.
-
- Let cap : Ty := ty.cap.
- Let bool : Ty := ty.bool.
- Let int : Ty := ty.int.
- Let word : Ty := ty.word.
-
- Definition fun_exec_sd : Stm ["rs1" :: ty.src; "rs2" :: ty.src; "imm" :: ty.int] ty.bool :=
+ let: "base_cap" :: cap := call read_reg_cap (exp_var "rs1") in
- let*: ["perm", "beg", "end", "cursor"] := (exp_var "base_cap") in
+ (let: "c" :: cap := exp_record capability
+ [ exp_var "perm";
+ exp_var "beg";
+ exp_var "end";
+ exp_var "cursor" + exp_var "imm"
+ ] in
+ let: p :: bool := call write_allowed (exp_var "perm") in
- stm_assert p (exp_string "Err: [store] no write permission") ;;
+ let: w :: ty.word := call read_reg (exp_var "rs2") in
+ let: "tmp" := exp_val ty.perm RW in
- use lemma subperm_not_E [exp_var "tmp"; exp_var "perm"] ;;
- use lemma safe_move_cursor [exp_var "c"; exp_var "base_cap"] ;;
+ call write_mem c w ;;
+ call update_pc ;;
+ stm_val ty.bool true).
-
- Definition fun_exec_ld : Stm ["cd" :: ty.dst; "cs" :: ty.src; "imm" :: ty.int] ty.bool :=
+ let: "base_cap" :: cap := call read_reg_cap (exp_var "cs") in
- let*: ["perm", "beg", "end", "cursor"] := (exp_var "base_cap") in
+ (let: "c" :: cap := exp_record capability
+ [ exp_var "perm";
+ exp_var "beg";
+ exp_var "end";
+ exp_var "cursor" + exp_var "imm"
+ ] in
+ let: p :: bool := call read_allowed (exp_var "perm") in
- stm_assert p (exp_string "Err: [load] no read permission") ;;
+ let: "tmp" := exp_val ty.perm R in
- use lemma subperm_not_E [exp_var "tmp"; exp_var "perm"] ;;
- use lemma safe_move_cursor [exp_var "c"; exp_var "base_cap"] ;;
- let: n :: ty.memval := call read_mem c in
+ call write_reg (exp_var "cd") n ;;
+ call update_pc ;;
+ stm_val ty.bool true).
-
- Definition fun_exec_cincoffset : Stm ["cd" :: ty.dst; "cs" :: ty.src; "rs" :: ty.src] ty.bool :=
+ let: "base_cap" :: cap := call read_reg_cap (exp_var "cs") in
+ let: "offset" :: ty.int := call read_reg_num (exp_var "rs") in
- let*: ["perm", "beg", "end", "cursor"] := (exp_var "base_cap") in
+ (match: exp_var "perm" in permission with
+ | E => fail "Err: [cincoffset] not permitted on enter capability"
+ | _ =>
+ let: "c" :: cap := exp_record capability
+ [ exp_var "perm";
+ exp_var "beg";
+ exp_var "end";
+ exp_var "cursor" + exp_var "offset"
+ ] in
- use lemma safe_move_cursor [exp_var "c"; exp_var "base_cap"] ;;
+ call write_reg (exp_var "cd") (exp_inr (exp_var "c")) ;;
+ call update_pc ;;
+ stm_val ty.bool true
+ end).
-
- Definition fun_exec_candperm : Stm ["cd" :: ty.dst; "cs" :: ty.src; "rs" :: ty.src] ty.bool :=
+ let: "cs_val" := call read_reg_cap (exp_var "cs") in
+ let: "rs_val" := call read_reg_num (exp_var "rs") in
- let*: ["p", "b", "e", "a"] := exp_var "cs_val" in
+ let: "p'" := call perm_from_bits (exp_var "rs_val") in
+ let: "new_p" := call and_perm (exp_var "p") (exp_var "p'") in
- let: "new_cap" :: cap := exp_record capability
+ [ exp_var "new_p";
+ exp_var "b";
+ exp_var "e";
+ exp_var "a"
+ ] in
- use lemma safe_sub_perm [exp_var "new_cap"; exp_var "cs_val"] ;;
+ call write_reg (exp_var "cd") (exp_inr (exp_var "new_cap")) ;;
+ stm_val ty.bool true.
-
- Definition fun_exec_addi : Stm ["rd" :: ty.dst; "rs" :: ty.src; "imm" :: ty.int] ty.bool :=
- let: "v" :: ty.int := call read_reg_num (exp_var "rs") in
- let: "res" :: ty.int := stm_exp (exp_var "v" + exp_var "imm") in
- use lemma int_safe [exp_var "res"] ;;
- call write_reg (exp_var "rd") (exp_inl (exp_var "res")) ;;
- call update_pc ;;
- stm_val ty.bool true.
-
- Definition fun_exec_add : Stm ["rd" :: ty.dst; "rs1" :: ty.src; "rs2" :: ty.src] ty.bool :=
- let: "v1" :: int := call read_reg_num (exp_var "rs1") in
- let: "v2" :: int := call read_reg_num (exp_var "rs2") in
- let: "res" :: int := stm_exp (exp_var "v1" + exp_var "v2") in
- use lemma int_safe [exp_var "res"] ;;
- call write_reg (exp_var "rd") (exp_inl (exp_var "res")) ;;
- call update_pc ;;
- stm_val ty.bool true.
-
- Definition fun_exec_sub : Stm ["rd" :: ty.dst; "rs1" :: ty.src; "rs2" :: ty.src] ty.bool :=
- let: "v1" :: int := call read_reg_num (exp_var "rs1") in
- let: "v2" :: int := call read_reg_num (exp_var "rs2") in
- let: "res" :: int := stm_exp (exp_var "v1" - exp_var "v2") in
- use lemma int_safe [exp_var "res"] ;;
- call write_reg (exp_var "rd") (exp_inl (exp_var "res")) ;;
- call update_pc ;;
- stm_val ty.bool true.
-
- Definition fun_abs : Stm ["i" :: ty.int] ty.int :=
- if: exp_var "i" < (exp_val ty.int 0%Z)
- then exp_var "i" * (exp_val ty.int (-1)%Z)
- else exp_var "i".
-
- Definition fun_is_not_zero : Stm ["i" :: ty.int] ty.bool :=
- if: exp_var "i" = exp_val ty.int 0%Z
- then stm_val ty.bool false
- else stm_val ty.bool true.
-
- Definition fun_can_incr_cursor : Stm ["c" :: ty.cap; "imm" :: ty.int] ty.bool :=
- let*: ["p", "b", "e", "a"] := exp_var "c" in
- let: "tmp1" := call is_perm (exp_var "p") (exp_val ty.perm E) in
- if: exp_var "tmp1"
- then
- let: "tmp2" := call is_not_zero (exp_var "imm") in
- if: exp_var "tmp2"
- then stm_val ty.bool false
- else
- stm_val ty.bool true
- else stm_val ty.bool true.
-
- Definition fun_exec_slt : Stm ["rd" :: ty.dst; "rs1" :: ty.src; "rs2" :: ty.src] ty.bool :=
- let: "v1" :: int := call read_reg_num (exp_var "rs1") in
- let: "v2" :: int := call read_reg_num (exp_var "rs2") in
- (if: exp_var "v1" < exp_var "v2"
- then
- use lemma int_safe [exp_val ty.int 1%Z] ;;
- call write_reg (exp_var "rd") (exp_inl (exp_val ty.int 1%Z))
- else
- use lemma int_safe [exp_val ty.int 0%Z] ;;
- call write_reg (exp_var "rd") (exp_inl (exp_val ty.int 0%Z))) ;;
- call update_pc ;;
- stm_val ty.bool true.
-
- Definition fun_exec_slti : Stm ["rd" :: ty.dst; "rs" :: ty.src; "imm" :: ty.int] ty.bool :=
- let: "v1" :: int := call read_reg_num (exp_var "rs") in
- let: "v2" :: int := exp_var "imm" in
- (if: exp_var "v1" < exp_var "v2"
- then
- use lemma int_safe [exp_val ty.int 1%Z] ;;
- call write_reg (exp_var "rd") (exp_inl (exp_val ty.int 1%Z))
- else
- use lemma int_safe [exp_val ty.int 0%Z] ;;
- call write_reg (exp_var "rd") (exp_inl (exp_val ty.int 0%Z))) ;;
- call update_pc ;;
- stm_val ty.bool true.
-
- Definition fun_exec_sltu : Stm ["rd" :: ty.dst; "rs1" :: ty.src; "rs2" :: ty.src] ty.bool :=
- let: "v1" :: int := call read_reg_num (exp_var "rs1") in
- let: "uv1" :: int := call abs (exp_var "v1") in
- let: "v2" :: int := call read_reg_num (exp_var "rs2") in
- let: "uv2" :: int := call abs (exp_var "v2") in
- (if: exp_var "uv1" < exp_var "uv2"
- then
- use lemma int_safe [exp_val ty.int 1%Z] ;;
- call write_reg (exp_var "rd") (exp_inl (exp_val ty.int 1%Z))
- else
- use lemma int_safe [exp_val ty.int 0%Z] ;;
- call write_reg (exp_var "rd") (exp_inl (exp_val ty.int 0%Z))) ;;
- call update_pc ;;
- stm_val ty.bool true.
-
- Definition fun_exec_sltiu : Stm ["rd" :: ty.dst; "rs" :: ty.src; "imm" :: ty.int] ty.bool :=
- let: "v1" :: int := call read_reg_num (exp_var "rs") in
- let: "uv1" :: int := call abs (exp_var "v1") in
- let: "v2" :: int := exp_var "imm" in
- let: "uv2" :: int := call abs (exp_var "v2") in
- (if: exp_var "uv1" < exp_var "uv2"
- then
- use lemma int_safe [exp_val ty.int 1%Z] ;;
- call write_reg (exp_var "rd") (exp_inl (exp_val ty.int 1%Z))
- else
- use lemma int_safe [exp_val ty.int 0%Z] ;;
- call write_reg (exp_var "rd") (exp_inl (exp_val ty.int 0%Z))) ;;
- call update_pc ;;
- stm_val ty.bool true.
-
- Definition fun_perm_to_bits : Stm ["p" :: ty.perm] ty.int :=
- match: exp_var "p" in permission with
- | O => stm_val ty.int 0%Z
- | R => stm_val ty.int 1%Z
- | RW => stm_val ty.int 2%Z
- | E => stm_val ty.int 3%Z
- end.
-
- Definition fun_perm_from_bits : Stm ["i" :: ty.int] ty.perm :=
- if: exp_var "i" = exp_val ty.int 1%Z
- then exp_val ty.perm R
- else if: exp_var "i" = exp_val ty.int 2%Z
- then exp_val ty.perm RW
- else if: exp_var "i" = exp_val ty.int 3%Z
- then exp_val ty.perm E
- else exp_val ty.perm O.
-
- Definition fun_and_perm : Stm ["p1" :: ty.perm; "p2" :: ty.perm] ty.perm :=
- match: exp_var "p1" in permission with
- | O => exp_val ty.perm O
- | R => match: exp_var "p2" in permission with
- | R => exp_val ty.perm R
- | RW => exp_val ty.perm R
- | _ => exp_val ty.perm O
- end
- | RW => match: exp_var "p2" in permission with
- | R => exp_val ty.perm R
- | RW => exp_val ty.perm RW
- | _ => exp_val ty.perm O
- end
- | E => match: exp_var "p2" in permission with
- | E => exp_val ty.perm E
- | _ => exp_val ty.perm O
- end
- end.
-
- Definition fun_is_sub_perm : Stm ["p" :: ty.perm; "p'" :: ty.perm] ty.bool :=
- match: exp_var "p" in permission with
- | O =>
- stm_val ty.bool true
- | E => match: exp_var "p'" in permission with
- | O => stm_val ty.bool false
- | _ => stm_val ty.bool true
- end
- | R => match: exp_var "p'" in permission with
- | O => stm_val ty.bool false
- | E => stm_val ty.bool false
- | _ =>
- stm_val ty.bool true
- end
- | RW => match: exp_var "p'" in permission with
- | RW =>
- stm_val ty.bool true
- | _ => stm_val ty.bool false
- end
- end.
-
- Definition fun_is_within_range : Stm ["b'" :: ty.addr; "e'" :: ty.addr;
- "b" :: ty.addr; "e" :: ty.addr] ty.bool :=
- (exp_var "b" <= exp_var "b'") && (exp_var "e'" <= exp_var "e").
-
- Definition fun_exec_csetbounds : Stm ["cd" :: ty.dst; "cs" :: ty.src; "rs" :: ty.src] ty.bool :=
- let: c :: cap := call read_reg_cap (exp_var "cs") in
- let*: ["p", "b", "e", "a"] := exp_var "c" in
- let: "new_begin" :: ty.int := exp_var "a" in
- let: "rs_val" :: ty.int := call read_reg_num (exp_var "rs") in
- let: "new_end" :: ty.int := (exp_var "new_begin") + (exp_var "rs_val") in
- match: exp_var "p" in permission with
- | E => fail "Err: [csetbounds] not permitted on enter capability"
- | _ =>
- let: "b" :: ty.bool :=
- call is_within_range (exp_var "new_begin") (exp_var "new_end")
- (exp_var "b") (exp_var "e") in
- stm_assert (exp_var "b") (exp_string "Err: [csetbounds] tried to increase range of authority") ;;
- let: "c'" :: cap := exp_record capability
- [ exp_var "p";
- exp_var "new_begin";
- exp_var "new_end";
- exp_var "a"
- ] in
- use lemma safe_within_range [exp_var "c'"; exp_var "c"] ;;
- call write_reg (exp_var "cd") (exp_inr (exp_var "c'")) ;;
- call update_pc ;;
- stm_val ty.bool true
- end.
-
- Definition fun_exec_csetboundsimm : Stm ["cd" :: ty.dst; "cs" :: ty.src; "imm" :: ty.int] ty.bool :=
- let: c :: cap := call read_reg_cap (exp_var "cs") in
- let*: ["p", "b", "e", "a"] := exp_var "c" in
- let: "new_begin" :: ty.int := exp_var "a" in
- let: "new_end" :: ty.int := (exp_var "new_begin") + (exp_var "imm") in
- match: exp_var "p" in permission with
- | E => fail "Err: [csetboundsimm] not permitted on enter capability"
- | _ =>
- let: "b" :: ty.bool :=
- call is_within_range (exp_var "new_begin") (exp_var "new_end")
- (exp_var "b") (exp_var "e") in
- stm_assert (exp_var "b") (exp_string "Err: [csetboundsimm] tried to increase range of authority") ;;
- let: "c'" :: cap := exp_record capability
- [ exp_var "p";
- exp_var "new_begin";
- exp_var "new_end";
- exp_var "a"
- ] in
- use lemma safe_within_range [exp_var "c'"; exp_var "c"] ;;
- call write_reg (exp_var "cd") (exp_inr (exp_var "c'")) ;;
- call update_pc ;;
- stm_val ty.bool true
- end.
-
- Definition fun_exec_cgettag : Stm ["rd" :: ty.dst; "cs" :: ty.src] ty.bool :=
- let: w :: ty.word := call read_reg (exp_var "cs") in
- match: w with
- | inl i =>
- use lemma int_safe [exp_val ty.int 0%Z] ;;
- call write_reg (exp_var "rd") (exp_inl (exp_val ty.int 0%Z))
- | inr c =>
- use lemma int_safe [exp_val ty.int 1%Z] ;;
- call write_reg (exp_var "rd") (exp_inl (exp_val ty.int 1%Z))
- end ;;
- call update_pc ;;
- stm_val ty.bool true.
-
- Definition fun_exec_cgetperm : Stm ["rd" :: ty.dst; "cs" :: ty.src] ty.bool :=
- let: c :: cap := call read_reg_cap (exp_var "cs") in
- let*: ["perm", "beg", "end", "cursor"] := (exp_var "c") in
- let: "i" :: ty.int := call perm_to_bits (exp_var "perm") in
- use lemma int_safe [exp_var "i"] ;;
- call write_reg (exp_var "rd") (exp_inl (exp_var "i")) ;;
- call update_pc ;;
- stm_val ty.bool true.
-
- Definition fun_exec_cgetbase : Stm ["rd" :: ty.dst; "cs" :: ty.src] ty.bool :=
- let: c :: cap := call read_reg_cap (exp_var "cs") in
- let*: ["perm", "beg", "end", "cursor"] := (exp_var "c") in
- use lemma int_safe [exp_var "beg"] ;;
- call write_reg (exp_var "rd") (exp_inl (exp_var "beg")) ;;
- call update_pc ;;
- stm_val ty.bool true.
-
- Definition fun_exec_cgetlen : Stm ["rd" :: ty.dst; "cs" :: ty.src] ty.bool :=
- let: c :: cap := call read_reg_cap (exp_var "cs") in
- let*: ["perm", "beg", "end", "cursor"] := (exp_var "c") in
- let: "res" := (exp_var "end") - (exp_var "beg") in
- use lemma int_safe [exp_var "res"] ;;
- call write_reg (exp_var "rd") (exp_inl (exp_var "res")) ;;
- call update_pc ;;
- stm_val ty.bool true.
-
- Definition fun_exec_cgetaddr : Stm ["rd" :: ty.dst; "cs" :: ty.src] ty.bool :=
- let: c :: cap := call read_reg_cap (exp_var "cs") in
- let*: ["perm", "beg", "end", "cursor"] := (exp_var "c") in
- use lemma int_safe [exp_var "cursor"] ;;
- call write_reg (exp_var "rd") (exp_inl (exp_var "cursor")) ;;
- call update_pc ;;
- stm_val ty.bool true.
-
- Definition fun_exec_fail : Stm [] ty.bool :=
- fail "machine failed".
-
- Definition fun_exec_ret : Stm [] ty.bool :=
- stm_exp exp_false.
-
- Definition fun_exec_cmove : Stm ["cd" :: ty.dst; "cs" :: ty.src] ty.bool :=
- let: w :: word := call read_reg (exp_var "cs") in
- call write_reg (exp_var "cd") w ;;
- call update_pc ;;
- stm_val ty.bool true.
-
- Definition fun_exec_jalr_cap : Stm ["cd" :: ty.dst; "cs" :: ty.src] ty.bool :=
- call exec_cjalr (exp_var "cd") (exp_var "cs") (exp_val ty.int 0%Z).
-
- Definition fun_exec_cjalr : Stm ["cd" :: ty.dst; "cs" :: ty.src; "imm" :: ty.int] ty.bool :=
- let: "opc" := stm_read_register pc in
- let: "npc" := call next_pc in
- lemma_correctPC_not_E (exp_var "opc") ;;
- use lemma safe_move_cursor [exp_var "npc"; exp_var "opc"] ;;
- call write_reg (exp_var "cd") (exp_inr (exp_var "npc")) ;;
- let: "c" :: ty.cap := call read_reg_cap (exp_var "cs") in
- let*: ["p", "b", "e", "a"] := exp_var "c" in
- let: "tmp" := call can_incr_cursor (exp_var "c") (exp_var "imm") in
- if: exp_not (exp_var "tmp")
- then fail "Err: [cjalr] cannot increment cursor of enter capability"
- else
- let: "c'" := (exp_record capability
- [ exp_var "p";
- exp_var "b";
- exp_var "e";
- exp_var "a" + exp_var "imm"]) in
- use lemma safe_move_cursor [exp_var "c'"; exp_var "c"] ;;
- let: "c'" := call update_pc_perm (exp_var "c'") in
- stm_write_register pc (exp_var "c'") ;;
- stm_val ty.bool true.
-
- Definition fun_exec_cjal : Stm ["cd" :: ty.dst; "imm" :: ty.int] ty.bool :=
- let: "opc" := stm_read_register pc in
- let: "npc" := call next_pc in
- lemma_correctPC_not_E (exp_var "opc") ;;
- use lemma safe_move_cursor [exp_var "npc"; exp_var "opc"] ;;
- call write_reg (exp_var "cd") (exp_inr (exp_var "npc")) ;;
- call add_pc (exp_binop bop.times (exp_var "imm") (exp_int 2)) ;;
- stm_val ty.bool true.
-
- Definition fun_exec_bne : Stm ["rs1" :: ty.src; "rs2" :: ty.src; "imm" :: ty.int] ty.bool :=
- let: "a" :: ty.int := call read_reg_num (exp_var "rs1") in
- let: "b" :: ty.int := call read_reg_num (exp_var "rs2") in
- stm_if (exp_var "a" = exp_var "b")
- (call update_pc ;; stm_val ty.bool true)
- (call add_pc (exp_var "imm") ;; stm_val ty.bool true).
-
- Definition fun_exec_instr : Stm [i :: ty.instr] ty.bool :=
- stm_match_union_alt
- instruction (exp_var i)
- (fun K =>
- match K with
- | kjalr_cap => MkAlt (pat_pair "cd" "cs")
- (call exec_jalr_cap (exp_var "cd") (exp_var "cs"))%exp
- | kcjalr => MkAlt (pat_tuple ("cd" , "cs" , "imm"))
- (call exec_cjalr (exp_var "cd") (exp_var "cs") (exp_var "imm"))%exp
- | kcjal => MkAlt (pat_pair "cd" "imm")
- (call exec_cjal (exp_var "cd") (exp_var "imm"))%exp
- | kbne => MkAlt (pat_tuple ("rs1" , "rs2" , "imm"))
- (call exec_bne (exp_var "rs1") (exp_var "rs2") (exp_var "imm"))%exp
- | kcmove => MkAlt (pat_pair "cd" "cs")
- (call exec_cmove (exp_var "cd") (exp_var "cs"))%exp
- | kld => MkAlt (pat_tuple ("cd" , "cs" , "imm"))
- (call exec_ld (exp_var "cd") (exp_var "cs") (exp_var "imm"))%exp
- | ksd => MkAlt (pat_tuple ("rs1" , "rs2" , "imm"))
- (call exec_sd (exp_var "rs1") (exp_var "rs2") (exp_var "imm"))%exp
- | kcincoffset => MkAlt (pat_tuple ("cd" , "cs" , "rs"))
- (call exec_cincoffset (exp_var "cd") (exp_var "cs") (exp_var "rs"))%exp
- | kcandperm => MkAlt (pat_tuple ("cd" , "cs" , "rs"))
- (call exec_candperm (exp_var "cd") (exp_var "cs") (exp_var "rs"))%exp
- | kcsetbounds => MkAlt (pat_tuple ("cd" , "cs" , "rs"))
- (call exec_csetbounds (exp_var "cd") (exp_var "cs") (exp_var "rs"))%exp
- | kcsetboundsimm => MkAlt (pat_tuple ("cd" , "cs" , "imm"))
- (call exec_csetboundsimm (exp_var "cd") (exp_var "cs") (exp_var "imm"))%exp
- | kaddi => MkAlt (pat_tuple ("rd" , "rs" , "imm"))
- (call exec_addi (exp_var "rd") (exp_var "rs") (exp_var "imm"))%exp
- | kadd => MkAlt (pat_tuple ("rd" , "rs1" , "rs2"))
- (call exec_add (exp_var "rd") (exp_var "rs1") (exp_var "rs2"))%exp
- | ksub => MkAlt (pat_tuple ("rd" , "rs1" , "rs2"))
- (call exec_sub (exp_var "rd") (exp_var "rs1") (exp_var "rs2"))%exp
- | kslt => MkAlt (pat_tuple ("rd" , "rs1" , "rs2"))
- (call exec_slt (exp_var "rd") (exp_var "rs1") (exp_var "rs2"))%exp
- | kslti => MkAlt (pat_tuple ("rd" , "rs" , "imm"))
- (call exec_slti (exp_var "rd") (exp_var "rs") (exp_var "imm"))%exp
- | ksltu => MkAlt (pat_tuple ("rd" , "rs1" , "rs2"))
- (call exec_sltu (exp_var "rd") (exp_var "rs1") (exp_var "rs2"))%exp
- | ksltiu => MkAlt (pat_tuple ("rd" , "rs" , "imm"))
- (call exec_sltiu (exp_var "rd") (exp_var "rs") (exp_var "imm"))%exp
- | kcgettag => MkAlt (pat_pair "rd" "cs")
- (call exec_cgettag (exp_var "rd") (exp_var "cs"))%exp
- | kcgetperm => MkAlt (pat_pair "rd" "cs")
- (call exec_cgetperm (exp_var "rd") (exp_var "cs"))%exp
- | kcgetbase => MkAlt (pat_pair "rd" "cs")
- (call exec_cgetbase (exp_var "rd") (exp_var "cs"))%exp
- | kcgetlen => MkAlt (pat_pair "rd" "cs")
- (call exec_cgetlen (exp_var "rd") (exp_var "cs"))%exp
- | kcgetaddr => MkAlt (pat_pair "rd" "cs")
- (call exec_cgetaddr (exp_var "rd") (exp_var "cs"))%exp
- | kfail => MkAlt pat_unit
- (call exec_fail)%exp
- | kret => MkAlt pat_unit
- (call exec_ret)%exp
- end).
-
- Definition fun_read_mem : Stm ["c" ∷ ty.cap] ty.memval :=
- let*: ["perm", "beg", "end", "cursor"] := (exp_var "c") in
- (let: q :: bool := call within_bounds c in
- stm_assert q (exp_string "Err: [read_mem] out of bounds") ;;
- foreign rM (exp_var "cursor")).
-
- Definition fun_write_mem : Stm ["c" ∷ ty.cap; "v" ∷ ty.memval] ty.unit :=
- let*: ["perm", "beg", "end", "cursor"] := (exp_var "c") in
- (let: q :: bool := call within_bounds c in
- stm_assert q (exp_string "Err: [write_mem] out of bounds") ;;
- foreign wM (exp_var "cursor") (exp_var "v")).
-
- Definition fun_exec : Stm [] ty.bool :=
- let: "c" := stm_read_register pc in
- (let*: ["perm", "beg", "end", "cursor"] := (exp_var "c") in
- use lemma correctPC_subperm_R [exp_var "c"] ;;
- let: n :: ty.memval := call read_mem c in
- match: n with
- | inl n =>
- let: i :: ty.instr := foreign dI n in
- call exec_instr i
- | inr c => fail "Err [exec]: instructions cannot be capabilities"
- end).
-
- Definition fun_step : Stm [] ty.unit :=
- let: "tmp1" := stm_read_register pc in
- let: "tmp2" := call is_correct_pc (exp_var "tmp1") in
- if: exp_var "tmp2"
- then
- call exec ;;
- stm_val ty.unit tt
- else
- fail "Err [step]: incorrect PC".
-
- Definition fun_loop : Stm [] ty.unit :=
- call step ;; call loop.
-
- End ExecStore.
-
- Definition FunDef {Δ τ} (f : Fun Δ τ) : Stm Δ τ :=
- match f with
- | read_reg => fun_read_reg
- | read_reg_cap => fun_read_reg_cap
- | read_reg_num => fun_read_reg_num
- | write_reg => fun_write_reg
- | next_pc => fun_next_pc
- | update_pc => fun_update_pc
- | update_pc_perm => fun_update_pc_perm
- | is_correct_pc => fun_is_correct_pc
- | is_perm => fun_is_perm
- | add_pc => fun_add_pc
- | read_mem => fun_read_mem
- | write_mem => fun_write_mem
- | read_allowed => fun_read_allowed
- | write_allowed => fun_write_allowed
- | within_bounds => fun_within_bounds
- | perm_to_bits => fun_perm_to_bits
- | perm_from_bits => fun_perm_from_bits
- | and_perm => fun_and_perm
- | is_sub_perm => fun_is_sub_perm
- | is_within_range => fun_is_within_range
- | abs => fun_abs
- | is_not_zero => fun_is_not_zero
- | can_incr_cursor => fun_can_incr_cursor
- | exec_jalr_cap => fun_exec_jalr_cap
- | exec_cjalr => fun_exec_cjalr
- | exec_cjal => fun_exec_cjal
- | exec_bne => fun_exec_bne
- | exec_cmove => fun_exec_cmove
- | exec_ld => fun_exec_ld
- | exec_sd => fun_exec_sd
- | exec_cincoffset => fun_exec_cincoffset
- | exec_candperm => fun_exec_candperm
- | exec_csetbounds => fun_exec_csetbounds
- | exec_csetboundsimm => fun_exec_csetboundsimm
- | exec_addi => fun_exec_addi
- | exec_add => fun_exec_add
- | exec_sub => fun_exec_sub
- | exec_slt => fun_exec_slt
- | exec_slti => fun_exec_slti
- | exec_sltu => fun_exec_sltu
- | exec_sltiu => fun_exec_sltiu
- | exec_cgettag => fun_exec_cgettag
- | exec_cgetperm => fun_exec_cgetperm
- | exec_cgetbase => fun_exec_cgetbase
- | exec_cgetlen => fun_exec_cgetlen
- | exec_cgetaddr => fun_exec_cgetaddr
- | exec_fail => fun_exec_fail
- | exec_ret => fun_exec_ret
- | exec_instr => fun_exec_instr
- | exec => fun_exec
- | step => fun_step
- | loop => fun_loop
- end.
-
- End FunDefKit.
-
- Include DefaultRegStoreKit MinCapsBase.
-
- Section ForeignKit.
- Definition fun_rM (μ : Memory) (addr : Val ty.int) : Val ty.memval :=
- μ addr.
-
- Definition fun_wM (μ : Memory) (addr : Val ty.int) (val : Val ty.memval) : Memory :=
- fun addr' => if Z.eqb addr addr' then val else μ addr'.
-
- (* We postulate a pure decode function and assume that that's what the decode primitive implements. *)
- (* Similarly for *_{from,to}_bits functions, ideally we would move to actual bitvectors for values... *)
- Axiom pure_decode : Z -> string + Instruction.
-
- #[derive(equations=no)]
- Equations ForeignCall {σs σ} (f : 𝑭𝑿 σs σ) (args : NamedEnv Val σs) (res : string + Val σ) (γ γ' : RegStore) (μ μ' : Memory) : Prop :=
- ForeignCall rM [addr] res γ γ' μ μ' :=
- (γ' , μ' , res) = (γ , μ , inr (fun_rM μ addr));
- ForeignCall wM [addr; val] res γ γ' μ μ' =>
- (γ' , μ' , res) = (γ , fun_wM μ addr val , inr tt);
- ForeignCall dI [code] res γ γ' μ μ' :=
- (γ' , μ' , res) = (γ , μ , pure_decode code).
-
- Lemma ForeignProgress {σs σ} (f : 𝑭𝑿 σs σ) (args : NamedEnv Val σs) γ μ :
- exists γ' μ' res, ForeignCall f args res γ γ' μ μ'.
- Proof. destruct f; env.destroy args; repeat econstructor. Qed.
- End ForeignKit.
-
- Include ProgramMixin MinCapsBase.
-
- End MinCapsProgram.